{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:08:36Z","timestamp":1725548916155},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540236351"},{"type":"electronic","value":"9783540376217"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-37621-7_1","type":"book-chapter","created":{"date-parts":[[2010,2,28]],"date-time":"2010-02-28T19:29:47Z","timestamp":1267385387000},"page":"1-24","source":"Crossref","is-referenced-by-count":4,"title":["Verifying Confidentiality and Authentication in Kerberos\u00a05"],"prefix":"10.1007","author":[{"given":"Frederick","family":"Butler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Iliano","family":"Cervesato","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aaron D.","family":"Jaggard","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andre","family":"Scedrov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Kohl, J., Neuman, C.: The Kerberos Network Authentication Service (V5) (1993) Network Working Group Request for Comments: 1510","DOI":"10.17487\/rfc1510"},{"key":"1_CR2","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1109\/35.312841","volume":"32","author":"B.C. Neuman","year":"1994","unstructured":"Neuman, B.C., Ts\u2019o, T.: Kerberos: An Authentication Service for Computer Networks. IEEE Communications\u00a032, 33\u201338 (1994)","journal-title":"IEEE Communications"},{"key":"1_CR3","unstructured":"Neuman, C., Kohl, J., Ts\u2019o, T., Raeburn, K., Yu, T.: The Kerberos Network Authentication Service (V5) (2001) Internet draft (expires May 20, 2002)"},{"key":"1_CR4","first-page":"175","volume-title":"Proceedings of the 15th Computer Security Foundations Workshop","author":"F. Butler","year":"2002","unstructured":"Butler, F., Cervesato, I., Jaggard, A.D., Scedrov, A.: A Formal Analysis of Some Properties of Kerberos 5 Using MSR. In: Proceedings of the 15th Computer Security Foundations Workshop, pp. 175\u2013190. IEEE Computer Society Press, Los Alamitos (2002)"},{"key":"1_CR5","unstructured":"Butler, F., Cervesato, I., Jaggard, A.D., Scedrov, A.: A formal analysis of some properties of kerberos 5 using MSR. Technical Report CIS-MS-04-04, University of Pennsylvania, Department of Computer and Information Science, p. 59 (2004), Available from: ftp:\/\/ftp.cis.upenn.edu\/pub\/papers\/scedrov\/ms-cis-04-04.pdf\/ps"},{"key":"1_CR6","first-page":"1337","volume":"3","author":"G. Bella","year":"1997","unstructured":"Bella, G., Riccobene, E.: Formal Analysis of the Kerberos Authentication System. J. Universal Comp. Sci.\u00a03, 1337\u20131381 (1997)","journal-title":"J. Universal Comp. Sci."},{"key":"1_CR7","unstructured":"Bella, G.: Inductive Verification of Cryptographic Protocols. PhD thesis, University of Cambridge (2000)"},{"key":"1_CR8","unstructured":"Bella, G., Paulson, L.C.: Using Isabelle to Prove Properties of the Kerberos Authentication System. In: Orman, H., Meadows, C. (eds.) Proc. of DIMACS 1997, Workshop on Design and Formal Verification of Security Protocols (CD-ROM) (1997)"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/BFb0055875","volume-title":"Computer Security \u2013 ESORICS 98","author":"G. Bella","year":"1998","unstructured":"Bella, G., Paulson, L.C.: Kerberos Version IV: Inductive Analysis of the Secrecy Goals. In: Quisquater, J.-J., Deswarte, Y., Meadows, C., Gollmann, D. (eds.) ESORICS 1998. LNCS, vol.\u00a01485, pp. 361\u2013375. Springer, Heidelberg (1998)"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028763","volume-title":"Computer Aided Verification","author":"G. Bella","year":"1998","unstructured":"Bella, G., Paulson, L.C.: Mechanising BAN Kerberos by the Inductive Method. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427. Springer, Heidelberg (1998)"},{"key":"1_CR11","first-page":"141","volume-title":"Proc. of the IEEE Symposium on Security and Privacy","author":"J.C. Mitchell","year":"1997","unstructured":"Mitchell, J.C., Mitchell, M., Stern, U.: Automated Analysis of Cryptographic Protocols Using Mur\u03d5. In: Proc. of the IEEE Symposium on Security and Privacy, pp. 141\u2013153. IEEE Computer Society Press, Los Alamitos (1997)"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Cervesato, I., Durgin, N.A., Lincoln, P., Mitchell, J., Scedrov, A.: A Meta-notation for Protocol Analysis. In: Proc. of the Twelfth IEEE Computer Security Foundations Workshop, pp. 55\u201369 (1999)","DOI":"10.1109\/CSFW.1999.779762"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Cervesato, I.: Typed Multiset Rewriting Specifications of Security Protocols. In: Proc. of the First Irish Conference on the Mathematical Foundations of Computer Science and Information Technology\u2013MFCSIT 2000. Elsevier ENTCS 40 (2000)","DOI":"10.1016\/S1571-0661(05)80035-0"},{"key":"1_CR14","volume-title":"Proc. of the First International Workshop on Mathematical Methods, Models and Architectures for Computer Network Security \u2014 MMM 2001","author":"I. Cervesato","year":"2001","unstructured":"Cervesato, I.: Typed MSR: Syntax and Examples. In: Proc. of the First International Workshop on Mathematical Methods, Models and Architectures for Computer Network Security \u2014 MMM 2001. Springer, Heidelberg (2001), St. Petersburg, Russia, 21\u201323 May 2001"},{"key":"1_CR15","unstructured":"Durgin, N.A., Lincoln, P.D., Mitchell, J.C., Scedrov, A.: Multiset Rewriting and the Complexity of Bounded Security Protocols, pages 63 (2002) (manuscript)"},{"key":"1_CR16","doi-asserted-by":"publisher","first-page":"741","DOI":"10.1109\/32.713329","volume":"24","author":"S. Schneider","year":"1998","unstructured":"Schneider, S.: Verifying Authentication Protocols in CSP. IEEE Transactions on Software Engineering\u00a024, 741\u2013758 (1998)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"1_CR17","unstructured":"Neuman, C.: Personal communication (2002)"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Neuman, C., Yu, T., Hartman, S., Raeburn, K.: The Kerberos Network Authentication Service (V5) (2004) Internet draft (expires August 15, 2004), http:\/\/www.ietf.org\/internet-drafts\/draft-ietf-krb-wg-kerberos-clarifications-05.txt","DOI":"10.17487\/rfc4120"},{"key":"1_CR19","unstructured":"Jeffrey, A.: Personal communication (2002)"},{"key":"1_CR20","unstructured":"Raeburn, K.: Personal communication (2002)"}],"container-title":["Lecture Notes in Computer Science","Software Security - Theories and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-37621-7_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:40:50Z","timestamp":1605742850000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-37621-7_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540236351","9783540376217"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-37621-7_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}