@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@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},
}