arXiv · 1103.0220
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é 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.
Explore related subjects
Keep this discovery
Tigran Avanesov, Yannick Chevalier, Michaël Rusinowitch, Mathieu Turuani. 2011-03-01. Satisfiability of General Intruder Constraints with and without a Set Constructor. https://arxiv.org/abs/1103.0220
Cite the original work for its findings. Save a collection to share your selection of sources.