<div class="csl-bib-body">
<div class="csl-entry">Cortier, V., Grimm, N., Lallemand, J., & Maffei, M. (2018). Equivalence Properties by Typing in Cryptographic Branching Protocols. In L. Bauer & R. Küsters (Eds.), <i>Principles of Security and Trust</i> (pp. 160–187). Springer LNCS. https://doi.org/10.1007/978-3-319-89722-6_7</div>
</div>
-
dc.identifier.isbn
9783319897226
-
dc.identifier.isbn
9783319897219
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/57359
-
dc.description.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.
en
dc.publisher
Springer LNCS
-
dc.relation.ispartofseries
Lecture Notes in Computer Science
-
dc.subject
Protocols
-
dc.subject
Properties
-
dc.subject
Typing
-
dc.subject
Cryptographic
-
dc.title
Equivalence Properties by Typing in Cryptographic Branching Protocols