Proving Physical Proximity Using Symbolic Methods

For many modern applications like e.g. contactless payment, and keyless systems, ensuring physical proximity is a security goal of paramount importance. Formal methods have proved their usefulness when analysing standard security protocols. However, existing results and tools do not apply to e.g. distance bounding that aims to ensure physical proximity between two entities. This is due in particular to the fact that existing models do not represent in a faithful way the locations of the participants, and the fact that transmission of messages takes time.
In this paper, we propose several reduction results: when looking for an attack, it is actually sufficient to consider a simple scenario involving at most four participants located at some specific locations. These reduction results allow one to use verification tools (e.g. ProVerif, Tamarin) developed for analysing more classical security properties. As an application, we analyse several distance bounding protocols, as well as a contactless payment protocol.

The reduction results presented in the report enable the use of a standard verification tool to analyse the security of Distance bounding protocols. The modeling in Proverif is described in the report (and the paper) and consists in using 3 phases to model the first initialisation phase, then the rapid phase and finally a verification phase. Intuitively, only agents close to the verifier are allowed to speak during phase 1.

A large number of protocols have been analysed in ProVerif w.r.t. Mafia frauds, Distance hijacking, Distance frauds and Simple distance frauds (the two last class of attacks are only described in the full report). All the ProVerif files are available at examplesDB.zip and summed up in the following table (each ✓ or ✗ are linked to the corresponding ProVerif file).
The archive contains two folders (in ProVerif/): the first one, "initial-model", contains the ProVerif files obtained applying reduction results and allowing an agent to be, at the same time, verifier and prover. The second one, "role-dependent-model", contains the ProVerif corresponding to the reduction results obtained in the model in which agents can not be simultaneously verifier and prover (Appendix F in the report).

As explained in the report, we must restrain the underlying attacker of ProVerif when considering topologies without dishonest agents close to the verifier (the non-modified ProVerif can still be used to verify Mafia fraud attacks). Indeed, the attacker model behind ProVerif allows him to interact with any participants, even those that are far away.
Therefore in the modified Proverif version, we prevent the attacker from forging new messages during Phase 1. He can only forward messages or send messages already forgeable in Phase 0. As presented in the report we need a modified version of the ProVerif tool to perform all the analyses.

Even if our development is formally described for the ProVerif tool, our theoretical results can be applied with other tools. We decided to apply our results to the Tamarin tool which have been recently extended to take into account the exclusive-or operator [1].

Tamarin is a verification tool for stafeful protocols based on multiset rewritting rules. To model the two locations in the reduced topologies, we decided to use an action fact nammed Slow() added to rules that cannot be executed by agent close to the verifier and a restriction to prevent such actions during the rapide phase.
To model distance hijacking attacks, like in ProVerif, we must restrict the capabilities of the attacker. In ProVerif we had to modify the tool itself, but, in Tamarin, to model such a restriction, we decided to not use the classical facts In(x) and Out(u); we use a specific persistent fact !Com(u) and two rules to transfer all the outputs to the attacker and get back all the messages he may send. Tagging these two rules with the action fact Slow() we prevent the attacker from talking during the rapid phase.

Case studies

Few examples have been analysed in Tamarin using the exclusive-or operator. When analysing the Hancke and Kuhn and the Swiss-Knife protocols we obtain the same results as in ProVerif and the verifications are almost automatic (we just had to write one source lemma). However, we did not succeed in analysing the Brands and Chaum protocol due to partial deconstructions. It seems that more expertise is needed to write additional lemmas and obtain meaningful results on this protocol.

Files are available at:

• Hancke and Kuhn: Mafia fraud, Distance hijacking
• Hancke and Kuhn: Mafia fraud, Distance hijacking
• Brands and Chaum: Mafia fraud, Distance hijacking

[1] J. Dreier, L. Hirschi, S. Radomirovic, and R. Sasse. Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR. In CSF'2018 - 31st IEEE Computer Security Foundations Symposium, Oxford, United Kingdom, July 2018.

Homepage