SAT-Equiv: An Efficient Tool for Equivalence Properties

Abstract : 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.
Type de document :
Communication dans un congrès
30th IEEE Computer Security Foundations Symposium (CSF'17), Jul 2017, Santa Barbara, United States. pp.481 - 494, 2017, 〈10.1109/CSF.2017.15〉
Liste complète des métadonnées

Littérature citée [33 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01624274
Contributeur : Véronique Cortier <>
Soumis le : jeudi 26 octobre 2017 - 10:44:47
Dernière modification le : jeudi 11 janvier 2018 - 06:28:14

Fichier

CSF2017-SATequiv(1).pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Véronique Cortier, Antoine Dallon, Stéphanie Delaune. SAT-Equiv: An Efficient Tool for Equivalence Properties. 30th IEEE Computer Security Foundations Symposium (CSF'17), Jul 2017, Santa Barbara, United States. pp.481 - 494, 2017, 〈10.1109/CSF.2017.15〉. 〈hal-01624274〉

Partager

Métriques

Consultations de la notice

105

Téléchargements de fichiers

10