{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T16:48:32Z","timestamp":1778258912815,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":48,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642038280","type":"print"},{"value":"9783642038297","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-03829-7_1","type":"book-chapter","created":{"date-parts":[[2009,8,10]],"date-time":"2009-08-10T09:05:20Z","timestamp":1249895120000},"page":"1-50","source":"Crossref","is-referenced-by-count":125,"title":["Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties"],"prefix":"10.1007","author":[{"given":"Santiago","family":"Escobar","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Catherine","family":"Meadows","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1-2","key":"1_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. Theoretical Computer Science\u00a0367(1-2), 2\u201332 (2006)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"1_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-004-2279-7","volume":"33","author":"S. Anantharaman","year":"2004","unstructured":"Anantharaman, S., Narendran, P., Rusinowitch, M.: Unification modulo CUI plus distributivity axioms. Journal of Automated Reasoning\u00a033(1), 1\u201328 (2004)","journal-title":"Journal of Automated Reasoning"},{"key":"1_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., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Drielsma, P.H., He\u00e1m, P.C., Kouchnarenko, O., Mantovani, J., M\u00f6dersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Vigan\u00f2, L., Vigneron, L.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 281\u2013285. Springer, Heidelberg (2005)"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"730","DOI":"10.1007\/978-3-540-30227-8_68","volume-title":"Logics in Artificial Intelligence","author":"A. Armando","year":"2004","unstructured":"Armando, A., Compagna, L., Lierler, Y.: SATMC: A SAT-based model checker for security protocols. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS, vol.\u00a03229, pp. 730\u2013733. Springer, Heidelberg (2004)"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Baader, F., Snyder, W.: Unification theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a02, pp. 445\u2013532. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"issue":"3","key":"1_CR6","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/s10207-004-0055-7","volume":"4","author":"D. Basin","year":"2005","unstructured":"Basin, D., M\u00f6dersheim, S., Vigan\u00f2, L.: OFMC: A symbolic model checker for security protocols. International Journal of Information Security\u00a04(3), 181\u2013208 (2005)","journal-title":"International Journal of Information Security"},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1007\/978-3-642-02348-4_11","volume-title":"RTA 2009","author":"M. Baudet","year":"2009","unstructured":"Baudet, M., Cortier, V., Delaune, S.: YAPA: A\u00a0generic tool for computing intruder knowledge. In: Treinen, R. (ed.) RTA 2009. LNCS, vol.\u00a05595, pp. 148\u2013163. Springer, Heidelberg (2009)"},{"key":"1_CR8","first-page":"82","volume-title":"14th IEEE Computer Security Foundations Workshop (CSFW-14)","author":"B. Blanchet","year":"2001","unstructured":"Blanchet, B.: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In: 14th IEEE Computer Security Foundations Workshop (CSFW-14), Cape Breton, Nova Scotia, Canada, pp. 82\u201396. IEEE Computer Society, Los Alamitos (2001)"},{"key":"1_CR9","unstructured":"Boichut, Y., H\u00e9am, P.-C., Kouchnarenko, O., Oehl, F.: Improvements on the Genet and Klay technique to automatically verify security protocols. In: Proceedings of Automated Verification of Infinite States Systems (AVIS 2004). ENTCS (2004)"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/978-3-642-02348-4_10","volume-title":"RTA 2009","author":"S. Bursuc","year":"2009","unstructured":"Bursuc, S., Comon-Lundh, H.: Protocol security and algebraic properties: decision results for a bounded number of sessions. In: Treinen, R. (ed.) RTA 2009. LNCS, vol.\u00a05595, pp. 133\u2013147. Springer, Heidelberg (2009)"},{"issue":"2-4","key":"1_CR11","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1016\/j.ic.2007.07.004","volume":"206","author":"Y. Chevalier","year":"2008","unstructured":"Chevalier, Y., Rusinowitch, M.: Hierarchical combination of intruder theories. Inf. Comput.\u00a0206(2-4), 352\u2013377 (2008)","journal-title":"Inf. Comput."},{"key":"1_CR12","series-title":"Lecture Notes in Artificial Intelligence","first-page":"355","volume-title":"CADE 2009","author":"\u015e. Ciob\u00e2c\u0103","year":"2009","unstructured":"Ciob\u00e2c\u0103, \u015e., Delaune, S., Kremer, S.: Computing knowledge in security protocols under convergent equational theories. In: Schmidt, R. (ed.) CADE 2009. LNCS (LNAI), vol.\u00a05663, pp. 355\u2013370. Springer, Heidelberg (2009)"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"380","DOI":"10.1007\/978-3-642-02348-4_27","volume-title":"RTA 2009","author":"M. Clavel","year":"2009","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Escobar, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: Unification and Narrowing in Maude 2.4. In: Treinen, R. (ed.) RTA 2009. LNCS, vol.\u00a05595, pp. 380\u2013390. Springer, Heidelberg (2009)"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M. Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"key":"1_CR15","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.\u00a03467, pp. 294\u2013307. Springer, Heidelberg (2005)"},{"key":"1_CR16","unstructured":"Contejean, E., March\u00e9, C.: The CiME system: tutorial and user\u2019s manual. Universit\u00e9 Paris-Sud, Centre d\u2019Orsay (manuscript)"},{"issue":"2","key":"1_CR17","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 Transaction on Information Theory\u00a029(2), 198\u2013208 (1983)","journal-title":"IEEE Transaction on Information Theory"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Durgin, N., Lincoln, P., Mitchell, J., Scedrov, A.: Multiset rewriting and the complexity of bounded security. Journal of Computer Security, 677\u2013722 (2004)","DOI":"10.3233\/JCS-2004-12203"},{"key":"1_CR19","unstructured":"Escobar, S., Hendrix, J., Meadows, C., Meseguer, J.: Diffie-Hellman cryptographic reasoning in the Maude-NRL protocol analyzer. In: Proc. 2nd International Workshop on Security and Rewriting Techniques, SecReT 2007 (2007)"},{"issue":"1-2","key":"1_CR20","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. Theoretical Compute Science\u00a0367(1-2), 162\u2013202 (2006)","journal-title":"Theoretical Compute Science"},{"key":"1_CR21","series-title":"ENTCS","first-page":"23","volume-title":"Proc. 1st International Workshop on Security and Rewriting Techniques (SecReT 2006)","author":"S. Escobar","year":"2007","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: Equational cryptographic reasoning in the Maude-NRL protocol analyzer. In: Proc. 1st International Workshop on Security and Rewriting Techniques (SecReT 2006). ENTCS, vol.\u00a0171(4), pp. 23\u201336. Elsevier, Amsterdam (2007)"},{"key":"1_CR22","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.\u00a05283, pp. 548\u2013562. Springer, Heidelberg (2008)"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA, version 1.0. University of Illinois at Urbana-Champaign (March 2009), http:\/\/maude.cs.uiuc.edu\/tools\/Maude-NPA","DOI":"10.1007\/978-3-642-03829-7_1"},{"key":"1_CR24","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.\u00a04533, pp. 153\u2013168. Springer, Heidelberg (2007)"},{"key":"1_CR25","unstructured":"Escobar, S., Meseguer, J., Sasse, R.: Variant narrowing and equational unification. Technical Report UIUCDCS-R-2007-2910, Dept. of Computer Science, University of Illinois at Urbana-Champaign (October 2007)"},{"key":"1_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-540-70590-1_6","volume-title":"Rewriting Techniques and Applications","author":"S. Escobar","year":"2008","unstructured":"Escobar, S., Meseguer, J., Sasse, R.: Effectively checking the finite variant property. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol.\u00a05117, pp. 79\u201393. Springer, Heidelberg (2008)"},{"key":"1_CR27","series-title":"ENTCS","volume-title":"Proc. 7th. Intl. Workshop on Rewriting Logic and its Applications","author":"S. Escobar","year":"2008","unstructured":"Escobar, S., Meseguer, J., Sasse, R.: Variant narrowing and equational unification. In: Rossu, G. (ed.) Proc. 7th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS. Elsevier, Amsterdam (2008) (to appear)"},{"key":"1_CR28","doi-asserted-by":"publisher","first-page":"191","DOI":"10.3233\/JCS-1999-72-304","volume":"7","author":"F.J.T. Fabrega","year":"1999","unstructured":"Fabrega, F.J.T., Herzog, J., Guttman, J.: Strand Spaces: What Makes a Security Protocol Correct? Journal of Computer Security\u00a07, 191\u2013230 (1999)","journal-title":"Journal of Computer Security"},{"key":"1_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1007\/3-540-10009-1_25","volume-title":"5th Conference on Automated Deduction","author":"J.-M. Hullot","year":"1980","unstructured":"Hullot, J.-M.: Canonical forms and unification. In: Bibel, W., Kowalski, R. (eds.) CADE 1980. LNCS, vol.\u00a087, pp. 318\u2013334. Springer, Heidelberg (1980)"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Millen, S.F.J.K., Clark, S.C.: The interrogator: Protocol secuity analysis. IEEE Transactions on Software Engineering, 274\u2013288 (February 1987)","DOI":"10.1109\/TSE.1987.233151"},{"key":"1_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/BFb0036921","volume-title":"Automata, Languages and Programming","author":"J.-P. Jouannaud","year":"1983","unstructured":"Jouannaud, J.-P., Kirchner, C., Kirchner, H.: Incremental construction of unification algorithms in equational theories. In: D\u00edaz, J. (ed.) ICALP 1983. LNCS, vol.\u00a0154, pp. 361\u2013373. Springer, Heidelberg (1983)"},{"key":"1_CR32","first-page":"93","volume":"17","author":"G. Lowe","year":"1996","unstructured":"Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. Software Concepts and Tools\u00a017, 93\u2013102 (1996)","journal-title":"Software Concepts and Tools"},{"key":"1_CR33","unstructured":"Lynch, C., Meadows, C.: On the relative soundness of the free algebra model for public key encryption. In: Workshop on Issues in Theory of Security 2004 (2004)"},{"key":"1_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-540-30191-2_21","volume-title":"Information and Communications Security","author":"C. Lynch","year":"2004","unstructured":"Lynch, C., Meadows, C.: Sound Approximations to Diffie-Hellman Using Rewrite Rules. In: L\u00f3pez, J., Qing, S., Okamoto, E. (eds.) ICICS 2004. LNCS, vol.\u00a03269, pp. 262\u2013277. Springer, Heidelberg (2004)"},{"key":"1_CR35","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1109\/CSFW.1996.503690","volume-title":"Ninth IEEE Computer Security Foundations Workshop","author":"C. Meadows","year":"1996","unstructured":"Meadows, C.: Language generation and verification in the NRL protocol analyzer. In: Ninth IEEE Computer Security Foundations Workshop, Dromquinna Manor, Kenmare, County Kerry, Ireland, March 10-12, pp. 48\u201361. IEEE Computer Society, Los Alamitos (1996)"},{"issue":"2","key":"1_CR36","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"C. Meadows","year":"1996","unstructured":"Meadows, C.: The NRL protocol analyzer: An overview. Journal of logic programming\u00a026(2), 113\u2013131 (1996)","journal-title":"Journal of logic programming"},{"issue":"1","key":"1_CR37","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. Theoretical Computer Science\u00a096(1), 73\u2013155 (1992)","journal-title":"Theoretical Computer Science"},{"key":"1_CR38","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: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol.\u00a01376, pp. 18\u201361. Springer, Heidelberg (1998)"},{"key":"1_CR39","doi-asserted-by":"crossref","unstructured":"Millen, J.: On the freedom of decryption. Information Processing Letters\u00a086(3) (2003)","DOI":"10.1016\/S0020-0190(03)00211-4"},{"key":"1_CR40","volume-title":"IEEE Symposium on Security and Privacy","author":"J. Mitchell","year":"1997","unstructured":"Mitchell, J., Mitchell, M., Stern, U.: Automated analysis of cryptographic protocols using Murphi. In: IEEE Symposium on Security and Privacy. IEEE Computer Society, Los Alamitos (1997)"},{"issue":"1-2","key":"1_CR41","doi-asserted-by":"publisher","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L.C. Paulson","year":"1998","unstructured":"Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security\u00a06(1-2), 85\u2013128 (1998)","journal-title":"Journal of Computer Security"},{"key":"1_CR42","doi-asserted-by":"crossref","unstructured":"Rusinowitch, M., Turuani, M.: Protocol insecurity with a finite number of sessions and composed keys is NP-complete. In: 14th IEEE Computer Security Foundations Workshop, pp. 174\u2013190 (2001)","DOI":"10.1109\/CSFW.2001.930145"},{"issue":"1","key":"1_CR43","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1016\/S0020-0190(97)00180-4","volume":"65","author":"P.Y.A. Ryan","year":"1998","unstructured":"Ryan, P.Y.A., Schneider, S.A.: An attack on a recursive authentication protocol. a cautionary tale. Inf. Process. Lett.\u00a065(1), 7\u201310 (1998)","journal-title":"Inf. Process. Lett."},{"key":"1_CR44","doi-asserted-by":"crossref","unstructured":"Santiago, S., Talcott, C., Escobar, S., Meadows, C., Meseguer, J.: A graphical user interface for Maude-NPA. Technical Report DSIC-II\/02\/09, Universidad Polit\u00e9cnica de Valencia (June 2009)","DOI":"10.1016\/j.entcs.2009.12.002"},{"key":"1_CR45","volume-title":"11th Computer Security Foundations Workshop \u2014 CSFW-11","author":"V. Shmatikov","year":"1998","unstructured":"Shmatikov, V., Stern, U.: Efficient finite-state analysis for large security protocols. In: 11th Computer Security Foundations Workshop \u2014 CSFW-11. IEEE Computer Society Press, Los Alamitos (1998)"},{"issue":"4","key":"1_CR46","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1109\/49.839933","volume":"18","author":"S. Stubblebine","year":"2000","unstructured":"Stubblebine, S., Meadows, C.: Formal characterization and automated analysis of known-pair and chosen-text attacks. IEEE Journal on Selected Areas in Communications\u00a018(4), 571\u2013581 (2000)","journal-title":"IEEE Journal on Selected Areas in Communications"},{"key":"1_CR47","volume-title":"Term Rewriting Systems","year":"2003","unstructured":"TeReSe (ed.): Term Rewriting Systems. Cambridge University Press, Cambridge (2003)"},{"issue":"1-2","key":"1_CR48","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10990-007-9000-6","volume":"20","author":"P. Thati","year":"2007","unstructured":"Thati, P., Meseguer, J.: Symbolic reachability analysis using narrowing and its application verification of cryptographic protocols. J. Higher-Order and Symbolic Computation\u00a020(1-2), 123\u2013160 (2007)","journal-title":"J. Higher-Order and Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Foundations of Security Analysis and Design V"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03829-7_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,11]],"date-time":"2025-02-11T18:13:23Z","timestamp":1739297603000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03829-7_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642038280","9783642038297"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03829-7_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}