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 metadatas

Cited literature [35 references]  Display  Hide  Download

https://hal.inria.fr/hal-01900079
Contributor : Véronique Cortier <>
Submitted on : Saturday, October 20, 2018 - 9:36:43 PM
Last modification on : Tuesday, December 18, 2018 - 4:38:25 PM

File

post18(2).pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01900079, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

93

Files downloads

88