{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T05:09:19Z","timestamp":1742965759710,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540446019"},{"type":"electronic","value":"9783540446057"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11863908_23","type":"book-chapter","created":{"date-parts":[[2006,9,16]],"date-time":"2006-09-16T03:28:46Z","timestamp":1158377326000},"page":"362-383","source":"Crossref","is-referenced-by-count":19,"title":["Cryptographically Sound Security Proofs for Basic and Public-Key Kerberos"],"prefix":"10.1007","author":[{"given":"M.","family":"Backes","sequence":"first","affiliation":[]},{"given":"I.","family":"Cervesato","sequence":"additional","affiliation":[]},{"given":"A. D.","family":"Jaggard","sequence":"additional","affiliation":[]},{"given":"A.","family":"Scedrov","sequence":"additional","affiliation":[]},{"given":"J. -K.","family":"Tsay","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"23_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11513988_27","volume-title":"Computer Aided Verification","author":"A. Armando","year":"2005","unstructured":"Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Drielsma, P.H., He\u00e1m, P.C., Kouchnarenko, O., Mantovani, J., M\u00f6dersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Vigan\u00f2, L., Vigneron, L.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 281\u2013285. Springer, Heidelberg (2005)"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-45500-0_4","volume-title":"Theoretical Aspects of Computer Software","author":"M. Abadi","year":"2001","unstructured":"Abadi, M., J\u00fcrjens, J.: Formal eavesdropping and its computational interpretation. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol.\u00a02215, p. 82. Springer, Heidelberg (2001)"},{"key":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/3-540-44929-9_1","volume-title":"Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics","author":"M. Abadi","year":"2000","unstructured":"Abadi, M., Rogaway, P.: Reconciling two views of cryptography. In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol.\u00a01872, pp. 3\u201322. Springer, Heidelberg (2000)"},{"key":"23_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-540-30108-0_6","volume-title":"Computer Security \u2013 ESORICS 2004","author":"M. Backes","year":"2004","unstructured":"Backes, M.: A cryptographically sound dolev-yao style security proof of the otway-rees protocol. In: Samarati, P., Ryan, P.Y.A., Gollmann, D., Molva, R. (eds.) ESORICS 2004. LNCS, vol.\u00a03193, pp. 89\u2013108. Springer, Heidelberg (2004)"},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"Backes, M., Cervesato, I., Jaggard, A.D., Scedrov, A., Tsay, J.-K.: Cryptographically sound security proofs for basic and public-key Kerberos. IACR Cryptology ePrint Archive, Report 2006\/219 (June 2006), http:\/\/eprint.iacr.org\/","DOI":"10.1007\/11863908_23"},{"key":"23_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1007\/3-540-36494-3_59","volume-title":"STACS 2003","author":"M. Backes","year":"2003","unstructured":"Backes, M., Jacobi, C.: Cryptographically sound and machine-assisted verification of security protocols. In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol.\u00a02607, pp. 675\u2013686. Springer, Heidelberg (2003)"},{"issue":"10","key":"23_CR7","doi-asserted-by":"publisher","first-page":"2075","DOI":"10.1109\/JSAC.2004.836016","volume":"22","author":"M. Backes","year":"2004","unstructured":"Backes, M., Pfitzmann, B.: A cryptographically sound security proof of the Needham-Schroeder-Lowe public-key protocol. Journal on Selected Areas in Communications\u00a022(10), 2075\u20132086 (2004)","journal-title":"Journal on Selected Areas in Communications"},{"key":"23_CR8","doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B.: Symmetric encryption in a simulatable Dolev-Yao style cryptographic library. In: Proc. CSFW 2004, pp. 204\u2013218 (June 2004)","DOI":"10.1109\/CSFW.2004.1310742"},{"issue":"2","key":"23_CR9","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1109\/TDSC.2005.25","volume":"2","author":"M. Backes","year":"2005","unstructured":"Backes, M., Pfitzmann, B.: Relating symbolic and cryptographic secrecy. IEEE Trans. Dependable Secure Comp.\u00a02(2), 109\u2013123 (2005)","journal-title":"IEEE Trans. Dependable Secure Comp."},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B.: Relating symbolic and cryptographic secrecy. In: Proc. 26th IEEE Symposium on Security & Privacy, Extended version in IACR Cryptology ePrint Archive 2004\/300, pp. 171\u2013182 (2005)","DOI":"10.1109\/SP.2005.17"},{"key":"23_CR11","unstructured":"Backes, M., Pfitzmann, B.: On the cryptographic key secrecy of the stregthened Yahalom protocol. In: Proceedings of 21st IFIP SEC 2006 (to appear, 2006)"},{"key":"23_CR12","doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations (extended abstract). In: Proc. CCS 2003, pp. 220\u2013230 (2003)","DOI":"10.1145\/948109.948140"},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-540-39650-5_16","volume-title":"Computer Security \u2013 ESORICS 2003","author":"M. Backes","year":"2003","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: Symmetric authentication within a simulatable cryptographic library. In: Snekkenes, E., Gollmann, D. (eds.) ESORICS 2003. LNCS, vol.\u00a02808, pp. 271\u2013290. Springer, Heidelberg (2003)"},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: A universally composable cryptographic library. IACR Cryptology ePrint Archive, Report 2003\/015 (January 2003), http:\/\/eprint.iacr.org\/","DOI":"10.1145\/948109.948140"},{"key":"23_CR15","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":"23_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1007\/3-540-48329-2_21","volume-title":"Advances in Cryptology - CRYPTO \u201993","author":"M. Bellare","year":"1994","unstructured":"Bellare, M., Rogaway, P.: Entity authentication and key distribution. In: Stinson, D.R. (ed.) CRYPTO 1993. LNCS, vol.\u00a0773, pp. 232\u2013249. Springer, Heidelberg (1994)"},{"key":"23_CR17","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: A computationally sound mechanized prover for security protocols. In: Proc. 27th IEEE Symposium on Security & Privacy (2006)","DOI":"10.1109\/SP.2006.1"},{"key":"23_CR18","unstructured":"Butler, F., Cervesato, I., Jaggard, A.D., Scedrov, A.: An Analysis of Some Properties of Kerberos\u00a05 Using MSR. In: Proc. CSFW 2002 (2002)"},{"key":"23_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/11681878_20","volume-title":"Theory of Cryptography","author":"R. Canetti","year":"2006","unstructured":"Canetti, R., Herzog, J.C.: Universally composable symbolic analysis of mutual authentication and key-exchange protocols. In: Halevi, S., Rabin, T. (eds.) TCC 2006. LNCS, vol.\u00a03876, pp. 380\u2013403. Springer, Heidelberg (2006)"},{"key":"23_CR20","doi-asserted-by":"crossref","unstructured":"Cervesato, I., Jaggard, A.D., Scedrov, A., Tsay, J.-K., Walstad, C.: Breaking and fixing public-key Kerberos. In: Proc. WITS 2006 (2006)","DOI":"10.1007\/978-3-540-77505-8_13"},{"key":"23_CR21","doi-asserted-by":"crossref","unstructured":"Cervesato, I., Jaggard, A.D., Scedrov, A., Walstad, C.: Specifying Kerberos 5 Cross-Realm Authentication. In: Proc. WITS 2005, pp. 12\u201326 (2005)","DOI":"10.1145\/1045405.1045408"},{"key":"23_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-540-31987-0_12","volume-title":"Programming Languages and Systems","author":"V. Cortier","year":"2005","unstructured":"Cortier, V., Warinschi, B.: Computationally sound, automated proofs for security protocols. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 157\u2013171. Springer, Heidelberg (2005)"},{"key":"23_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/11523468_2","volume-title":"Automata, Languages and Programming","author":"A. Datta","year":"2005","unstructured":"Datta, A., Derek, A., Mitchell, J.C., Shmatikov, V., Turuani, M.: Probabilistic polynomial-time semantics for a protocol security logic. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol.\u00a03580, pp. 16\u201329. Springer, Heidelberg (2005)"},{"key":"23_CR24","volume-title":"19th IEEE Computer Security Foundations Workshop (CSFW 19)","author":"A. Datta","year":"2006","unstructured":"Datta, A., Derek, A., Mitchell, J., Warinschi, B.: Key exchange protocols: Security definition, proof method, and applications. In: 19th IEEE Computer Security Foundations Workshop (CSFW 19), Venice, Italy. IEEE Press, Los Alamitos (2006)"},{"issue":"29","key":"23_CR25","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"2","author":"D. Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.: On the security of public-key protocols. IEEE Trans. Info. Theory\u00a02(29), 198\u2013208 (1983)","journal-title":"IEEE Trans. Info. Theory"},{"key":"23_CR26","doi-asserted-by":"crossref","unstructured":"Goldreich, O., Micali, S., Wigderson, A.: How to play any mental game \u2013 or \u2013 a completeness theorem for protocols with honest majority. In: Proc. STOC, pp. 218\u2013229 (1987)","DOI":"10.1145\/28395.28420"},{"key":"23_CR27","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1016\/0022-0000(84)90070-9","volume":"28","author":"S. Goldwasser","year":"1984","unstructured":"Goldwasser, S., Micali, S.: Probabilistic encryption. Journal of Computer and System Sciences\u00a028, 270\u2013299 (1984)","journal-title":"Journal of Computer and System Sciences"},{"key":"23_CR28","doi-asserted-by":"crossref","unstructured":"Guttman, J.D., Thayer Fabrega, F.J., Zuck, L.: The faithfulness of abstract protocol analysis: Message authentication. In: Proc. CCS-8, pp. 186\u2013195 (2001)","DOI":"10.1145\/501983.502009"},{"key":"23_CR29","unstructured":"He, C., Mitchell, J.C.: Security Analysis and Improvements for IEEE 802.11i. In: Proc. NDSS 2005 (2005)"},{"key":"23_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"548","DOI":"10.1007\/978-3-540-45146-4_32","volume-title":"Advances in Cryptology - CRYPTO 2003","author":"J.C. Herzog","year":"2003","unstructured":"Herzog, J.C., Liskov, M., Micali, S.: Plaintext awareness via key registration. In: Boneh, D. (ed.) CRYPTO 2003. LNCS, vol.\u00a02729, pp. 548\u2013564. Springer, Heidelberg (2003)"},{"key":"23_CR31","unstructured":"IETF. Public Key Cryptography for Initial Authentication in Kerberos (1996\u20132006), Sequence of Internet drafts, available from: http:\/\/tools.ietf.org\/wg\/krb-wg\/draft-ietf-cat-kerberos-pk-init\/"},{"key":"23_CR32","doi-asserted-by":"crossref","unstructured":"Impagliazzo, R., Kapron, B.M.: Logics for reasoning about cryptographic constructions. In: Proc. FOCS, pp. 372\u2013381 (2003)","DOI":"10.1109\/SFCS.2003.1238211"},{"key":"23_CR33","doi-asserted-by":"crossref","unstructured":"Laud, P.: Symmetric encryption in automatic analyses for confidentiality against active adversaries. In: Proc. Symp. Security and Privacy, pp. 71\u201385 (2004)","DOI":"10.1109\/SECPRI.2004.1301316"},{"key":"23_CR34","doi-asserted-by":"crossref","unstructured":"Meadows, C.: Analysis of the internet key exchange protocol using the NRL Protocol Analyzer. In: Proc. IEEE Symp. Security and Privacy, pp. 216\u2013231 (1999)","DOI":"10.21236\/ADA465466"},{"key":"23_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-540-24638-1_8","volume-title":"Theory of Cryptography","author":"D. Micciancio","year":"2004","unstructured":"Micciancio, D., Warinschi, B.: Soundness of formal encryption in the presence of active adversaries. In: Naor, M. (ed.) TCC 2004. LNCS, vol.\u00a02951, pp. 133\u2013151. Springer, Heidelberg (2004)"},{"key":"23_CR36","unstructured":"Microsoft. Security Bulletin MS05-042 (August 2005), http:\/\/www.microsoft.com\/technet\/security\/bulletin\/MS05-042.mspx"},{"key":"23_CR37","first-page":"1","volume":"47","author":"J. Mitchell","year":"2001","unstructured":"Mitchell, J., Mitchell, M., Scedrov, A., Teague, V.: A probabilistic polynominal-time process calculus for analysis of cryptographic protocols (preliminary report). Electronic Notes in Theoretical Computer Science\u00a047, 1\u201331 (2001)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"9","key":"23_CR38","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1109\/35.312841","volume":"32","author":"C. Neuman","year":"1994","unstructured":"Neuman, C., Ts\u2019o, T.: Kerberos: An Authentication Service for Computer Networks. IEEE Communications\u00a032(9), 33\u201338 (1994)","journal-title":"IEEE Communications"},{"key":"23_CR39","doi-asserted-by":"crossref","unstructured":"Neuman, C., Yu, T., Hartman, S., Raeburn, K.: The Kerberos Network Authentication Service (V5) (July 2005), http:\/\/www.ietf.org\/rfc\/rfc4120.txt","DOI":"10.17487\/rfc4120"},{"key":"23_CR40","doi-asserted-by":"crossref","unstructured":"Pfitzmann, B., Waidner, M.: A model for asynchronous reactive systems and its application to secure message transmission. In: Proc. S&P, pp. 184\u2013200 (2001)","DOI":"10.1109\/SECPRI.2001.924298"}],"container-title":["Lecture Notes in Computer Science","Computer Security \u2013 ESORICS 2006"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11863908_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T21:47:36Z","timestamp":1736545656000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11863908_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540446019","9783540446057"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/11863908_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}