Formal verification of privacy for RFID systems

M. Bruso, K. Chatzikokolakis, J.I. Hartog, den

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

44 Citations (Scopus)
2 Downloads (Pure)


RFID tags are being widely employed in a variety of applications, ranging from barcode replacement to electronic passports. Their extensive use, however, in combination with their wireless nature, introduces privacy concerns as a tag could leak information about the owner's behaviour. In this paper we define two privacy notions, unlinkability and forward privacy, using a formal model based on the applied pi calculus, and we show the relationship between them. Then we focus on a generic class of simple privacy protocols, giving sufficient and necessary conditions for unlinkability and forward privacy for this class. These conditions are based on the concept of frame independence that we develop in this paper. Finally, we apply our techniques to two identification protocols, formally proving their privacy guarantees.
Original languageEnglish
Title of host publicationProceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF'10, Edinburgh, UK, July 17-19, 2010)
PublisherIEEE Computer Society
ISBN (Print)978-1-4244-7510-0
Publication statusPublished - 2010


Dive into the research topics of 'Formal verification of privacy for RFID systems'. Together they form a unique fingerprint.

Cite this