Document Open Access Logo

Knowledge Problems in Security Protocols: Going Beyond Subterm Convergent Theories

Authors Saraid Dwyer Satterfield, Serdar Erbatur , Andrew M. Marshall , Christophe Ringeissen

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2023.30.pdf
  • Filesize: 0.73 MB
  • 19 pages

Document Identifiers

Author Details

Saraid Dwyer Satterfield
  • University of Mary Washington, Fredericksburg, VA, USA
Serdar Erbatur
  • University of Texas at Dallas, TX, USA
Andrew M. Marshall
  • University of Mary Washington, Fredericksburg, VA, USA
Christophe Ringeissen
  • Université de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France

Funding

  • Ringeissen, Christophe: This work has been partly supported by the ANR Research and teaching chair in AI ASAP (ANR-20-CHIA-0024) and the Région Grand Est.

Acknowledgements

We would like to thank Steve Kremer for his comments on the paper as they were very helpful in improving several technical results.

Cite AsGet BibTex

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). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.FSCD.2023.30

Abstract

We introduce a new form of restricted term rewrite system, the graph-embedded term rewrite system. These systems, and thus the name, are inspired by the graph minor relation and are more flexible extensions of the well-known homeomorphic-embedded property of term rewrite systems. As a motivating application area, we consider the symbolic analysis of security protocols, and more precisely the two knowledge problems defined by the deduction problem and the static equivalence problem. In this field restricted term rewrite systems, such as subterm convergent ones, have proven useful since the knowledge problems are decidable for such systems. However, many of the same decision procedures still work for examples of systems which are "beyond subterm convergent". However, the applicability of the corresponding decision procedures to these examples must often be proven on an individual basis. This is due to the problem that they don't fit into an existing syntactic definition for which the procedures are known to work. Here we show that many of these systems belong to a particular subclass of graph-embedded convergent systems, called contracting convergent systems. On the one hand, we show that the knowledge problems are decidable for the subclass of contracting convergent systems. On the other hand, we show that the knowledge problems are undecidable for the class of graph-embedded systems.

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Automated reasoning
Keywords
  • Term rewriting
  • security protocols
  • verification

Metrics

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

References

  1. Martín Abadi and Véronique Cortier. Deciding knowledge in security protocols under equational theories. Theor. Comput. Sci., 367(1-2):2-32, 2006. Google Scholar
  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. Google Scholar
  3. Siva Anantharaman, Hai Lin, Christopher Lynch, Paliath Narendran, and Michaël Rusinowitch. Unification modulo homomorphic encryption. J. Autom. Reason., 48(2):135-158, 2012. Google Scholar
  4. Siva Anantharaman, Paliath Narendran, and Michael Rusinowitch. Intruders with caps. Research report, Laboratoire d'Informatique Fondamentale d'Orléans, 2007. URL: https://hal.science/hal-00144178.
  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. Google Scholar
  6. Mauricio Ayala-Rincón, Maribel Fernández, and Daniele Nantes-Sobrinho. Intruder deduction problem for locally stable theories with normal forms and inverses. Theor. Comput. Sci., 672:64-100, 2017. Google Scholar
  7. Franz Baader and Tobias Nipkow. Term rewriting and all that. Cambridge University Press, 1998. Google Scholar
  8. Franz Baader and Wayne Snyder. Unification theory. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, pages 445-532. Elsevier and MIT Press, 2001. Google Scholar
  9. Mathieu Baudet, Véronique Cortier, and Stéphanie Delaune. YAPA: A generic tool for computing intruder knowledge. ACM Trans. Comput. Log., 14(1):4, 2013. Google Scholar
  10. Bruno Blanchet. Automatic proof of strong secrecy for security protocols. In 2004 IEEE Symposium on Security and Privacy (S&P 2004), 9-12 May 2004, Berkeley, CA, USA, pages 86-100. IEEE Computer Society, 2004. Google Scholar
  11. Christopher Bouchard, Kimberly A. Gero, Christopher Lynch, and Paliath Narendran. On forward closure and the finite variant property. In Pascal Fontaine, Christophe Ringeissen, and Renate A. Schmidt, editors, Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Nancy, France, September 18-20, 2013. Proceedings, volume 8152 of Lecture Notes in Computer Science, pages 327-342. Springer, 2013. Google Scholar
  12. Rohit Chadha, Vincent Cheval, Ştefan Ciobâcă, and Steve Kremer. Automated verification of equivalence properties of cryptographic protocols. ACM Trans. Comput. Log., 17(4):23:1-23:32, 2016. Google Scholar
  13. Hubert Comon-Lundh and Stéphanie Delaune. The finite variant property: How to get rid of some algebraic properties. In Jürgen Giesl, editor, Term Rewriting and Applications, 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings, volume 3467 of Lecture Notes in Computer Science, pages 294-307. Springer, 2005. Google Scholar
  14. Véronique Cortier, Stéphanie Delaune, and Pascal Lafourcade. A survey of algebraic properties used in cryptographic protocols. J. Comput. Secur., 14(1):1-43, 2006. Google Scholar
  15. Ştefan Ciobâcă, Stéphanie Delaune, and Steve Kremer. Computing knowledge in security protocols under convergent equational theories. J. Autom. Reasoning, 48(2):219-262, 2012. Google Scholar
  16. Reinhard Diestel. Graph Theory, volume 173 of Graduate Texts in Mathematics. Springer, third edition, 2006. Google Scholar
  17. 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. Springer, 2017. Google Scholar
  18. Santiago Escobar, Ralf Sasse, and José Meseguer. Folding variant narrowing and optimal variant termination. J. Log. Algebr. Program., 81(7-8):898-928, 2012. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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