A decision procedure for the verification of security protocols with explicit destructors

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 nference system based on basic narrowing techniques for deciding satisfiability of combinations of first-order equations and intruder deduction constraints.