Anonymity and privacy properties
The
project investigates systems designed to offer privacy guarantees to
on-line users, such as anonymity of payment, privacy of shopping
preference, of email patterns and associations between correspondents,
or candidate choice in an election. It aims to develop a taxonomy
of anonymity and privacy properties within two verification formalisms (strand spaces and applied pi calculus)
and to develop techniques for analysing protocols that are designed to
provide such properties. We shall also analyse some well-known
protocols, such as private authentication protocols direct anonymous attestation protocol.
Relevant papers
The project proposal is given here:
Papers produced related to the project are here:
- S. Delaune, S. Kremer and M. Ryan. Verifying Privacy-type properties of Electronic Voting Protocols. Journal of Computer Security (in print). Draft.
- A. Mukhamedov and M. D. Ryan. Anonymity Protocol with Identity Escrow and Analysis in the Applied pi-calculus. Submitted (TSC). Draft.
- S. Delaune, S. Kremer and M. Ryan. Symbolic bisimulation for the applied pi calculus. Submitted (JCS). Draft.
- A. Mukhamedov and M. Ryan. Anonymity protocol with identity escrow, and analysis in the applied pi calculus. In G. Barthe and C. Fournet, eds, Trustworthy Global Computing, LNCS, Springer-Verlag, 2007
- B. Smyth, L. Chen, and M. D. Ryan, Direct Anonymous Attestation: ensuring privacy with corrupt administrators. F. Stajano et al. (eds.), Procedings of the Fourth European Workshop on Security and Privacy in Ad hoc and Sensor Networks, pp. 218-231, LNCS 4572, Springer-Verlag 2007
- S. Delaune, M. Ryan and B. Smyth, Automatic verification of privacy properties in the applied pi calculus". In Proceedings of the 2nd Joint iTrust and PST Conferences on Privacy, Trust Management and Security (IFIPTM'08). IFIP International Federation for Information Processing, volume 263, pp. 263-278, Springer-Verlag 2008.