{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:32:44Z","timestamp":1754487164810},"publisher-location":"Berlin, Heidelberg","reference-count":49,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540593393"},{"type":"electronic","value":"9783540492368"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0000430","type":"book-chapter","created":{"date-parts":[[2005,10,7]],"date-time":"2005-10-07T15:27:29Z","timestamp":1128698849000},"page":"133-150","source":"Crossref","is-referenced-by-count":40,"title":["Formal verification of cryptographic protocols: A survey"],"prefix":"10.1007","author":[{"given":"Catherine A.","family":"Meadows","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Catherine A.","family":"Meadows","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,9,8]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Mart\u00edn Abadi and Mark Tuttle. A Semantics for a Logic of Authentication. In Proceedings of the Tenth ACM Symposium on Principles of Distributed Computing, pages 201\u2013216. ACM Press, August 1991.","DOI":"10.1145\/112600.112618"},{"issue":"1","key":"11_CR2","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1109\/98.295357","volume":"1","author":"A. Aziz","year":"1994","unstructured":"A. Aziz and W. Diffie. Privacy and Authentication for Wireless Local Area Networks. IEEE Personal Communications, 1(1):25\u201331, 1994.","journal-title":"IEEE Personal Communications"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"M. Bellare and P. Rogaway. Entity Authentication and Key Distribution. In Advances in Cryptology \u2014 CRYPTO '93, volume to appear. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-48329-2_21"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"P. Bieber. A Logic of Communication in a Hostile Environment. In Proceedings of the Computer Security Foundations Workshop III, pages 14\u201322. IEEE Computer Society Press, June 1990.","DOI":"10.1109\/CSFW.1990.128181"},{"key":"11_CR5","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/0167-4048(90)90159-Q","volume":"19","author":"J. Burns","year":"1990","unstructured":"J. Burns and C. J. Mitchell. A Security Scheme for Resource Sharing Over a Network. Computers and Security, 19:67\u201376, February 1990.","journal-title":"Computers and Security"},{"issue":"1","key":"11_CR6","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1145\/77648.77649","volume":"8","author":"M. Burrows","year":"1990","unstructured":"Michael Burrows, Mart\u00edn Abadi, and Roger Needham. A Logic of Authentication. ACM Transactions in Computer Systems, 8(1):18\u201336, February 1990.","journal-title":"ACM Transactions in Computer Systems"},{"issue":"2","key":"11_CR7","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1145\/382258.382790","volume":"24","author":"M. Burrows","year":"1990","unstructured":"Michael Burrows, Mart\u00edn Abadi, and Roger Needham. Rejoinder to Nessett. Operating Systems Review, 24(2):39\u201340, April 1990.","journal-title":"Operating Systems Review"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"U. Carlsen. Generating Formal Cryptographic Protocol Specifications. In Proceedings of the 1994 IEEE Computer Society Symposium on Research in Security and Privacy, pages 137\u2013146. IEEE Computer Society Press, May 16\u201318 1994.","DOI":"10.1109\/RISP.1994.296586"},{"key":"11_CR9","unstructured":"CCITT. CCITT Draft Recomendation X.509. The Directory-Authentication Framework, Version 7, November 1987."},{"issue":"8","key":"11_CR10","first-page":"198","volume":"24","author":"D. E. Denning","year":"1981","unstructured":"D. E. Denning and G. M. Sacco. Timestamps in Key Distribution Protocols. Communications of the ACM, 24(8):198\u2013208, 1981.","journal-title":"Communications of the ACM"},{"key":"11_CR11","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/BF00124891","volume":"2","author":"W. Diffie","year":"1992","unstructured":"Whitfield Diffie, Paul C. van Oorschot, and Michael J. Wiener. Authentication and Authenticated Key Exchanges. Designs, Codes, and Cryptography, 2:107\u2013125, 1992.","journal-title":"Designs, Codes, and Cryptography"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"D. Dolev, S. Even, and R. Karp. On the Security of Ping-Pong Protocols. Information and Control, pages 57\u201368, 1982.","DOI":"10.1016\/S0019-9958(82)90401-6"},{"issue":"2","key":"11_CR13","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D. Dolev","year":"1983","unstructured":"D. Dolev and A. Yao. On the Security of Public Key Protocols. IEEE Transactions on Information Theory, 29(2):198\u2013208, March 1983.","journal-title":"IEEE Transactions on Information Theory"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Shimon Even, Oded Goldreich, and Adi Shamir. On the Security of Ping-Pong Protocols When Implemented Using the RSA. In Hugh C. Williams, editor, Advances in Cryptology \u2014 CRYPTO '85, pages 58\u201372. Springer-Verlag, 1985.","DOI":"10.1007\/3-540-39799-X_7"},{"key":"11_CR15","unstructured":"Joan Feigenbaum. Overview of Interactive Proof Systems and Zero Knowledge. In G. J. Simmons, editor, Contemperary Cryptology: The Science of Information Integrity, chapter 8, pages 423\u2013439. IEEE Press, 1991."},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"L. Gong, R. Needham, and R. Yahalom. Reasoning about belief in cryptographic protocols. In IEEE Computer Society Symposiun in Security and Privacy, pages 234\u2013248. IEEE Computer Society Press, May 1990.","DOI":"10.1109\/RISP.1990.63854"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Nevin Heintze and J. D. Tygar. A Model for Secure Protocols and Their Compositions. In 1994 IEEE Computer Society Symposium on Research in Security and Privacy, pages 2\u201313. IEEE Computer Society Press, May 1994.","DOI":"10.1109\/RISP.1994.296596"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"R. Kailar, V. D. Gligor, and L. Gong. On the Security Effectiveness of Cryptographic Protocols. In Proceedings of the Fourth Internation Working Conference on Dependable Computing For Critical Applications, 1994. to appear.","DOI":"10.1007\/978-3-7091-9396-9_12"},{"issue":"4","key":"11_CR19","doi-asserted-by":"crossref","first-page":"448","DOI":"10.1109\/49.17707","volume":"7","author":"R. Kemmerer","year":"1989","unstructured":"Richard Kemmerer. Using Formal Methods to Analyze Encryption Protocols. IEEE Journal on Selected Areas in Communication, 7(4):448\u2013457, 1989.","journal-title":"IEEE Journal on Selected Areas in Communication"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Richard Kemmerer, Catherine Meadows, and Jonathan Millen. Three Systems for Cryptographic Protocol Analysis. Journal of Cryptology, 7(2), 1994.","DOI":"10.1007\/BF00197942"},{"issue":"5","key":"11_CR21","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1145\/74851.74853","volume":"23","author":"T. M. A. Lomas","year":"1989","unstructured":"T. M. A. Lomas, L. Gong, J. H. Saltzer, and R. H. Needham. Reducing Risks From Poorly Chosen Keys. Operating Systems Reviews, 23(5):14\u201318, 1989.","journal-title":"Operating Systems Reviews"},{"issue":"1","key":"11_CR22","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/0167-4048(92)90222-D","volume":"11","author":"D. Longley","year":"1992","unstructured":"D. Longley and S. Rigby. An Automatic Search for Security Flaws in Key Management Schemes. Computers and Security, 11(1):75\u201390, 1992.","journal-title":"Computers and Security"},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"C. Meadows. Representing Partial Knowledge in an Algebraic Security Model. In Proceedings of the Computer Security Foundations Workshop III, pages 23\u201331. IEEE Computer Society Press, June 1990.","DOI":"10.1109\/CSFW.1990.128182"},{"key":"11_CR24","first-page":"182","volume-title":"A System for the Specification and Analysis of Key Management Protocols","author":"C. Meadows","year":"1991","unstructured":"C. Meadows. A System for the Specification and Analysis of Key Management Protocols. In Proceedings of the 1991 IEEE Computer Society Symposium on Research in Security and Privacy, pages 182\u2013195. IEEE Computer Society Press, Los Alamitos, California, 1991."},{"key":"11_CR25","doi-asserted-by":"crossref","first-page":"5","DOI":"10.3233\/JCS-1992-1102","volume":"1","author":"C. Meadows","year":"1992","unstructured":"C. Meadows. Applying Formal Methods to the Analysis of a Key Management Protocol. Journal of Computer Security, 1:5\u201353, 1992.","journal-title":"Journal of Computer Security"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"C. Meadows. A Model of Computation for the NRL Protocol Analyzer. In Proceedings of the 7th Computer Security Foundations Workshop. IEEE Computer Society Press, June 1994.","DOI":"10.1109\/CSFW.1994.315945"},{"key":"11_CR27","unstructured":"M. J. Merritt. Cryptographic Protocols. Ph.d. thesis, Georgia Institute of Technology, 1983."},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"J. K. Millen, S. C. Clark, and S. B. Freedman. The Interrogator: Protocol Security Analysis. IEEE Transactions on Software Engineering, SE-13(2), 1987.","DOI":"10.1109\/TSE.1987.233151"},{"key":"11_CR29","doi-asserted-by":"crossref","unstructured":"L. Moser. A Logic of Knowledge and Belief for Reasoning About Computer Security. In Proceedings of the Computer Security Foundations Workshop II, pages 57\u201363. IEEE Computer Society Press, June 1989.","DOI":"10.1109\/CSFW.1989.40587"},{"issue":"12","key":"11_CR30","doi-asserted-by":"crossref","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"R. M. Needham","year":"1978","unstructured":"R. M. Needham and M. D. Schroeder. Using Encryption for Authentication in Large Networks of Computers. Communications of the ACM, 21(12):993\u2013999, December 1978.","journal-title":"Communications of the ACM"},{"issue":"2","key":"11_CR31","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1145\/382258.382789","volume":"24","author":"D. M. Nessett","year":"1990","unstructured":"D. M. Nessett. A Critique of the Burrows, Abadi, and Needham Logic. Operating Systems Review, 24(2):35\u201338, April 1990.","journal-title":"Operating Systems Review"},{"key":"11_CR32","doi-asserted-by":"crossref","unstructured":"Birgit Pfitzmann. Sorting Out Signature Schemes. In Proceedings of the First ACM Conference on Computer and Communications Security, pages 74\u201385. ACM SIGSAC, ACM, November 3\u20135 1993.","DOI":"10.1145\/168588.168597"},{"key":"11_CR33","doi-asserted-by":"crossref","unstructured":"G. B. Purdy, G. J. Simmons, and J. A. Studier. A Software Protection Scheme. In Proceedings of the 1982 Symposium on Security and Privacy, pages 99\u2013103. IEEE Computer Society Press, April 1982.","DOI":"10.1109\/SP.1982.10012"},{"key":"11_CR34","doi-asserted-by":"crossref","unstructured":"P. V. Rangan. An Axiomatic Basis of Trust in Distributed Systems. In Proceedings of the 1988 Symposium on Security and Privacy, pages 204\u2013211. IEEE Computer Society Press, April 1988.","DOI":"10.1109\/SECPRI.1988.8112"},{"key":"11_CR35","doi-asserted-by":"crossref","unstructured":"G. J. Simmons. How to (Selectively) Broadcast a Secret. In Proceedings of the 1985 Symposium on Security and Privac, pages 108\u2013113. IEEE Computer Society Press, April 1985.","DOI":"10.1109\/SP.1985.10006"},{"key":"11_CR36","doi-asserted-by":"crossref","unstructured":"S. Stubblebine and V. Gligor. On Message Integrity in Cryptographic Protocols. In Proceedings of the 1992 Symposium on Security and Privacy, pages 85\u2013104. IEEE Computer Society Press, May 1992.","DOI":"10.1109\/RISP.1992.213268"},{"key":"11_CR37","unstructured":"S. Stubblebine and V. Gligor. Protecting the Integrity of Privacy-Enhanced Mail. In PSRG Workshop on Network and Distributed System Security, pages 75\u201380, February 11\u201312 1993."},{"key":"11_CR38","doi-asserted-by":"crossref","unstructured":"P. Syverson. Formal Semantics for Logics of Cryptographic Protocols. In Proceedings of the Computer Security Foundations Workshop III, pages 32\u201341. IEEE Computer Society Press, June 1990.","DOI":"10.1109\/CSFW.1990.128183"},{"key":"11_CR39","doi-asserted-by":"crossref","unstructured":"Paul Syverson. Adding Time to a Logic of Authentication. In Proceedings of the First ACM Conference on Computer and Communications Security, pages 97\u2013101. ACM SIGSAC, ACM, November 3\u20135 1993.","DOI":"10.1145\/168588.168600"},{"key":"11_CR40","doi-asserted-by":"crossref","first-page":"165","DOI":"10.21236\/ADA463014","volume-title":"A Logical Language for Specifying Cryptographic Protocol Requirements","author":"P. Syverson","year":"1993","unstructured":"Paul Syverson and Catherine Meadows. A Logical Language for Specifying Cryptographic Protocol Requirements. In Proceedings of the 1993 IEEE Computer Society Symposium on Research in Security and Privacy, pages 165\u2013177. IEEE Computer Society Press, Los Alamitos, California, 1993."},{"key":"11_CR41","doi-asserted-by":"crossref","unstructured":"Paul Syverson and Catherine Meadows. Formal Requirements for Key Distribution Protocols. In Proceedings of Eurocrypt '94, 1994. to appear.","DOI":"10.21236\/ADA463018"},{"issue":"3","key":"11_CR42","doi-asserted-by":"crossref","first-page":"317","DOI":"10.3233\/JCS-1992-13-407","volume":"1","author":"P. F. Syverson","year":"1992","unstructured":"Paul F. Syverson. Knowledge, Belief, and Semantics in the Analysis of Cryptographic Protocols. Journal of Computer Security, 1(3):317\u2013334, 1992.","journal-title":"Journal of Computer Security"},{"key":"11_CR43","doi-asserted-by":"crossref","unstructured":"Paul F. Syverson and Paul C. van Oorschot. On Unifying Some Cryptographic Protocol Logics. In 1994 IEEE Computer Society Symposium on Research in Security and Privacy, pages 14\u201328. IEEE Computer Society, May 1994.","DOI":"10.1109\/RISP.1994.296595"},{"key":"11_CR44","volume-title":"Ph.d. thesis","author":"M.-J. Toussaint","year":"1991","unstructured":"M.-J. Toussaint. Verification of Cryptographic Protocols. Ph.d. thesis, Universite de Liege (Belgium), 1991."},{"key":"11_CR45","doi-asserted-by":"crossref","unstructured":"M.-J. Toussaint. Deriving the Complete Knowledge of Participants in Cryptographic Protocols. In CRYPTO '91 (Advances in Cryptology\u2014 CRYPTO '91). Springer-Verlag, 1992.","DOI":"10.1007\/3-540-46766-1_2"},{"key":"11_CR46","doi-asserted-by":"crossref","unstructured":"M.-J. Toussaint. Separating the Specification and Implementation. Phases in Cryptology. In Computer Security \u2014 ESORICS 92, volume LMCS 638, pages 77\u2013102. Springer-Verlag, 1992.","DOI":"10.1007\/BFb0013893"},{"key":"11_CR47","doi-asserted-by":"crossref","unstructured":"T. Y. C. Woo and S. Lam. A Semantic Model for Authentication Protocols. In Proceedings of the 1993 Symposium on Research in Security and Privacy, pages 178\u2013194. IEEE Computer Society Press, May 1993.","DOI":"10.1109\/RISP.1993.287633"},{"issue":"2\u20133","key":"11_CR48","first-page":"191","volume":"2","author":"R. Yahalom","year":"1994","unstructured":"R. Yahalom. Optimality of Asynchronous Two-Party Secure Data-Exchange Protocols. Journal of Computer Security, 2(2\u20133):191\u2013209, 1994.","journal-title":"Journal of Computer Security"},{"key":"11_CR49","doi-asserted-by":"crossref","unstructured":"R. Yahalom, Birgit Klein, and Thomas Beth. Trust relationships in secure systems: A distributed authentication perspective. In Proceedings of the 1993 IEEE Symposium on Security and Privacy, pages 150\u2013164. IEEE Computer Society Press, May 1993.","DOI":"10.1109\/RISP.1993.287635"}],"container-title":["Lecture Notes in Computer Science","Advances in Cryptology \u2014 ASIACRYPT'94"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0000430","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,10]],"date-time":"2020-04-10T06:17:49Z","timestamp":1586499469000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0000430"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540593393","9783540492368"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/bfb0000430","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}