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
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : 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.
Complete list of metadatas

Cited literature [46 references]  Display  Hide  Download

https://hal.inria.fr/hal-01698177
Contributor : Vincent Cheval <>
Submitted on : Wednesday, January 31, 2018 - 11:55:27 PM
Last modification on : Monday, August 19, 2019 - 7:02:01 PM
Long-term archiving on : Saturday, May 26, 2018 - 12:00:05 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01698177, version 1

Collections

Citation

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

Share

Metrics

Record views

695

Files downloads

712