Skip to Main content Skip to Navigation
Conference papers

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], Inria Saclay - Ile de France
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [13 references]  Display  Hide  Download
Contributor : Florent Jacquemard Connect in order to contact the contributor
Submitted on : Tuesday, March 22, 2011 - 11:24:04 PM
Last modification on : Thursday, January 20, 2022 - 4:12:12 PM
Long-term archiving on: : Saturday, December 3, 2016 - 7:24:00 PM


Files produced by the author(s)


  • HAL Id : inria-00579015, version 1


Adel Bouhoula, Florent Jacquemard. Verifying Regular Trace Properties of Security Protocols with Explicit Destructors and Implicit Induction. Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA), Jul 2007, Poland. pp.27-44. ⟨inria-00579015⟩



Record views


Files downloads