Untraceability in the applied pi-calculus

The use of RFID tags in personal items, such as passports, may make it possible to track a person´s movements. Even RFID protocols that encrypt their identity may leak enough information to let an attacker trace a tag. In this paper we define strong and weak forms of untraceablility, and illustrate these definitions with a simple example. We formally define these concepts in the applied pi-calculus which in some cases makes it possible to automatically check if an RFID tag running a particular protocol is untraceable.