BlanchetJaggardScedrovTsayDagstuhl07

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.

Links

Seminar homepage: http://www.dagstuhl.de/07421/

Abstract

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.

Bibtex


@INPROCEEDINGS{BlanchetJaggardScedrovTsayDagstuhl07,
  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,
  MONTH = OCT
}

E-mail/Courrier électronique : Bruno.Blanchet@trap-inria.fr (remove trap-)