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) 
[University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
