Computationally sound mechanized proofs for basic and public-key Kerberos
Bruno Blanchet, Aaron D. Jaggard, Andre Scedrov, Joe-Kai Tsay · 2008
We present a computationally sound mechanized analysis of Kerberos 5, both with and without its public-key extension PKINIT. We prove authentication and key secrecy properties using the prover CryptoVerif, which works directly in the computational model; these are the first mechanical proofs of a full industrial protocol at the computational level. We also generalize the notion of key usability and use CryptoVerif to prove that this definition is satisfied by keys in Kerberos.