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

Computationally sound mechanized proofs for basic and public-key Kerberos

B. Blanchet, A. D. Jaggard, A. Scedrov, J.-K. Tsay
ASIACCS '08 Proceedings of the 2008 ACM symposium on Information, computer and communications security, 2008

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