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.

Properties, Typing, Cryptographic, Protocols

"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)

Electronic version of the publication:

Created from the Publication Database of the Vienna University of Technology.