next up previous
Next: The Inductive Method Up: Using Isabelle to Prove Previous: Introduction


  Developed a decade ago as part of the project Athena at MIT [5], Kerberos has gone through many updates aimed at improving its security.

Kerberos relies on the use of timestamps to assure freshness of precious pieces of information as session keys. Kerberos checks twice the identity of Alice before she can get access to the network resource Bob, first by means of Kas (Kerberos Authentication Server) and then by means of Tgs (Ticket Granting Server). Alice receives by Kas a session key to be used for the communication with Tgs. Then, each time Alice wants to reach Bob, Tgs issues her with another session key which is to be used only for the communication between Alice and Bob.

Although the use of Kerberos as an authentication system for LANs is today widespread, the literature contains little work about the application of formal methods to it. This was the main motivation to our choice. Until a short time ago, the work of Burrows et al. [3] was the only significant attempt, but showed very few properties and has been widely criticised. A complete formalisation pointing out rigorously all the numerous details of the operation of Kerberos has been only recently achieved by means of the Gurevich's Abstract State Machine [1], but lacks automation. That work has been the basis to ours, which is, to our knowledge, the first attempt to mechanise such a complex protocol.

Giampaolo Bella
Mon Aug 4 18:43:12 BST 1997