Formal verification of privacy for RFID systems

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

doi:10.1109/CSF.2010.13

Formal verification of privacy for RFID systems

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

44 Citations (Scopus)

2 Downloads (Pure)

Abstract

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 language	English
Title of host publication	Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF'10, Edinburgh, UK, July 17-19, 2010)
Publisher	IEEE Computer Society
Pages	75-88
ISBN (Print)	978-1-4244-7510-0
DOIs	https://doi.org/10.1109/CSF.2010.13
Publication status	Published - 2010

Access to Document

10.1109/CSF.2010.13

Cite this

@inproceedings{9570d95586474df380e260d4b563cea6,

title = "Formal verification of privacy for RFID systems",

abstract = "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.",

author = "M. Bruso and K. Chatzikokolakis and {Hartog, den}, J.I.",

year = "2010",

doi = "10.1109/CSF.2010.13",

language = "English",

isbn = "978-1-4244-7510-0",

pages = "75--88",

booktitle = "Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF'10, Edinburgh, UK, July 17-19, 2010)",

publisher = "IEEE Computer Society",

address = "United States",

}

TY - GEN

T1 - Formal verification of privacy for RFID systems

AU - Bruso, M.

AU - Chatzikokolakis, K.

AU - Hartog, den, J.I.

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

U2 - 10.1109/CSF.2010.13

DO - 10.1109/CSF.2010.13

M3 - Conference contribution

SN - 978-1-4244-7510-0

SP - 75

EP - 88

BT - Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF'10, Edinburgh, UK, July 17-19, 2010)

PB - IEEE Computer Society

ER -

Formal verification of privacy for RFID systems

Abstract

Access to Document

Fingerprint

Cite this