A Method for Proving Unlinkability of Stateful Protocols
In: 33rd IEEE Computer Security Foundations Symposium ; https://hal.science/hal-02459984 ; 33rd IEEE Computer Security Foundations Symposium, Jun 2020, Boston, United States, 2020
Online
Konferenz
Zugriff:
International audience ; The rise of contactless and wireless devices such as mobile phones and RFID chips justifies significant concerns over privacy, and calls for communication protocols that ensure some form of unlinkability. Formally specifying this property is difficult and context-dependent, and analysing it is very complex; as is common with security protocols, several incorrect unlinkability claims can be found in the literature. Formal verification is therefore desirable, but current techniques are not sufficient to directly analyse unlinkability. In [Hirschi et al., S&P'19], two conditions have been identified that imply unlinkability and can be automatically verified. This work, however, only considers a restricted class of protocols. We adapt their formal definition as well as their proof method to the common setting of RFID authentication protocols, where readers access a central database of authorised users. Moreover, we also consider protocols where readers may update their database, and tags may also carry a mutable state. We propose sufficient conditions to ensure unlinkability, find new attacks, and obtain new proofs of unlinkability using Tamarin to establish our sufficient conditions.
Titel: |
A Method for Proving Unlinkability of Stateful Protocols
|
---|---|
Autor/in / Beteiligte Person: | Baelde, David ; Delaune, Stéphanie ; Moreau, Solène ; Laboratoire Spécification et Vérification (LSV) ; Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay) ; Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay) ; Université de Rennes (UR) ; Centre National de la Recherche Scientifique (CNRS) ; 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) ; EMbedded SEcurity and Cryptography (EMSEC) ; SYSTÈMES LARGE ÉCHELLE (IRISA-D1) ; 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)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-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)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA) ; 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)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS) ; 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) ; ANR-17-CE39-0004,TECAP,Analyse de protocoles - unir les outils existants(2017) ; European Project: 714955,H2020,ERC-2016-STG,ERC-POPSTAR(2017) |
Link: | |
Zeitschrift: | 33rd IEEE Computer Security Foundations Symposium ; https://hal.science/hal-02459984 ; 33rd IEEE Computer Security Foundations Symposium, Jun 2020, Boston, United States, 2020 |
Veröffentlichung: | HAL CCSD, 2020 |
Medientyp: | Konferenz |
Schlagwort: |
|
Sonstiges: |
|