Abstract
We present an extension of the applied pi-calculus that can be used to model distance bounding protocols. A range of different security properties have been suggested for distance bounding protocols; we show how these can be encoded in our model and prove a partial order between them. We also relate the different security properties to particular attacker models. In doing so, we identify a new property, which we call uncompromised distance bounding, that captures the attacker model for protecting devices such as contactless payment cards or car entry systems, which assumes that the prover being tested has not been compromised, though other provers may have been. We show how to compile our new calculus into the applied pi-calculus so that protocols can be automatically checked with the ProVerif tool and we use this to analyse distance bounding protocols from MasterCard and NXP.
Original language | English |
---|---|
Title of host publication | Proceedings of the 27th USENIX Security Symposium |
Publisher | USENIX Association |
Pages | 1563-1580 |
Number of pages | 18 |
ISBN (Electronic) | 9781939133045 |
Publication status | Published - 2018 |
Event | 27th USENIX Security Symposium - Baltimore Marriott Waterfront, Baltimore, United States Duration: 15 Aug 2018 → 17 Aug 2018 |
Publication series
Name | Proceedings of the 27th USENIX Security Symposium |
---|
Conference
Conference | 27th USENIX Security Symposium |
---|---|
Abbreviated title | USENIX Security '18 |
Country/Territory | United States |
City | Baltimore |
Period | 15/08/18 → 17/08/18 |
Bibliographical note
Funding Information:Acknowledgements This work has been supported by the Netherlands Organisation for Scientific Research (NWO) through Veni project 639.021.750. We would like to thank Ioana Boureanu and Sjouke Mauw for useful comments on a draft of this paper.
Publisher Copyright:
© 2018 Proceedings of the 27th USENIX Security Symposium. All rights reserved.
ASJC Scopus subject areas
- Computer Networks and Communications
- Information Systems
- Safety, Risk, Reliability and Quality