### Cryptographically Sound Security Proofs for Basic and Public-Key Kerberos

Michael Backes, Iliano Cervesato, Aaron D. Jaggard, Andre Scedrov, and Joe-Kai Tsay

##### Abstract

We present a computational analysis of basic Kerberos with and without its public-key extension PKINIT in which we consider authentication and key secrecy properties. Our proofs rely on the Dolev--Yao-style model of Backes, Pfitzmann, and Waidner, which allows for mapping results obtained symbolically within this model to cryptographically sound proofs if certain assumptions are met. This work was the first verification at the computational level of such a complex fragment of an industrial protocol. By considering a recently fixed version of PKINIT, we extend symbolic correctness results we previously attained in the Dolev--Yao model to cryptographically sound results in the computational model.

Note: Revised full version. This updates the formalization of the certificates binding keys to principals.

Available format(s)
Category
Cryptographic protocols
Publication info
Published elsewhere. Unknown where it was published
Keywords
Kerberoscomputational analysisauthenticationkey secrecy
Contact author(s)
History
2010-01-29: revised
See all versions
Short URL
https://ia.cr/2006/219

CC BY

BibTeX

@misc{cryptoeprint:2006/219,
author = {Michael Backes and Iliano Cervesato and Aaron D.  Jaggard and Andre Scedrov and Joe-Kai Tsay},
title = {Cryptographically Sound Security Proofs for Basic and Public-Key Kerberos},
howpublished = {Cryptology ePrint Archive, Paper 2006/219},
year = {2006},
note = {\url{https://eprint.iacr.org/2006/219}},
url = {https://eprint.iacr.org/2006/219}
}

Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.