Equivalence Properties by Typing in Cryptographic Branching Protocols - Archive ouverte HAL Access content directly
Conference Papers Year :

Equivalence Properties by Typing in Cryptographic Branching Protocols

(1, 2) , (3) , (2, 1) , (3)
1
2
3

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

Dates and versions

hal-01900079 , version 1 (20-10-2018)

Identifiers

  • HAL Id : hal-01900079 , version 1

Cite

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⟩
111 View
52 Download

Share

Gmail Facebook Twitter LinkedIn More