@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@InProceedings{SAT-Equiv-Esorics18,
  author = 	 {V\'eronique Cortier and St\'ephanie Delaune and Antoine Dallon},
  title = 	 {Efficiently deciding equivalence for standard primitives and phases},
  booktitle = {{P}roceedings of the 23rd {E}uropean {S}ymposium on {R}esearch in {C}omputer {S}ecurity (ESORICS'18)},
  year = 	 {2018},
  abstract = {Privacy properties like anonymity or untraceability are now well
identified, desirable goals of many security protocols. Such
properties are typically stated as equivalence properties. 
However, automatically checking equivalence of protocols often yields
efficiency issues.
\par
We propose an efficient algorithm, based on graph planning and
SAT-solving. It can decide equivalence for a bounded number of
sessions, for protocols with standard cryptographic primitives and
phases (often necessary to specify privacy properties), provided
protocols are well-typed, that is encrypted messages cannot be
confused.
The resulting implementation, SAT-Equiv, demonstrates a significant
speed-up w.r.t. other existing tools that decide equivalence,
covering typically more than 100 sessions. 
Combined with a previous result, 
SAT-Equiv can now be used to prove security, 
for some protocols, for an unbounded number of sessions.
},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  pages = 	 {491--511},
  OPTmonth = 	 {},
  OPTaddress = 	 {},
  OPTorganization = {},
  publisher = {LNCS},
  OPTnote = 	 {},
  OPTannote = 	 {},
  doi = {10.1007/978-3-319-99073-6_24},
}
