SPOOC: SAT-Equiv: an efficient tool for equivalence properties

SAT-Equiv: an efficient tool for equivalence properties

Véronique Cortier, Stéphanie Delaune, and Antoine Dallon. SAT-Equiv: an efficient tool for equivalence properties. In Proceedings of the 30th IEEE Computer Security Foundations Symposium (CSF'17), IEEE Computer Society Press, August 2017.

Download

[PDF]

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.

BibTeX

@InProceedings{CSF2017-SATequiv,
  author =	 {V\'eronique Cortier and St\'ephanie Delaune and
                  Antoine Dallon},
  title =	 {SAT-Equiv: an efficient tool for equivalence
                  properties},
  booktitle =	 {{P}roceedings of the 30th {IEEE} {C}omputer
                  {S}ecurity {F}oundations {S}ymposium ({CSF}'17)},
  year =	 2017,
  month =	 {August},
  publisher =	 {{IEEE} Computer Society Press},
  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. \par
                  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.  \par 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. },
                  ={https://members.loria.fr/VCortier/files/Papers/CSF2017-SATequiv.pdf},
}