Automated analysis of equivalence properties for security protocols using else branches

Ivan Gazeau 1 Steve Kremer 1
1 PESTO - Proof techniques for security protocols
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : In this paper we present an extension of the AKISS protocol verification tool which allows to verify equivalence properties for protocols with else branches, i.e., disequality tests. While many protocols are represented as linear sequences or inputs, outputs and equality tests, the reality is often more complex. When verifying equivalence properties one needs to model precisely the error messages sent out when equality tests fail. While ignoring these branches may often be safe when studying trace properties this is not the case for equivalence properties, as for instance witnessed by an attack on the European electronic passport. One appealing feature of our approach is that our extension re-uses the saturation procedure which is at the heart of the verification procedure of AKISS as a black box, without need to modify it. As a result we obtain the first tool that is able verify equivalence properties for protocols that may use xor and else branches. We demonstrate the tool's effectiveness on several case studies, including the AKA protocol deployed in mobile telephony.
Type de document :
Communication dans un congrès
22nd European Symposium on Research in Computer Security (ESORICS'17), 2017, Oslo, Norway. Springer, 2017
Liste complète des métadonnées

https://hal.inria.fr/hal-01566035
Contributeur : Steve Kremer <>
Soumis le : jeudi 20 juillet 2017 - 16:04:06
Dernière modification le : lundi 30 avril 2018 - 14:32:03

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01566035, version 1

Relations

Citation

Ivan Gazeau, Steve Kremer. Automated analysis of equivalence properties for security protocols using else branches. 22nd European Symposium on Research in Computer Security (ESORICS'17), 2017, Oslo, Norway. Springer, 2017. 〈hal-01566035〉

Partager

Métriques

Consultations de la notice

194

Téléchargements de fichiers

116