in Proceedings of 11th European Symposium on Research in Computer Security(ESORICS), Lecture Notes in Computer Science vol. 4189, Springer, pp. 362-383, September 2006. Preprint on IACR ePrint 2006/219.
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.
This publication is accompanied by links to downloadable versions of this publication. These documents do not necessarily correspond exactly to the cited version. Instead, in most cases full or updated versions are provided. For access to the official version, follow the "Official version" link to the publishers site.