With the proliferation of contactless applications, obtaining reliable information about distance is becoming an important security goal, and specific protocols have been designed for that purpose. These protocols typically measure the round trip time of messages and use this information to infer a distance.

Formal methods have proved their usefulness when analysing standard security protocols such as confidentiality or authentication protocols. However, existing results and tools do not apply to distance bounding protocols. This is due in particular to the fact that the communication model is too abstract and do not reflect constraints from the physical world (e.g. messages can not travel faster than the speed of the light).

In this paper, we propose a symbolic model suitable to analyse distance bounding protocols. We propose a new procedure for analysing (a bounded number of sessions of) protocols in this model. The procedure has been integrated in the Akiss tool and tested on various distance bounding protocols among which MasterCard and NXP.