Alexandre Debant, Stéphanie Delaune, and Cyrille Wiedling. So Near and Yet So Far - Symbolic Verification of Distance-Bounding Protocols. ACM Transactions on Privacy and Security (ToPS), 25(2):11:1–11:39, 2022.
The continuous adoption of Near Field Communication (NFC) tags offers many new applications whose security is essential (e.g. contactless payments). In order to prevent flaws and attacks, we develop in this paper a framework allowing us to analyse the underlying security protocols, taking into account the location of the agents and the transmission delay when exchanging messages.We propose two reduction resultsto render automatic verification possible relying on the existingverification tool Proverif. Our first result allows one to consider aunique topology to catch all the possible attacks, and the second onesimplifies the security analysis when considering Terrorist fraud.Then, based on these results, we perform acomprehensive case studies analysis (27 protocols), where weobtain newproofs of security for some protocols and detect attacks on some others.
@article{DDW-tops22,
abstract = {The continuous adoption of Near Field Communication (NFC) tags
offers many new applications whose security is essential (e.g. contactless payments).
In order to prevent flaws and attacks, we develop in this paper a framework allowing us to
analyse the underlying security protocols, taking into account
the location of the agents and the transmission delay when exchanging messages.
We propose two reduction results
to render automatic verification possible relying on the existing
verification tool Proverif. Our first result allows one to consider a
unique topology to catch all the possible attacks, and the second one
simplifies the security analysis when considering Terrorist fraud.
Then, based on these results, we perform a
comprehensive case studies analysis (27 protocols), where we
obtain new
proofs of security
for some protocols and detect attacks on some others.
},
author = {Alexandre Debant and
St{\'{e}}phanie Delaune and
Cyrille Wiedling},
title = {So Near and Yet So Far - Symbolic Verification of Distance-Bounding
Protocols},
journal = {{ACM} Transactions on Privacy and Security (ToPS)},
volume = {25},
number = {2},
pages = {11:1--11:39},
year = {2022},
url = {https://doi.org/10.1145/3501402},
doi = {10.1145/3501402},
}