Symbolic verification of privacy-type properties for security protocols with XOR
In: CSF 2017 - 30th IEEE Computer Security Foundations Symposium ; https://inria.hal.science/hal-01533708 ; CSF 2017 - 30th IEEE Computer Security Foundations Symposium, Aug 2017, Santa Barbara, United States. pp.15, 2017
Online
Konferenz
Zugriff:
International audience ; In symbolic verification of security protocols, process equivalences have recently been used extensively to model strong secrecy, anonymity and unlinkability properties. However, tool support for automated analysis of equivalence properties is limited compared to trace properties, e.g., modeling authentication and weak notions of secrecy. In this paper, we present a novel procedure for verifying equivalences on finite processes, i.e., without replication, for protocols that rely on various cryptographic primitives including exclusive or (xor). We have implemented our procedure in the tool AKISS, and successfully used it on several case studies that are outside the scope of existing tools, e.g., unlinkability on various RFID protocols, and resistance against guessing attacks on protocols that use xor.
| Titel: |
Symbolic verification of privacy-type properties for security protocols with XOR
|
|---|---|
| Autor/in / Beteiligte Person: | Baelde, David ; Delaune, Stéphanie ; Gazeau, Ivan ; Kremer, Steve ; Laboratoire Spécification et Vérification Cachan (LSV) ; École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS) ; EMbedded SEcurity and Cryptography (EMSEC) ; 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)-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) ; Proof techniques for security protocols (PESTO) ; Inria Nancy - Grand Est ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM) ; Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS) ; ANR-14-CE28-0030,Sequoia,Propriété de sécurité, équivalence de processes et vérification automatique(2014) ; ANR-11-JS02-0006,VIP,Vérification de propriétés d'indistinguabilité(2011) ; European Project: 645865,H2020 ERC,ERC-2014-CoG,SPOOC(2015) ; European Project: 714955,H2020,ERC-2016-STG,POPSTAR(2017) |
| Link: | |
| Zeitschrift: | CSF 2017 - 30th IEEE Computer Security Foundations Symposium ; https://inria.hal.science/hal-01533708 ; CSF 2017 - 30th IEEE Computer Security Foundations Symposium, Aug 2017, Santa Barbara, United States. pp.15, 2017 |
| Veröffentlichung: | HAL CCSD ; IEEE, 2017 |
| Medientyp: | Konferenz |
| Schlagwort: |
|
| Sonstiges: |
|