Title : Satisfiability of general intruder constraints with a set constructor
Language : English
Author, co-author : Avanesov, Tigran [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
Chevalier, Yannick [> >]
Rusinowitch, Michael [> >]
Turuani, Mathieu [> >]
Publication date : 2010
Main document title : CRiSIS 2010, Proceedings of the Fifth International Conference on Risks and Security of Internet and Systems, Montreal, QC, Canada, October 10-13, 2010.
Publisher : IEEE
Pages : 1-8
Peer reviewed : Yes
ISBN : 978-1-4244-8641-0
Event name : CRiSIS 2010
Event date : October 10-13, 2010
Event place (city) : Montreal, QC
Event country : Canada
Abstract : [en] 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 an NP decision procedure for solving general intruder constraints (that do not have these properties). 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 give several new applications of the result.
Permalink : http://hdl.handle.net/10993/3840
DOI : 10.1109/CRISIS.2010.5764919
Commentary : Proceedings of the Fifth International Conference on Risks and Security of Internet and Systems (CRiSIS 2010)