{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,28]],"date-time":"2026-07-28T07:25:31Z","timestamp":1785223531013,"version":"3.55.0"},"reference-count":46,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2020,3,2]],"date-time":"2020-03-02T00:00:00Z","timestamp":1583107200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2020,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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.<\/jats:p>","DOI":"10.1017\/s0960129520000031","type":"journal-article","created":{"date-parts":[[2020,3,2]],"date-time":"2020-03-02T08:19:02Z","timestamp":1583137142000},"page":"683-709","source":"Crossref","is-referenced-by-count":3,"title":["Computing knowledge in equational extensions of subterm convergent theories"],"prefix":"10.1017","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7574-195X","authenticated-orcid":false,"given":"Serdar","family":"Erbatur","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0522-8384","authenticated-orcid":false,"given":"Andrew M.","family":"Marshall","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5937-6059","authenticated-orcid":false,"given":"Christophe","family":"Ringeissen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2020,3,2]]},"reference":[{"key":"S0960129520000031_ref28","volume-title":"32nd International Workshop on Unification (UNIF-2018)","author":"Erbatur","year":"2018"},{"key":"S0960129520000031_ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03829-7_6"},{"key":"S0960129520000031_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/2926715"},{"key":"S0960129520000031_ref25","first-page":"350","volume-title":"22nd Annual Symposium on Foundations of Computer Science","author":"Dolev","year":"1981"},{"key":"S0960129520000031_ref7","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752"},{"key":"S0960129520000031_ref46","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1145\/2643135.2643154","volume-title":"Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming","author":"Yang","year":"2014"},{"key":"S0960129520000031_ref42","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22444-7_11"},{"key":"S0960129520000031_ref45","first-page":"277","volume-title":"Term Rewriting and Applications, 17th International Conference, RTA 2006","volume":"4098","author":"Turuani","year":"2006"},{"key":"S0960129520000031_ref38","unstructured":"Nguyen, K. (2019). Formal verification of a messaging protocol. Work done under the supervision of Vincent Cheval and V\u00e9ronique Cortier."},{"key":"S0960129520000031_ref19","first-page":"294","volume-title":"Rewriting Techniques and Applications","volume":"3467","author":"Comon-Lundh","year":"2005"},{"key":"S0960129520000031_ref34","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45620-1_37"},{"key":"S0960129520000031_ref13","first-page":"28","volume-title":"Computer Aided Verification \u2013 30th International Conference, CAV 2018","volume":"10982","author":"Cheval","year":"2018"},{"key":"S0960129520000031_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/2422085.2422089"},{"key":"S0960129520000031_ref10","first-page":"82","volume-title":"14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), 11\u201313 June 2001, Cape Breton, Nova Scotia","author":"Blanchet","year":"2001"},{"key":"S0960129520000031_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9208-8"},{"key":"S0960129520000031_ref15","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.01.015"},{"key":"S0960129520000031_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24597-1_11"},{"key":"S0960129520000031_ref29","first-page":"1","volume-title":"Foundations of Security Analysis and Design V, FOSAD 2007\/2008\/2009 Tutorial Lectures","volume":"5705","author":"Escobar","year":"2007"},{"key":"S0960129520000031_ref26","first-page":"359","volume-title":"31st IEEE Computer Security Foundations Symposium","author":"Dreier","year":"2018"},{"key":"S0960129520000031_ref6","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2017.01.027"},{"key":"S0960129520000031_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.08.032"},{"key":"S0960129520000031_ref35","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.09.001"},{"key":"S0960129520000031_ref3","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360213"},{"key":"S0960129520000031_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.07.004"},{"key":"S0960129520000031_ref4","first-page":"281","volume-title":"17th International Conference on Computer Aided Verification, CAV 2005","volume":"3576","author":"Armando","year":"2005"},{"key":"S0960129520000031_ref20","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1043"},{"key":"S0960129520000031_ref33","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1990.113753"},{"key":"S0960129520000031_ref41","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-22102-7_24"},{"key":"S0960129520000031_ref32","doi-asserted-by":"publisher","DOI":"10.1137\/0215084"},{"key":"S0960129520000031_ref40","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1998-61-205"},{"key":"S0960129520000031_ref12","first-page":"344","volume-title":"31st IEEE Computer Security Foundations Symposium","author":"Cheval","year":"2018"},{"key":"S0960129520000031_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27836-8_7"},{"key":"S0960129520000031_ref44","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80037-9"},{"key":"S0960129520000031_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9197-7"},{"key":"S0960129520000031_ref21","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2003.1210067"},{"key":"S0960129520000031_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_38"},{"key":"S0960129520000031_ref18","unstructured":"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\u20131819."},{"key":"S0960129520000031_ref9","doi-asserted-by":"publisher","DOI":"10.1561\/3300000004"},{"key":"S0960129520000031_ref31","first-page":"318","volume-title":"5th Conference on Automated Deduction","volume":"87","author":"Hullot","year":"1980"},{"key":"S0960129520000031_ref39","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1990.113754"},{"key":"S0960129520000031_ref43","first-page":"78","volume-title":"25th IEEE Computer Security Foundations Symposium","author":"Schmidt","year":"2012"},{"key":"S0960129520000031_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44618-4_28"},{"key":"S0960129520000031_ref22","first-page":"11","volume-title":"Proceedings of RTA 2011, Novi Sad, Serbia","volume":"10","author":"Conchinha","year":"2011"},{"key":"S0960129520000031_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63046-5_5"},{"key":"S0960129520000031_ref30","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.01.002"},{"key":"S0960129520000031_ref36","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1145\/501983.502007","volume-title":"Proceedings of the 8th ACM Conference on Computer and Communications Security","author":"Millen","year":"2001"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129520000031","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,1]],"date-time":"2021-03-01T22:53:31Z","timestamp":1614639211000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129520000031\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,3,2]]},"references-count":46,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2020,6]]}},"alternative-id":["S0960129520000031"],"URL":"https:\/\/doi.org\/10.1017\/s0960129520000031","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,3,2]]}}}