Document Open Access Logo

How Term Rewriting Structures Shape the Decidability of Knowledge Problems

Authors Raja O. P. Damanik , Alwen Tiu

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2026.14.pdf
  • Filesize: 0.82 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Automated reasoning
  • Security and privacy → Formal security models
  • Security and privacy → Logic and verification
Keywords
  • Security Protocol
  • Intruder Deduction
  • Static Equivalence
  • Term Rewriting

Metrics

Abstract

Deduction and static equivalence are central knowledge problems in the formal analysis of security protocols and are known to be undecidable for general equational theories. Several decidable classes have been identified through structural restrictions, including subterm convergent theories, shallow permutative theories, contracting theories and some are implemented in tools such as ProVerif and DeepSec. 
We identify two recurring themes: symbol preservation, where symbols are maintained across axioms, and symbol contraction, where symbols decrease in depth or number from left to right. 
For symbol-preserving systems, we introduce measure-invariant (MI) and separate measure-invariant (SMI) theories, generalizing permutative classes and providing new decidable fragments for deduction and static equivalence. Depth-sensitive refinements, including depth-preserving permutative (DPP) and depth-preserving variable-permuting (DPVP) theories, are case studies to understand whether the depth of occurrences of symbols matter. For symbol-contraction systems, we define depth-decreasing (DD) and variable-preserving function-decreasing (VBFD) theories, capturing some simple relaxations of term contraction; while deduction is undecidable in general, these restrictions highlight potential decidable fragments. 
Overall, our results show that controlling symbol dynamics in rewrite rules provides a unifying perspective on the decidability of knowledge problems, offering conceptual clarity on what makes these problems hard for different equational theories.

Cite As Get BibTex

Raja O. P. Damanik and Alwen Tiu. How Term Rewriting Structures Shape the Decidability of Knowledge Problems. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.FSCD.2026.14

Author Details

Raja O. P. Damanik
  • School of Computing, Australian National University, ACT, Australia
Alwen Tiu
  • School of Computing, Australian National University, ACT, Australia

Acknowledgements

We are grateful to the anonymous reviewers for their careful reading and insightful suggestions, which greatly helped improve this work.

References

  1. Martín Abadi and Véronique Cortier. Deciding knowledge in security protocols under equational theories. Theoretical Computer Science, 367(1-2):2-32, 2006. URL: https://doi.org/10.1016/J.TCS.2006.08.032.
  2. 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.
  3. Zümrüt Akçam, Kimberly A Cornell, Daniel S Hono II, Paliath Narendran, and Andrew Pulver. On problems dual to unification: The string-rewriting case. arXiv preprint, 2021. URL: https://arxiv.org/abs/2103.00386.
  4. Siva Anantharaman, Hai Lin, Christopher Lynch, Paliath Narendran, and Michaël Rusinowitch. Unification modulo homomorphic encryption. Journal of automated reasoning, 48(2):135-158, 2012. URL: https://doi.org/10.1007/S10817-010-9205-Y.
  5. Franz Baader and Tobias Nipkow. Term rewriting and all that. Cambridge university press, 1998. Google Scholar
  6. Mouhebeddine Berrima, Narjes Ben Rajeb, and Véronique Cortier. Deciding knowledge in security protocols under some e-voting theories. RAIRO-Theoretical Informatics and Applications, 45(3):269-299, 2011. URL: https://doi.org/10.1051/ITA/2011119.
  7. Bruno Blanchet, Martín Abadi, and Cédric Fournet. Automated verification of selected equivalences for security protocols. The Journal of Logic and Algebraic Programming, 75(1):3-51, 2008. URL: https://doi.org/10.1016/J.JLAP.2007.06.002.
  8. Johannes Borgström. Static equivalence is harder than knowledge. Electronic Notes in Theoretical Computer Science, 154(3):45-57, 2006. URL: https://doi.org/10.1016/J.ENTCS.2006.05.006.
  9. Carter Bunch, Saraid Dwyer Satterfield, Serdar Erbatur, Andrew M Marshall, and Christophe Ringeissen. Knowledge problems in protocol analysis: Extending the notion of subterm convergent. arXiv preprint arXiv:2401.17226, 2024. URL: https://doi.org/10.48550/arXiv.2401.17226.
  10. Rohit Chadha, Vincent Cheval, Ştefan Ciobâcă, and Steve Kremer. Automated verification of equivalence properties of cryptographic protocols. ACM Transactions on Computational Logic (TOCL), 17(4):1-32, 2016. Google Scholar
  11. Vincent Cheval. APTE: an algorithm for proving trace equivalence. In Erika Ábrahám and Klaus Havelund, editors, Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014. Proceedings, volume 8413 of Lecture Notes in Computer Science, pages 587-592. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54862-8_50.
  12. Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina. Deepsec: deciding equivalence properties in security protocols theory and practice. In 2018 IEEE symposium on security and privacy (SP), pages 529-546. IEEE, 2018. URL: https://doi.org/10.1109/SP.2018.00033.
  13. Ştefan Ciobâcă, Stéphanie Delaune, and Steve Kremer. Computing knowledge in security protocols under convergent equational theories. Journal of Automated Reasoning, 48(2):219-262, 2012. URL: https://doi.org/10.1007/S10817-010-9197-7.
  14. 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 Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, pages 1802-1819, 2018. URL: https://doi.org/10.1145/3243734.3243747.
  15. Véronique Cortier, Antoine Dallon, and Stéphanie Delaune. Sat-equiv: An efficient tool for equivalence properties. In 30th IEEE Computer Security Foundations Symposium, CSF 2017, pages 481-494. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/CSF.2017.15.
  16. Véronique Cortier, Stéphanie Delaune, and Pascal Lafourcade. A survey of algebraic properties used in cryptographic protocols. Journal of Computer Security, 14(1):1-43, 2006. URL: https://doi.org/10.3233/JCS-2006-14101.
  17. Danny Dolev and Andrew Yao. On the security of public key protocols. IEEE Transactions on information theory, 29(2):198-208, 1983. URL: https://doi.org/10.1109/TIT.1983.1056650.
  18. Serdar Erbatur, Andrew M Marshall, Paliath Narendran, and Christophe Ringeissen. Deciding knowledge problems modulo classes of permutative theories. In International Symposium on Logic-Based Program Synthesis and Transformation, pages 47-63. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-71294-4_3.
  19. 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), volume 337 of Leibniz International Proceedings in Informatics (LIPIcs), pages 18:1-18:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.FSCD.2025.18.
  20. Serdar Erbatur, Andrew M Marshall, and Christophe Ringeissen. Notions of knowledge in combinations of theories sharing constructors. In International Conference on Automated Deduction, pages 60-76. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63046-5_5.
  21. Serdar Erbatur, Andrew M Marshall, and Christophe Ringeissen. Computing knowledge in equational extensions of subterm convergent theories. Mathematical Structures in Computer Science, 30(6):683-709, 2020. URL: https://doi.org/10.1017/S0960129520000031.
  22. Paliath Narendran and Friedrich Otto. Single versus simultaneous equational unification and equational unification for variable-permuting theories. Journal of Automated Reasoning, 19(1):87-115, 1997. URL: https://doi.org/10.1023/A:1005764526878.
  23. Ky Nguyen. Formal verification of a messaging protocol. Work done under the supervision of Vincent Cheval and Véronique Cortier, 2019. Google Scholar
  24. Saraid Dwyer Satterfield, Serdar Erbatur, Andrew M Marshall, and Christophe Ringeissen. Knowledge problems in security protocols: going beyond subterm convergent theories. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), volume 260, pages 30-1, 2023. Google Scholar
  25. Manfred Schmidt-Schauß. Unification in permutative equational theories is undecidable. Journal of symbolic computation, 8(4):415-421, 1989. URL: https://doi.org/10.1016/S0747-7171(89)80037-9.
  26. Alwen Tiu, Nam Nguyen, and Ross Horne. SPEC: an equivalence checker for security protocols. In Atsushi Igarashi, editor, Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings, volume 10017 of Lecture Notes in Computer Science, pages 87-95, 2016. URL: https://doi.org/10.1007/978-3-319-47958-3_5.
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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact