Symbolic Analysis of Terrorist Fraud Resistance

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.

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.