Document Open Access Logo

Knowledge Problems vs Unification and Matching: Dichotomy Results

Authors Serdar Erbatur , Andrew M. Marshall , Paliath Narendran , Christophe Ringeissen

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.FSCD.2025.18.pdf
  • Filesize: 0.7 MB
  • 17 pages
HTML5 Logo HTML (experimental)
LIPIcs.FSCD.2025.18.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
Keywords
  • Knowledge Problems
  • Unification
  • Matching
  • Decidability

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

The research area of cryptographic protocol analysis contains a number of innovative algorithms and procedures for checking various security properties of protocols. Most of these procedures focus on solving one of several "knowledge problems" that model intruder knowledge. Solving these problems can demonstrate the ability of the intruder to obtain some forbidden information of the protocol, such as secret keys. Two important examples of these problems are the deduction problem and the static equivalence problem.
Deduction is concerned with the ability to derive a term from a set of terms (or knowledge) obtained from the observation of a protocol instance. Static equivalence, on the other hand, is concerned with distinguishing between two runs of a protocol based on two sets of knowledge. These two knowledge problems at first inspection appear to be very close to the older automated reasoning problems of matching and unification. However, this first impression is wrong, and there have been a few results that have shown theories where one problem, such as unification, is undecidable but another problem, such as deduction, is decidable. These existing dichotomy results were, however, incomplete, and not all cases had been examined, thus leaving the possibility of some connection between the problems for those unexamined cases.
In this paper, we consider the missing dichotomy cases. For each of the remaining cases, we demonstrate a theory that separates the two problems. In addition, once the dichotomy results are completed, it leaves open the question of the existence of non-trivial classes of theories for which all four of the problems are decidable. One example for which this is true is the well-known class of subterm convergent term rewrite systems. In this paper, we develop another example, a class of restrictive permutative theories for which all problems are likewise decidable.

Cite As Get BibTex

Serdar Erbatur, Andrew M. Marshall, Paliath Narendran, and Christophe Ringeissen. Knowledge Problems vs Unification and Matching: Dichotomy Results. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.FSCD.2025.18

Author Details

Serdar Erbatur
  • University of Texas at Dallas, Richardson, TX, USA
Andrew M. Marshall
  • University of Mary Washington, Fredericksburg, VA, USA
Paliath Narendran
  • University at Albany, SUNY, Albany, NY, USA
Christophe Ringeissen
  • Université de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France

References

  1. Martín Abadi, Mathieu Baudet, and Bogdan Warinschi. Guessing attacks and the computational soundness of static equivalence. In Luca Aceto and Anna Ingólfsdóttir, editors, Foundations of Software Science and Computation Structures, 9th International Conference, FOSSACS 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25-31, 2006, Proceedings, volume 3921 of Lecture Notes in Computer Science, pages 398-412, Berlin, Heidelberg, 2006. Springer. URL: https://doi.org/10.1007/11690634_27.
  2. Martín Abadi and Véronique Cortier. Deciding knowledge in security protocols under equational theories. Theor. Comput. Sci., 367(1-2):2-32, 2006. URL: https://doi.org/10.1016/j.tcs.2006.08.032.
  3. Martín Abadi and Cédric Fournet. Mobile values, new names, and secure communication. In Chris Hankin and Dave Schmidt, editors, Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, UK, January 17-19, 2001, pages 104-115. ACM, 2001. URL: https://doi.org/10.1145/360204.360213.
  4. Siva Anantharaman, Hai Lin, Christopher Lynch, Paliath Narendran, and Michaël Rusinowitch. Unification modulo homomorphic encryption. J. Autom. Reason., 48(2):135-158, 2012. URL: https://doi.org/10.1007/s10817-010-9205-y.
  5. Siva Anantharaman, Paliath Narendran, and Michaël Rusinowitch. Intruders with caps. In Franz Baader, editor, Term Rewriting and Applications, 18th International Conference, RTA 2007, Paris, France, June 26-28, 2007, Proceedings, volume 4533 of Lecture Notes in Computer Science, pages 20-35. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73449-9_4.
  6. Franz Baader and Tobias Nipkow. Term rewriting and all that. Cambridge University Press, New York, NY, USA, 1998. Google Scholar
  7. Franz Baader and Wayne Snyder. Unification theory. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes), pages 445-532. Elsevier and MIT Press, 2001. URL: https://doi.org/10.1016/B978-044450813-3/50010-2.
  8. Mathieu Baudet, Véronique Cortier, and Stéphanie Delaune. YAPA: A generic tool for computing intruder knowledge. ACM Trans. Comput. Log., 14(1):4:1-4:32, 2013. URL: https://doi.org/10.1145/2422085.2422089.
  9. Johannes Borgström. Static equivalence is harder than knowledge. Electronic Notes in Theoretical Computer Science, 154(3):45-57, 2005. URL: https://doi.org/10.1016/j.entcs.2006.05.006.
  10. Carter Bunch, Saraid Dwyer Satterfield, Serdar Erbatur, Andrew M. Marshall, and Christophe Ringeissen. Knowledge problems in protocol analysis: Extending the notion of subterm convergent. CoRR, abs/2401.17226, 2024. URL: https://doi.org/10.48550/arXiv.2401.17226.
  11. Rohit Chadha, Vincent Cheval, Stefan Ciobaca, and Steve Kremer. Automated verification of equivalence properties of cryptographic protocols. ACM Trans. Comput. Log., 17(4):23, 2016. URL: https://doi.org/10.1145/2926715.
  12. Stefan Ciobaca, Stéphanie Delaune, and Steve Kremer. Computing knowledge in security protocols under convergent equational theories. J. Autom. Reason., 48(2):219-262, 2012. URL: https://doi.org/10.1007/s10817-010-9197-7.
  13. Katriel Cohn-Gordon, Cas Cremers, Luke Garratt, Jon Millican, and Kevin Milner. On ends-to-ends encryption: Asynchronous group messaging with strong security guarantees. In David Lie, Mohammad Mannan, Michael Backes, and XiaoFeng Wang, editors, Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, October 15-19, 2018, pages 1802-1819. ACM, 2018. URL: https://doi.org/10.1145/3243734.3243747.
  14. Jannik Dreier, Charles Duménil, Steve Kremer, and Ralf Sasse. Beyond subterm-convergent equational theories in automated verification of stateful protocols. In Matteo Maffei and Mark Ryan, editors, Principles of Security and Trust - 6th International Conference, POST 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10204 of Lecture Notes in Computer Science, pages 117-140, Berlin, Heidelberg, 2017. Springer. URL: https://doi.org/10.1007/978-3-662-54455-6_6.
  15. Serdar Erbatur, Andrew M. Marshall, Paliath Narendran, and Christophe Ringeissen. Deciding knowledge problems modulo classes of permutative theories. In Juliana Bowles and Harald Søndergaard, editors, Logic-Based Program Synthesis and Transformation - 34th International Symposium, LOPSTR 2024, Milan, Italy, September 9-10, 2024, Proceedings, volume 14919 of Lecture Notes in Computer Science, pages 47-63. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-71294-4_3.
  16. Serdar Erbatur, Andrew M. Marshall, and Christophe Ringeissen. Notions of knowledge in combinations of theories sharing constructors. In Leonardo de Moura, editor, Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, volume 10395 of Lecture Notes in Computer Science, pages 60-76. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63046-5_5.
  17. Serdar Erbatur, Andrew M. Marshall, and Christophe Ringeissen. Computing knowledge in equational extensions of subterm convergent theories. Math. Struct. Comput. Sci., 30(6):683-709, 2020. URL: https://doi.org/10.1017/S0960129520000031.
  18. Serdar Erbatur, Andrew M. Marshall, and Christophe Ringeissen. Non-disjoint combined unification and closure by equational paramodulation. In Boris Konev and Giles Reger, editors, Frontiers of Combining Systems - 13th International Symposium, FroCoS 2021, Birmingham, UK, September 8-10, 2021, Proceedings, volume 12941 of Lecture Notes in Computer Science, pages 25-42. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-86205-3_2.
  19. Kimberly A. Gero. Deciding Static Inclusion for Delta-strong and Omega Delta-strong Intruder Theories: Applications to Cryptographic Protocol Analysis. PhD thesis, University at Albany-SUNY, 2015. Google Scholar
  20. Christopher Lynch and Barbara Morawska. Basic syntactic mutation. In Andrei Voronkov, editor, Automated Deduction - CADE-18, 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings, volume 2392 of Lecture Notes in Computer Science, pages 471-485. Springer, 2002. URL: https://doi.org/10.1007/3-540-45620-1_37.
  21. Paliath Narendran and Friedrich Otto. Single versus simultaneous equational unification and equational unification for variable-permuting theories. J. Autom. Reason., 19(1):87-115, 1997. URL: https://doi.org/10.1023/A:1005764526878.
  22. Paliath Narendran, Frank Pfenning, and Richard Statman. On the unification problem for cartesian closed categories. J. Symb. Log., 62(2):636-647, 1997. URL: https://doi.org/10.2307/2275552.
  23. Ky Nguyen. Formal verification of a messaging protocol. Internship report, 2019. Work done under the supervision of Vincent Cheval and Véronique Cortier. Google Scholar
  24. Robert Nieuwenhuis. Decidability and complexity analysis by basic paramodulation. Inf. Comput., 147(1):1-21, 1998. URL: https://doi.org/10.1006/inco.1998.2730.
  25. Saraid Dwyer Satterfield, Serdar Erbatur, Andrew M. Marshall, and Christophe Ringeissen. Knowledge problems in security protocols: Going beyond subterm convergent theories. In Marco Gaboardi and Femke van Raamsdonk, editors, 8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023, July 3-6, 2023, Rome, Italy, volume 260 of LIPIcs, pages 30:1-30:19, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2023.30.
  26. Manfred Schmidt-Schauß. Unification in permutative equational theories is undecidable. J. Symb. Comput., 8(4):415-421, 1989. URL: https://doi.org/10.1016/S0747-7171(89)80037-9.
  27. Katherine A. Yelick. Unification in combinations of collapse-free regular theories. J. Symb. Comput., 3(1/2):153-181, 1987. URL: https://doi.org/10.1016/S0747-7171(87)80025-1.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact