Cryptology ePrint Archive: Report 2006/219

Cryptographically Sound Security Proofs for Basic and Public-Key Kerberos

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

Abstract: We present a computational analysis of core Kerberos with public-key authentication (PKINIT) in which we consider authentication and key secrecy properties. These 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. Our work constitutes the first formal verification of a significant subset of an industrial protocol at the computational level. 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.

Category / Keywords: cryptographic protocols / Kerberos, computational analysis, authentication, key secrecy

Date: received 29 Jun 2006

Contact author: adj at math tulane edu

Available formats: Postscript (PS) | Compressed Postscript (PS.GZ) | PDF | BibTeX Citation

Version: 20060630:124723 (All versions of this report)

Discussion forum: Show discussion | Start new discussion