2010 • In CRiSIS 2010, Proceedings of the Fifth International Conference on Risks and Security of Internet and Systems, Montreal, QC, Canada, October 10-13, 2010.
[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.
Disciplines :
Computer science
Identifiers :
UNILU:UL-CONFERENCE-2012-442
Author, co-author :
Avanesov, Tigran ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT)
Chevalier, Yannick
Rusinowitch, Michael
Turuani, Mathieu
Language :
English
Title :
Satisfiability of general intruder constraints with a set constructor
Publication date :
2010
Event name :
CRiSIS 2010
Event place :
Montreal, QC, Canada
Event date :
October 10-13, 2010
Main work 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
ISBN/EAN :
978-1-4244-8641-0
Pages :
1-8
Peer reviewed :
Peer reviewed
Commentary :
Proceedings of the Fifth International Conference on Risks and Security of Internet and Systems (CRiSIS 2010)
J. Millen and V. Shmatikov, "Constraint solving for bounded-process cryptographic protocol analysis," in Proceedings of the 8th ACM conference on Computer and Communications Security, ser. CCS '01. New York, NY, USA: ACM, 2001, pp. 166-175.
D. Basin, S. Mödersheim, and L. Viganò, "Ofmc: A symbolic model checker for security protocols," International Journal of Information Security, vol. 4, pp. 181-208, Jun. 2005.
M. Turuani, "The CL-Atse Protocol Analyser," in Term Rewriting and Applications (RTA), 2006, pp. 277-286.
C. Cremers, "The Scyther Tool: Verification, falsification, and analysis of security protocols," in Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, USA, Proc., ser. Lecture Notes in Computer Science, vol. 5123/2008. Springer, 2008, pp. 414-418.
D. Basin, S. Mödersheim, and L. Viganò, "Algebraic intruder deductions," in Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), 2005, pp. 549-564.
V. Cortier, S. Delaune, and P. Lafourcade, "A survey of algebraic properties used in cryptographic protocols," Journal of Computer Security, vol. 14, no. 1, pp. 1-43, 2006.
S. Delaune, P. Lafourcade, D. Lugiez, and R. Treinen, "Symbolic protocol analysis for monoidal equational theories," Information and Computation, vol. 206, no. 2-4, pp. 312-351, Feb.-Apr. 2008.
L. Mazaré, "Satisfiability of Dolev-Yao Constraints," Electronic Notes in Theoretical Computer Science, vol. 125, no. 1, pp. 109-124, 2005.
-, "Computational Soundness of Symbolic Models for Cryptographic Protocols," Ph.D. dissertation, Institut National Polytechnique de Grenoble, Oct. 2006.
P. Syverson, C. Meadows, and I. Cervesato, "Dolev-Yao is no better than Machiavelli," in First Workshop on Issues in the Theory of Security - WITS'00, 2000, pp. 87-92.
M. Rusinowitch and M. Turuani, "Protocol insecurity with a finite number of sessions, composed keys is np-complete," Theor. Comput. Sci., vol. 1-3, no. 299, pp. 451-475, 2003.
Y. Chevalier, R. Küsters, M. Rusinowitch, and M. Turuani, "An NP decision procedure for protocol insecurity with XOR," Theor. Comput. Sci., vol. 338, no. 1-3, pp. 247-274, 2005.
V. Shmatikov, "Decidable analysis of cryptographic protocols with products and modular exponentiation," in In Proc. 13th European Symposium on Programming (ESOP '04), volume 2986 of LNCS. Springer-Verlag, 2004, pp. 355-369.
Y. Chevalier, D. Lugiez, and M. Rusinowitch, "Towards an automatic analysis of web service security," in FroCoS 2007, Liverpool, UK, September 10-12, ser. Lecture Notes in Computer Science, vol. 4720. Springer, 2007, pp. 133-147.
T. Avanesov, Y. Chevalier, M. Rusinowitch, and M. Turuani, "Satisfiability of General Intruder Constraints with and without a Set Constructor," INRIA, Research Report RR-7276, 05 2010. [Online]. Available: http://hal.inria.fr/inria-00480632/en/
