Modelling and Analysis of a Hierarchy of Distance Bounding Attacks

A Hierarchy of Distance
        Bounding Security Properites

Wireless devices are often used as authentication tokens, for example, contactless EMV bank cards are used to authorise payments and keyless car systems are used to open and start cars. However, these devices are vul- nerable to relay attacks in which one attacker stands near the victim (and their authentication device) and relays signals from that device to a second attacker near the payment terminal, car, door lock etc. (see here for a video of such an attack).

Our work presents 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 (as shown above).

We identify a property that we call uncompromised distance bounding (top left in the figure above) 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.

Details of our work are described in the paper:

For more information about our PaySafe protocol for stopping relay attacks against contactless EMV see here.