乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,2]],"date-time":"2025-01-02T05:21:48Z","timestamp":1735795308024,"version":"3.32.0"},"reference-count":33,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"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":4958,"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":[[2000]]},"DOI":"10.1016\/s1571-0661(05)80141-0","type":"journal-article","created":{"date-parts":[[2005,5,25]],"date-time":"2005-05-25T12:37:08Z","timestamp":1117024628000},"page":"235-256","source":"Crossref","is-referenced-by-count":7,"special_numbering":"C","title":["Maude versus Haskell: an Experimental Comparison in Security Protocol Analysis"],"prefix":"10.1016","volume":"36","author":[{"given":"David","family":"Basin","sequence":"first","affiliation":[]},{"given":"Grit","family":"Denker","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(05)80141-0_BIB1","unstructured":"P. Borovansk\u00fd, C. Kirchner, and H. Kirchner. Strategies and Rewriting in ELAN. In B. Gramlich and H. Kirchner, editors, Proceedings of the CADE-14 Workshop on Strategies in Automated Deduction (Townsville, Australia, July 1997), 1997."},{"key":"10.1016\/S1571-0661(05)80141-0_BIB2","unstructured":"P. Borovansk\u00fd, C. Kirchner, H. Kirchner, P.-E. Moreau, and M. Vittek. ELAN: A Logical Framework Based on Computational Systems. In Meseguer [24]."},{"key":"10.1016\/S1571-0661(05)80141-0_BIB3","unstructured":"S. Brackin. Automatically Detecting Most Vulnerabilities in Cryptographic Protocols. In Maughan et al. [21], pages 251-266. http:\/\/schafercorp-ballston.com\/discex\/."},{"key":"10.1016\/S1571-0661(05)80141-0_BIB4","unstructured":"CafeOBJ Project. Proc. of the CafeOBJ Symposium '98, Numazu, Japan. April 1998."},{"key":"10.1016\/S1571-0661(05)80141-0_BIB5","first-page":"55","article-title":"A Meta-Notation for Protocol Analysis","author":"Cervesato","year":"1999"},{"key":"10.1016\/S1571-0661(05)80141-0_BIB6","unstructured":"M. Clavel, F. Duran, S. Eker, P. Lincoln, N. Mart\u00ed-Oliet, J. Meseguer, and J. Quesada. Maude: Specification and Programming in Rewriting Logic. SRI International, Computer Science Laboratory, Menlo Park, CA, January 1999. http:\/\/maude.csl.sri.com\/manual\/."},{"key":"10.1016\/S1571-0661(05)80141-0_BIB7","doi-asserted-by":"crossref","unstructured":"M. Clavel, S. Eker, P. Lincoln, and J. Meseguer. Principles of Maude. In Meseguer [24], pages 65-89.","DOI":"10.1016\/S1571-0661(04)00034-9"},{"key":"10.1016\/S1571-0661(05)80141-0_BIB8","unstructured":"M. Clavel and J. Meseguer. Reflection and Strategies in Rewriting Logic. In Meseguer [24], pages 125-147."},{"key":"10.1016\/S1571-0661(05)80141-0_BIB9","series-title":"Proc. of Workshop on Formal Methods and Security Protocols, 25 June 1998, Indianapolis, Indiana","article-title":"Protocol Specification and Analysis in Maude","author":"Denker","year":"1998"},{"key":"10.1016\/S1571-0661(05)80141-0_BIB10","doi-asserted-by":"crossref","unstructured":"G. Denker, J. Meseguer, and C. Talcott. Formal Specification and Analysis of Active Networks and Communication Protocols: The Maude Experience. In Maughan et al. [21], pages 251-266. http:\/\/schafercorp-ballston.com\/discex\/.","DOI":"10.1109\/DISCEX.2000.825030"},{"key":"10.1016\/S1571-0661(05)80141-0_BIB11","doi-asserted-by":"crossref","unstructured":"G. Denker and J. Millen. CAPSL Integrated Protocol Environment. In Maughan et al. [21], pages 207-222. http:\/\/schafercorp-ballston.com\/discex\/.","DOI":"10.1109\/DISCEX.2000.824980"},{"key":"10.1016\/S1571-0661(05)80141-0_BIB12","first-page":"52","article-title":"Optimizing Protocol Rewrite Rules of CIL Specifications","author":"Denker","year":"2000","journal-title":"13th IEEE Computer Security Foundations Workshop (CSFW'2000), 3-5 July 2000, Cambridge, United Kingdom. IEEE Computer Society"},{"key":"10.1016\/S1571-0661(05)80141-0_BIB13","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 Transactions on Information Theory"},{"key":"10.1016\/S1571-0661(05)80141-0_BIB14","series-title":"Research Topics in Functional Programming","article-title":"Higher-order functions considered unnecessary for higher-order programming","author":"Goguen","year":"1990"},{"key":"10.1016\/S1571-0661(05)80141-0_BIB15","unstructured":"S. P. Jones and J. H. (editors). Report on the Programming Language Haskell 98. http:\/\/www.haskell.org\/definition\/haskell98-report.ps.gz."},{"key":"10.1016\/S1571-0661(05)80141-0_BIB16","unstructured":"S. P. Jones, C. Hall, K. Hammond, W. Partain, and P. Wadler. The Glasgow Haskell compiler: a technical overview. In Proceedings of Joint Framework for Information Technology Technical Conference, pages 249-257, Keele, March 1993."},{"key":"10.1016\/S1571-0661(05)80141-0_BIB17","doi-asserted-by":"crossref","unstructured":"G. Lowe. Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR. In Proceedings of TAGAS, volume 1055 of Lecture Notes in Computer Science, pages 147-166. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61042-1_43"},{"issue":"1","key":"10.1016\/S1571-0661(05)80141-0_BIB18","doi-asserted-by":"crossref","first-page":"53","DOI":"10.3233\/JCS-1998-61-204","article-title":"Casper: A Compiler For the Analysis of Security Protocols","volume":"6","author":"Lowe","year":"1998","journal-title":"Journal of Computer Security"},{"key":"10.1016\/S1571-0661(05)80141-0_BIB19","unstructured":"N. Mart\u00ed-Oliet and J. Meseguer. Rewriting Logic As a Logical and Semantic Framework. In Meseguer [24], pages 189-225."},{"key":"10.1016\/S1571-0661(05)80141-0_BIB20","unstructured":"Maude Web Site. http:\/\/maude.csl.sri.com\/, 2000."},{"key":"10.1016\/S1571-0661(05)80141-0_BIB21","unstructured":", pages 251-266. http:\/\/schafercorp-ballston.com\/discex\/."},{"issue":"2","key":"10.1016\/S1571-0661(05)80141-0_BIB22","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":"Journal of Logic Programming"},{"issue":"1","key":"10.1016\/S1571-0661(05)80141-0_BIB23","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":"Theoretical Comput. Sci"},{"key":"10.1016\/S1571-0661(05)80141-0_BIB24","doi-asserted-by":"crossref","unstructured":"J. Meseguer, editor. Rewriting Logic and Its Applications, First International Workshop, Asilomar Conference Center, Pacific Grove, CA, September 3-6, 1996. Elsevier Science B.V., Electronic Notes in Theoretical Computer Science, Volume 4, http:\/\/www.elsevier.nl\/locate\/entcs\/volume4.html, 1996.","DOI":"10.21236\/ADA314817"},{"key":"10.1016\/S1571-0661(05)80141-0_BIB25","doi-asserted-by":"crossref","unstructured":"J. Meseguer. Rewriting Logic as a Semantic Framework for Concurrency: A Progress Report. In U. Montanari and V. Sassone, editors, Proc. 7th Intern. Conf. on Concurrency Theory: CONCUR'96, Pisa, August 1996, pages 331-372, 1996. LNCS 1119.","DOI":"10.1007\/3-540-61604-7_64"},{"key":"10.1016\/S1571-0661(05)80141-0_BIB26","series-title":"Computational Logic, NATO Advanced Study Institute, Marktoberdorf, Germany, July 29 - August 6, 1997","first-page":"347","article-title":"Research Directions in Rewriting Logic","author":"Meseguer","year":"1998"},{"key":"10.1016\/S1571-0661(05)80141-0_BIB27","series-title":"2000 IEEE Symposium on Security and Privacy","article-title":"Protocol-Independent Secrecy","author":"Millen","year":"2000"},{"key":"10.1016\/S1571-0661(05)80141-0_BIB28","first-page":"141","article-title":"Automated Analysis of Cryptographic Protocols Using Mur\u00f8","author":"Mitchell","year":"1997","journal-title":"IEEE Symposium on Security and Privacy. IEEE Computer Society"},{"issue":"12","key":"10.1016\/S1571-0661(05)80141-0_BIB29","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":"Communications of the ACM"},{"key":"10.1016\/S1571-0661(05)80141-0_BIB30","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":"Journal of Computer Security"},{"key":"10.1016\/S1571-0661(05)80141-0_BIB31","first-page":"106","article-title":"Efficient Finite State Analysis for Large Security Protocols","author":"Shmatikov","year":"1998"},{"key":"10.1016\/S1571-0661(05)80141-0_BIB32","first-page":"192","article-title":"Athena, an Automatic Checker for Security Protocol Analysis","author":"Song","year":"1999"},{"key":"10.1016\/S1571-0661(05)80141-0_BIB33","series-title":"Proc. of LFM'99: Workshop on Logical Frameworks and Meta-languages, Paris, France, September 28, 1999","article-title":"Pure Type Systems in Rewriting Logic","author":"Stehr","year":"1999"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105801410?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105801410?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T10:16:13Z","timestamp":1735726573000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066105801410"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"references-count":33,"alternative-id":["S1571066105801410"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(05)80141-0","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[2000]]}}}