{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,16]],"date-time":"2026-01-16T05:30:30Z","timestamp":1768541430316,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540650041","type":"print"},{"value":"9783540497844","type":"electronic"}],"license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"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":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055875","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T16:50:09Z","timestamp":1154019009000},"page":"361-375","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":59,"title":["Kerberos Version IV: Inductive analysis of the secrecy goals"],"prefix":"10.1007","author":[{"given":"Giampaolo","family":"Bella","sequence":"first","affiliation":[]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,28]]},"reference":[{"key":"24_CR1","unstructured":"G. Bella, L. C. Paulson. Using Isabelle to Prove Properties of the Kerberos Authentication System. Proc. of DIMACS Workshop on Design and Formal Verification of Security Protocols, Orman and Meadows (eds.), 1997."},{"key":"24_CR2","doi-asserted-by":"crossref","unstructured":"G. Bella, L. C. Paulson. Mechanising BAN Kerberos by the Inductive Method. Proc. of Conference on Computer Aided Verification, Springer, LNCS Series, 1998.","DOI":"10.1007\/BFb0028763"},{"key":"24_CR3","unstructured":"G. Bella, E. Riccobene. Formal Analysis of the Kerberos Authentication System. Journal of Universal Computer Science: Special Issue on Gurevich\u2019s Abstract State Machine, Springer, 1997."},{"issue":"5","key":"24_CR4","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1145\/381906.381946","volume":"20","author":"S. M. Bellovin","year":"1990","unstructured":"S. M. Bellovin, M. Meritt. Limitations of the Kerberos authentication system. Computer Comm. Review, 20(5) 119\u2013132, 1990.","journal-title":"Computer Comm. Review"},{"key":"24_CR5","unstructured":"S. H. Brackin. A HOL Extension of GNY for Automatically Analyzing Cryptographic Protocols. Proc. of Computer Security Foundations Workshop, IEEE Press, 1996."},{"key":"24_CR6","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1098\/rspa.1989.0125","volume":"426","author":"M. Burrows","year":"1989","unstructured":"M. Burrows, M. Abadi, R. M. Needham. A logic of authentication. Proceedings of the Royal Society of London, 426:233\u2013271, 1989.","journal-title":"Proceedings of the Royal Society of London"},{"key":"24_CR7","unstructured":"Y. Gurevich. Evolving Algebras 1993: Lipari Guide. In Specification and Validation Methods, Oxford University Press, E. B\u00f6rger (ed.), 1995."},{"issue":"2","key":"24_CR8","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/BF00197942","volume":"7","author":"R. Kemmerer","year":"1994","unstructured":"R. Kemmerer, C. Meadows, J. Millen. Three Systems for Cryptographic Protocol Analysis. Journal of Cryptology, 7(2), 79\u2013130, 1994.","journal-title":"Journal of Cryptology"},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"J. Kohl, B. Neuman. The Kerberos Network Authentication Service (Version V). Internet Request for Comment RFC-1510, 1993.","DOI":"10.17487\/rfc1510"},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"J. Kohl, B. Neuman, T. Ts\u2019o. The Evolution of the Kerberos Authentication Service. IEEE Press, 78\u201394, 1994.","DOI":"10.17487\/rfc1510"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"G. Lowe. Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR. Tools and Algorithms for the Construction and Analysis of Systems, Margaria and Steffen (eds.), LNCS1055, Springer Verlag, 147\u2013166, 1996.","DOI":"10.1007\/3-540-61042-1_43"},{"key":"24_CR12","unstructured":"G. Lowe. Casper: a Compiler for the Analysis of Security Protocols. Oxford University, Computing Laboratory, Technical Report, 1996."},{"issue":"2","key":"24_CR13","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"C. Meadows","year":"1996","unstructured":"C. Meadows. The NRL Protocol Analyzer: An Overview. Journal of Logic Programming, 26(2), 113\u2013131, 1996.","journal-title":"Journal of Logic Programming"},{"key":"24_CR14","unstructured":"S. P. Miller, J. I. Neuman, J. I. Schiller, J. H. Saltzer. Kerberos authentication and authorisation system. Project Athena Technical Plan, Sec. E.2.1, 1\u201336, MIT, 1989."},{"key":"24_CR15","unstructured":"J. C. Mitchell, M. Mitchell, U. Stern: Automated Analysis of Cryptographic Protocols Using Murphi. Proc. of IEEE Symposium on Security and Privacy, 141\u2013151, 1997."},{"key":"24_CR16","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Isabelle: A Generic Theorem Prover. Springer, 1994. LNCS 828.","DOI":"10.1007\/BFb0030541"},{"key":"24_CR17","unstructured":"L. C. Paulson. Proving properties of security protocols by induction. Proc. of Computer Security Foundations Workshop, IEEE Press, 1997."},{"key":"24_CR18","unstructured":"L. C. Paulson. On Two Formal Analyses of the Yahalom Protocol. Cambridge University, Computer Laboratory, Technical Report No. 432, July 1997."},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Inductive Analysis of the Internet Protocol TLS. Cambridge University, Computer Laboratory, Technical Report No. 440, Dec. 1997.","DOI":"10.1007\/3-540-49135-X_1"},{"key":"24_CR20","unstructured":"S. Schneider. Verifying Authentication Protocols Using CSP. Proc. of Computer Security Foundations Workshop, IEEE Press, 1997."}],"container-title":["Lecture Notes in Computer Science","Computer Security \u2014 ESORICS 98"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0055875","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,2]],"date-time":"2019-06-02T20:07:40Z","timestamp":1559506060000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055875"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540650041","9783540497844"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/bfb0055875","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998]]},"assertion":[{"value":"28 May 2006","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}