Proving physical proximity using symbolic models

Authors: Alexandre Debant, Stephanie Delaune and Cyrille Wiedling

Paper Information

Title:Proving physical proximity using symbolic models
Authors:Alexandre Debant, Stephanie Delaune and Cyrille Wiedling
Proceedings:FCS Informal Proceedings
Editors: Charles Morisset and Limin Jia
Keywords:formal verification, security protocols, symbolic models, distance bounding protocols

ABSTRACT. 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. An interesting consequence of our reduction results is that it allows one to reuse ProVerif, an automated tool developed for analysing standard security protocols. As an application, we analyse several distance bounding protocols, as well as a contactless payment protocol, and our experimental results confirm existing results on these protocols.

Talk:Jul 08 11:30 (Session 38E: Formal Modelling & Analysis)