DEEPSEC: Deciding Equivalence Properties in Security Protocols Theory and Practice

Vincent Cheval (1) , Steve Kremer (1) , Itsaka Rakotonirina (1)

1 PESTO - Proof techniques for security protocols

We study the automated verification of behavioural equivalences in the applied pi calculus, an essential problem in formal, symbolic analysis of cryptographic protocols. We establish new complexity results for static equivalence, trace equivalence and labelled bisimilarity and propose a new decision procedure for these equivalences. Our procedure is the first tool to decide trace equivalence and labelled bisimilarity exactly for a family of equational theories, namely those that can be represented by a subterm convergent destructor rewrite system. Finally, we implement the procedure in a new tool, called Deepsec and demonstrate the applicability of the tool on several case studies.

Domaines: Informatique [cs]; Cryptographie et sécurité [cs.CR]; Complexité [cs.CC]

Vincent Cheval, Steve Kremer, Itsaka Rakotonirina. DEEPSEC: Deciding Equivalence Properties in Security Protocols Theory and Practice. [Research Report] INRIA Nancy. 2018. ⟨hal-01698177⟩