Skip to Main content Skip to Navigation
New interface
Reports (Research report)

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

Rémy Chrétien 1 Véronique Cortier 2 Stéphanie Delaune 1 
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Document type :
Reports (Research report)
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download
Contributor : Véronique Cortier Connect in order to contact the contributor
Submitted on : Monday, June 16, 2014 - 8:08:03 PM
Last modification on : Wednesday, October 26, 2022 - 8:16:11 AM
Long-term archiving on: : Tuesday, September 16, 2014 - 11:42:07 AM


Files produced by the author(s)


  • HAL Id : hal-01007580, version 1


Rémy Chrétien, Véronique Cortier, Stéphanie Delaune. Typing messages for free in security protocols: the case of equivalence properties. [Research Report] RR-8546, INRIA. 2014, pp.46. ⟨hal-01007580⟩



Record views


Files downloads