So near and yet so far - Symbolic verification of distance-bounding protocols
| Autor: | Alexandre Debant, Stéphanie Delaune, Cyrille Wiedling |
|---|---|
| Přispěvatelé: | Centre National de la Recherche Scientifique (CNRS), SYSTÈMES LARGE ÉCHELLE (IRISA-D1), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Embedded Security and Cryptography / Sécurité cryptographie embarquée (EMSEC), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Security & PrIvaCY (SPICY), DGA Maîtrise de l'information (DGA.MI), Direction générale de l'Armement (DGA), European Project: 714955,H2020,ERC-2016-STG,ERC-POPSTAR(2017) |
| Jazyk: | angličtina |
| Rok vydání: | 2022 |
| Předmět: | |
| Zdroj: | ACM Transactions on Privacy and Security ACM Transactions on Privacy and Security, 2022, 25 (2), pp.39 |
| ISSN: | 2471-2566 2471-2574 |
| Popis: | International audience; 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|