{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T11:49:33Z","timestamp":1783684173738,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540883128","type":"print"},{"value":"9783540883135","type":"electronic"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-88313-5_35","type":"book-chapter","created":{"date-parts":[[2008,10,4]],"date-time":"2008-10-04T00:41:44Z","timestamp":1223080904000},"page":"548-562","source":"Crossref","is-referenced-by-count":14,"title":["State Space Reduction in the Maude-NRL Protocol Analyzer"],"prefix":"10.1007","author":[{"given":"Santiago","family":"Escobar","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Catherine","family":"Meadows","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"3","key":"35_CR1","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. Int\u2019l Journal of Information Security\u00a04(3), 181\u2013208 (2005)","journal-title":"Int\u2019l Journal of Information Security"},{"key":"35_CR2","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50026-6","volume-title":"Model Checking","author":"E.M. Clarke","year":"2001","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2001)"},{"issue":"2","key":"35_CR3","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":"35_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"Proc. of Term Rewriting and Applications, RTA 2008","author":"S. Escobar","year":"2008","unstructured":"Escobar, S., Meseguer, J., Sasse, R.: Effectively checking or disproving the finite variant property. In: Proc. of Term Rewriting and Applications, RTA 2008. LNCS. Springer, Heidelberg (to appear, 2008)"},{"key":"35_CR5","unstructured":"Escobar, S., Meseguer, J., Sasse, R.: Variant narrowing and equational unification. In: Proc. of Rewriting Logic and its Applications, WRLA 2008 (2008)"},{"key":"35_CR6","doi-asserted-by":"crossref","unstructured":"Escobar, S., Hendrix, J., Meadows, C., Meseguer, J.: Diffie-hellman cryptographic reasoning in the Maude-NRL Protocol Analyzer. In: Proc. of Security and Rewriting Techniques, SecReT 2007 (2007)","DOI":"10.1016\/j.entcs.2007.02.053"},{"key":"35_CR7","doi-asserted-by":"crossref","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: A rewriting-based inference system for the NRL Protocol Analyzer and its meta-logical properties. Theoretical Computer Science\u00a0367(1-2) (2006)","DOI":"10.1016\/j.tcs.2006.08.035"},{"issue":"4","key":"35_CR8","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/j.entcs.2007.02.053","volume":"171","author":"S. Escobar","year":"2007","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: Equational cryptographic reasoning in the maude-nrl protocol analyzer. Electronic Notes in Theoretical Computer Science\u00a0171(4), 23\u201336 (2007)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"35_CR9","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":"35_CR10","doi-asserted-by":"publisher","first-page":"191","DOI":"10.3233\/JCS-1999-72-304","volume":"7","author":"F.J. Thayer Fabrega","year":"1999","unstructured":"Thayer Fabrega, F.J., 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"},{"issue":"2","key":"35_CR11","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":"35_CR12","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":"35_CR13","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)"},{"issue":"1-2","key":"35_CR14","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. Higher-Order and Symbolic Computation\u00a020(1-2), 123\u2013160 (2007)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"35_CR15","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)"},{"key":"35_CR16","volume-title":"Term Rewriting Systems","year":"2003","unstructured":"Terese (ed.): Term Rewriting Systems. Cambridge University Press, Cambridge (2003)"}],"container-title":["Lecture Notes in Computer Science","Computer Security - ESORICS 2008"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-88313-5_35","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,2]],"date-time":"2019-06-02T20:13:49Z","timestamp":1559506429000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-88313-5_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540883128","9783540883135"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-88313-5_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008]]}}}