Laurent Mazare
An NP Decision Procedure for Generic Dolev-Yao Constraints with Atomic Keys (2004)
An NP Decision Procedure for Generic Dolev-Yao Constraints with Atomic Keys (2004)
TR-2004-21.ps
Keywords: Security, Cryptographic protocols, Dolev-Yao constraints, Fairness, Protocol composition
Abstract: When considering only a finite number of sessions, protocol insecurity is equivalent to satisfiability of a constraint involving an operator derived from Dolev and Yao $vdash$. Considering only constraints satisfying some properties (these constraints are called well-formed constraints), their satisfiability has been proven NP-complete. As constraints coming from verification of protocol insecurity are well-formed, this result can be generalised to prove that protocol insecurity is a NP-complete problem (when considering a finite number of sessions). However, if we consider constraints with no restriction at all, this allows us to model more complex properties on protocols such as fairness or protocols composition. This paper extends the NP-completness result to general constraints, giving a sketch of the proof that is more complex than the proof for well-formed constraints. We then show how this could be used to verify other security properties.
