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-)