Automated verification of equivalence properties of cryptographic protocols

Rohit Chadha 1 Stefan Ciobaca 1, 2 Steve Kremer 2
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 : Indistinguishability properties are essential in formal verification of cryptographic protocols. They are needed to model anonymity of cryptographic protocols. They are needed to model anonymity properties, strong versions of confidentiality and resistance to offline guessing attacks, and can be conveniently modeled using process equivalences. We present a novel procedure to verify equivalence properties for bounded number of sessions. Our procedure is able to verify trace equivalence for determinate cryptographic protocols. On determinate protocols, trace equivalence coincides with observational equivalence which can therefore be automatically verified for such processes. When protocols are not determinate our procedure can be used for both under- and over-approximations of trace equivalence, which proved successful on examples. The procedure can handle a large set of cryptographic primitives, namely those which can be modeled by an optimally reducing convergent rewrite system. Although, we were unable to prove its termination, it has been implemented in a prototype tool and has been effectively tested on examples, some of which were outside the scope of existing tools.
Type de document :
Communication dans un congrès
Helmut Seidl. 21th European Symposium on Programming (ESOP'12), Mar 2012, Talinn, Estonia. Springer, 7211, pp.108-127, 2012, Proceedings of the 21th European Symposium on Programming (ESOP'12). 〈10.1007/978-3-642-28869-2_6〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00732905
Contributeur : Steve Kremer <>
Soumis le : jeudi 8 octobre 2015 - 20:39:43
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10
Document(s) archivé(s) le : samedi 9 janvier 2016 - 10:42:04

Fichier

CCK-esop12.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Rohit Chadha, Stefan Ciobaca, Steve Kremer. Automated verification of equivalence properties of cryptographic protocols. Helmut Seidl. 21th European Symposium on Programming (ESOP'12), Mar 2012, Talinn, Estonia. Springer, 7211, pp.108-127, 2012, Proceedings of the 21th European Symposium on Programming (ESOP'12). 〈10.1007/978-3-642-28869-2_6〉. 〈hal-00732905〉

Partager

Métriques

Consultations de la notice

625

Téléchargements de fichiers

61