Equivalence properties by typing in cryptographic branching protocols

Equivalence properties by typing in cryptographic branching protocols. Véronique Cortier, Niklas Grimm, Joseph Lallemand, and Matteo Maffei. In Proceedings of the 7th International Conference on Principles of Security and Trust (POST'18), pp. 160–187, April 2018.

Download

[PDF] [HTML]

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.

BibTeX

@InProceedings{POST2018-type,
  author = 	 {V\'eronique Cortier and
              Niklas Grimm and
              Joseph Lallemand and
              Matteo Maffei},
  title = 	 {Equivalence properties by typing in cryptographic branching protocols},
  booktitle = {{P}roceedings of the 7th {I}nternational {C}onference on {P}rinciples of {S}ecurity and {T}rust ({POST}'18)},
  year = 	 {2018},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  pages = 	 {160--187},
  month = 	 {April},
  OPTaddress = 	 {},
  OPTorganization = {},
  OPTpublisher = {},
  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. 
\par
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.},
  doi = {10.1007/978-3-319-89722-6_7},
}