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}, }