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):

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

==> AuthTicket : 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.Says Tgs' A (Crypt AuthKey {|ServKey, Agent B, Tt, ServTicket|}): set_of_list evs

==> ServTicket : parts(sees Spy evs)

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:

Note the assumption that A has not lost her key to the spy. Similar is the counterpart for Tgs:[|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(CryptKey_A{|Key AuthKey, Agent Tgs, Tk,(Crypt Key_Tgs {|Agent A, Agent Tgs, Key AuthKey, Tk|})|}) : set_of_list evs

Also this second theorem relies on the encryption keys being secure. This is formalised by[|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(CryptAuthKey{|Key ServKey, Agent B, Tt,(Crypt Key_B {|Agent A, Agent B, Key ServKey, Tt|})|}) : set_of_list evs

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

Mon Aug 4 18:43:12 BST 1997