{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,16]],"date-time":"2025-09-16T20:13:49Z","timestamp":1758053629617,"version":"3.44.0"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032041661","type":"print"},{"value":"9783032041678","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T00:00:00Z","timestamp":1757894400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T00:00:00Z","timestamp":1757894400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>In this paper, we consider the knowledge problems of <jats:italic>deduction<\/jats:italic> and <jats:italic>static equivalence<\/jats:italic> in the formal analysis of security protocols. We extend a recent result that developed a decision procedure for these problems in the non-disjoint combination <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$R \\cup E$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>R<\/mml:mi>\n                    <mml:mo>\u222a<\/mml:mo>\n                    <mml:mi>E<\/mml:mi>\n                  <\/mml:mrow>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>, where <jats:italic>R<\/jats:italic> is a subterm <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$E$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>E<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>-convergent term rewrite system (TRS) and <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$E$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>E<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> is a restricted form of permutative theory. Here, we consider the same combination problem but replace the subterm <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$E$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>E<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>-convergent TRS with a superclass of subterm <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$E$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>E<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>-convergent, called <jats:italic>contracting<\/jats:italic>\n            <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$E$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>E<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>-convergent. We show that the previous decision procedure can be extended to obtain a new algorithm for this larger class of combined theories.<\/jats:p>\n          <jats:p>We also explore the gap between the contracting TRSs, for which deduction and static-equivalence are decidable, and a larger superclass called <jats:italic>graph-embedded<\/jats:italic> for which these problems are undecidable. This gap is of interest since one would like to get closer to graph-embedded and still maintain decidability of the above \u201cknowledge problems.\u201d We show that at least one way of weakening the restrictions of the contracting definition will not work, as it leads to undecidability results for deduction and static equivalence. We also show that a subset of the graph-embedded rules is still sufficient to obtain undecidability.<\/jats:p>","DOI":"10.1007\/978-3-032-04167-8_12","type":"book-chapter","created":{"date-parts":[[2025,9,14]],"date-time":"2025-09-14T22:04:08Z","timestamp":1757887448000},"page":"209-227","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Graph-Embedded Rewrite Systems: Combination and\u00a0Undecidability Results"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7574-195X","authenticated-orcid":false,"given":"Serdar","family":"Erbatur","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0522-8384","authenticated-orcid":false,"given":"Andrew M.","family":"Marshall","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4521-5892","authenticated-orcid":false,"given":"Paliath","family":"Narendran","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5937-6059","authenticated-orcid":false,"given":"Christophe","family":"Ringeissen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,9,15]]},"reference":[{"issue":"1\u20132","key":"12_CR1","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2006.08.032","volume":"367","author":"M Abadi","year":"2006","unstructured":"Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theor. Comput. Sci. 367(1\u20132), 2\u201332 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Hankin, C., Schmidt, D. (eds.) Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, UK, 17\u201319 January 2001, pp. 104\u2013115. ACM (2001)","DOI":"10.1145\/360204.360213"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11513988_27","volume-title":"Computer Aided Verification","author":"A Armando","year":"2005","unstructured":"Armando, A., et al.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281\u2013285. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_27"},{"key":"12_CR4","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1016\/j.tcs.2017.01.027","volume":"672","author":"M Ayala-Rinc\u00f3n","year":"2017","unstructured":"Ayala-Rinc\u00f3n, M., Fern\u00e1ndez, M., Nantes-Sobrinho, D.: Intruder deduction problem for locally stable theories with normal forms and inverses. Theor. Comput. Sci. 672, 64\u2013100 (2017)","journal-title":"Theor. Comput. Sci."},{"key":"12_CR5","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, New York (1998)"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Baader, F., Snyder, W.: Unification theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 445\u2013532. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"issue":"1","key":"12_CR7","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1145\/2422085.2422089","volume":"14","author":"M Baudet","year":"2013","unstructured":"Baudet, M., Cortier, V., Delaune, S.: YAPA: a generic tool for computing intruder knowledge. ACM Trans. Comput. Log. 14(1), 4 (2013)","journal-title":"ACM Trans. Comput. Log."},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), Cape Breton, Nova Scotia, Canada, 11\u201313 June 2001, pp. 82\u201396. IEEE Computer Society (2001)","DOI":"10.1109\/CSFW.2001.930138"},{"key":"12_CR9","unstructured":"Bunch, C., Satterfield, S.D., Erbatur, S., Marshall, A.M., Ringeissen, C.: Knowledge problems in protocol analysis: extending the notion of subterm convergent (2025). https:\/\/arxiv.org\/abs\/2401.17226"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Chadha, R., Cheval, V., Ciob\u00e2c\u0103, S., Kremer, S.: Automated verification of equivalence properties of cryptographic protocols. ACM Trans. Comput. Log. 17(4), 23:1\u201323:32 (2016)","DOI":"10.1145\/2926715"},{"issue":"2","key":"12_CR11","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10817-010-9197-7","volume":"48","author":"S Ciob\u00e2c\u0103","year":"2012","unstructured":"Ciob\u00e2c\u0103, S., Delaune, S., Kremer, S.: Computing knowledge in security protocols under convergent equational theories. J. Autom. Reasoning 48(2), 219\u2013262 (2012)","journal-title":"J. Autom. Reasoning"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Cohn-Gordon, K., Cremers, C., Garratt, L., Millican, J., Milner, K.: On ends-to-ends encryption: asynchronous group messaging with strong security guarantees. In: Lie, D., Mannan, M., Backes, M., Wang, X. (eds.) Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, 15\u201319 October 2018, pp. 1802\u20131819. ACM (2018)","DOI":"10.1145\/3243734.3243747"},{"key":"12_CR13","unstructured":"Conchinha, B., Basin, D.A., Caleiro, C.: FAST: an efficient decision procedure for deduction and static equivalence. In: Schmidt-Schau\u00df, M. (ed.) Proceedings of RTA 2011, Novi Sad, Serbia. LIPIcs, vol.\u00a010, pp. 11\u201320. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2011)"},{"key":"12_CR14","doi-asserted-by":"publisher","unstructured":"Cortier, V., Delaune, S.: Decidability and combination results for two notions of knowledge in security protocols. J. Autom. Reasoning 48(4), 441\u2013487 (2010). https:\/\/doi.org\/10.1007\/s10817-010-9208-8","DOI":"10.1007\/s10817-010-9208-8"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1007\/978-3-540-70545-1_38","volume-title":"Computer Aided Verification","author":"CJF Cremers","year":"2008","unstructured":"Cremers, C.J.F.: The scyther tool: verification, falsification, and analysis of security protocols. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 414\u2013418. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_38"},{"key":"12_CR16","doi-asserted-by":"publisher","unstructured":"Dwyer\u00a0Satterfield, S., Erbatur, S., Marshall, A.M., Ringeissen, C.: Knowledge problems in security protocols: going beyond subterm convergent theories. In: Gaboardi, M., van Raamsdonk, F. (eds.) 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0260, pp. 30:1\u201330:19. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2023). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2023.30. https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.FSCD.2023.30","DOI":"10.4230\/LIPIcs.FSCD.2023.30"},{"key":"12_CR17","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-031-71294-4_3","volume-title":"LOPSTR 2024","author":"S Erbatur","year":"2024","unstructured":"Erbatur, S., Marshall, A.M., Narendran, P., Ringeissen, C.: Deciding knowledge problems modulo classes of permutative theories. In: Bowles, J., S\u00f8ndergaard, H. (eds.) LOPSTR 2024. LNCS, vol. 14919, pp. 47\u201363. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-71294-4_3"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-319-63046-5_5","volume-title":"Automated Deduction \u2013 CADE 26","author":"S Erbatur","year":"2017","unstructured":"Erbatur, S., Marshall, A.M., Ringeissen, C.: Notions of knowledge in combinations of theories sharing constructors. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 60\u201376. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_5"},{"issue":"6","key":"12_CR19","doi-asserted-by":"publisher","first-page":"683","DOI":"10.1017\/S0960129520000031","volume":"30","author":"S Erbatur","year":"2020","unstructured":"Erbatur, S., Marshall, A.M., Ringeissen, C.: Computing knowledge in equational extensions of subterm convergent theories. Math. Struct. Comput. Sci. 30(6), 683\u2013709 (2020)","journal-title":"Math. Struct. Comput. Sci."},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-03829-7_1","volume-title":"Foundations of Security Analysis and Design V","author":"S Escobar","year":"2009","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cryptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007-2009. LNCS, vol. 5705, pp. 1\u201350. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03829-7_1"},{"key":"12_CR21","doi-asserted-by":"publisher","unstructured":"Jouannaud, J., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15(4), 1155\u20131194 (1986). https:\/\/doi.org\/10.1137\/0215084","DOI":"10.1137\/0215084"},{"key":"12_CR22","doi-asserted-by":"publisher","unstructured":"Kirchner, C., Klay, F.: Syntactic theories and unification. In: Logic in Computer Science, LICS 1990, Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pp. 270\u2013277 (1990). https:\/\/doi.org\/10.1109\/LICS.1990.113753","DOI":"10.1109\/LICS.1990.113753"},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1007\/3-540-45620-1_37","volume-title":"Automated Deduction\u2014CADE-18","author":"C Lynch","year":"2002","unstructured":"Lynch, C., Morawska, B.: Basic syntactic mutation. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 471\u2013485. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45620-1_37"},{"key":"12_CR24","doi-asserted-by":"publisher","unstructured":"Millen, J., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: Proceedings of the 8th ACM Conference on Computer and Communications Security, CCS 2001, pp. 166\u2013175. ACM, New York (2001). https:\/\/doi.org\/10.1145\/501983.502007","DOI":"10.1145\/501983.502007"},{"key":"12_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-642-03829-7_6","volume-title":"Foundations of Security Analysis and Design V","author":"S M\u00f6dersheim","year":"2009","unstructured":"M\u00f6dersheim, S., Vigan\u00f2, L.: The open-source fixed-point model checker for symbolic analysis of security protocols. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007-2009. LNCS, vol. 5705, pp. 166\u2013194. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03829-7_6"},{"issue":"1","key":"12_CR26","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1023\/A:1005764526878","volume":"19","author":"P Narendran","year":"1997","unstructured":"Narendran, P., Otto, F.: Single versus simultaneous equational unification and equational unification for variable-permuting theories. J. Autom. Reason. 19(1), 87\u2013115 (1997)","journal-title":"J. Autom. Reason."},{"key":"12_CR27","unstructured":"Nguyen, K.: Formal verification of a messaging protocol. Internship report (2019). Work done under the supervision of Vincent Cheval and V\u00e9ronique Cortier"},{"key":"12_CR28","doi-asserted-by":"publisher","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"LC Paulson","year":"1998","unstructured":"Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Comput. Secur. 6, 85\u2013128 (1998)","journal-title":"Comput. Secur."},{"key":"12_CR29","doi-asserted-by":"crossref","unstructured":"Schmidt, B., Meier, S., Cremers, C.J.F., Basin, D.A.: 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, 25\u201327 June 2012, pp. 78\u201394. IEEE Computer Society (2012)","DOI":"10.1109\/CSF.2012.25"},{"key":"12_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/11805618_21","volume-title":"Term Rewriting and Applications","author":"M Turuani","year":"2006","unstructured":"Turuani, M.: The CL-Atse protocol analyser. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 277\u2013286. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11805618_21"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-04167-8_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,14]],"date-time":"2025-09-14T22:04:10Z","timestamp":1757887450000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-04167-8_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,15]]},"ISBN":["9783032041661","9783032041678"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-04167-8_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,15]]},"assertion":[{"value":"15 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FroCoS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Frontiers of Combining Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Reykjavik","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Iceland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"frocos2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icetcs.github.io\/frocos-itp-tableaux25\/frocos\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}