Typing messages for free in security protocols: the case of equivalence properties
Rémy Chrétien, Véronique Cortier, Stéphanie Delaune
Abstract: Privacy properties such as untraceability, vote secrecy, or
anonymity are typically expressed as behavioural equivalence in a
process algebra that models security protocols. In this talk, we study
how to decide one particular relation, namely trace equivalence, for
an unbounded number of sessions.
Our first main contribution is to reduce the search space for
attacks. 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 and a large class of determinate security
protocols. Assuming finitely many nonces and keys, we can derive from
this result that trace equivalence is decidable for an unbounded
number of sessions for a class of tagged protocols, yielding one of
the first decidability results for the unbounded case. As an
intermediate result, we also provide a novel decision procedure in the
case of a bounded number of sessions.