Typing messages for free in security protocols: the case of equivalence properties

Typing messages for free in security protocols: the case of equivalence properties. Rémy Chrétien, Véronique Cortier, and Stéphanie Delaune. Rapport de recherche RR-8546, INRIA, 2014.

Download

[PDF] [HTML]

Abstract

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.

BibTeX

@techreport{chretien:hal-01007580,
    doi = {http://hal.inria.fr/hal-01007580},
    title = {{Typing messages for free in security protocols: the case of equivalence properties}},
    author = {Chr{\'e}tien, R{\'e}my and Cortier, V{\'e}ronique and Delaune, St{\'e}phanie},
    abstract = {{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.}},
    language = {Anglais},
    affiliation = {Laboratoire Sp{\'e}cification et V{\'e}rification [Cachan] - LSV , CASSIS - INRIA Nancy - Grand Est / LORIA / LIFC},
    pages = {46},
    type = {Rapport de recherche},
    institution = {INRIA},
    number = {RR-8546},
    year = {2014},
    month = Jun,
}