Verifying Regular Trace Properties of Security Protocols with Explicit Destructors and Implicit Induction

Adel Bouhoula 1 Florent Jacquemard 2
2 DAHU - Verification in databases
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 : We present a procedure for the verification of cryptographic protocols based on a new method for automatic implicit induction theorem proving for specifications made of conditional and constrained rewrite rules. The method handles axioms between constructor terms which are used to introduce explicit destructor symbols for the specification of cryptographic operators. Moreover, it can deal with non-confluent rewrite systems. This is required in the context of the verification of security protocols because of the non-deterministic behavior of attackers. Our induction method makes an intensive use of constrained tree grammars, which are used in proofs both as induction schemes and as oracles for checking validity and redundancy criteria by reduction to an emptiness problem. The grammars make possible the development of a generic framework for the specification and verification of protocols, where the specifications can be parametrized with (possibly infinite) regular sets of user names or attacker’s initial knowledge and complex security properties can be expressed, referring to some fixed regular sets of bad traces representing potential vulnerabilities. We present some case studies giving very promising results, for the detection of attacks (our procedure is complete for refutation), and also for the validation of protocols.
Type de document :
Communication dans un congrès
Degano, Pierpaolo and Ksters, Ralf and Vigan, Luca and Zdancewic, Steve. Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA), Jul 2007, Poland. pp.27-44, 2007, Proceedings of the Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA)
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00579015
Contributeur : Florent Jacquemard <>
Soumis le : mardi 22 mars 2011 - 23:24:04
Dernière modification le : mardi 5 juin 2018 - 15:54:02
Document(s) archivé(s) le : samedi 3 décembre 2016 - 19:24:00

Fichier

BJ-arspa07.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00579015, version 1

Collections

Citation

Adel Bouhoula, Florent Jacquemard. Verifying Regular Trace Properties of Security Protocols with Explicit Destructors and Implicit Induction. Degano, Pierpaolo and Ksters, Ralf and Vigan, Luca and Zdancewic, Steve. Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA), Jul 2007, Poland. pp.27-44, 2007, Proceedings of the Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA). 〈inria-00579015〉

Partager

Métriques

Consultations de la notice

167

Téléchargements de fichiers

154