{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T23:14:37Z","timestamp":1768518877412,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540646082","type":"print"},{"value":"9783540693390","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0028763","type":"book-chapter","created":{"date-parts":[[2005,12,1]],"date-time":"2005-12-01T06:48:09Z","timestamp":1133419689000},"page":"416-427","source":"Crossref","is-referenced-by-count":9,"title":["Mechanising BAN Kerberos by the inductive method"],"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":[[2005,6,18]]},"reference":[{"key":"38_CR1","unstructured":"G. Bella, L. C. Paulson. Using Isabelle to Prove Properties of the Kerberos Authentication System. In Proc. of Workshop on Design and Formal Verification of Security Protocols, Orman and Meadows (eds.), DIMACS, 1997."},{"issue":"5","key":"38_CR2","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. Merritt. Limitations of the Kerberos authentication system. Computer Comm. Review, 20(5), 119\u2013132, 1990.","journal-title":"Computer Comm. Review"},{"key":"38_CR3","doi-asserted-by":"crossref","unstructured":"D. Bolignano. Towards a Mechanization of Cryptographic Protocol Verification. In Proc. of Conference on Computer Aided Verification, Springer Verlag, 1997.","DOI":"10.1007\/3-540-63166-6_15"},{"key":"38_CR4","doi-asserted-by":"crossref","unstructured":"S. H. Brackin. A HOL Extension of GNY for Automatically Analyzing Cryptographic Protocols. In Proc. of Computer Security Foundations Workshop, IEEE Press, 1996.","DOI":"10.1109\/CSFW.1996.503691"},{"key":"38_CR5","doi-asserted-by":"crossref","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":"38_CR6","doi-asserted-by":"crossref","unstructured":"G. Lowe. Breaking and Fixing the Needham-Schroeder Pubfic-Key Protocol using FDR. In 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":"38_CR7","unstructured":"G. Lowe. Casper: a Compiler for the Analysis of Security Protocols. Oxford University, Computing Laboratory, Technical Report, 1996."},{"issue":"2","key":"38_CR8","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":"38_CR9","unstructured":"J. C. Mitchell, M. Mitchell, U. Stern: Automated Analysis of Cryptographic Protocols Using Murphi. In Proc. of Symposium on Security and Privacy, IEEE Press, 1997."},{"issue":"12","key":"38_CR10","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"R. M. Needham","year":"1978","unstructured":"R. M. Needham, M. Schroeder. Using encryption for authentication in large networks of computers. Communications of the ACM, 21(12), 993\u2013999, 1978.","journal-title":"Communications of the ACM"},{"key":"38_CR11","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Isabelle: A Generic Theorem Prover. Springer, 1994. LNCS 828.","DOI":"10.1007\/BFb0030541"},{"key":"38_CR12","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Proving properties of security protocols by induction. In Proc. of Computer Security Foundations Workshop, IEEE Press, 1997.","DOI":"10.1109\/CSFW.1997.596788"},{"key":"38_CR13","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Mechanized proofs for a recursive authentication protocol. In Proc. of Computer Security Foundations Workshop, IEEE Press, 1997.","DOI":"10.1109\/CSFW.1997.596790"},{"key":"38_CR14","unstructured":"L. C. Paulson. On Two Formal Analyses of the Yahalom Protocol. Cambridge University, Computer Laboratory, Technical Report No. 432, 1997."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0028763","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T08:24:01Z","timestamp":1586593441000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0028763"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646082","9783540693390"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/bfb0028763","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998]]}}}