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.