×

Computing knowledge in equational extensions of subterm convergent theories. (English) Zbl 1495.68113

Summary: We study decision procedures for two knowledge problems critical to the verification of security protocols, namely the intruder deduction and the static equivalence problems. These problems can be related to particular forms of context matching and context unification. Both problems are defined with respect to an equational theory and are known to be decidable when the equational theory is given by a subterm convergent term rewrite system (TRS). In this work, we extend this to consider a subterm convergent TRS defined modulo an equational theory, like Commutativity. We present two pairs of solutions for these important problems. The first solves the deduction and static equivalence problems in rewrite systems modulo shallow theories such as Commutativity. The second provides a general procedure that solves the deduction and static equivalence problems in subterm convergent systems modulo syntactic permutative theories, provided a finite measure is ensured. Several examples of such theories are also given.

MSC:

68Q42 Grammars and rewriting systems
68M25 Computer security
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abadi, M. and Cortier, V. (2004). Deciding knowledge in security protocols under equational theories. Research Report RR-5169, INRIA. · Zbl 1099.94026
[2] Abadi, M. and Cortier, V. (2006). Deciding knowledge in security protocols under equational theories. Theoretical Computer Science367 (1-2) 2-32. · Zbl 1153.94339
[3] Abadi, M. and Fournet, C. (2001). Mobile values, new names, and secure communication. In: Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2001), ACM, 104-115. · Zbl 1323.68398
[4] Armando, A., Basin, D. A., Boichut, Y., Chevalier, Y., Compagna, L., Cuéllar, J., Drielsma, P. H., Héam, P., Kouchnarenko, O., Mantovani, J., Mödersheim, S., Von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Viganò, L. and Vigneron, L. (2005). The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K. and Rajamani, S. K. (eds.) 17th International Conference on Computer Aided Verification, CAV 2005, Edinburgh, Scotland, UK, Proceedings, Lecture Notes in Computer Science, vol. 3576, Springer, 281-285. · Zbl 1081.68523
[5] Amadio, R. and Lugiez, D. (2000). On the reachability problem in cryptographic protocols. In: Proceedings of CONCUR 2000 — Concurrency Theory, Springer, 380-394. · Zbl 0999.94538
[6] Ayala-Rincón, M., Fernández, M. and Nantes-Sobrinho, D. (2017). Intruder deduction problem for locally stable theories with normal forms and inverses. Theoretical Computer Science67264-100. · Zbl 1386.68078
[7] Baader, F. and Nipkow, T. (1998). Term Rewriting and All That. Cambridge University Press. · Zbl 0948.68098
[8] Baudet, M., Cortier, V. and Delaune, S. (2013). YAPA: A generic tool for computing intruder knowledge. ACM Transactions on Computational Logic14 (1) 4. · Zbl 1353.68019
[9] Blanchet, B. (2016). Modeling and verifying security protocols with the applied Pi calculus and ProVerif. Foundations and Trends in Privacy and Security1 (1-2) 1-135.
[10] Blanchet, B. (2001). An efficient cryptographic protocol verifier based on prolog rules. In : 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), 11-13 June 2001, Cape Breton, Nova Scotia, Canada. IEEE Computer Society, 82-96.
[11] Chadha, R., Cheval, V., Ciobâcă, S. and Kremer, S. (2016). Automated verification of equivalence properties of cryptographic protocols. ACM Transactions on Computational Logic17 (4) 23:1-23:32. · Zbl 1367.68184
[12] Cheval, V., Cortier, V. and Turuani, M. (2018). A little more conversation, a little less action, a lot more satisfaction: global states in ProVerif. In: 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, IEEE Computer Society, 344-358.
[13] Cheval, V., Kremer, S. and Rakotonirina, I. (2018). The DEEPSEC prover. In: Chockler, H. and Weissenbacher, G. (eds.) Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, Lecture Notes in Computer Science, vol. 10982, Springer, 28-36.
[14] Chevalier, Y., Küsters, R., Rusinowitch, M. and Turuani, M. (2003). Deciding the security of protocols with Diffie-Hellman exponentiation and products in exponents. In Pandya, P. K. and Radhakrishnan, J. (eds.) FSTTCS 2003: Foundations of Software Technology and Theoretical Computer Science, 23rd Conference, Mumbai, India, Lecture Notes in Computer Science, vol. 2914, Springer, 124-135s. · Zbl 1205.94078
[15] Chevalier, Y., Küsters, R., Rusinowitch, M. and Turuani, M. (2005). An NP decision procedure for protocol insecurity with XOR. Theoretical Computer Science338247-274. · Zbl 1068.68057
[16] Chevalier, Y. and Rusinowitch, M. (2008). Hierarchical combination of intruder theories. Information and Computation206 (2-4) 352-377. · Zbl 1147.68396
[17] Ciobâcă, S., Delaune, S. and Kremer, S. (2012). Computing knowledge in security protocols under convergent equational theories. Journal of Automated Reasoning48 (2) 219-262. · Zbl 1242.68098
[18] Cohn-Gordon, K., Cremers, C., Garratt, L., Millican, J. and Milner, K. (2018). On ends-to-ends encryption: Asynchronous group messaging with strong security guarantees. In: Conference on Computer and Communications Security, CCS 2018, Toronto, Canada, ACM, 1802-1819.
[19] Comon-Lundh, H. and Delaune, S. (2005). The finite variant property: How to get rid of some algebraic properties. In: Giesl, J. (ed.) Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 3467, Springer, 294-307. · Zbl 1078.68059
[20] Comon, H., Haberstrau, M. and Jouannaud, J.-P. (1994). Syntacticness, cycle-syntacticness, and shallow theories. Information and Computation111(1) 154-191. · Zbl 0807.68062
[21] Comon-Lundh, H. and Shmatikov, V. (2003). Intruder deductions, constraint solving and insecurity decision in presence of exclusive or. In: 18th Annual IEEE Symposium on Logic in Computer Science (LICS 2003), 271-280.
[22] Conchinha, B., Basin, D. A. and Caleiro, C. (2011). FAST: An efficient decision procedure for deduction and static equivalence. In: Schmidt-Schauß, M. (ed.) Proceedings of RTA 2011, Novi Sad, Serbia, LIPIcs, vol. 10, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 11-20. · Zbl 1236.94073
[23] Cortier, V. and Delaune, S. (2010). Decidability and combination results for two notions of knowledge in security protocols. Journal of Automated Reasoning48(4) 441-487. · Zbl 1242.68099
[24] Cremers, C. J. F. (2008). The Scyther tool: Verification, falsification, and analysis of security protocols. In: Gupta, A. and Malik, S. (eds.) 20th International Conference on Computer Aided Verification (CAV 2008), Princeton, NJ, USA, July 7-14, 2008, Proceedings, Lecture Notes in Computer Science, vol. 5123, Springer, 414-418.
[25] Dolev, D. and Yao, A. C. (1981). On the security of public key protocols (extended abstract). In: 22nd Annual Symposium on Foundations of Computer Science, Nashville, Tennessee, USA, IEEE Computer Society, 350-357.
[26] Dreier, J., Hirschi, L., Radomirovic, S. and Sasse, R. (2018). Automated unbounded verification of stateful cryptographic protocols with exclusive or. In: 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, IEEE Computer Society, 359-373.
[27] Erbatur, S., Marshall, A. M. and Ringeissen, C. (2017). Notions of knowledge in combinations of theories sharing constructors. In: De Moura, L. (ed.) Automated Deduction - CADE-26, 26th International Conference on Automated Deduction, Gothenburg, Sweden, Proceedings, Lecture Notes in Computer Science, vol. 10395, Springer, 60-76. · Zbl 1494.68035
[28] Erbatur, S., Marshall, A. M. and Ringeissen, C. (2018). Knowledge problems in equational extensions of subterm convergent theories. In: 32nd International Workshop on Unification (UNIF-2018), Oxford, UK.
[29] Escobar, S., Meadows, C. A. and Meseguer, J. (2007). Maude-NPA: Cryptographic protocol analysis modulo equational properties. In: Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures, Lecture Notes in Computer Science, vol. 5705, Springer, 1-50. · Zbl 1252.94061
[30] Escobar, S., Sasse, R. and Meseguer, J. (2012). Folding variant narrowing and optimal variant termination. Journal of Logic and Algebraic Programming81 (7-8) 898-928. · Zbl 1291.68217
[31] Hullot, J. (1980). Canonical forms and unification. In: Bibel, W. and Kowalski, R. A. (eds.) 5th Conference on Automated Deduction, Les Arcs, France, July 8-11, 1980, Proceedings, Lecture Notes in Computer Science, vol. 87, Springer, 318-334. · Zbl 0441.68108
[32] Jouannaud, J.-P. and Kirchner, H. (1986). Completion of a set of rules modulo a set of equations. SIAM Journal on Computing15 (4) 1155-1194. · Zbl 0665.03005
[33] Kirchner, C. and Klay, F. (1990). Syntactic theories and unification. In: Fifth Annual IEEE Symposium on Logic in Computer Science (LICS 1990), 270-277.
[34] Lynch, C. and Morawska, B. (2002). Basic syntactic mutation. In: Voronkov, A. (ed.) Automated Deduction - CADE-18, 18th International Conference on Automated Deduction, Proceedings, Lecture Notes in Computer Science, vol. 2392, Springer, 471-485. · Zbl 1072.68581
[35] Meseguer, J. (2018). Variant-based satisfiability in initial algebras. Science of Computer Programming1543-41.
[36] Millen, J. and Shmatikov, V. (2001). Constraint solving for bounded-process cryptographic protocol analysis. In: Proceedings of the 8th ACM Conference on Computer and Communications Security (CCS 2001), ACM, 166-175.
[37] Mödersheim, S. and Viganò, L. (2009). The open-source fixed-point model checker for symbolic analysis of security protocols. In: Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures, Lecture Notes in Computer Science, vol. 5705, Springer, 166-194. · Zbl 1252.68193
[38] Nguyen, K. (2019). Formal verification of a messaging protocol. Work done under the supervision of Vincent Cheval and Véronique Cortier.
[39] Nipkow, T. (1990). Proof transformations for equational theories. In: Fifth Annual IEEE Symposium on Logic in Computer Science (LICS 1990), 278-288.
[40] Paulson, L. C. (1998). The inductive approach to verifying cryptographic protocols. Computer Security6(1-2) 85-128.
[41] Ringeissen, C. (2019). Building and combining matching algorithms. In: Lutz, C., Sattler, U., Tinelli, C., Turhan, A. Y. and Wolter, F. (eds.) Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, Lecture Notes in Computer Science, vol. 11560, Springer, 523-541. · Zbl 1428.68036
[42] Sasse, R., Escobar, S., Meadows, C., Meseguer, J. (2011). Protocol analysis modulo combination of theories: A case study in Maude-NPA. In: Proceedings of International Workshop on Security and Trust Management, Springer, 163-178.
[43] Schmidt, B., Meier, S., Cremers, C. J. F. and Basin, D. A. (2012). Automated analysis of Diffie-Hellman protocols and advanced security properties. In: Chong, S. (ed.) 25th IEEE Computer Security Foundations Symposium, CSF 2012, Cambridge, MA, USA, June 25-27, 2012, IEEE Computer Society, 78-94.
[44] Schmidt-Schauß, M. (1989). Unification in permutative equational theories is undecidable. Journal of Symbolic Computation8 (4) 415-421. · Zbl 0684.03019
[45] Turuani, M. (2006). The CL-Atse protocol analyser. In: Pfenning, F. (ed.) Term Rewriting and Applications, 17th International Conference, RTA 2006, Seattle, WA, USA, August 12-14, 2006, Proceedings, Lecture Notes in Computer Science, vol. 4098, Springer, 277-286. · Zbl 1151.68454
[46] Yang, F., Escobar, S., Meadows, C., Meseguer, J. and Narendran, P. (2014). Theories of homomorphic encryption, unification, and the finite variant property. In: Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming (PPDP 2014), ACM, 123-133.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.