Analysing Unlinkability and Anonymity Using the Applied Pi Calculus
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. The authors present a framework for analyzing unlinkability and anonymity in the applied pi calculus. They show that unlinkability and anonymity are complementary properties; one does not imply the other. Using their framework they show that the French RFID e-passport preserves anonymity but it is linkable therefore anyone carrying a French e-passport can be physically traced.