Automated Verification of Equivalence Properties of Cryptographic Protocols

Rohit Chadha 1 Vincent Cheval 2 Stefan Ciobaca 3 Steve Kremer 4
4 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 properties, strong versions of confidentiality and resistance against offline guessing attacks, which can be conveniently modeled using process equivalences. We present a novel procedure to verify equivalence properties for a bounded number of sessions of cryptographic protocols. As in the applied pi-calculus, our protocol specification language is parametrized by a first-order sorted term signature and an equational theory which allows formalization of algebraic properties of cryptographic primitives. Our procedure is able to verify trace equivalence for determi-nate 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 that can be modeled by an optimally reducing convergent rewrite system. The procedure is based on a fully abstract modelling of the traces of a bounded number of sessions of the protocols into first-order Horn clauses on which a dedicated resolution procedure is used to decide equivalence properties. We have shown that our procedure terminates for the class of subterm convergent equational theories. Moreover, the procedure has been implemented in a prototype tool A-KiSs (Active Knowledge in Security Protocols) and has been effectively tested on examples. Some of the examples were outside the scope of existing tools, including checking anonymity of an electronic voting protocol.
Type de document :
Rapport
[Technical Report] Inria. 2012
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00632564
Contributeur : Steve Kremer <>
Soumis le : mercredi 16 décembre 2015 - 15:08:25
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10
Document(s) archivé(s) le : samedi 29 avril 2017 - 16:48:48

Fichier

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

Identifiants

Citation

Rohit Chadha, Vincent Cheval, Stefan Ciobaca, Steve Kremer. Automated Verification of Equivalence Properties of Cryptographic Protocols. [Technical Report] Inria. 2012. 〈inria-00632564v4〉

Partager

Métriques

Consultations de la notice

356

Téléchargements de fichiers

203