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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [13 references]  Display  Hide  Download

https://hal.inria.fr/inria-00579015
Contributor : Florent Jacquemard <>
Submitted on : Tuesday, March 22, 2011 - 11:24:04 PM
Last modification on : Thursday, February 7, 2019 - 5:29:23 PM
Long-term archiving on : Saturday, December 3, 2016 - 7:24:00 PM

File

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

Identifiers

  • 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. Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA), Jul 2007, Poland. pp.27-44. ⟨inria-00579015⟩

Share

Metrics

Record views

208

Files downloads

164