SAT-Equiv: an efficient tool for equivalence properties
In: [Research Report] LSV, ENS Cachan, CNRS, INRIA, Université Paris-Saclay, Cachan (France); IRISA, Inria Rennes; LORIA-Université de Lorraine; CNRS. 2017; (2017-05-31) S. 2017
Online
unknown
Zugriff:
Automatic tools based on symbolic models have been successful in analyzing security protocols. Such tools are particularly adapted for trace properties (e.g. secrecy or authentication), while they often fail to analyse equivalence properties. Equivalence properties can express a variety of security properties , including in particular privacy properties (vote privacy, anonymity, untraceability). Several decision procedures have already been proposed but the resulting tools are rather inefficient. In this paper, we propose a novel algorithm, based on graph planning and SAT-solving, which significantly improves the efficiency of the analysis of equivalence properties. The resulting implementation, SAT-Equiv, can analyze several sessions where most tools have to stop after one or two sessions.; Les outils automatiques issues de la modélisation symbolique ont permis d'analyser la sécurité des protocoles, en particulier pour les propriétés de trace telles que le secret ou l'authentification, tandis qu'ils échouent souvent à vérifier les propriétés d'équivalence, utiles à la formalisation des garanties de protection de la vie privée (secret du vote, anonymat, intraçabilité). Les outils correspondant aux nombreuses procédures de décision proposées n'ont fait preuve que d'une efficacité limitée. Dans ce rapport de recherche, nous proposons un nouvel algorithme qui améliore cette efficacité en s'appuyant sur le graphe de planification et la résolution de problèmes SAT, comme le démontre l'outil SAT-Equiv, qui peut analyser plusieurs sessions quand la plupart des outils sont limités à une ou deux.
Titel: |
SAT-Equiv: an efficient tool for equivalence properties
|
---|---|
Autor/in / Beteiligte Person: | Cortier, Véronique ; Dallon, Antoine ; Delaune, Stéphanie ; 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) ; Centre National de la Recherche Scientifique (CNRS) ; Laboratoire Spécification et Vérification [Cachan] (LSV) ; École normale supérieure - Cachan (ENS Cachan)-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) ; DGA ; LSV, ENS Cachan, CNRS, INRIA, Université Paris-Saclay, Cachan (France) ; IRISA, Inria Rennes ; LORIA - Université de Lorraine ; CNRS ; European Project: 645865,H2020 ERC,ERC-2014-CoG,SPOOC(2015) ; European Project: 714955,H2020,ERC-2016-STG,ERC-POPSTAR(2017) ; Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA) ; Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL) ; Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes) ; Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1) ; Université de Rennes (UNIV-RENNES)-CentraleSupélec-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique) ; CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1) ; Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes) ; Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1) ; Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA) ; Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA) ; Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes) |
Link: | |
Quelle: | [Research Report] LSV, ENS Cachan, CNRS, INRIA, Université Paris-Saclay, Cachan (France); IRISA, Inria Rennes; LORIA-Université de Lorraine; CNRS. 2017; (2017-05-31) S. 2017 |
Veröffentlichung: | HAL CCSD, 2017 |
Medientyp: | unknown |
Schlagwort: |
|
Sonstiges: |
|