Symbolic Verification of Distance-Bounding Protocols

Alexandre Debant and Stéphanie Delaune

Download: [pdf]


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.


How to use?

After the compilation an executable file is generated in the src/ folder: execute "./akiss-db < your-protocol.api" to verify it.

Case studies

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.

Protocols Mafia fraud   Distance hijacking
roles/tr time  status    roles/tr time  status 
TREAD-Asymmetric       2/-       1s         2/-       1s   
SPADE    2/-       2s         2/-       4s   
TREAD-Symmetric    4/7500       18min         2/-       1s   
Brands and Chaum    4/5635       37min       ✓         2/-       1s   
Swiss-Knife    3/1080       25s       ✓         3/7470       4min   
Hancke and Kuhn    3/20       1s       ✓         3/20       1s   
   4/3360       58s       ✓         4/3360       47s   
   5/30240       14min       ✓         5/30240       12min   
Results on our case studies of distance bounding protocols
(✗: attack found, ✓: proved secure)
Protocols Mafia fraud
  roles/tr       time       status  
NXP    2/126       4s       ✓   
MasterCard RRP       2/35       6min       ✓   
PaySafe    2/4       308s       ✓   
PaySafe-V2    2/-       26s       ✗   
PaySafe-V3    2/-       149s       ✗   
Results on our case studies of payment protocols
(✗: attack found, ✓: proved secure)

[1] R. Chadha, V. Cheval, S. Ciobaca, and S. Kremer. Automated verification of equivalence properties of cryptographic protocol. ACM Transactions on Computational Logic., 2016.