{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,28]],"date-time":"2026-07-28T01:30:30Z","timestamp":1785202230618,"version":"3.55.0"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031124402","type":"print"},{"value":"9783031124419","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-12441-9_8","type":"book-chapter","created":{"date-parts":[[2022,7,29]],"date-time":"2022-07-29T10:23:34Z","timestamp":1659090214000},"page":"151-170","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["An Efficient Canonical Narrowing Implementation for\u00a0Protocol Analysis"],"prefix":"10.1007","author":[{"given":"Ra\u00fal","family":"L\u00f3pez-Rueda","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Santiago","family":"Escobar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,7,30]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Aparicio-S\u00e1nchez, D., Escobar, S., Sapi\u00f1a, J.: Variant-based equational unification under constructor symbols. In: Ricca, F., et al. (eds.) Proceedings 36th International Conference on Logic Programming (Technical Communications), ICLP Technical Communications 2020 (Technical Communications) UNICAL, Rende (CS), Italy, 18\u201324th September 2020, EPTCS, vol. 325, pp. 38\u201351 (2020)","DOI":"10.4204\/EPTCS.325.10"},{"issue":"4","key":"8_CR2","doi-asserted-by":"publisher","first-page":"23:1","DOI":"10.1145\/2926715","volume":"17","author":"R Chadha","year":"2016","unstructured":"Chadha, R., Cheval, V., Ciob\u00e2c\u0103, \u015e, Kremer, S.: Automated verification of equivalence properties of cryptographic protocols. ACM Trans. Comput. Log. 17(4), 23:1-23:32 (2016)","journal-title":"ACM Trans. Comput. Log."},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-32033-3_22","volume-title":"Term Rewriting and Applications","author":"H Comon-Lundh","year":"2005","unstructured":"Comon-Lundh, H., Delaune, S.: The finite variant property: how to get rid of some algebraic properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 294\u2013307. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-32033-3_22"},{"key":"8_CR4","doi-asserted-by":"publisher","first-page":"100497","DOI":"10.1016\/j.jlamp.2019.100497","volume":"110","author":"F Dur\u00e1n","year":"2020","unstructured":"Dur\u00e1n, F., et al.: Programming and symbolic computation in Maude. J. Log. Algebraic Methods Program. 110, 100497 (2020)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-642-38574-2_16","volume-title":"Automated Deduction \u2013 CADE-24","author":"S Erbatur","year":"2013","unstructured":"Erbatur, S., et al.: Asymmetric unification: a new unification paradigm for cryptographic protocol analysis. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 231\u2013248. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_16"},{"key":"8_CR6","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/j.ic.2014.07.007","volume":"238","author":"S Escobar","year":"2014","unstructured":"Escobar, S., Meadows, C., Meseguer, J., Santiago, S.: State space reduction in the Maude-NRL protocol analyzer. Inf. Comput. 238, 157\u2013186 (2014)","journal-title":"Inf. Comput."},{"key":"8_CR7","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":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-030-19052-1_4","volume-title":"Foundations of Security, Protocols, and Equational Reasoning","author":"S Escobar","year":"2019","unstructured":"Escobar, S., Meseguer, J.: Canonical narrowing with irreducibility constraints as a symbolic protocol analysis method. In: Guttman, J.D., Landwehr, C.E., Meseguer, J., Pavlovic, D. (eds.) Foundations of Security, Protocols, and Equational Reasoning. LNCS, vol. 11565, pp. 15\u201338. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-19052-1_4"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Escobar, S., Sapi\u00f1a, J.: Most general variant unifiers. In: Bogaerts, B., et al. (eds.) Proceedings 35th International Conference on Logic Programming (Technical Communications), ICLP 2019 Technical Communications, Las Cruces, NM, USA, 20\u201325 September 2019, EPTCS, vol. 306, pp. 154\u2013167 (2019)","DOI":"10.4204\/EPTCS.306.21"},{"issue":"7\u20138","key":"8_CR10","doi-asserted-by":"publisher","first-page":"898","DOI":"10.1016\/j.jlap.2012.01.002","volume":"81","author":"S Escobar","year":"2012","unstructured":"Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Log. Algebr. Program. 81(7\u20138), 898\u2013928 (2012)","journal-title":"J. Log. Algebr. Program."},{"issue":"4","key":"8_CR11","doi-asserted-by":"publisher","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J-P Jouannaud","year":"1986","unstructured":"Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15(4), 1155\u20131194 (1986)","journal-title":"SIAM J. Comput."},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-642-39799-8_48","volume-title":"Computer Aided Verification","author":"S Meier","year":"2013","unstructured":"Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696\u2013701. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_48"},{"issue":"1","key":"8_CR13","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditioned rewriting logic as a united model of concurrency. Theor. Comput. Sci. 96(1), 73\u2013155 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/3-540-64299-4_26","volume-title":"Recent Trends in Algebraic Development Techniques","author":"J Meseguer","year":"1998","unstructured":"Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Presicce, F.P. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18\u201361. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-64299-4_26"},{"key":"8_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2016.12.026","volume":"672","author":"J Meseguer","year":"2017","unstructured":"Meseguer, J.: Strict coherence of conditional rewriting modulo axioms. Theor. Comput. Sci. 672, 1\u201335 (2017)","journal-title":"Theor. Comput. Sci."},{"issue":"1\u20132","key":"8_CR16","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10990-007-9000-6","volume":"20","author":"J Meseguer","year":"2007","unstructured":"Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. High. Order Symb. Comput. 20(1\u20132), 123\u2013160 (2007)","journal-title":"High. Order Symb. Comput."},{"key":"8_CR17","unstructured":"TeReSe (ed.): Term Rewriting Systems. Cambridge University Press, Cambridge (2003)"}],"container-title":["Lecture Notes in Computer Science","Rewriting Logic and Its Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-12441-9_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,29]],"date-time":"2022-07-29T10:24:27Z","timestamp":1659090267000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-12441-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031124402","9783031124419"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-12441-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"30 July 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"WRLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Rewriting Logic and its Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"wrla2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/sv.postech.ac.kr\/wrla2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}