{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,2]],"date-time":"2024-07-02T06:51:43Z","timestamp":1719903103606},"reference-count":33,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2014,11,1]],"date-time":"2014-11-01T00:00:00Z","timestamp":1414800000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2018,11,1]],"date-time":"2018-11-01T00:00:00Z","timestamp":1541030400000},"content-version":"vor","delay-in-days":1461,"URL":"http:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"funder":[{"name":"the EU (FEDER) and the Spanish MEC\/MICINN","award":["TIN 2010-21062-C02-02"]},{"DOI":"10.13039\/501100003359","name":"Generalitat Valenciana","doi-asserted-by":"publisher","award":["PROMETEO2011\/052"],"id":[{"id":"10.13039\/501100003359","id-type":"DOI","asserted-by":"publisher"}]},{"name":"NSF","award":["CNS 09-04749","CCF 09-05584"]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Information and Computation"],"published-print":{"date-parts":[[2014,11]]},"DOI":"10.1016\/j.ic.2014.07.007","type":"journal-article","created":{"date-parts":[[2014,7,16]],"date-time":"2014-07-16T20:27:30Z","timestamp":1405542450000},"page":"157-186","update-policy":"http:\/\/dx.doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":17,"special_numbering":"C","title":["State space reduction in the Maude-NRL Protocol Analyzer"],"prefix":"10.1016","volume":"238","author":[{"given":"Santiago","family":"Escobar","sequence":"first","affiliation":[]},{"given":"Catherine","family":"Meadows","sequence":"additional","affiliation":[]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[]},{"given":"Sonia","family":"Santiago","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.ic.2014.07.007_br0010","series-title":"Concur '00","first-page":"380","article-title":"On the reachability problem in cryptographic protocols","author":"Amadio","year":"2000"},{"key":"10.1016\/j.ic.2014.07.007_br0020","author":"Basin"},{"issue":"3","key":"10.1016\/j.ic.2014.07.007_br0030","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1007\/s10207-004-0055-7","article-title":"OFMC: a symbolic model checker for security protocols","volume":"4","author":"Basin","year":"2005","journal-title":"Int. J. Inf. Secur."},{"key":"10.1016\/j.ic.2014.07.007_br0040","series-title":"ESORICS","first-page":"253","article-title":"An on-the-fly model-checker for security protocol analysis","volume":"vol. 2808","author":"Basin","year":"2003"},{"key":"10.1016\/j.ic.2014.07.007_br0050","series-title":"14th IEEE Computer Security Foundations Workshop","first-page":"82","article-title":"An efficient cryptographic protocol verifier based on prolog rules","author":"Blanchet","year":"2001"},{"issue":"4","key":"10.1016\/j.ic.2014.07.007_br0060","doi-asserted-by":"crossref","DOI":"10.1145\/1380572.1380573","article-title":"Complexity results for security protocols with Diffie\u2013Hellman exponentiation and commuting public key encryption","volume":"9","author":"Chevalier","year":"2008","journal-title":"ACM Trans. Comput. Log."},{"key":"10.1016\/j.ic.2014.07.007_br0070","series-title":"Scyther \u2013 semantics and verification of security protocols","author":"Cremers","year":"2006"},{"key":"10.1016\/j.ic.2014.07.007_br0080","series-title":"ACM Conference on Computer and Communications Security","first-page":"119","article-title":"Unbounded verification, falsification, and characterization of security protocols by pattern refinement","author":"Cremers","year":"2008"},{"issue":"2","key":"10.1016\/j.ic.2014.07.007_br0090","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","article-title":"On the security of public key protocols","volume":"29","author":"Dolev","year":"1983","journal-title":"IEEE Trans. Inf. Theory"},{"key":"10.1016\/j.ic.2014.07.007_br0100","series-title":"Proc. 2nd International Workshop on Security and Rewriting Techniques","article-title":"Diffie\u2013Hellman cryptographic reasoning in the Maude-NRL protocol analyzer","author":"Escobar","year":"2007"},{"issue":"1\u20132","key":"10.1016\/j.ic.2014.07.007_br0110","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1016\/j.tcs.2006.08.035","article-title":"A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties","volume":"367","author":"Escobar","year":"2006","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/j.ic.2014.07.007_br0120","series-title":"Proc. 1st International Workshop on Security and Rewriting Techniques","first-page":"23","article-title":"Equational cryptographic reasoning in the Maude-NRL protocol analyzer","author":"Escobar","year":"2007"},{"key":"10.1016\/j.ic.2014.07.007_br0130","series-title":"Computer Security \u2013 ESORICS 2008, 13th European Symposium on Research in Computer Security. Proceedings","first-page":"548","article-title":"State space reduction in the Maude-NRL Protocol Analyzer","volume":"vol. 5283","author":"Escobar","year":"2008"},{"key":"10.1016\/j.ic.2014.07.007_br0140","series-title":"FOSAD 2008\/2009 Tutorial Lectures","first-page":"1","article-title":"Maude-NPA: cryptographic protocol analysis modulo equational properties","volume":"vol. 5705","author":"Escobar","year":"2009"},{"key":"10.1016\/j.ic.2014.07.007_br0150","author":"Escobar"},{"key":"10.1016\/j.ic.2014.07.007_br0160","series-title":"Proceedings of the 18th International Conference on Rewriting Techniques and Applications","first-page":"153","article-title":"Symbolic model checking of infinite-state systems using narrowing","volume":"vol. 4533","author":"Escobar","year":"2007"},{"key":"10.1016\/j.ic.2014.07.007_br0170","series-title":"Rewriting Techniques and Applications, 19th International Conference. Proceedings","first-page":"79","article-title":"Effectively checking the finite variant property","volume":"vol. 5117","author":"Escobar","year":"2008"},{"issue":"3","key":"10.1016\/j.ic.2014.07.007_br0180","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/j.entcs.2009.05.015","article-title":"Variant narrowing and equational unification","volume":"238","author":"Escobar","year":"2009","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"10.1016\/j.ic.2014.07.007_br0190","series-title":"Rewriting Logic and Its Applications \u2013 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010. Revised Selected Papers","first-page":"52","article-title":"Folding variant narrowing and optimal variant termination","volume":"vol. 6381","author":"Escobar","year":"2010"},{"key":"10.1016\/j.ic.2014.07.007_br0200","article-title":"Folding variant narrowing and optimal variant termination","author":"Escobar","year":"2011","journal-title":"J. Log. Algebr. Program."},{"key":"10.1016\/j.ic.2014.07.007_br0210","doi-asserted-by":"crossref","first-page":"191","DOI":"10.3233\/JCS-1999-72-304","article-title":"Strand spaces: what makes a security protocol correct?","volume":"7","author":"Fabrega","year":"1999","journal-title":"J. Comput. Secur."},{"key":"10.1016\/j.ic.2014.07.007_br0220","series-title":"Proc. FLOC'99 Workshop on Formal Methods and Security Protocols","article-title":"Efficient infinite-state analysis of security protocols","author":"Huima","year":"1999"},{"key":"10.1016\/j.ic.2014.07.007_br0230","series-title":"Ninth IEEE Computer Security Foundations Workshop","first-page":"48","article-title":"Language generation and verification in the NRL protocol analyzer","author":"Meadows","year":"1996"},{"issue":"2","key":"10.1016\/j.ic.2014.07.007_br0240","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","article-title":"The NRL protocol analyzer: an overview","volume":"26","author":"Meadows","year":"1996","journal-title":"J. Log. Program."},{"issue":"1","key":"10.1016\/j.ic.2014.07.007_br0250","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","article-title":"Conditional rewriting logic as a unified model of concurrency","volume":"96","author":"Meseguer","year":"1992","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/j.ic.2014.07.007_br0260","series-title":"Proc. WADT'97","first-page":"18","article-title":"Membership algebra as a logical framework for equational specification","volume":"vol. 1376","author":"Meseguer","year":"1998"},{"key":"10.1016\/j.ic.2014.07.007_br0270","series-title":"ACM Conference on Computer and Communications Security","first-page":"166","article-title":"Constraint solving for bounded-process cryptographic protocol analysis","author":"Millen","year":"2001"},{"issue":"4","key":"10.1016\/j.ic.2014.07.007_br0280","doi-asserted-by":"crossref","first-page":"575","DOI":"10.3233\/JCS-2009-0351","article-title":"Constraint differentiation: search-space reduction for the constraint-based analysis of security protocols","volume":"18","author":"M\u00f6dersheim","year":"2010","journal-title":"J. Comput. Secur."},{"key":"10.1016\/j.ic.2014.07.007_br0290","series-title":"Security and Trust Management \u2013 6th International Workshop, Revised Selected Papers","first-page":"163","article-title":"Protocol analysis modulo combination of theories: a case study in Maude-NPA","volume":"vol. 6710","author":"Sasse","year":"2011"},{"key":"10.1016\/j.ic.2014.07.007_br0300","series-title":"11th Computer Security Foundations Workshop","article-title":"Efficient finite-state analysis for large security protocols","author":"Shmatikov","year":"1998"},{"key":"10.1016\/j.ic.2014.07.007_br0310","series-title":"Term Rewriting Systems","year":"2003"},{"issue":"1\u20132","key":"10.1016\/j.ic.2014.07.007_br0320","first-page":"123","article-title":"Symbolic reachability analysis using narrowing and its application verification of cryptographic protocols","volume":"20","author":"Thati","year":"2007","journal-title":"High.-Order Symb. Comput."},{"key":"10.1016\/j.ic.2014.07.007_br0330","series-title":"CADE","first-page":"314","article-title":"Towards an automatic analysis of security protocols in first-order logic","volume":"vol. 1632","author":"Weidenbach","year":"1999"}],"container-title":["Information and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0890540114000935?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0890540114000935?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2018,11,12]],"date-time":"2018-11-12T23:30:35Z","timestamp":1542065435000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0890540114000935"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11]]},"references-count":33,"alternative-id":["S0890540114000935"],"URL":"https:\/\/doi.org\/10.1016\/j.ic.2014.07.007","relation":{},"ISSN":["0890-5401"],"issn-type":[{"value":"0890-5401","type":"print"}],"subject":[],"published":{"date-parts":[[2014,11]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"State space reduction in the Maude-NRL Protocol Analyzer","name":"articletitle","label":"Article Title"},{"value":"Information and Computation","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.ic.2014.07.007","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2014 Elsevier Inc. Published by Elsevier Inc. All rights reserved.","name":"copyright","label":"Copyright"}]}}  <script>parent.window.postMessage('ixistenz.url:https://api.crossref.org/works/10.1016%2FJ.IC.2014.07.007', '*'); </script> <div id='browserdiffcontainer' style='position: fixed; right: 10px; top: 10vh; min-width: 60px;  border: 1px solid white; background: rgb(251, 189, 0);; opacity: 0.9; font-family: helvetica, arial, sans serif;  font-size: 12px; z-index: 20001; padding-bottom: 20px;'><div onclick="toggle('browserdiffcontainerlist'); return false;" style='background: rgb(151, 89, 0);; color: white; '><strong>&nbsp; <span class='glyphicon glyphicon-minus'></span> NODES</strong></div><div id='browserdiffcontainerlist' style='padding-left: 10px; padding-right: 5px; max-height: 50vh; overflow: auto; '><div><a href='#diffid123' style='color: white;' onClick="parent.window.postMessage('ixistenz.opendiff:123', '*');; return false;" style='text-decoration: none; '>INTERN </a> <a style='color: white;' href='#diffid123'><sup>6</sup></a></div><div><a href='#diffid878' style='color: white;' onClick="parent.window.postMessage('ixistenz.opendiff:878', '*');; return false;" style='text-decoration: none; '>Note </a> <a style='color: white;' href='#diffid878'><sup>1</sup></a></div></div></div>
<script>
function toggle( divname ) {
  var x = document.getElementById( divname );
  if (x.style.display === 'none') {
    x.style.display = 'block';
  } else {
    x.style.display = 'none';
  }
} </script>