Modelling and Analysis of a Hierarchy of Distance Bounding Attacks


Tom Chothia, Univ. of Birmingham; Joeri de Ruiter, Radboud University Nijmegen; Ben Smyth, University of Luxembourg


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 sug- gested 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 Master- Card and NXP.

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

@inproceedings {217503,
author = {Tom Chothia and Joeri de Ruiter and Ben Smyth},
title = {Modelling and Analysis of a Hierarchy of Distance Bounding Attacks},
booktitle = {27th USENIX Security Symposium (USENIX Security 18)},
year = {2018},
isbn = {978-1-939133-04-5},
address = {Baltimore, MD},
pages = {1563--1580},
url = {},
publisher = {USENIX Association},
month = aug

Presentation Video 

Presentation Audio