[Zurück]


Beiträge in Tagungsbänden:

V. Cortier, N. Grimm, J. Lallemand, M. Maffei:
"Equivalence Properties by Typing in Cryptographic Branching Protocols";
in: "Principles of Security and Trust", LNCS 10804; herausgegeben von: Springer, Cham; Springer LNCS, Schwitzerland, 2018, ISBN: 978-3-319-89721-9, S. 160 - 187.



Kurzfassung englisch:
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.

Schlagworte:
Properties, Typing, Cryptographic, Protocols


"Offizielle" elektronische Version der Publikation (entsprechend ihrem Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/978-3-319-89722-6

Elektronische Version der Publikation:
https://publik.tuwien.ac.at/files/publik_270457.pdf


Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.