Symbolic Verification of Distance-Bounding Protocols

Abstract. 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, due to their abstract communication model, existing results and tools do not apply to distance bounding.
In this paper, we consider a symbolic model suitable to analyse distance bounding protocols, and 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 and payment protocols (e.g. MasterCard, NXP, ...).

Akiss is a tool implementing a procedure proposed by Chadha et al. [1] enabling the verification of equivalence-based properties. It proceeds in two steps: first it computes a knowledge base which is a finite representation of all possible traces (including recipes) executable by the process under study. Relying on these knowledge bases it decides whether two processes are equivalent or not. This is the part we reuse in this work.
However, we had to completely redesign the update function used during the computation of these knowledge bases to ensure the completeness of our procedure.

We applied our procedure to analyse a large number of distance bounding protocols and payment protocols. For each distance bounding protocol, we consider two distinct topologies: one to analyse mafia fraud scenarios and one to analyse distance hijacking. When considering payment protocols we only consider one topology to analyse mafia fraud scenarios - the only relevant ones. All the files are available at examples.tar.gz and summed up in the following tables.
We indicate the number of roles (running in parallel) we consider and the number of traces (due to all the possible interleaving of the roles remaning after having performed POR optimisation) that have been analysed by the tool in order to conclude. Our algorithm stops as soon as an attack is found, and thus the number of possible interleavings is not relevant in this case.