Satisfiability of general intruder constraints with and without a set constructor. (May 2017)

• Record Type: Journal Article
• Authors: Avanesov, Tigran; Chevalier, Yannick; Rusinowitch, Michael; Turuani, Mathieu
• Is Part Of: Journal of symbolic computation. Volume 80:Part 1(2017)
• Page Start: 27
• Page End: 61
• Publication Date: 2017-05
• Subjects: ACI -- Deducibility constraints -- Dolev–Yao deduction system -- Multiple intruders -- Security; Mathematics -- Data processing -- Periodicals; Numerical analysis -- Data processing -- Periodicals; Automatic programming (Computer science) -- Periodicals; Mathématiques -- Informatique -- Périodiques; Analyse numérique -- Informatique -- Périodiques; Programmation automatique -- Périodiques; Automatic programming (Computer science); Mathematics -- Data processing; Numerical analysis -- Data processing; Periodicals; Electronic journals; 510.285
• DOI: 10.1016/j.jsc.2016.07.009
• Languages: English
• ISSNs: 0747-7171

Abstract

Abstract: Many decision problems on security protocols can be reduced to solving deduction constraints expressing whether an instance of a given message pattern can be constructed by the intruder. 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. The result is also valid modulo an associative, commutative and idempotent theory. The procedure can be applied to verify security protocols in presence of multiple intruders.