Alexandre Debant, Stéphanie Delaune, and Cyrille Wiedling. A Symbolic Framework to Analyse Physical Proximity in Security Protocols. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS'18), LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018.
For many modernapplications like e.g. contactless payment, and keylesssystems, ensuring physical proximity is a security goal of paramountimportance. Formal methods have provedtheir usefulness when analysing standard security protocols. However, existing results and tools do not apply to e.g. distance bounding protocols 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: whenlooking for an attack, it is actually sufficient to consider a simplescenario involving at most four participants located at some specificlocations. 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 acontactless payment protocol.
@inproceedings{DDW-fsttcs18,
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 protocols 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.
},
author = {Alexandre Debant and
St{\'{e}}phanie Delaune and
Cyrille Wiedling},
title = {A Symbolic Framework to Analyse Physical Proximity in Security Protocols},
booktitle = {38th {IARCS} Annual Conference on Foundations of Software Technology
and Theoretical Computer Science (FST\&TCS'18)},
year = {2018},
series = {LIPIcs},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
acronym = {{FST\&TCS}'18},
}