International Association for Cryptologic Research

International Association
for Cryptologic Research


Paper: Cryptographically Sound Security Proofs for Basic and Public-Key Kerberos

Michael Backes
Iliano Cervesato
Aaron D. Jaggard
Andre Scedrov
Joe-Kai Tsay
Search ePrint
Search Google
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.
  title={Cryptographically Sound Security Proofs for Basic and Public-Key Kerberos},
  booktitle={IACR Eprint archive},
  keywords={cryptographic protocols / Kerberos, computational analysis, authentication, key secrecy},
  note={ 14638 received 29 Jun 2006, last revised 28 Jan 2010},
  author={Michael Backes and Iliano Cervesato and Aaron D. Jaggard and Andre Scedrov and Joe-Kai Tsay},