Skip to Main content Skip to Navigation
Conference papers

Equivalence Properties by Typing in Cryptographic Branching Protocols

Abstract : Recently, many tools have been proposed for automatically analysing, in symbolic models, equivalence of security protocols. Equivalence is a property needed to state privacy properties or game-based properties like strong secrecy. Tools for a bounded number of sessions can decide equivalence but typically suffer from efficiency issues. Tools for an unbounded number of sessions like Tamarin or ProVerif prove a stronger notion of equivalence (diff-equivalence) that does not properly handle protocols with else branches. Building upon a recent approach, we propose a type system for reasoning about branching protocols and dynamic keys. We prove our type system to entail equivalence , for all the standard primitives. Our type system has been implemented and shows a significant speedup compared to the tools for a bounded number of sessions, and compares similarly to ProVerif for an unbounded number of sessions. Moreover, we can also prove security of protocols that require a mix of bounded and unbounded number of sessions, which ProVerif cannot properly handle.
Document type :
Conference papers
Complete list of metadata

Cited literature [60 references]  Display  Hide  Download
Contributor : Véronique Cortier Connect in order to contact the contributor
Submitted on : Saturday, October 20, 2018 - 9:36:43 PM
Last modification on : Wednesday, November 3, 2021 - 7:10:23 AM


Files produced by the author(s)


  • HAL Id : hal-01900079, version 1



Véronique Cortier, Niklas Grimm, Joseph Lallemand, Matteo Maffei. Equivalence Properties by Typing in Cryptographic Branching Protocols. POST'18 - 7th International Conference on Principles of Security and Trust, Apr 2018, Thessaloniki, Greece. ⟨hal-01900079⟩



Record views


Files downloads