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.

As a result of the following paper:

Bruno Blanchet, Aaron D. Jaggard, Jesse Rao, Andre Scedrov, and Joe-Kai Tsay. Refining Computationally Sound Mechanized Proofs for Kerberos. In Workshop on Formal and Computational Cryptography (FCC 2009), Port Jefferson, NY, July 2009.

we improved our scripts for public-key Kerberos. The improved versions are below:

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

All scripts as an archive.

Furthermore, with the evolution of CryptoVerif, we were able to prove key usability without manual inspection of the final game. Up-to-date scripts for Kerberos are included in the CryptoVerif distribution, in directory examples/kerberos.

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