A Decision Procedure for the Verification of Security Protocols with Explicit Destructors

Stéphanie Delaune 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 non-deterministic polynomial time procedure to decide the problem of insecurity, in the presence of a bounded number of sessions, for cryptographic protocols containing explicit destructor symbols, like decryption and projection. These operators are axiomatized by an arbitrary convergent rewrite system satisfying some syntactic restrictions. This approach, with parameterized semantics, allows us to weaken the security hypotheses for verification, i.e. to address a larger class of attacks than for models based on free algebra. Our procedure is defined by an inference system based on basic narrowing techniques for deciding satisfiability of combinations of first-order equations and intruder deduction constraints.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/inria-00579012
Contributor : Florent Jacquemard <>
Submitted on : Tuesday, March 22, 2011 - 11:11:38 PM
Last modification on : Thursday, February 7, 2019 - 5:29:22 PM
Long-term archiving on : Thursday, June 23, 2011 - 2:59:30 AM

Files

DJ-ccs-2004.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00579012, version 1

Collections

Citation

Stéphanie Delaune, Florent Jacquemard. A Decision Procedure for the Verification of Security Protocols with Explicit Destructors. 11th ACM Conference on Computer and Communications Security (CCS), Oct 2004, Washington D.C., United States. pp.278-287. ⟨inria-00579012⟩

Share

Metrics

Record views

183

Files downloads

184