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.
Type de document :
Rapport
[Research Report] RR-8546, INRIA. 2014, pp.46
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01007580
Contributeur : Véronique Cortier <>
Soumis le : lundi 16 juin 2014 - 20:08:03
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10
Document(s) archivé(s) le : mardi 16 septembre 2014 - 11:42:07

Fichier

RR-8546.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

675

Téléchargements de fichiers

242