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.

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:

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. To sum up, our best scripts for Kerberos are the following:

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


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