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 (TOCL), 21(1):1:1–1:52, 2020.
(unavailable)
@article{CCDD-tocl20,
abtract = {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 equivalence 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 encompasses 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.
},
author = {Chr{\'e}tien, R{\'e}my and Cortier, V{\'e}ronique and Dallon, Antoine and
Delaune, St{\'e}phanie},
title = {Typing messages for free in security protocols},
journal = {ACM Transactions on Computational Logic (TOCL)},
volume = {21},
number = {1},
pages = {1:1--1:52},
year = {2020},
}