Véronique Cortier, Antoine Dallon, and Stéphanie Delaune. A small bound on the number of sessions for security protocols. In Proceedings of the 35th IEEE Computer Security Foundations Symposium (CSF'22), pp. 33–48, IEEE Computer Society Press, Haifa, Israel, August 2022.
Bounding the number of sessions is a long-standing problem in thecontext of security protocols. It is well known that even simpleproperties like secrecy are undecidable when an unbounded number ofsessions is considered. Yet, attacks on existing protocols onlyrequire a few sessions.In this paper, we propose a sound algorithm that computes a sufficientset of scenarios that need to be considered to detect an attack. Our approach can be applied for both reachability andequivalence properties, for protocols with standard primitives thatare type-compliant (unifiable messages have thesame type). Moreover, when equivalence properties are considered,else branches are disallowed, and protocols are supposed to be simple (an attacker knows from which role and session amessage comes from).Since this class remains undecidable, ouralgorithm may return an infinite set. However, our experiments showthat on most basic protocols of the literature, our algorithm computesa small number of sessions (a dozen). As a consequence, tools for abounded number of sessions like DeepSec can then be used to concludethat a protocol is secure for an unbounded number of sessions.
@inproceedings{CDD-csf22,
abstract = {Bounding the number of sessions is a long-standing problem in the
context of security protocols. It is well known that even simple
properties like secrecy are undecidable when an unbounded number of
sessions is considered. Yet, attacks on existing protocols only
require a few sessions.
In this paper, we propose a sound algorithm that computes a sufficient
set of scenarios that need to be considered to detect an attack. Our approach can be applied for both reachability and
equivalence properties, for protocols with standard primitives that
are type-compliant (unifiable messages have the
same type). Moreover, when equivalence properties are considered,
else branches are disallowed, and protocols are supposed to be simple (an attacker knows from which role and session a
message comes from).
Since this class remains undecidable, our
algorithm may return an infinite set. However, our experiments show
that on most basic protocols of the literature, our algorithm computes
a small number of sessions (a dozen). As a consequence, tools for a
bounded number of sessions like DeepSec can then be used to conclude
that a protocol is secure for an unbounded number of sessions.
},
address = {Haifa, Israel},
author = {Cortier, V{\'e}ronique and Dallon, Antoine and Delaune, St{\'e}phanie},
booktitle = {{P}roceedings of the 35th {IEEE} {C}omputer
{S}ecurity {F}oundations {S}ymposium ({CSF}'22)},
month = aug,
pages = {33--48},
publisher = {{IEEE} Computer Society Press},
title = {A small bound on the number of sessions for security protocols},
year = {2022},
acronym = {{CSF}'22},
nmonth = {8},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}