Satisfiability of General Intruder Constraints with and without a Set Constructor
Abstract
Many decision problems on security protocols can be reduced to solving so-called intruder constraints in Dolev Yao model. Most constraint solving procedures for protocol security rely on two properties of constraint systems called monotonicity and variable origination. In this work we relax these restrictions by giving a decision procedure for solving general intruder constraints (that do not have these properties) that stays in NP. Our result extends a first work by L. Mazar\'e in several directions: we allow non-atomic keys, and an associative, commutative and idempotent symbol (for modeling sets). We also discuss several new applications of the results.
Cite
@article{arxiv.1103.0220,
title = {Satisfiability of General Intruder Constraints with and without a Set Constructor},
author = {Tigran Avanesov and Yannick Chevalier and Michaël Rusinowitch and Mathieu Turuani},
journal= {arXiv preprint arXiv:1103.0220},
year = {2011}
}
Comments
Submitted to the Special issue of Information and Computation on Security and Rewriting Techniques (SecReT), 2011. 59 pages