DEEPSEC: Deciding Equivalence Properties in Security Protocols Theory and Practice - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 2018

DEEPSEC: Deciding Equivalence Properties in Security Protocols Theory and Practice

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

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.
Fichier principal
Vignette du fichier
main.pdf (738.94 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01698177 , version 1 (31-01-2018)

Identifiers

  • HAL Id : hal-01698177 , version 1

Cite

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

Share

Gmail Facebook Twitter LinkedIn More