Security Protocol Verification with Implicit Induction and Explicit Destructors

Adel Bouhoula 1 Florent Jacquemard 2
2 DAHU - Verification in databases
CNRS - Centre National de la Recherche Scientifique : UMR8643, Inria Saclay - Ile de France, ENS Cachan - École normale supérieure - Cachan, LSV - Laboratoire Spécification et Vérification [Cachan]
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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [7 references]  Display  Hide  Download

https://hal.inria.fr/inria-00579018
Contributor : Florent Jacquemard <>
Submitted on : Tuesday, March 22, 2011 - 11:36:15 PM
Last modification on : Thursday, February 7, 2019 - 5:29:24 PM
Long-term archiving on : Thursday, June 23, 2011 - 3:00:44 AM

File

BJ-secret06.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00579018, version 1

Collections

Citation

Adel Bouhoula, Florent Jacquemard. Security Protocol Verification with Implicit Induction and Explicit Destructors. 1st International Workshop on Security and Rewriting Techniques (SecReT), Jul 2006, Venice, Italy. pp.37-44. ⟨inria-00579018⟩

Share

Metrics

Record views

153

Files downloads

260