Using Isabelle to Prove Properties of the
Kerberos Authentication System

Giampaolo Bella    Lawrence C Paulson

Computer Laboratory - University of Cambridge
New Museums Site, Pembroke Street
Cambridge CB2 3QG (UK)

Abstract:

The Inductive method, previously used to analyse classical, nonce-based cryptographic protocols, is here tailored to formalise Kerberos, a real-world, timestamp-based protocol. A complete formalisation of the whole protocol is achieved, and several guarantees about its entangled operation are proved using the theorem prover Isabelle.

• Introduction
• Kerberos
• The Inductive Method
  • Overview
  • Operators
  • Guarantees
• The Analysis of Kerberos
  • Guarantees about Kerberos
• Conclusion
• References
• Appendix: Specifying Kerberos in Isabelle
• About this document...