Véronique Cortier, Antoine Dallon, and Stéphanie Delaune. Efficiently deciding equivalence for standard primitives and phases. In * Proceedings of the 23rd European Symposium on Research in Computer Security (ESORICS'18)*, Lecture Notes in Computer Science, Springer, Barcelona, Spain, 2018.

Privacy properties like anonymity or untraceability are now wellidentified, desirable goals of many security protocols. Suchproperties are typically stated as equivalence properties. However, automatically checking equivalence of protocols often yieldsefficiency issues.We propose an efficient algorithm, based on graph planning andSAT-solving. It can decide equivalence for a bounded number ofsessions, for protocols with standard cryptographic primitives andphases (often necessary to specify privacy properties), providedprotocols are well-typed, that is encrypted messages cannot beconfused.The resulting implementation, SAT-Equiv, demonstrates a significantspeed-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.

@inproceedings{CDD-esorics18, 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.}, address = {Barcelona, Spain}, author = {Cortier, V{\'e}ronique and Dallon, Antoine and Delaune, St{\'e}phanie}, 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}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, acronym = {{ESORICS}'18}, }