So near and yet so far - Symbolic verification of distance-bounding protocols - Archive ouverte HAL Access content directly
Journal Articles ACM Transactions on Privacy and Security Year : 2022

So near and yet so far - Symbolic verification of distance-bounding protocols

(1, 2, 3) , (1, 2, 3, 4) , (5)
1
2
3
4
5

Abstract

The rise of new technologies, and in particular Near Field Communication (NFC) tags, offers new applications such as contactless payments, key-less entry systems, transport ticketing. .. Due to their security concerns, new security protocols, called distance-bounding protocols, have been developed to ensure physical proximity of the devices during a session. In order to prevent flaws and attacks, these protocols require formal verification. In this paper, we propose a new symbolic model allowing us to take into account the location of the agents and to model the fact that transmitting a message takes time. We propose two reduction results to render automatic verification possible relying on the existing verification tool ProVerif. Then, we perform a comprehensive case studies analysis (more than 25 protocols) relying on our new framework and its integration in ProVerif. We obtain new proofs of security for some protocols and detect attacks on some others.
Fichier principal
Vignette du fichier
full-version.pdf (769.92 Ko) Télécharger le fichier
Vignette du fichier
supplementary-material.zip (1.88 Mo) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-02965322 , version 1 (13-10-2020)
hal-02965322 , version 2 (26-11-2021)

Identifiers

  • HAL Id : hal-02965322 , version 2

Cite

Alexandre Debant, Stéphanie Delaune, Cyrille Wiedling. So near and yet so far - Symbolic verification of distance-bounding protocols. ACM Transactions on Privacy and Security, 2022, 25 (2), pp.39. ⟨hal-02965322v2⟩
147 View
174 Download

Share

Gmail Facebook Twitter LinkedIn More