The Analysis of Kerberos

  Modelling Kerberos required the definition of two trusted parties Kas and Tgs, and of timestamps as parts of the messages. These main modifications were quickly applied to the existing framework based on one trusted party and on nonces, thus proving that it easily adapts to different protocol structures. Since Kas and Tgs are the foundation of the entire authentication procedure, our model assumes their private keys to be secure.

The Isabelle specification of Kerberos is presented in Appendix, where some mathematical symbols have taken the place of their ASCII equivalents to improve readability. The base of the induction is achieved by the Nil rule, while the power of the spy is formalised by the Fake rule. There are two Oops rules to model respectively the accidental loss of an authentication key (the session key used for the communication between Alice and Tgs) and of a service key (the session key used for the communication between Alice and Bob). They are currently omitted to simplify some proofs.

Each timestamp is obviously taken as the current time, which is formalised by the function CT mapping the current trace into an integer. Four lifetimes are defined as global constants, since sending the lifetimes inside the messages is a redundancy already addressed in [2].

AuthLife

is the lifetime of the authentication key and usually lasts several hours; each authentication key can be used within this lifetime between Alice and Tgs.

ServLife

is the lifetime of the service key and usually lasts a few minutes; each service key can be used within this lifetime between Alice and Bob. It is so short to prevent the re-use of a service key.

RecentAuth

is the lifetime within which an authenticator is considered acceptable (Each time Alice sends a message to anybody, she builds an authenticator containing a timestamp and sends it inside the message).

RecentResp

is the lifetime within which Alice considers acceptable a server's reply.

The need for the first two is straightforward. The reason for the last two is that, if an authenticator or a server's reply are ``old'' (i.e. they contain a timestamp older than RecentAuth or RecentResp respectively), then they are very likely to have been faked.

The timestamps Ta, Ta1, Ta2 mark the moments that Alice sends a message to Kas, Tgs, and Bob respectively. Similarly, Tk marks the moment of the Kas's reply and Tt the moment of the Tgs's reply.

Each rule consists of some assumptions (which are enclosed between [| and |]) and a conclusion (which appears after the ==> ). If the assumptions hold, then the event mentioned in the conclusion may occur. Then, the gist of the protocol should arise easily.

• Guarantees about Kerberos