Formal Verification of Privacy for RFID Systems

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, untraceability 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 untraceability 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.

• Type: Conference
• Year: 2010
• Where: CSFW
• Authors: Mayla Brusò, Konstantinos Chatzikokolakis, Jerry den Hartog
• Keywords: CSFW 2010, Privacy, Privacy Concerns, Security Privacy, Simple Privacy Protocols