SPOOC: Efficiently deciding equivalence for standard primitives and phases

Efficiently deciding equivalence for standard primitives and phases

Véronique Cortier, Stéphanie Delaune, and Antoine Dallon. Efficiently deciding equivalence for standard primitives and phases. In Proceedings of the 23rd European Symposium on Research in Computer Security, Part I (ESORICS'18), pp. 491–511, Lecture Notes in Computer Science 11098, Springer, September 2018.
doi:10.1007/978-3-319-99073-6_24

Download

[PDF] [HTML]

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.
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.

BibTeX

@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, Part I
                  (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.},
  pages =	 {491--511},
  month =	 sep,
  publisher =	 {Springer},
  series =	 {Lecture Notes in Computer Science},
  volume =	 11098,
  acronym =	 {{ESORICS}'18},
  nmonth =	 9,
  doi =		 {10.1007/978-3-319-99073-6_24},
                  ={https://hal.archives-ouvertes.fr/hal-01819366/document},
}