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