next up previous
Next: Future Work Up: CryptoLog: A Theorem Prover Previous: The CryptoLog Analyser

An Example: The Kerberos Protocol

Figures 1 and 2 show the input for the Kerberos protocol. It consists of three Horn-clauses, kerberos, kerberosAssumptions and kerberosProtocol. A call of the first clause: ?- kerberos.

starts the analyser. In this section, the input and output will be briefly explained. Comments are written between curly braces ( { ... }).

 

kerberos :-
   Principals ([C, S, AS, TGS]),
   kerberosAssumptions,
   kerberosProtocol.

kerberosAssumptions :-
   BeginAssumptions,
      { ------------------------------------------- }
      { I) Pre-installed keys / passwords / secrets }
      { ------------------------------------------- }
      (C,AS) Trust PWDc :=: Password(C,AS),    { Client C and the AS share a password }
      (AS,TGS) Trust Kt :=: SharedKey(AS,TGS), { The AS and TGS share a key }
      (S,TGS) Trust Ks :=: SharedKey(S,TGS),   { Server S and the TGS share a key }
      { ----------------- }
      { II) Jurisdictions }
      { ----------------- }
      (C, TGS) Trusts AS ==> CompetentHonest,        { The AS is competent & honest and }
      (C, TGS) Trusts AS ==> QualitySecrets(C,TGS),  { generates good keys }
      (C, S) Trust TGS ==> CompetentHonest, 
      (C, S) Trust TGS ==> QualitySecrets(C,S),
      
      { -------------------------------- }
      { III) Definitions / Abbreviations }
      { -------------------------------- }
      Define ticket(Client,SessionKey,Timestamp,Lifetime,MasterKey) :=:
              Enc(Client,SessionKey,Timestamp,Lifetime,MasterKey),
      Define auth(Client,Timestamp, SessionKey) :=: 
              Enc(Client, Timestamp, SessionKey),
EndAssumptions.

Figure 1:  Parser's input for the Kerberos protocol (part a)

In figure 1, the participants that play a role are listed: C (the client), S (the server), AS (the authentication server) and TGS (the ticket granting server).

In the first part of the initial assumptions, the pre-installed password and keys are listed: PWDc is the password shared between the client C and the AS; Kt is the key shared between the AS and the TGS; finally Ks is the key known by S and TGS.

The second part consists of the jurisdictions: who trusts who to generate good keys, and who trusts whose competence and honesty.

In the last part, a few abbreviations are defined. A call of these functions will be expanded according to the definition.

Figure 2 shows the last clause kerberosProtocol, which implements the actual protocol. It consists of three parts: the single sign-on, the retrieval of an appropriate ticket for the server, and the mutual authentication.

 

kerberosProtocol :-
   BeginProtocol,
      C: NcP := Nonce,  { Client generates a Nonce }
      C Knows TGS,
   
      { ----------------- }
      { A) Single Sign On }
      { ----------------- }

      C   --->   AS : (C, TGS, NcP),
                 AS: Kc := SharedKey (C, TGS),
                 AS: LTtgt := Value,          { AS generates the LifeTime }
                 AS: TStgt := CurrentTime,    { AS reads its clock }
      C   <---   AS : Enc(TGS, Kc, NcP, TStgt, LTtgt, ticket(C, Kc, TStgt, LTtgt, Kt), PWDc),

      { ------------------------------ }
      { B) Get a ticket for the server }
      { ------------------------------ }

      C Knows S,
      C: fresh(TStgt),        { Timestamp is fresh? i.e. no replay? }
      C: TSc := CurrentTime,  { Client reads its clock }
      C   --->   TGS: (S, ticket(C, Kc, TStgt, LTtgt, Kt), auth(C, TSc, Kc)),
                 TGS: fresh(TStgt), 
                 TGS: fresh(TSc),
                 TGS: Kcs := SharedKey (C, S),   { TGS generates a new key }
                 TGS: TSt := CurrentTime,
                 TGS: LTt := Value,
      C   <---   TGS: Enc(S, Kcs, TSt, LTt, ticket(C, Kcs, TSt, LTt, Ks), Kc),
      C: valid(TSt),
      C: TScs := CurrentTime,

      { ------------------------ }
      { C) Mutual Authentication }
      { ------------------------ }

      C   --->    S : (ticket(C, Kcs, TSt, LTt, Ks), auth(C, TScs, Kcs)),
                  S: fresh(TSt),
                  S: fresh(TScs),
      C   <---    S : Enc(F(TScs), Kcs),

      EndProtocol.

Figure 2:  Parser's input for the Kerberos protocol (part b)

Figure 3 shows part of the result produced by the analyser. For every participant, it lists the holds- and beliefs-relations. At the end, an overview of leaked secret information is shown, and possible victims for a dictionary attack. For every successful attack, the consequences are listed too.

 

...
TGS >- Kc                                 >- means: holds
TGS >- Kcs                                |= means: believes
TGS |= # Kc                               #  means: is fresh
TGS |= # Kcs                              O  means: is recognizable
TGS |= C >- Kc
TGS |= AS |= C <-Kc-> TGS
TGS |= AS <-Kt-> TGS                       AS >- Kc
TGS |= C <-Kc-> TGS                        AS |= # Kc
TGS |= C <-Kcs-> S                         AS |= C <-Kc-> TGS
...                                        ...
S >- Kcs                                   C >- Kcs
S |= # Kcs                                 C |= S >- Kcs
S |= C >- Kcs                              C |= AS |= C <-Kc-> TGS
S |= TGS |= C <-Kcs-> S                    C |= AS |= # Kc
S |= C <-Kcs-> S                           C |= TGS |= # Kcs
...                                        C |= TGS |= C <-Kc-> TGS
                                           C |= TGS |= C <-Kcs-> S
                                           C |= C <-Kc-> TGS
                                           C |= C <-Kcs-> S
                                           ...

+--------------------------------+
| Leakages of secret information |
+--------------------------------+

No Leakages Found!

+---------------------------+
| Dictionary attack victims |
+---------------------------+

DICTIONARY ATTACK POSSIBLE ON: 
	- Enc([TGS,Kc,NcP,TStgt,LTtgt,Enc([C,Kc,TStgt | LTtgt],Kt)],PWDc)
		 through enumerating PWDc

Hence, the following information will be disclosed:
	- [TGS,Kc,NcP,TStgt,LTtgt,Enc([C,Kc,TStgt | LTtgt],Kt)]
	- PWDc

+====================================+
| IF DICTIONARY ATTACK SUCCEEDS, ... |
+====================================+


+===================+============+====================+===========+
| Secret leaked to  | Trusted by | As being a secret  | Issued by |
| to the world      | principals | between principals | Principal |
+===================+============+====================+===========+
|       PWDc        |      AS, C |              C, AS |   ??????? |
+-------------------+------------+--------------------+-----------+
|         Kc        | TGS, C, AS |             C, TGS |        AS |
+-------------------+------------+--------------------+-----------+
|        Kcs        |  S, C, TGS |               C, S |       TGS |
+-------------------+------------+--------------------+-----------+

Figure 3:  Partial output of the analyser



next up previous
Next: Future Work Up: CryptoLog: A Theorem Prover Previous: The CryptoLog Analyser



Bart De Decker
Mon Aug 4 16:31:43 MET DST 1997