{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:35Z","timestamp":1761611135197},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1994,6,1]],"date-time":"1994-06-01T00:00:00Z","timestamp":770428800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J. Cryptology"],"published-print":{"date-parts":[[1994,6]]},"DOI":"10.1007\/bf00197942","type":"journal-article","created":{"date-parts":[[2004,8,28]],"date-time":"2004-08-28T23:10:30Z","timestamp":1093734630000},"page":"79-130","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":142,"title":["Three systems for cryptographic protocol analysis"],"prefix":"10.1007","volume":"7","author":[{"given":"R.","family":"Kemmerer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C.","family":"Meadows","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J.","family":"Millen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"BF00197942_CR1","first-page":"201","volume-title":"Proceedings of the 10th Annual ACM Symposium on Distributed Computing","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., and M. R. Tuttle, A Semantics for a Logic of Authentication, Proceedings of the 10th Annual ACM Symposium on Distributed Computing, ACM Press, New York, August 1991, pp. 201\u2013206."},{"key":"BF00197942_CR2","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1109\/CSFW.1990.128181","volume-title":"Proceedings of the Computer Security Foundations Workshop III","author":"P. Bieber","year":"1990","unstructured":"Bieber, P., A Logic of Communication in a Hostile Environment, Proceedings of the Computer Security Foundations Workshop III, IEEE Computer Society Press, New York, June 1990, pp. 14\u201322."},{"key":"BF00197942_CR3","doi-asserted-by":"crossref","first-page":"292","DOI":"10.1007\/3-540-52885-7_95","volume-title":"Proceedings of the 10th International Conference on Automated Deduction","author":"A. Boudet","year":"1990","unstructured":"Boudet, A., Unification in a Combination of Equational Theories: an Efficient Algorithm, Proceedings of the 10th International Conference on Automated Deduction, Springer-Verlag, New York, 1990, pp. 292\u2013307."},{"key":"BF00197942_CR4","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/0167-4048(90)90159-Q","volume":"Vol. 9","author":"J. Burns","year":"1990","unstructured":"Burns, J., and C. J. Mitchell, A Security Scheme for Resource Sharing Over a Network, Comput. Security, Vol. 9, 1990, pp. 67\u201376.","journal-title":"Comput. Security"},{"issue":"No. 1","key":"BF00197942_CR5","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1145\/77648.77649","volume":"Vol. 8","author":"M. Burrows","year":"1990","unstructured":"Burrows, M., M. Abadi, and R. M. Needham, A Logic of Authentication, ACM Trans. Comput. Systems, Vol. 8, No. 1, February 1990, pp. 18\u201336.","journal-title":"ACM Trans. Comput. Systems"},{"key":"BF00197942_CR6","volume-title":"Programming in Prolog","author":"W. F. Clocksin","year":"1984","unstructured":"Clocksin, W. F., and C. S. Mellish, Programming in Prolog, Springer-Verlag, New York, 1984."},{"issue":"No. 8","key":"BF00197942_CR7","doi-asserted-by":"crossref","first-page":"533","DOI":"10.1145\/358722.358740","volume":"Vol. 24","author":"D. E. Denning","year":"1981","unstructured":"Denning, D. E., and G. M. Sacco, Timestamps in Key Distribution Protocols, Comm. ACM, Vol. 24, No. 8, August 1981, pp. 533\u2013536.","journal-title":"Comm. ACM"},{"key":"BF00197942_CR8","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"Vol. 29","author":"D. Dolev","year":"1983","unstructured":"Dolev, D., and A. Yao, On the Security of Public-Key Protocols, IEEE Trans. Inform. Theory, Vol. 29, 1983, pp. 198\u2013203.","journal-title":"IEEE Trans. Inform. Theory"},{"key":"BF00197942_CR9","doi-asserted-by":"crossref","unstructured":"Eckmann, S. T., and R. A. Kemmerer, INATEST: An Interactive Environment for Testing Formal Specifications, Third Workshop on Formal Verification, Pajaro Dunes, CA, February, 1985, ACM\u2014Software Engrg Notes, Vol. 10, No. 4, August 1985, pp. 17\u201318.","DOI":"10.1145\/1012497.1012504"},{"issue":"No. 1","key":"BF00197942_CR10","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1137\/0218012","volume":"Vol. 18","author":"S. Goldwasser","year":"1989","unstructured":"Goldwasser, S., S. Micali, and C. Rackoff, The Knowledge Complexity of Interactive Proof Systems, Siam J. Comput., Vol. 18, No. 1, February 1989, pp. 186\u2013208.","journal-title":"Siam J. Comput."},{"key":"BF00197942_CR11","volume-title":"The Design and Validation of Computer Protocols","author":"G. Holzmann","year":"1991","unstructured":"Holzmann, G., The Design and Validation of Computer Protocols, Prentice-Hall, Englewood Cliffs, NJ, 1991."},{"issue":"No. 4","key":"BF00197942_CR12","doi-asserted-by":"crossref","first-page":"448","DOI":"10.1109\/49.17707","volume":"Vol. 7","author":"R. A. Kemmerer","year":"1989","unstructured":"Kemmerer, R. A., Analyzing Encryption Protocols Using Formal Verification Techniques, IEEE J. Selected Areas Commun., Vol. 7, No. 4, May 1989, pp. 448\u2013457.","journal-title":"IEEE J. Selected Areas Commun."},{"key":"BF00197942_CR13","doi-asserted-by":"crossref","unstructured":"Kemmerer, R. A., Integrating Formal Methods into the Development Process, IEEE Software, September 1990, pp. 37\u201350.","DOI":"10.1109\/52.57891"},{"key":"BF00197942_CR14","series-title":"UCSB Report No. TRCS91-05","volume-title":"Analyzing the Tatebayashi-Matsuzaki-Newman Protocol Using Inatest","author":"R. A. Kemmerer","year":"1991","unstructured":"Kemmerer, R. A., Analyzing the Tatebayashi-Matsuzaki-Newman Protocol Using Inatest, UCSB Report No. TRCS91\u201305, Computer Science Department, University of California, Santa Barbara, CA, April 1991."},{"key":"BF00197942_CR15","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1016\/0167-4048(87)90126-X","volume":"Vol. 6","author":"D. Longley","year":"1987","unstructured":"Longley, D., Expert Systems Applied to the Analysis of Key Management Schemes, Comput. Security, Vol. 6, 1987, pp. 54\u201367.","journal-title":"Comput. Security"},{"key":"BF00197942_CR16","volume-title":"Proceedings of the Workshop on Mathematical Concepts of Dependable Systems","author":"J. L. Massey","year":"1990","unstructured":"Massey, J. L., Cryptography and Provability, Proceedings of the Workshop on Mathematical Concepts of Dependable Systems, Mathematisches Forschunginstitut Oberwolfach, Oberwolfach, April 1990."},{"key":"BF00197942_CR17","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1109\/RISP.1991.130786","volume-title":"Proceedings of the 1991 IEEE Symposium on Security and Privacy","author":"C. Meadows","year":"1991","unstructured":"Meadows, C., A System for the Specification and Verification of Key Management Protocols, Proceedings of the 1991 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, New York, 1991, pp. 182\u2013195."},{"issue":"No. 1","key":"BF00197942_CR18","doi-asserted-by":"crossref","first-page":"5","DOI":"10.3233\/JCS-1992-1102","volume":"Vol. 1","author":"C. Meadows","year":"1992","unstructured":"Meadows, C., Applying Formal Methods to the Analysis of a Key Management Protocol, J. Comput. Security, Vol. 1, No. 1, 1992, pp. 5\u201353.","journal-title":"J. Comput. Security"},{"key":"BF00197942_CR19","unstructured":"Merritt, M., and P. Wolper, States of Knowledge in Cryptographic Protocols, unpublished manuscript, 1985."},{"key":"BF00197942_CR20","doi-asserted-by":"crossref","unstructured":"Millen, J. K., The Interrogator: A Tool for Cryptographic Protocol Security, Proceedings of the 1984 Symposium on Security and Privacy, IEEE Computer Society Press, New York, pp. 134\u2013141.","DOI":"10.1109\/SP.1984.10003"},{"key":"BF00197942_CR21","doi-asserted-by":"crossref","unstructured":"Millen, J. K., S. C. Clark, and S. B. Freedman, The Interrogator: Protocol Security Analysis, IEEE Trans. Software Engrg., Vol. 13, No. 2, February 1987.","DOI":"10.1109\/TSE.1987.233151"},{"issue":"No. 5","key":"BF00197942_CR22","doi-asserted-by":"crossref","first-page":"564","DOI":"10.1109\/5.4444","volume":"Vol. 76","author":"J. H. Moore","year":"1988","unstructured":"Moore, J. H., Protocol Failures in Cryptosystems, Proc. IEEE, Vol. 76, No. 5, May 1988, pp. 564\u2013602.","journal-title":"Proc. IEEE"},{"issue":"No. 12","key":"BF00197942_CR23","doi-asserted-by":"crossref","first-page":"993","DOI":"10.1145\/359657.359659","volume":"Vol. 21","author":"R. M. Needham","year":"1978","unstructured":"Needham, R. M., and M. D. Schroeder, Using Encryption for Authentication in Large Networks of Computers, Comm. ACM, Vol. 21, No. 12, December 1978, pp. 993\u2013999.","journal-title":"Comm. ACM"},{"key":"BF00197942_CR24","doi-asserted-by":"crossref","unstructured":"Rety, P., C. Kirchner, H. Kirchner, and P. Lescanne, NARROWER: A New Algorithm for Unification and Its Applications to Logic Programming, in Rewriting Techniques and Applications, Lecture Notes in Computer Science, Vol. 202, Jean-Pierre Jouannaud, ed., Springer-Verlag, Berlin, 1985, pp. 141\u2013157.","DOI":"10.1007\/3-540-15976-2_7"},{"key":"BF00197942_CR25","series-title":"TM-6021","volume-title":"Ina Jo Specification Language Reference Manual","author":"J. Scheid","year":"1989","unstructured":"Scheid, J., and S. Holtsberg, Ina Jo Specification Language Reference Manual, TM-6021, Unisys Corporation, Culver City, CA, May 1989."},{"key":"BF00197942_CR26","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1109\/SP.1985.10006","volume-title":"Proceedings of the 1985 IEEE Symposium on Security and Privacy","author":"G. J. Simmons","year":"1985","unstructured":"Simmons, G. J., How To (Selectively) Broadcast a Secret, Proceedings of the 1985 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, New York, 1985, pp. 108\u2013113."},{"key":"BF00197942_CR27","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1109\/RISP.1993.287634","volume-title":"Proceedings of the 1993 IEEE Computer Society Symposium on Security and Privacy","author":"P. Syverson","year":"1993","unstructured":"Syverson, P. and Meadows, C., A Logical Language for Specifying Cryptographic Protocol Requirements, in Proceedings of the 1993 IEEE Computer Society Symposium on Security and Privacy, IEEE Computer Society Press, New York, 1993, pp. 165\u2013177."},{"key":"BF00197942_CR28","doi-asserted-by":"crossref","unstructured":"Tatebayashi, M., N. Matsuzaki, and D. B. Newman, Key Distribution Protocol for Digital Mobile Communication Systems, in Advances in Cryptology\u2014CRYPTO '89, Lecture Notes in Computer Science, Vol. 435, G. Brassard, ed., Springer-Verlag, New York, 1991, pp. 324\u2013333.","DOI":"10.1007\/0-387-34805-0_30"},{"key":"BF00197942_CR29","doi-asserted-by":"crossref","unstructured":"Toussaint, M.-J., Separating the Specification and Implementation Phases in Cryptology (Extended Abstract), Computer Security, ESORICS 92, Lecture Notes in Computer Science, Vol. 648, Springer-Verlag, Berlin, 1992, pp. 77\u2013101.","DOI":"10.1007\/BFb0013893"}],"container-title":["Journal of Cryptology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00197942.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00197942\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00197942","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00197942.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,8]],"date-time":"2020-04-08T08:25:04Z","timestamp":1586334304000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00197942"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,6]]},"references-count":29,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1994,6]]}},"alternative-id":["BF00197942"],"URL":"https:\/\/doi.org\/10.1007\/bf00197942","relation":{},"ISSN":["0933-2790","1432-1378"],"issn-type":[{"value":"0933-2790","type":"print"},{"value":"1432-1378","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994,6]]},"assertion":[{"value":"25 March 1992","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 August 1993","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}