{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,13]],"date-time":"2025-11-13T07:22:31Z","timestamp":1763018551149,"version":"3.40.3"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031124402"},{"type":"electronic","value":"9783031124419"}],"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_13","type":"book-chapter","created":{"date-parts":[[2022,7,29]],"date-time":"2022-07-29T10:23:34Z","timestamp":1659090214000},"page":"253-273","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Parallel Maude-NPA for\u00a0Cryptographic Protocol Analysis"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1601-4584","authenticated-orcid":false,"given":"Canh","family":"Minh Do","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9716-4612","authenticated-orcid":false,"given":"Adri\u00e1n","family":"Riesco","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3550-4781","authenticated-orcid":false,"given":"Santiago","family":"Escobar","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4441-3259","authenticated-orcid":false,"given":"Kazuhiro","family":"Ogata","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,7,30]]},"reference":[{"key":"13_CR1","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":"13_CR2","doi-asserted-by":"publisher","unstructured":"Barnat, J., Brim, L., Chaloupka, J.: Parallel breadth-first search LTL model-checking. In: Proceedings of the 18th IEEE International Conference on Automated Software Engineering, pp. 106\u2013115 (2003). https:\/\/doi.org\/10.1109\/ASE.2003.1240299","DOI":"10.1109\/ASE.2003.1240299"},{"key":"13_CR3","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/978-3-319-63516-3_12","volume-title":"Handbook of Parallel Constraint Reasoning","author":"J Barnat","year":"2018","unstructured":"Barnat, J., et al.: Parallel model checking algorithms for linear-time temporal logic. In: Handbook of Parallel Constraint Reasoning, pp. 457\u2013507. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-63516-3_12"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"863","DOI":"10.1007\/978-3-642-39799-8_60","volume-title":"Computer Aided Verification","author":"J Barnat","year":"2013","unstructured":"Barnat, J., et al.: DiVinE 3.0 \u2013 an explicit-state model checker for multithreaded C & C++ programs. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 863\u2013868. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_60"},{"issue":"3","key":"13_CR5","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/s10207-004-0055-7","volume":"4","author":"D Basin","year":"2004","unstructured":"Basin, D., M\u00f6dersheim, S., Vigan\u00f2, L.: OFMC: a symbolic model checker for security protocols. Int. J. Inf. Secur. 4(3), 181\u2013208 (2004). https:\/\/doi.org\/10.1007\/s10207-004-0055-7","journal-title":"Int. J. Inf. Secur."},{"key":"13_CR6","doi-asserted-by":"publisher","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: Proceedings of the 14th IEEE Computer Security Foundations Workshop, pp. 82\u201396 (2001). https:\/\/doi.org\/10.1109\/CSFW.2001.930138","DOI":"10.1109\/CSFW.2001.930138"},{"key":"13_CR7","doi-asserted-by":"publisher","unstructured":"Bulu\u00e7, A., Madduri, K.: Parallel breadth-first search on distributed memory systems. In: Proceedings of 2011 International Conference for High Performance Computing, Networking, Storage and Analysis, SC 2011, New York, NY, USA. Association for Computing Machinery (2011). https:\/\/doi.org\/10.1145\/2063384.2063471","DOI":"10.1145\/2063384.2063471"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71999-1","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M Clavel","year":"2007","unstructured":"Clavel, M., et al.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1"},{"key":"13_CR9","volume-title":"Introduction to Algorithms","author":"TH Cormen","year":"2009","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. The MIT Press, Cambridge (2009)","edition":"3"},{"key":"13_CR10","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":"13_CR11","doi-asserted-by":"publisher","unstructured":"Do, C.M., Phyo, Y., Riesco, A., Ogata, K.: A parallel stratified model checking technique\/tool for leads-to properties. In: 2021 7th International Symposium on System and Software Reliability (ISSSR), pp. 155\u2013166 (2021). https:\/\/doi.org\/10.1109\/ISSSR53171.2021.00011","DOI":"10.1109\/ISSSR53171.2021.00011"},{"issue":"2","key":"13_CR12","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198\u2013208 (1983). https:\/\/doi.org\/10.1109\/TIT.1983.1056650","journal-title":"IEEE Trans. Inf. Theory"},{"key":"13_CR13","doi-asserted-by":"publisher","unstructured":"Dong, L., Chen, K.: Introduction of cryptographic protocols. In: Cryptographic Protocol, pp. 1\u201312. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-24073-7_1","DOI":"10.1007\/978-3-642-24073-7_1"},{"issue":"1","key":"13_CR14","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/j.tcs.2006.08.035","volume":"367","author":"S Escobar","year":"2006","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties. Theor. Comput. Sci. 367(1), 162\u2013202 (2006). https:\/\/doi.org\/10.1016\/j.tcs.2006.08.035","journal-title":"Theor. Comput. Sci."},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"548","DOI":"10.1007\/978-3-540-88313-5_35","volume-title":"Computer Security - ESORICS 2008","author":"S Escobar","year":"2008","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: State space reduction in the Maude-NRL protocol analyzer. In: Jajodia, S., Lopez, J. (eds.) ESORICS 2008. LNCS, vol. 5283, pp. 548\u2013562. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-88313-5_35"},{"key":"13_CR16","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":"13_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-540-73449-9_13","volume-title":"Term Rewriting and Applications","author":"S Escobar","year":"2007","unstructured":"Escobar, S., Meseguer, J.: Symbolic model checking of infinite-state systems using narrowing. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 153\u2013168. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73449-9_13"},{"key":"13_CR18","doi-asserted-by":"publisher","unstructured":"Fabrega, F., Herzog, J., Guttman, J.: Strand spaces: why is a security protocol correct? In: Proceedings of the 1998 IEEE Symposium on Security and Privacy, pp. 160\u2013171 (1998). https:\/\/doi.org\/10.1109\/SECPRI.1998.674832","DOI":"10.1109\/SECPRI.1998.674832"},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/3-540-19242-5_22","volume-title":"Conditional Term Rewriting Systems","author":"J Goguen","year":"1988","unstructured":"Goguen, J., Kirchner, C., Kirchner, H., M\u00e9grelis, A., Meseguer, J., Winkler, T.: An introduction to OBJ 3. In: Kaplan, S., Jouannaud, J.-P. (eds.) CTRS 1987. LNCS, vol. 308, pp. 258\u2013263. Springer, Heidelberg (1988). https:\/\/doi.org\/10.1007\/3-540-19242-5_22"},{"issue":"10","key":"13_CR20","doi-asserted-by":"publisher","first-page":"659","DOI":"10.1109\/TSE.2007.70724","volume":"33","author":"GJ Holzmann","year":"2007","unstructured":"Holzmann, G.J., Bosnacki, D.: The design of a multicore extension of the SPIN model checker. IEEE Trans. Software Eng. 33(10), 659\u2013674 (2007). https:\/\/doi.org\/10.1109\/TSE.2007.70724","journal-title":"IEEE Trans. Software Eng."},{"key":"13_CR21","volume-title":"Term Rewriting Systems","author":"JW Klop","year":"2001","unstructured":"Klop, J.W., Bezem, M., Vrijer, R.C.D.: Term Rewriting Systems. Cambridge University Press, Cambridge (2001)"},{"key":"13_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-030-65277-7_8","volume-title":"Progress in Cryptology \u2013 INDOCRYPT 2020","author":"N Kobeissi","year":"2020","unstructured":"Kobeissi, N., Nicolas, G., Tiwari, M.: Verifpal: cryptographic protocol analysis for the real world. In: Bhargavan, K., Oswald, E., Prabhakaran, M. (eds.) INDOCRYPT 2020. LNCS, vol. 12578, pp. 151\u2013202. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-65277-7_8"},{"key":"13_CR23","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.jisa.2016.08.001","volume":"31","author":"W Kong","year":"2016","unstructured":"Kong, W., Hou, G., Hu, X., Ando, T., Hisazumi, K., Fukuda, A.: Garakabu2: an SMT-based bounded model checker for HSTM designs in ZIPC. J. Inf. Sec. Appl. 31, 61\u201374 (2016). https:\/\/doi.org\/10.1016\/j.jisa.2016.08.001","journal-title":"J. Inf. Sec. Appl."},{"issue":"11","key":"13_CR24","doi-asserted-by":"publisher","first-page":"2824","DOI":"10.1093\/comjnl\/bxu127","volume":"58","author":"W Kong","year":"2015","unstructured":"Kong, W., Liu, L., Ando, T., Yatsu, H., Hisazumi, K., Fukuda, A.: Facilitating multicore bounded model checking with stateless explicit-state exploration. Comput. J. 58(11), 2824\u20132840 (2015). https:\/\/doi.org\/10.1093\/comjnl\/bxu127","journal-title":"Comput. J."},{"key":"13_CR25","unstructured":"Korf, R.E., Schultze, P.: Large-scale parallel breadth-first search. In: Proceedings of the 20th National Conference on Artificial Intelligence, AAAI 2005, vol. 3, pp. 1380\u20131385. AAAI Press (2005)"},{"key":"13_CR26","doi-asserted-by":"publisher","unstructured":"Leiserson, C.E., Schardl, T.B.: A work-efficient parallel breadth-first search algorithm (or how to cope with the nondeterminism of reducers). In: Proceedings of the Twenty-Second Annual ACM Symposium on Parallelism in Algorithms and Architectures, SPAA 2010, New York, NY, USA, pp. 303\u2013314. Association for Computing Machinery (2010). https:\/\/doi.org\/10.1145\/1810479.1810534","DOI":"10.1145\/1810479.1810534"},{"issue":"3","key":"13_CR27","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/0020-0190(95)00144-2","volume":"56","author":"G Lowe","year":"1995","unstructured":"Lowe, G.: An attack on the Needham-Schroeder public-key authentication protocol. Inf. Process. Lett. 56(3), 131\u2013133 (1995). https:\/\/doi.org\/10.1016\/0020-0190(95)00144-2","journal-title":"Inf. Process. Lett."},{"key":"13_CR28","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":"13_CR29","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.: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci. 96(1), 73\u2013155 (1992). https:\/\/doi.org\/10.1016\/0304-3975(92)90182-F","journal-title":"Theor. Comput. Sci."},{"key":"13_CR30","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"},{"issue":"7\u20138","key":"13_CR31","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1016\/j.jlap.2012.06.003","volume":"81","author":"J Meseguer","year":"2012","unstructured":"Meseguer, J.: Twenty years of rewriting logic. J. Log. Algebraic Methods Program. 81(7\u20138), 721\u2013781 (2012). https:\/\/doi.org\/10.1016\/j.jlap.2012.06.003","journal-title":"J. Log. Algebraic Methods Program."},{"key":"13_CR32","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/j.entcs.2004.06.024","volume":"117","author":"J Meseguer","year":"2005","unstructured":"Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. Electron. Notes Theor. Comput. Sci. 117, 153\u2013182 (2005). https:\/\/doi.org\/10.1016\/j.entcs.2004.06.024. Proceedings of the Fifth International Workshop on Rewriting Logic and Its Applications (WRLA 2004)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"12","key":"13_CR33","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"RM Needham","year":"1978","unstructured":"Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993\u2013999 (1978). https:\/\/doi.org\/10.1145\/359657.359659","journal-title":"Commun. ACM"},{"key":"13_CR34","doi-asserted-by":"publisher","unstructured":"Song, D.X.: Athena: a new efficient automatic checker for security protocol analysis. In: Proceedings of the 12th IEEE Computer Security Foundations Workshop, pp. 192\u2013202 (1999). https:\/\/doi.org\/10.1109\/CSFW.1999.779773","DOI":"10.1109\/CSFW.1999.779773"},{"key":"13_CR35","doi-asserted-by":"publisher","unstructured":"Yoo, A., Chow, E., Henderson, K., McLendon, W., Hendrickson, B., Catalyurek, U.: A scalable distributed parallel breadth-first search algorithm on BlueGene\/L. In: Proceedings of the 2005 ACM\/IEEE Conference on Supercomputing, SC 2005, p. 25 (2005). https:\/\/doi.org\/10.1109\/SC.2005.4","DOI":"10.1109\/SC.2005.4"}],"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_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,29]],"date-time":"2022-07-29T10:24:42Z","timestamp":1659090282000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-12441-9_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031124402","9783031124419"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-12441-9_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"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"}}]}}