Computationally Sound Mechanized Proofs for Basic and Public-key Kerberos

Bruno Blanchet, Aaron D. Jaggard, Andre Scedrov, and Joe-Kai Tsay. Computationally Sound Mechanized Proofs for Basic and Public-key Kerberos. In ACM Symposium on Information, Computer and Communications Security (ASIACCS'08), pages 87-99, Tokyo, Japan, March 2008. ACM.

The CryptoVerif scripts for our study of Kerberos are distributed below under the CeCILL license. Please read this license before downloading the scripts.

Authentication properties (Theorems 1-5) Basic Kerberos Public-key Kerberos
Secrecy of AK (Theorem 6) Basic Kerberos Public-key Kerberos
Secrecy of SK (Theorem 7) Basic Kerberos Public-key Kerberos
Secrecy of the optional subkey (Theorem 8)
- generated by the client Basic Kerberos Public-key Kerberos
- generated by the server Basic Kerberos Public-key Kerberos
Usability of AK (Theorem 9)
- for the client Basic Kerberos Public-key Kerberos
- for the KAS Basic Kerberos Public-key Kerberos
- for the TGS Basic Kerberos Public-key Kerberos
Usability of SK (Theorem 11)
- for the client Basic Kerberos Public-key Kerberos
- for the server Basic Kerberos Public-key Kerberos
- for the TGS Basic Kerberos Public-key Kerberos

All scripts as an archive.

These scripts require the automatic verifier CryptoVerif, version 1.07 or later. This verifier is available here.

Bruno Blanchet, Aaron D. Jaggard, Andre Scedrov, and Joe-Kai Tsay