Symbolic Analysis of Terrorist Fraud Resistance

Alexandre Debant, Stéphanie Delaune, and Cyrille Wiedling.

Accepted paper: [pdf]

Full version with proofs: [pdf]


Distance-bounding protocols aim at preventing several kinds of attacks, amongst which terrorist fraud, where a far away malicious prover colludes with an attacker to authenticate once, without giving him any advantage for future authentication. In this paper, we consider a symbolic setting and propose a formal definition of terrorist fraud, as well as two reduction results. When looking for an attack, we can first restrict ourselves to consider a particular (and quite simple) topology. Moreover, under some mild hypotheses, the far away malicious prover has a best strategy on which we can focus on when looking for an attack. These two reduction results make possible the analysis of terrorist fraud resistance using an existing verification tool. As an application, we analyse several distance-bounding protocols, as well as some contactless payment protocols using the ProVerif tool.


The reduction results presented in the report enable the use of a standard verification tool to analyse the security of distance-bounding protocols. We reuse the encoding described in [1] to model the guarded input of a Verifier. However we add an extra phase at the beginning to enrich the knowledge of the attacker with the trace resulting from the execution between the Verifier and the most-general semi-dishonest Prover.

Case studies

A large number of protocols met the hypothesis of our approach and have been analysed in ProVerif. All the ProVerif files are available at case-studies.tar.gz and summed up in the following table.

Protocols MFR TFR   Protocols MFR TFR
Basin's Toy Example    ✓       ✓      TREAD-PKey V1    ✗       ✓   
Hancke and Kuhn   TREAD-PKey V1 Fixed         ✓       ✓   
Modified Hancke and Kuhn        TREAD-PKey V2    ✗       ✓   
Swiss-Knife   TREAD-PKey V2 Fixed    ✓       ✓   
Munilla et al.   SKI    ✓       ✓   
SPADE   PaySafe    ✓       ✗   
SPADE Fixed   NXP    ✓       ✗   
Results on our case studies ( ✗: attack found, ✓: proved secure)

[1] A. Debant, S. Delaune, and C. Wiedling. A symbolic framework to analyse physi- cal proximity in security protocols In FSTTCS'2018 - 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Ahmedabad, India, 2018.