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.
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 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 |
+-------------------+------------+--------------------+-----------+