{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T03:49:40Z","timestamp":1778298580771,"version":"3.51.4"},"reference-count":22,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2004,4,1]],"date-time":"2004-04-01T00:00:00Z","timestamp":1080777600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3406,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2004,4]]},"DOI":"10.1016\/s1571-0661(05)82536-8","type":"journal-article","created":{"date-parts":[[2005,5,19]],"date-time":"2005-05-19T09:46:30Z","timestamp":1116495990000},"page":"208-222","source":"Crossref","is-referenced-by-count":9,"special_numbering":"C","title":["Rewriting-Based Verification of Authentication Protocols"],"prefix":"10.1016","volume":"71","author":[{"given":"Kazuhiro","family":"Ogata","sequence":"first","affiliation":[]},{"given":"Kokichi","family":"Futatsugi","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(05)82536-8_BIB1","unstructured":"CafeOBJ web page. URL http:\/\/www.ldl.jaist.ac.jp\/cafeobj\/"},{"key":"10.1016\/S1571-0661(05)82536-8_BIB2","first-page":"55","article-title":"A meta-notation for protocol analysis","author":"Cervesato","year":"1999","journal-title":"12th IEEE CSFW"},{"key":"10.1016\/S1571-0661(05)82536-8_BIB3","series-title":"\u201cParallel program design: a foundation,\u201d","author":"Chandy","year":"1988"},{"key":"10.1016\/S1571-0661(05)82536-8_BIB4","article-title":"Protocol specification and analysis in Maude","author":"Denker","year":"1998","journal-title":"Formal Methods and Security Protocols Workshop"},{"key":"10.1016\/S1571-0661(05)82536-8_BIB5","series-title":"AMAST Series in Computing, 6","doi-asserted-by":"crossref","DOI":"10.1142\/3831","article-title":"\u201cCafeOBJ report,\u201d","author":"Diaconescu","year":"1998"},{"key":"10.1016\/S1571-0661(05)82536-8_BIB6","first-page":"74","article-title":"Behavioural coherence in object-oriented algebraic specification","volume":"6","author":"Diaconescu","year":"2000","journal-title":"Universal Computer Science"},{"key":"10.1016\/S1571-0661(05)82536-8_BIB7","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","article-title":"On the security of public key protocols","volume":"IT-29","author":"Dolev","year":"1983","journal-title":"IEEE Trans. Inform. Theory"},{"key":"10.1016\/S1571-0661(05)82536-8_BIB8","article-title":"Strand space pictures","author":"F\u00e1brega","year":"1998","journal-title":"Formal Methods and Security Protocols Workshop"},{"key":"10.1016\/S1571-0661(05)82536-8_BIB9","doi-asserted-by":"crossref","first-page":"191","DOI":"10.3233\/JCS-1999-72-304","article-title":"Strand spaces: Proving security protocols correct","volume":"7","author":"F\u00e1brega","year":"1999","journal-title":"J. Computer Security"},{"key":"10.1016\/S1571-0661(05)82536-8_BIB10","first-page":"60","article-title":"Rewriting can verify distributed real-time systems","author":"Futatsugi","year":"2001","journal-title":"Int'l Symposium on Rewriting, Proof, and Computation"},{"key":"10.1016\/S1571-0661(05)82536-8_BIB11","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/S0304-3975(99)00275-3","article-title":"A hidden agenda","volume":"245","author":"Goguen","year":"2000","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/S1571-0661(05)82536-8_BIB12","series-title":"\u201cSoftware Engineering with OBJ: algebraic specification in action,\u201d","author":"Goguen","year":"2000"},{"key":"10.1016\/S1571-0661(05)82536-8_BIB13","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1023\/A:1013323127548","article-title":"Web-based support for cooperative software engineering","volume":"12","author":"Goguen","year":"2001","journal-title":"Annals of Software Engineering"},{"key":"10.1016\/S1571-0661(05)82536-8_BIB14","series-title":"Ph.D. thesis","article-title":"\u201cRefutational Theorem Proving using Term Rewriting Systems,\u201d","author":"Hsiang","year":"1981"},{"key":"10.1016\/S1571-0661(05)82536-8_BIB15","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1016\/0020-0190(95)00144-2","article-title":"An attack on the Needham-Schroeder public-key authentication protocol","volume":"56","author":"Lowe","year":"1995","journal-title":"Inf. Process. Lett."},{"key":"10.1016\/S1571-0661(05)82536-8_BIB16","first-page":"147","article-title":"Breaking and fixing the Needham-Schroeder public-key protocol using FDR. TACAS \u203296","author":"Lowe","year":"1996","journal-title":"LNCS 1055"},{"key":"10.1016\/S1571-0661(05)82536-8_BIB17","unstructured":"Maude web page. URL http:\/\/maude.csl.sri.com\/"},{"key":"10.1016\/S1571-0661(05)82536-8_BIB18","doi-asserted-by":"crossref","first-page":"993","DOI":"10.1145\/359657.359659","article-title":"Using encryption for authentication in large networks of computers","volume":"21","author":"Needham","year":"1978","journal-title":"Comm. ACM"},{"key":"10.1016\/S1571-0661(05)82536-8_BIB19","first-page":"185","article-title":"Modeling and verification of distributed real-time systems based on CafeOBJ","author":"Ogata","year":"2001","journal-title":"ASE \u203201"},{"key":"10.1016\/S1571-0661(05)82536-8_BIB20","first-page":"181","article-title":"Formal analysis of Suzuki&Kasami distributed mutual exclusion algorithm","author":"Ogata","year":"2002","journal-title":"FMOODS \u203202"},{"key":"10.1016\/S1571-0661(05)82536-8_BIB21","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","article-title":"The inductive approach to verifying cryptographic protocols","volume":"6","author":"Paulson","year":"1998","journal-title":"J. Computer Security"},{"key":"10.1016\/S1571-0661(05)82536-8_BIB22","doi-asserted-by":"crossref","first-page":"741","DOI":"10.1109\/32.713329","article-title":"Verifying authentication protocols in CSP","volume":"24","author":"Schneider","year":"1998","journal-title":"IEEE Trans. on Softw. Eng."}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105825368?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105825368?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,1,26]],"date-time":"2019-01-26T05:58:00Z","timestamp":1548482280000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066105825368"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,4]]},"references-count":22,"alternative-id":["S1571066105825368"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(05)82536-8","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2004,4]]}}}