Stéphanie Delaune and Florent Jacquemard. Narrowing-Based Constraint Solving for the Verification of Security Protocols. In Proceedings of the 18th International Workshop on Unification (UNIF'04), Cork, Ireland, July 2004.
We investigate the resolution of a class of symbolic constraints modulo an equational theory presented by a convergent rewriting system. These constraints are combinations of first-order equations and so-called deduction constraints which can be seen as restricted second-order unification problems. We propose an inference system based on basic narrowing techniques for deciding satisfiability of such constraints, and show its completeness and termination when the rewrite system satisfies some syntactic restrictions.
This result is applied to show NP-completeness of the cryptographic protocols insecurity problem for a bounded number of sessions, when the protocol and intruder semantics are defined by an arbitrary convergent rewrite system in our class. This generalizes former results, as we show that the use of parameterized semantics permits to weaken the security hypotheses for verification, i.e. to address a larger class of attacks.
@inproceedings{dj-unif2004,
abstract = {We investigate the resolution of a class of symbolic
constraints modulo an equational theory presented by
a convergent rewriting system. These constraints are
combinations of first-order equations and so-called
deduction constraints which can be seen as restricted
second-order unification problems. We propose an
inference system based on basic narrowing techniques
for deciding satisfiability of such constraints, and
show its completeness and termination when the
rewrite system satisfies some syntactic
restrictions.\par This result is applied to show
NP-completeness of the cryptographic protocols
insecurity problem for a bounded number of sessions,
when the protocol and intruder semantics are defined
by an arbitrary convergent rewrite system in our
class. This generalizes former results, as we show
that the use of parameterized semantics permits to
weaken the security hypotheses for verification, i.e.
to address a larger class of attacks.},
address = {Cork, Ireland},
author = {Delaune, St{\'e}phanie and Jacquemard, Florent},
booktitle = {{P}roceedings of the 18th {I}nternational {W}orkshop
on {U}nification ({UNIF}'04)},
editor = {Kohlhase, Michael},
month = jul,
title = {Narrowing-Based Constraint Solving for the
Verification of Security Protocols},
year = {2004},
acronym = {{UNIF}'04},
nmonth = {7},
}