We present a computational analysis of basic Kerberos and Kerberos with public-key authentication (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 is the most complex fragment of an industrial protocol that has yet been verified at the computational level. 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. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Backes, M., Cervesato, I., Jaggard, A. D., Scedrov, A., & Tsay, J. K. (2006). Cryptographically sound security proofs for basic and public-key Kerberos. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4189 LNCS, pp. 362–383). Springer Verlag. https://doi.org/10.1007/11863908_23
Mendeley helps you to discover research relevant for your work.