inria-00579018, version 1
Security Protocol Verification with Implicit Induction and Explicit Destructors
Adel Bouhoula 1Florent Jacquemard
2
1st International Workshop on Security and Rewriting Techniques (SecReT) (2006) 37-44
Résumé : 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.
- 1 : Ecole supérieure des télécommunications de Tunis (SUP'COM [TUNIS])
- SUP'COM
- 2 : DAHU (INRIA Saclay - Ile de France)
- INRIA – Ecole Nationale Supérieure de Cachan – CNRS : UMR8643
- Domaine : Informatique/Logique en informatique
- inria-00579018, version 1
- http://hal.inria.fr/inria-00579018
- oai:hal.inria.fr:inria-00579018
- Contributeur : Florent Jacquemard
- Soumis le : Mardi 22 Mars 2011, 23:36:15
- Dernière modification le : Mercredi 23 Mars 2011, 10:27:27
Documents associés
Exporter