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
Complete list of metadatas

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/hal-01007580
Contributor : Véronique Cortier <>
Submitted on : Monday, June 16, 2014 - 8:08:03 PM
Last modification on : Tuesday, December 18, 2018 - 4:38:25 PM
Long-term archiving on : Tuesday, September 16, 2014 - 11:42:07 AM

File

RR-8546.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01007580, version 1

Citation

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⟩

Share

Metrics

Record views

917

Files downloads

332