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. This paper defines strong and weak forms of untraceablility, and illustrates these definitions with a simple example. The paper formally defines 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.