Guarantees about Kerberos

Proving for Kerberos the possibility properties and the regularity lemmas already established for other protocols in [8] has not required much effort.

New forwarding lemmas have been established. One is proved for the ticket that Alice receives from Kas (and then forwards to Tgs):

 Says Kas' A (Crypt Key_A {|AuthKey, Agent Tgs, Tk, AuthTicket|})
   : set_of_list evs

  ==> AuthTicket : parts(sees Spy evs)

being Key_A Alice's secret key, and one is proved for the ticket that Alice gets from Tgs (and then forwards to Bob):

 Says Tgs' A (Crypt AuthKey {|ServKey, Agent B, Tt, ServTicket|})
   : set_of_list evs

  ==> ServTicket : parts(sees Spy evs)

In the real world, Alice does not know who the true senders of the messages she gets are. This is why Kas and Tgs are primed.

The proof of such theorems is now down to one Isabelle command thanks to the development of suitable proof tactics.

A crucial authenticity theorem formally states that if a certain encrypted message appears, then it originated with Kas:

 [|Crypt Key_A {|Key AuthKey, Agent Tgs, Tk, AuthTicket|}
		  : parts(sees Spy evs);
  A : lost; evs : kerberos|]

  ==> AuthTicket = Crypt Key_Tgs {|Agent A, Agent Tgs, Key AuthKey, Tk|} &

      Says Kas A (Crypt Key_A {|Key AuthKey, Agent Tgs, Tk,
		 	       (Crypt Key_Tgs {|Agent A, Agent Tgs, Key AuthKey, Tk|})
                 |}) : set_of_list evs

Note the assumption that A has not lost her key to the spy. Similar is the counterpart for Tgs:

 [|Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|}
		  : parts(sees Spy evs);
  Key AuthKey  : analz(sees Spy evs);
  B : lost; evs : kerberos|]

  ==> ServTicket = Crypt Key_B {|Agent A, Agent B, Key ServKey, Tt|} &

      Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt,
		 	       (Crypt Key_B {|Agent A, Agent B, Key ServKey, Tt|})
                 |}) : set_of_list evs

Also this second theorem relies on the encryption keys being secure. This is formalised by B lost for B's private key, and by Key AuthKey analz(sees Spy evs) for the session key AuthKey.

As for the secrecy theorems, not surprisingly the proof that no session key is used to encrypt other session keys failed. The reason is that the authentication key encrypts the service key; therefore, the theorem could be proved only for service keys. Proof methods recently applied to Yahalom [11] may yield results for Kerberos also.

Since the authentication key has a long lifetime, it is used to encrypt many service keys, so, from learning one authentication key, the spy could obtain a considerable number of other session keys. This addresses a protocol weakness already mentioned in [1].

The temporality of Kerberos suggested the definition of a new class of theorems, called temporal properties, expressing relations about the timestamps. They emphasise the key role played by the lifetimes, and can suggest the right values for them. This is of crucial importance since many replay attacks success because of too long lifetimes. For these reasons, more and more theorems of this class are being investigated.

For instance, the following is a theorem expressing that a service key is issued not later than the authentication key has expired:

 [|Says Kas' A (Crypt Key_A {|AuthKey, Agent Tgs, Tk, AuthTicket|})
    : set_of_list evs;
   Says Tgs' A (Crypt AuthKey {|ServKey, Agent B, Tt, ServTicket|})
    : set_of_list evs|]

 ==> Tt <= Tk + AuthLife