Analysing Unlinkability and Anonymity Using the Applied Pi Calculus

M. Arapinis, T. Chothia, Eike Ritter, Mark Ryan

Research output: Chapter in Book/Report/Conference proceedingConference contribution


An attacker that can identify messages as coming from the same source, can use this information to build up a picture of targets' behaviour, and so, threaten their privacy. In response to this danger, unlinkable protocols aim to make it impossible for a third party to identify two runs of a protocol as coming from the same device. We present a framework for analysing unlinkability and anonymity in the applied pi calculus. We show that unlinkability and anonymity are complementary properties; one does not imply the other. Using our framework we show that the French RFID e-passport preserves anonymity but it is linkable therefore anyone carrying a French e-passport can be physically traced.
Original languageEnglish
Title of host publicationComputer Security Foundations Symposium (CSF), 2010 23rd IEEE
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Number of pages15
ISBN (Electronic)978-1-4244-7511-7
ISBN (Print)978-1-4244-7510-0
Publication statusPublished - 2010


  • data privacy
  • pi calculus
  • protocols
  • radiofrequency identification
  • travel industry
  • French RFID e-passport
  • anonymity analysis
  • unlinkability analysis
  • unlinkable protocols
  • Calculus
  • Context
  • Mathematical model
  • Privacy
  • Protocols
  • Radiofrequency identification
  • Security


Dive into the research topics of 'Analysing Unlinkability and Anonymity Using the Applied Pi Calculus'. Together they form a unique fingerprint.

Cite this