Decidability of trace equivalence for protocols with nonces

Rémy Chrétien 1, 2 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 : Privacy properties such as anonymity, unlinkability, or vote secrecy are typically expressed as equivalence properties. In this paper, we provide the first decidability result for trace equivalence of security protocols, for an unbounded number of sessions and unlimited fresh nonces. Our class encompasses most symmetric key protocols of the literature, in their tagged variant.
Type de document :
Communication dans un congrès
28th IEEE Computer Security Foundations Symposium (CSF'15), Jul 2015, Verona, Italy. Proceedings of the 28th IEEE Computer Security Foundations Symposium (CSF'15), 〈10.1109/CSF.2015.19〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01206276
Contributeur : Véronique Cortier <>
Soumis le : lundi 28 septembre 2015 - 16:45:23
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10
Document(s) archivé(s) le : mardi 29 décembre 2015 - 10:52:33

Fichier

CCD-csf15.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Rémy Chrétien, Véronique Cortier, Stéphanie Delaune. Decidability of trace equivalence for protocols with nonces. 28th IEEE Computer Security Foundations Symposium (CSF'15), Jul 2015, Verona, Italy. Proceedings of the 28th IEEE Computer Security Foundations Symposium (CSF'15), 〈10.1109/CSF.2015.19〉. 〈hal-01206276〉

Partager

Métriques

Consultations de la notice

319

Téléchargements de fichiers

76