Hostname: page-component-cd9895bd7-7cvxr Total loading time: 0 Render date: 2024-12-23T19:52:53.142Z Has data issue: false hasContentIssue false
  • English
  • Français

Computing knowledge in equational extensions of subterm convergent theories

Published online by Cambridge University Press:  02 March 2020

Serdar Erbatur Open the ORCID record for Serdar Erbatur [Opens in a new window] ,
Andrew M. Marshall Open the ORCID record for Andrew M. Marshall [Opens in a new window]  and
Christophe Ringeissen Open the ORCID record for Christophe Ringeissen [Opens in a new window]
Serdar Erbatur
Affiliation:
University of Texas at Dallas, Richardson, TX, USA
Andrew M. Marshall
Affiliation:
University of Mary Washington, Fredericksburg, VA, USA
Christophe Ringeissen*
Affiliation:
Université de Lorraine, CNRS, Inria, LORIA, F-54000Nancy, France
*
*Corresponding author. Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

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.

Keywords

Equational theoriesdecision proceduressecurity protocolsdeductionstatic equivalence
Type
Paper
Information
Mathematical Structures in Computer Science , Volume 30 , Special Issue 6: Special Issue: Unification , June 2020 , pp. 683 - 709
Copyright
© The Author(s) 2020. Published by Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abadi, M. and Cortier, V. (2004). Deciding knowledge in security protocols under equational theories. Research Report RR-5169, INRIA.CrossRefGoogle Scholar
Abadi, M. and Cortier, V. (2006). Deciding knowledge in security protocols under equational theories. Theoretical Computer Science 367 (1–2) 2–32.CrossRefGoogle Scholar
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.CrossRefGoogle Scholar
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.Google Scholar
Amadio, R. and Lugiez, D. (2000). On the reachability problem in cryptographic protocols. In: Proceedings of CONCUR 2000 — Concurrency Theory, Springer, 380–394.CrossRefGoogle Scholar
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 Science 672 64–100.CrossRefGoogle Scholar
Baader, F. and Nipkow, T. (1998). Term Rewriting and All That. Cambridge University Press.CrossRefGoogle Scholar
Baudet, M., Cortier, V. and Delaune, S. (2013). YAPA: A generic tool for computing intruder knowledge. ACM Transactions on Computational Logic 14 (1) 4.CrossRefGoogle Scholar
Blanchet, B. (2016). Modeling and verifying security protocols with the applied Pi calculus and ProVerif. Foundations and Trends in Privacy and Security 1 (1–2) 1–135.CrossRefGoogle Scholar
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.Google Scholar
Chadha, R., Cheval, V., Ciobâcă, S. and Kremer, S. (2016). Automated verification of equivalence properties of cryptographic protocols. ACM Transactions on Computational Logic 17 (4) 23:1–23:32.CrossRefGoogle Scholar
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.Google Scholar
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.Google Scholar
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.CrossRefGoogle Scholar
Chevalier, Y., Küsters, R., Rusinowitch, M. and Turuani, M. (2005). An NP decision procedure for protocol insecurity with XOR. Theoretical Computer Science 338 247–274.CrossRefGoogle Scholar
Chevalier, Y. and Rusinowitch, M. (2008). Hierarchical combination of intruder theories. Information and Computation 206 (2–4) 352–377.CrossRefGoogle Scholar
Ciobâcă, S., Delaune, S. and Kremer, S. (2012). Computing knowledge in security protocols under convergent equational theories. Journal of Automated Reasoning 48 (2) 219–262.CrossRefGoogle Scholar
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.Google Scholar
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.Google Scholar
Comon, H., Haberstrau, M. and Jouannaud, J.-P. (1994). Syntacticness, cycle-syntacticness, and shallow theories. Information and Computation 111(1) 154–191.CrossRefGoogle Scholar
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.CrossRefGoogle Scholar
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.Google Scholar
Cortier, V. and Delaune, S. (2010). Decidability and combination results for two notions of knowledge in security protocols. Journal of Automated Reasoning 48(4) 441–487.CrossRefGoogle Scholar
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.CrossRefGoogle Scholar
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.Google Scholar
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.Google Scholar
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.CrossRefGoogle Scholar
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.Google Scholar
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.Google Scholar
Escobar, S., Sasse, R. and Meseguer, J. (2012). Folding variant narrowing and optimal variant termination. Journal of Logic and Algebraic Programming 81 (7–8) 898–928.CrossRefGoogle Scholar
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.Google Scholar
Jouannaud, J.-P. and Kirchner, H. (1986). Completion of a set of rules modulo a set of equations. SIAM Journal on Computing 15 (4) 1155–1194.CrossRefGoogle Scholar
Kirchner, C. and Klay, F. (1990). Syntactic theories and unification. In: Fifth Annual IEEE Symposium on Logic in Computer Science (LICS 1990), 270–277.CrossRefGoogle Scholar
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.CrossRefGoogle Scholar
Meseguer, J. (2018). Variant-based satisfiability in initial algebras. Science of Computer Programming 154 3–41.CrossRefGoogle Scholar
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.Google Scholar
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.CrossRefGoogle Scholar
Nguyen, K. (2019). Formal verification of a messaging protocol. Work done under the supervision of Vincent Cheval and Véronique Cortier.Google Scholar
Nipkow, T. (1990). Proof transformations for equational theories. In: Fifth Annual IEEE Symposium on Logic in Computer Science (LICS 1990), 278–288.CrossRefGoogle Scholar
Paulson, L. C. (1998). The inductive approach to verifying cryptographic protocols. Computer Security 6(1–2) 85–128.CrossRefGoogle Scholar
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.CrossRefGoogle Scholar
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.CrossRefGoogle Scholar
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.Google Scholar
Schmidt-Schauß, M. (1989). Unification in permutative equational theories is undecidable. Journal of Symbolic Computation 8 (4) 415–421.CrossRefGoogle Scholar
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.Google Scholar
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.Google Scholar