BlanchetJaggardScedrovTsayAsiaCCS08
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 ACM Symposium on Information, Computer and Communications
Security (ASIACCS'08), pages 87-99, Tokyo, Japan, March 2008. ACM.
Copyright
Permission to make digital/hard copy of all or part of
this material without fee for personal or classroom use
provided that the copies are not made or distributed for profit
or commercial advantage, the ACM copyright/server notice, the title of the
publication, and its date appear, and notice is given that copying is by
permission of the ACM, Inc. To copy otherwise, to republish, to post on
servers, or to redistribute to lists requires prior specific
permission and/or a fee. Copyright ACM.
Get the paper
.pdf, 272 Kb
Links
Official ACM version (you can download the full text from there):
CryptoVerif scripts available at http://cryptoverif.inria.fr/kerberos/
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{BlanchetJaggardScedrovTsayAsiaCCS08,
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 = {ACM Symposium on Information, Computer and Communications Security (ASIACCS'08)},
PAGES = {87--99},
YEAR = 2008,
ADDRESS = {Tokyo, Japan},
MONTH = MAR,
PUBLISHER = {ACM}
}
E-mail/Courrier électronique : Bruno.Blanchet@trap-inria.fr (remove trap-)