SPOOC: 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. Equivalence properties by typing in cryptographic branching protocols. In Proceedings of the 7th International Conference on Principles of Security and Trust (POST'18), pp. 160–187, April 2018.
doi:https://doi.org/10.1007/978-3-319-89722-6_7

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,
  pages =	 {160-187},
  month =	 {April},
  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 =		 {https://doi.org/10.1007/978-3-319-89722-6_7},
                  ={https://members.loria.fr/VCortier/files/Papers/post18.pdf},
}