Stéphanie Delaune: SAT-Equiv: an efficient tool for equivalence properties

SAT-Equiv: an efficient tool for equivalence properties

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

Download

[PDF]

Abstract

Automatic tools based on symbolic models have been successful inanalyzing security protocols. Such tools are particularly adaptedfor trace properties (e.g. secrecy or authentication), while theyoften 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 beenproposed but the resulting tools are rather inefficient.In this paper, we propose a novel algorithm, based on graph planning and SAT-solving, whichsignificantly improves the efficiency of the analysis of equivalence properties.The resulting implementation, SAT-Equiv, can analyzeseveral sessions where most tools have to stop after one or two sessions.

BibTeX

@inproceedings{CDD-csf17,
  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.
},
  address =       {Santa Barbara, CA, USA},
  author =        {Cortier, V{\'e}ronique and Dallon, Antoine and
                   Delaune, St{\'e}phanie},
  booktitle =     {{P}roceedings of the 30th {IEEE} {C}omputer
                   {S}ecurity {F}oundations {S}ymposium ({CSF}'17)},
  month =         aug,
  OPTpages =         {},
  publisher =     {{IEEE} Computer Society Press},
  title =         {SAT-Equiv: an efficient tool for equivalence properties},
  year =          {2017},
  acronym =       {{CSF}'17},
  nmonth =        {8},
  OPTLONGPDF =       {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/
                  CDD-csf17-long.pdf},
  lsv-category =  {intc},
  wwwpublic =     {public and ccsb},
}