Stéphanie Delaune and Florent Jacquemard. A Decision Procedure for the Verification of Security Protocols with Explicit Destructors. In Proceedings of the 11th ACM Conference on Computer and Communications Security (CCS'04), pp. 278–287, ACM Press, Washington, D.C., USA, October 2004.
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.
@inproceedings{dj-ccs-2004,
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, \emph{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.},
address = {Washington, D.C., USA},
author = {Delaune, St{\'e}phanie and Jacquemard, Florent},
booktitle = {{P}roceedings of the 11th {ACM} {C}onference on
{C}omputer and {C}ommunications {S}ecurity
({CCS}'04)},
editor = {Atluri, Vijayalakshmi and Pfitzmann, Birgit and
McDaniel, Patrick},
month = oct,
pages = {278-287},
publisher = {ACM Press},
title = {A Decision Procedure for the Verification of Security
Protocols with Explicit Destructors},
year = {2004},
acceptrate = {35/251},
acronym = {{CCS}'04},
nmonth = {10},
}