Typing messages for free in security protocols
Rémy Chrétien, Véronique Cortier, Antoine Dallon, and Stéphanie Delaune. Typing messages for free in security protocols. ACM Transactions on Computational Logic, 21(1):1–52, 2020.
doi:10.1145/3343507
Download
Abstract
Security properties of cryptographic protocols are typically expressed as reachability or equivalence properties. Secrecy and authentication are examples of reachability properties while privacy properties such as untraceability, vote secrecy, or anonymity are generally expressed as behavioral equivalence in a process algebra that models security protocols.
Our main contribution is to reduce the search space for attacks for reachability as well as equiva- lence properties. Specifically, we show that if there is an attack then there is one that is well-typed. Our result holds for a large class of typing systems, a family of equational theories that encom- passes all standard primitives, and protocols without else branches. For many standard protocols, we deduce that it is sufficient to look for attacks that follow the format of the messages expected in an honest execution, therefore considerably reducing the search space.
BibTeX
@Article{TOCL2020,
author = {R\'emy Chr\'etien and V\'eronique Cortier and
Antoine Dallon and St\'ephanie Delaune},
title = {Typing messages for free in security protocols},
journal = {ACM Transactions on Computational Logic},
year = 2020,
volume = 21,
number = 1,
pages = {1--52},
abstract = {Security properties of cryptographic protocols are
typically expressed as reachability or equivalence
properties. Secrecy and authentication are examples
of reachability properties while privacy properties
such as untraceability, vote secrecy, or anonymity
are generally expressed as behavioral equivalence in
a process algebra that models security protocols.
\par Our main contribution is to reduce the search
space for attacks for reachability as well as
equiva- lence properties. Specifically, we show that
if there is an attack then there is one that is
well-typed. Our result holds for a large class of
typing systems, a family of equational theories that
encom- passes all standard primitives, and protocols
without else branches. For many standard protocols,
we deduce that it is sufficient to look for attacks
that follow the format of the messages expected in
an honest execution, therefore considerably reducing
the search space.},
doi = {10.1145/3343507},
={https://members.loria.fr/VCortier/files/Papers/TOCL19.pdf},
}