Modelling and analysis of a hierarchy of distance bounding attacks

Tom Chothia, Joeri De Ruiter, Ben Smyth

Research output: Chapter in Book/Report/Conference proceedingConference contribution

11 Citations (Scopus)
49 Downloads (Pure)


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 calcu- lus 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 languageEnglish
Title of host publicationUsenix Security '18
PublisherUSENIX Association
Number of pages18
Publication statusPublished - 17 Aug 2018
Event27th USENIX Security Symposium - Baltimore Marriott Waterfront, Baltimore, United States
Duration: 15 Aug 201817 Aug 2018


Conference27th USENIX Security Symposium
Abbreviated titleUSENIX Security '18
Country/TerritoryUnited States

Cite this