Security Protocol Verification with Implicit Induction and Explicit Destructors

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 new method for automatic implicit induction theorem proving, and its application for the verification of a key distribution cryptographic protocol. The method can handle axioms between constructor terms, a feature generally not supported by other induction procedure. We use such axioms in order to specify explicit destructors representing cryptographic operators.
Type de document :
Communication dans un congrès
Fernández, Maribel and Kirchner, Claude. 1st International Workshop on Security and Rewriting Techniques (SecReT), Jul 2006, Venice, Italy. pp.37-44, 2006, Proceedings of the 1st International Workshop on Security and Rewriting Techniques (SecReT)
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00579018
Contributeur : Florent Jacquemard <>
Soumis le : mardi 22 mars 2011 - 23:36:15
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : jeudi 23 juin 2011 - 03:00:44

Fichier

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

Identifiants

  • HAL Id : inria-00579018, version 1

Collections

Citation

Adel Bouhoula, Florent Jacquemard. Security Protocol Verification with Implicit Induction and Explicit Destructors. Fernández, Maribel and Kirchner, Claude. 1st International Workshop on Security and Rewriting Techniques (SecReT), Jul 2006, Venice, Italy. pp.37-44, 2006, Proceedings of the 1st International Workshop on Security and Rewriting Techniques (SecReT). 〈inria-00579018〉

Partager

Métriques

Consultations de la notice

119

Téléchargements de fichiers

245