Bruno Blanchet Back to publications
Bruno Blanchet, Aaron D. Jaggard, Andre Scedrov, and Joe-Kai Tsay. Computationally Sound Mechanized Proofs for Basic and Public-key Kerberos. In Dagstuhl seminar Formal Protocol Verification Applied, October 2007.

Full text not available. Sorry !


Seminar homepage:


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.


  AUTHOR = {Bruno Blanchet and Aaron D. Jaggard and Andre Scedrov and Joe-Kai Tsay},
  TITLE = {Computationally Sound Mechanized Proofs for Basic and Public-key {K}erberos},
  BOOKTITLE = {Dagstuhl seminar "Formal Protocol Verification Applied"},
  YEAR = 2007,

E-mail/Courrier électronique : (remove trap-)