{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,20]],"date-time":"2026-05-20T22:09:09Z","timestamp":1779314949173,"version":"3.51.4"},"reference-count":61,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2011,4,20]],"date-time":"2011-04-20T00:00:00Z","timestamp":1303257600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Inf. Secur."],"published-print":{"date-parts":[[2011,6]]},"DOI":"10.1007\/s10207-011-0125-6","type":"journal-article","created":{"date-parts":[[2011,4,19]],"date-time":"2011-04-19T01:34:12Z","timestamp":1303176852000},"page":"107-134","source":"Crossref","is-referenced-by-count":7,"title":["Cryptographically sound security proofs for basic and public-key Kerberos"],"prefix":"10.1007","volume":"10","author":[{"given":"Michael","family":"Backes","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"}]},{"given":"Joe-Kai","family":"Tsay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,4,20]]},"reference":[{"key":"125_CR1","unstructured":"The AVISPA tool for the automated validation of internet security protocols and applications. In: Proceedings of the Computer-aided Verification (CAV). Springer, 2005. http:\/\/www.avispa-project.org (2005)"},{"key":"125_CR2","doi-asserted-by":"crossref","unstructured":"Abadi, M., J\u00fcrjens, J.: Formal eavesdropping and its computational interpretation. In: Proceedings of TACS, pp. 82\u201394 (2001)","DOI":"10.1007\/3-540-45500-0_4"},{"key":"125_CR3","unstructured":"Abadi, M., Rogaway, P.: Reconciling two views of cryptography: The computational soundness of formal encryption. In: Proceedings of the 1st IFIP International Conference on Theoretical Computer Science, LNCS, vol. 1872, pp. 3\u201322. Springer (2000)"},{"key":"125_CR4","doi-asserted-by":"crossref","unstructured":"Backes, M.: A cryptographically sound Dolev-Yao style security proof of the Otway-Rees protocol. In: Proceedings of ESORICS, LNCS, vol. 3193, pp. 89\u2013108. Springer (2004)","DOI":"10.1007\/978-3-540-30108-0_6"},{"key":"125_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. In: Proceedings of ESORICS, pp. 362\u2013383 (2006)","DOI":"10.1007\/11863908_23"},{"key":"125_CR6","doi-asserted-by":"crossref","unstructured":"Backes, M., Jacobi, C.: Cryptographically sound and machine-assisted verification of security protocols. In: Proceedings of the 20th STACS, LNCS, vol. 2607, pp. 675\u2013686. Springer (2003)","DOI":"10.1007\/3-540-36494-3_59"},{"issue":"10","key":"125_CR7","doi-asserted-by":"crossref","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. J. Sel. Areas Commun. 22(10), 2075\u20132086 (2004)","journal-title":"J. Sel. Areas Commun."},{"key":"125_CR8","doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B.: Symmetric encryption in a simulatable Dolev-Yao style cryptographic library. In: Proceedings of CSFW\u201904, pp. 204\u2013218, June 2004","DOI":"10.1109\/CSFW.2004.1310742"},{"issue":"2","key":"125_CR9","doi-asserted-by":"crossref","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 Secur. Comput. 2(2), 109\u2013123 (2005)","journal-title":"IEEE Trans. Dependable Secur. Comput."},{"key":"125_CR10","doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B.: On the cryptographic key secrecy of the strengthened Yahalom protocol. In: Proceedings of 21st IFIP International Information Security Conference (SEC), pp. 233\u2013245, May 2006","DOI":"10.1007\/0-387-33406-8_20"},{"key":"125_CR11","doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations (extended abstract). In: Proceedings of the CCS\u201903, pp. 220\u2013230 (2003)","DOI":"10.1145\/948109.948140"},{"key":"125_CR12","doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: Symmetric authentication within a simulatable cryptographic library. In: Proceedings of ESORICS\u201903, LNCS, vol. 2808, pp. 271\u2013290. Springer (2003)","DOI":"10.1007\/978-3-540-39650-5_16"},{"key":"125_CR13","doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: A universally composable cryptographic library. IACR Cryptology ePrint Archive, Report 2003\/015, http:\/\/www.eprint.iacr.org\/ , January 2003","DOI":"10.1145\/948109.948140"},{"key":"125_CR14","doi-asserted-by":"crossref","unstructured":"Bella, G., Paulson, L.C.: Kerberos Version IV: inductive analysis of the secrecy goals. In: Proceedings of ESORICS\u201998, LNCS, vol. 1485, pp. 361\u2013375. Springer (1998)","DOI":"10.1007\/BFb0055875"},{"issue":"12","key":"125_CR15","first-page":"1337","volume":"3","author":"G. Bella","year":"1997","unstructured":"Bella G., Riccobene E.: Formal analysis of the Kerberos authentication system. J. Univers. Comput. Sci. 3(12), 1337\u20131381 (1997)","journal-title":"J. Univers. Comput. Sci."},{"key":"125_CR16","doi-asserted-by":"crossref","unstructured":"Bellare, M., Rogaway, P.: Entity authentication and key distribution. In: Proceedings of CRYPTO \u201993, LNCS vol. 773, pp. 232\u2013249. Springer (1994)","DOI":"10.1007\/3-540-48329-2_21"},{"key":"125_CR17","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: A computationally sound mechanized prover for security protocols. In: Proceedings of the 27th IEEE Symposium on Security & Privacy (2006)","DOI":"10.1109\/SP.2006.1"},{"key":"125_CR18","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Jaggard, A.D., Jesse, R., Scedrov, A., Tsay, J.-K.: Refining computationally sound mechanized proofs for Kerberos, 2009. http:\/\/www.infsec.uni-trier.de\/fcc2009\/","DOI":"10.1145\/1368310.1368326"},{"key":"125_CR19","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Jaggard, A.D., Scedrov, A., Tsay, J.-K.: Computationally sound mechanized proofs for basic and public-key Kerberos. In: ASIACCS\u201908, pp. 87\u201399 (2008)","DOI":"10.1145\/1368310.1368326"},{"key":"125_CR20","doi-asserted-by":"crossref","unstructured":"Boldyreva, A., Kumar, V.: Provable-security analysis of authenticated encryption in Kerberos. In: IEEE Symposium on Security and Privacy (2007)","DOI":"10.1109\/SP.2007.19"},{"key":"125_CR21","unstructured":"Butler, F., Cervesato, I., Jaggard, A.D., Scedrov, A.: An Analysis of Some Properties of Kerberos 5 Using MSR. In: Proceedings of CSFW\u201902 (2002)"},{"issue":"1\u20132","key":"125_CR22","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/j.tcs.2006.08.040","volume":"367","author":"F. Butler","year":"2006","unstructured":"Butler F., Cervesato I., Jaggard A.D., Scedrov A., Walstad C.: Formal analysis of Kerberos 5. Theor. Comput. Sci. 367(1\u20132), 57\u201387 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"125_CR23","unstructured":"Cable Television Laboratories, Inc. PacketCable Security Specification. Technical document PKT-SP-SEC-I11-040730 (2004)"},{"key":"125_CR24","doi-asserted-by":"crossref","unstructured":"Canetti, R.: Universal composable security: a new paradigm for cryptographic protocols. In: 42nd Annual Syposium on Foundations of Computer Science (FOCS 2001), pp. 136\u2013145. IEEE Computer Society, October 2001","DOI":"10.1109\/SFCS.2001.959888"},{"key":"125_CR25","unstructured":"Canetti, R., Gajek, S.: Universally composable symbolic analysis of Diffie\u2013Hellman based key exchange. Cryptology ePrint Archive, Report 2010\/303, 2010. http:\/\/www.eprint.iacr.org\/"},{"key":"125_CR26","unstructured":"Canetti, R., Herzog, J.: Universally composable symbolic analysis of cryptographic protocols (the case of encryption-based mutual authentication and key exchange). In: Proceedings of the 3rd Theory of Cryptography Conference (TCC) (2006)"},{"key":"125_CR27","doi-asserted-by":"crossref","unstructured":"Cervesato, I., Jaggard, A.D., Scedrov, A., Tsay, J.-K., Walstad, C.: Breaking and fixing public-key Kerberos, 2006. Presented at WITS\u201906 (2006)","DOI":"10.1007\/978-3-540-77505-8_13"},{"key":"125_CR28","doi-asserted-by":"crossref","unstructured":"Cervesato, I., Jaggard, A.D., Scedrov, A., Tsay, J.-K., Walstad, C.: Breaking and fixing public-key Kerberos. In: Proceedings of ASIAN\u201906, LNCS, vol. 4435 (2006)","DOI":"10.1007\/978-3-540-77505-8_13"},{"issue":"2\u20134","key":"125_CR29","doi-asserted-by":"crossref","first-page":"402","DOI":"10.1016\/j.ic.2007.05.005","volume":"206","author":"I. Cervesato","year":"2008","unstructured":"Cervesato I., Jaggard A.D., Scedrov A., Tsay J.-K., Walstad C.: Breaking and fixing public-key Kerberos. Inf. Comput. 206(2\u20134), 402\u2013424 (2008)","journal-title":"Inf. Comput."},{"key":"125_CR30","doi-asserted-by":"crossref","unstructured":"Cervesato, I., Jaggard, A.D., Scedrov, A., Walstad, C.: Specifying Kerberos 5 Cross-Realm Authentication. In: Proceedings of WITS\u201905, pp. 12\u201326 (2005)","DOI":"10.1145\/1045405.1045408"},{"key":"125_CR31","doi-asserted-by":"crossref","unstructured":"Cervesato, I., Meadows, C., Pavlovic, D.: An encapsulated authentication logic for reasoning about key distribution protocol. In: Proceedings of CSFW-18, pp. 48\u201361, Aix-en-Provence, France, 20\u201322 June 2005. IEEE Computer Society Press","DOI":"10.1109\/CSFW.2005.7"},{"key":"125_CR32","doi-asserted-by":"crossref","unstructured":"Comon-Lundh, H., Cortier, V.: Computational soundness of observational equivalence. In: Proceedings of the 15th ACM Conference on Computer and Communications Security CCS 2008. ACM Press (2008)","DOI":"10.1145\/1455770.1455786"},{"key":"125_CR33","doi-asserted-by":"crossref","unstructured":"Cortier, V., Warinschi, B.: Computationally sound, automated proofs for security protocols. In: Proceedings of ESOP-14, pp. 157\u2013171 (2005)","DOI":"10.1007\/978-3-540-31987-0_12"},{"key":"125_CR34","doi-asserted-by":"crossref","unstructured":"Datta, A., Derek, A., Mitchell, J., Shmatikov, V., Turuani, M.: Probabilistic polynomial-time semantics for a protocol security logic. In: Proceedings of ICALP, pp. 16\u201329. Springer LNCS 3580 (2005)","DOI":"10.1007\/11523468_2"},{"key":"125_CR35","unstructured":"Datta, A., Derek, A., Mitchell, J., Warinschi, B.: Key exchange protocols: Security definition, proof method, and applications. In: Proceedings of the IEEE CSFW-19, Venice, Italy, 2006. IEEE Press (2006)"},{"key":"125_CR36","unstructured":"De Clercq, J., Balladelli, M.: Windows 2000 authentication. http:\/\/www.windowsitlibrary.com\/Content\/617\/06\/6.html , 2001. Digital Press (2001)"},{"issue":"29","key":"125_CR37","doi-asserted-by":"crossref","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. Inf. Theory 2(29), 198\u2013208 (1983)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"125_CR38","doi-asserted-by":"crossref","unstructured":"Gajek, S., Manulis, M., Pereira, O., Sadeghi, A.-R., Schwenk, J.: Universally Composable Security Analysis of TLS. In: Proceedings of the 2nd International Conference on Provable Security (ProvSec 2008), Lecture Notes in Computer Science, vol. 5324, pp. 313\u2013327. Springer (2008)","DOI":"10.1007\/978-3-540-88733-1_22"},{"key":"125_CR39","doi-asserted-by":"crossref","unstructured":"Goldreich, O., Micali, S., Wigderson, A.: How to play any mental game\u2014or\u2014a completeness theorem for protocols with honest majority. In: Proceedings of STOC, pp. 218\u2013229 (1987)","DOI":"10.1145\/28395.28420"},{"key":"125_CR40","doi-asserted-by":"crossref","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. J. Comput. Syst. Sci. 28, 270\u2013299 (1984)","journal-title":"J. Comput. Syst. Sci."},{"key":"125_CR41","doi-asserted-by":"crossref","unstructured":"Guttman, J.D., Thayer Fabrega, F.J., Zuck, L.: The faithfulness of abstract protocol analysis: message authentication. In: Proceedings of CCS-8, pp. 186\u2013195 (2001)","DOI":"10.1145\/501983.502009"},{"key":"125_CR42","unstructured":"He, C., Mitchell, J.C.: Security analysis and improvements for IEEE 802.11i. In: Proceedings of NDSS\u201905 (2005)"},{"key":"125_CR43","doi-asserted-by":"crossref","unstructured":"Herzog, J., Liskov, M., Micali, S.: Plaintext awareness via key registration. In: Proceedings of CRYPTO, pp. 548\u2013564. Springer LNCS 2729 (2003)","DOI":"10.1007\/978-3-540-45146-4_32"},{"key":"125_CR44","unstructured":"IETF. Public Key Cryptography for Initial Authentication in Kerberos, 1996\u20132006. Sequence of Internet drafts available from http:\/\/www.tools.ietf.org\/wg\/krb-wg\/draft-ietf-cat-kerberos-pk-init\/"},{"key":"125_CR45","doi-asserted-by":"crossref","unstructured":"Impagliazzo, R., Kapron, B.M.: Logics for reasoning about cryptographic constructions. In: Proceedings of FOCS, pp. 372\u2013381 (2003)","DOI":"10.1109\/SFCS.2003.1238211"},{"key":"125_CR46","doi-asserted-by":"crossref","unstructured":"Laud, P.: Semantics and program analysis of computationally secure information flow. In: Proceedings of ESOP, pp. 77\u201391 (2001)","DOI":"10.1007\/3-540-45309-1_6"},{"key":"125_CR47","doi-asserted-by":"crossref","unstructured":"Laud, P.: Symmetric encryption in automatic analyses for confidentiality against active adversaries. In: Proceedings of the Symposium Security and Privacy, pp. 71\u201385 (2004)","DOI":"10.1109\/SECPRI.2004.1301316"},{"key":"125_CR48","doi-asserted-by":"crossref","unstructured":"Meadows, C.: Analysis of the internet key exchange protocol using the NRL Protocol Analyzer. In: Proceedings of the IEEE Symposium Security and Privacy, pp. 216\u2013231 (1999)","DOI":"10.21236\/ADA465466"},{"key":"125_CR49","doi-asserted-by":"crossref","unstructured":"Micciancio, D., Warinschi, B.: Soundness of formal encryption in the presence of active adversaries. In: Proceedings of TCC, pp. 133\u2013151. Springer LNCS 2951 (2004)","DOI":"10.1007\/978-3-540-24638-1_8"},{"key":"125_CR50","unstructured":"Microsoft. Security Bulletin MS05-042. http:\/\/www.microsoft.com\/technet\/security\/bulletin\/MS05-042.mspx , August 2005"},{"key":"125_CR51","doi-asserted-by":"crossref","unstructured":"Mitchell, J., Mitchell, M., Scedrov, A.: A linguistic characterization of bounded oracle computation and probabilistic polynomial time. In: Proceedings of FOCS, pp. 725\u2013733 (1998)","DOI":"10.1109\/SFCS.1998.743523"},{"key":"125_CR52","doi-asserted-by":"crossref","unstructured":"Mitchell, J., Ramanathan, A., Scedrov, A., Teague, V.: A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols. Theor. Comput. Sci. 353(1\u20133) (2006)","DOI":"10.1016\/j.tcs.2005.10.044"},{"issue":"9","key":"125_CR53","doi-asserted-by":"crossref","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 Commun. 32(9), 33\u201338 (1994)","journal-title":"IEEE Commun."},{"key":"125_CR54","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","DOI":"10.17487\/rfc4120"},{"key":"125_CR55","doi-asserted-by":"crossref","unstructured":"Pfitzmann, B., Waidner, M.: A model for asynchronous reactive systems and its application to secure message transmission. In: Proceedings of the S&P, pp. 184\u2013200 (2001)","DOI":"10.1109\/SECPRI.2001.924298"},{"key":"125_CR56","doi-asserted-by":"crossref","unstructured":"Roy, A., Datta, A., Derek, A., Mitchell, J.C.: Inductive proofs of computational secrecy. In: Biskup, J., Lopez, J. (Eds.), ESORICS, Lecture Notes in Computer Science, vol. 4734, pp. 219\u2013234. Springer (2007)","DOI":"10.1007\/978-3-540-74835-9_15"},{"key":"125_CR57","doi-asserted-by":"crossref","unstructured":"Roy, A., Datta, A., Mitchell, J.C.: Formal proofs of cryptographic security of Diffie\u2013Hellman-based protocols. In: Barthe, G., Fournet, C., (Eds.), TGC, Lecture Notes in Computer Science, vol. 4912, pp. 312\u2013329. Springer (2007)","DOI":"10.1007\/978-3-540-78663-4_21"},{"key":"125_CR58","doi-asserted-by":"crossref","unstructured":"Sprenger, C., Backes, M., Basin, D., Pfitzmann, B., Waidner, M.: Cryptographically sound theorem proving. In: Computer Security Foundations Workshop (CSFW06), pp. 153\u2013166. IEEE Computer Society, July 2006","DOI":"10.1109\/CSFW.2006.10"},{"key":"125_CR59","doi-asserted-by":"crossref","unstructured":"Sprenger, C., Basin, D.: Cryptographically-sound protocol-model abstractions. In: Computer Security Foundations (CSF \u201908). IEEE Computer Society (2008)","DOI":"10.1109\/CSF.2008.19"},{"key":"125_CR60","unstructured":"The Internet Engineering Task Force. http:\/\/www.ietf.org"},{"key":"125_CR61","doi-asserted-by":"crossref","unstructured":"Zhu, L., Tung, B.: Public Key Cryptography for Initial Authentication in Kerberos (PKINIT), June 2006. http:\/\/www.ietf.org\/rfc\/rfc4556","DOI":"10.17487\/rfc4556"}],"container-title":["International Journal of Information Security"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10207-011-0125-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10207-011-0125-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10207-011-0125-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,5]],"date-time":"2025-03-05T04:13:24Z","timestamp":1741148004000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10207-011-0125-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,4,20]]},"references-count":61,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,6]]}},"alternative-id":["125"],"URL":"https:\/\/doi.org\/10.1007\/s10207-011-0125-6","relation":{},"ISSN":["1615-5262","1615-5270"],"issn-type":[{"value":"1615-5262","type":"print"},{"value":"1615-5270","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,4,20]]}}}