From security protocols to pushdown automata

Rémy Chrétien 1, 2 Véronique Cortier 1 Stéphanie Delaune 2
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
2 SECSI - Security of information systems
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : Formal methods have been very successful in analyzing security protocols for reachability properties such as secrecy or authentication. In contrast, there are very few results for equivalence-based properties, crucial for studying e.g. privacy-like properties such as anonymity or vote secrecy. We study the problem of checking equivalence of security protocols for an unbounded number of sessions. Since replication leads very quickly to undecidability (even in the simple case of secrecy), we focus on a limited fragment of protocols (standard primitives but pairs, one variable per protocol's rules) for which the secrecy preservation problem is known to be decidable. Surprisingly, this fragment turns out to be undecidable for equivalence. Then, restricting our attention to deterministic protocols, we propose the first decidability result for checking equivalence of protocols for an unbounded number of sessions. This result is obtained through a characterization of equivalence of protocols in terms of equality of languages of (generalized, real-time) deterministic pushdown automata.
Type de document :
Communication dans un congrès
Fedor V. Fomin and Rūsiņš Freivalds and Marta Kwiatkowska and David Peleg. ICALP'2013 - 40th International Colloquium on Automata, Languages and Programming - 2013, Jul 2013, Riga, Lithuania. Springer, 7966, pp.137-149, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-39212-2_15〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00881066
Contributeur : Véronique Cortier <>
Soumis le : jeudi 7 novembre 2013 - 14:11:37
Dernière modification le : jeudi 15 février 2018 - 08:48:14

Lien texte intégral

Identifiants

Citation

Rémy Chrétien, Véronique Cortier, Stéphanie Delaune. From security protocols to pushdown automata. Fedor V. Fomin and Rūsiņš Freivalds and Marta Kwiatkowska and David Peleg. ICALP'2013 - 40th International Colloquium on Automata, Languages and Programming - 2013, Jul 2013, Riga, Lithuania. Springer, 7966, pp.137-149, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-39212-2_15〉. 〈hal-00881066〉

Partager

Métriques

Consultations de la notice

333