Contributions to Proceedings:
V. Cortier, N. Grimm, J. Lallemand, M. Maffei:
"Equivalence Properties by Typing in Cryptographic Branching Protocols";
in: "Principles of Security and Trust",
LNCS 10804;
issued by: Springer, Cham;
Springer LNCS,
Schwitzerland,
2018,
ISBN: 978-3-319-89721-9,
160
- 187.
English abstract:
Recently, many tools have been proposed for automatically
analysing, in symbolic models, equivalence of security protocols. Equiv-
alence 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 rea-
soning 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.
Keywords:
Properties, Typing, Cryptographic, Protocols
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/978-3-319-89722-6
Electronic version of the publication:
https://publik.tuwien.ac.at/files/publik_270457.pdf
Created from the Publication Database of the Vienna University of Technology.