Computationally sound mechanized proofs for basic and public-key Kerberos

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Computationally sound mechanized proofs for basic and public-key Kerberos

Full text

Pdf (363 KB)

Source

ASIAN ACM Symposium on Information, Computer and Communications Security archive
Proceedings of the 2008 ACM symposium on Information, computer and communications security table of contents

Tokyo, Japan

SESSION: Formal verification table of contents

Pages 87-99

Year of Publication: 2008

ISBN:978-1-59593-979-1

Authors

B. Blanchet	Supérieure & INRIA
A. D. Jaggard	Rutgers University
A. Scedrov	University of Pennsylvania
J.-K. Tsay	University of Pennsylvania

Sponsor

SIGSAC: ACM Special Interest Group on Security, Audit, and Control

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 10, Downloads (12 Months): 108, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1368310.1368326 What is a DOI?

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.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Martín Abadi , Phillip Rogaway, Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption), Proceedings of the International Conference IFIP on Theoretical Computer Science, Exploring New Frontiers of Theoretical Informatics, p.3-22, August 17-19, 2000
	2	M. Abdalla, P.-A. Fouque, and D. Pointcheval. Password-Based Authenticated Key Exchange in the Three-Party Setting. IEE Proc. Information Security, 153(1), 2006.
	3	A. Armando et al. The Avispa tool for the automated validation of internet security protocols and applications. In CAV 2005, volume 3576 of LNCS. Springer.
	4	M. Backes, I. Cervesato, A. D. Jaggard, A. Scedrov, and J.-K. Tsay. Cryptographically Sound Security Proofs for Basic and Public-key Kerberos. In ESORICS 2006, volume 4189 of LNCS. Springer, September 2006.
	5	Michael Backes , Birgit Pfitzmann , Michael Waidner, A composable cryptographic library with nested operations, Proceedings of the 10th ACM conference on Computer and communications security, October 27-30, 2003, Washington D.C., USA [doi>10.1145/948109.948140]
	6	G. Bella and L. C. Paulson. Using Isabelle to Prove Properties of the Kerberos Authentication System. In DIMACS'97, Workshop on Design and Formal Verification of Security Protocols (CD-ROM), 1997.
	7	Giampaolo Bella , Lawrence C. Paulson, Kerberos Version 4: Inductive Analysis of the Secrecy Goals, Proceedings of the 5th European Symposium on Research in Computer Security, p.361-375, September 16-18, 1998
	8	Mihir Bellare , Ran Canetti , Hugo Krawczyk, Keying Hash Functions for Message Authentication, Proceedings of the 16th Annual International Cryptology Conference on Advances in Cryptology, p.1-15, August 18-22, 1996
	9	Mihir Bellare , Chanathip Namprempre, Authenticated Encryption: Relations among Notions and Analysis of the Generic Composition Paradigm, Proceedings of the 6th International Conference on the Theory and Application of Cryptology and Information Security: Advances in Cryptology, p.531-545, December 03-07, 2000
	10	S. M. Bellovin and M. Merritt. Limitations of the Kerberos Authentication System. In USENIX Conference Proceedings, Winter 1991.
	11	Bruno Blanchet, A Computationally Sound Mechanized Prover for Security Protocols, Proceedings of the 2006 IEEE Symposium on Security and Privacy, p.140-154, May 21-24, 2006 [doi>10.1109/SP.2006.1]
	12	Bruno Blanchet, An Efficient Cryptographic Protocol Verifier Based on Prolog Rules, Proceedings of the 14th IEEE workshop on Computer Security Foundations, p.82, June 11-13, 2001
	13	Bruno Blanchet, A Computationally Sound Mechanized Prover for Security Protocols, Proceedings of the 2006 IEEE Symposium on Security and Privacy, p.140-154, May 21-24, 2006 [doi>10.1109/SP.2006.1]
	14	Bruno Blanchet, Computationally Sound Mechanized Proofs of Correspondence Assertions, Proceedings of the 20th IEEE Computer Security Foundations Symposium, p.97-111, July 06-08, 2007 [doi>10.1109/CSF.2007.16]
	15	B. Blanchet and D. Pointcheval. Automated Security Proofs with Sequences of Games. In CRYPTO 2006, volume 4117 of LNCS. Springer, Aug. 2006.
	16	Alexandra Boldyreva , Virendra Kumar, Extended Abstract: Provable-Security Analysis of Authenticated Encryption in Kerberos, Proceedings of the 2007 IEEE Symposium on Security and Privacy, p.92-100, May 20-23, 2007 [doi>10.1109/SP.2007.19]
	17	Frederick Butler , Iliano Cervesato , Aaron D. Jaggard , Andre Scedrov , Christopher Walstad, Formal analysis of Kerberos 5, Theoretical Computer Science, v.367 n.1, p.57-87, 24 November 2006 [doi>10.1016/j.tcs.2006.08.040]
	18	R. Canetti and J. Herzog. Universally composable symbolic analysis of mutual authentication and key exchange protocols. In TCC'06, volume 3876 of LNCS. Springer, March 2006.
	19	Iliano Cervesato , Aaron D. Jaggard , Andre Scedrov , Joe-Kai Tsay , Christopher Walstad, Breaking and fixing public-key Kerberos, Information and Computation, v.206 n.2-4, p.402-424, February, 2008 [doi>10.1016/j.ic.2007.05.005]
	20	V. Cortier and B. Warinschi. Computationally sound, automated proofs for security protocols. In ESOP'05, volume 3444 of LNCS. Springer, Apr. 2005.
	21	Anupam Datta , Ante Derek , John C. Mitchell , Bogdan Warinschi, Computationally Sound Compositional Logic for Key Exchange Protocols, Proceedings of the 19th IEEE workshop on Computer Security Foundations, p.321-334, July 05-07, 2006 [doi>10.1109/CSFW.2006.9]
	22	Changhua He , Mukund Sundararajan , Anupam Datta , Ante Derek , John C. Mitchell, A modular correctness proof of IEEE 802.11i and TLS, Proceedings of the 12th ACM conference on Computer and communications security, November 07-11, 2005, Alexandria, VA, USA [doi>10.1145/1102120.1102124]
	23	IETF. Public Key Cryptography for Initial Authentication in Kerberos, 1996--2006. RFC 4556. Preliminary versions available as a sequence of Internet Drafts at http://tools.ietf.org/wg/krb-wg/draft-ietf-cat-kerberos-pk-init/.
	24	A. D. Jaggard, A. Scedrov, and J.-K. Tsay. Computationally Sound Mechanized Proof of PKINIT for Kerberos. Abstract presented at FCC'07.
	25	Peeter Laud, Secrecy types for a simulatable cryptographic library, Proceedings of the 12th ACM conference on Computer and communications security, November 07-11, 2005, Alexandria, VA, USA [doi>10.1145/1102120.1102126]
	26	P. Lincoln , J. Mitchell , M. Mitchell , A. Scedrov, A probabilistic poly-time framework for protocol analysis, Proceedings of the 5th ACM conference on Computer and communications security, p.112-121, November 02-05, 1998, San Francisco, California, United States [doi>10.1145/288090.288117]
	27	Patrick Lincoln , John C. Mitchell , Mark Mitchell , Andre Scedrov, Probabilistic Polynomial-Time Equivalence and Security Analysis, Proceedings of the Wold Congress on Formal Methods in the Development of Computing Systems-Volume I, p.776-793, September 20-24, 1999
	28	Gavin Lowe, Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR, Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.147-166, March 27-29, 1996
	29	C. Meadows. Analysis of the Internet Key Exchange Protocol using the NRL Protocol Analyzer. In IEEE Symp. Security and Privacy, 1999.
	30	C. A. Meadows. The NRL protocol analyzer: An overview. Journal of Logic Programming, 26(2), 1996.
	31	Microsoft. Security Bulletin MS05-042. http://www.microsoft.com/technet/security/bulletin/MS05-042.mspx, August 2005.
	32	John C. Mitchell , Ajith Ramanathan , Andre Scedrov , Vanessa Teague, A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols, Theoretical Computer Science, v.353 n.1, p.118-164, 14 March 2006 [doi>10.1016/j.tcs.2005.10.044]
	33	John C. Mitchell , Vitaly Shmatikov , Ulrich Stern, Finite-state analysis of SSL 3.0, Proceedings of the 7th conference on USENIX Security Symposium, p.16-16, January 26-29, 1998, San Antonio, Texas
	34	C. Neuman, T. Yu, S. Hartman, and K. Raeburn. The Kerberos Network Authentication Service (V5), July 2005. http://www.ietf.org/rfc/rfc4120.
	35	K. Raeburn. Encryption and Checksum Specifications for Kerberos 5. http://www.ietf.org/rfc/rfc3961.txt, Feb. 2005.
	36	A. Roy, A. Datta, A. Derek, and J. C. Mitchell. Inductive proofs of computational secrecy. In ESORICS 2007, volume 4734 of LNCS. Springer, Sept. 2007.
	37	A. Roy, A. Datta, and J. C. Mitchell. Formal proofs of cryptographic security of Diffie-Hellman-based protocols. In TGC'07, Nov. 2007. To appear.
	38	Christoph Sprenger , Michael Backes , David Basin , Birgit Pfitzmann , Michael Waidner, Cryptographically Sound Theorem Proving, Proceedings of the 19th IEEE workshop on Computer Security Foundations, p.153-166, July 05-07, 2006 [doi>10.1109/CSFW.2006.10]