Kerberos version 5 Protocol

Purpose

(taken from SPORE)
C is a client,
S is a a server (C wants to communicate with S),
U is a user on behalf of which A and S communicate,
G is a ticket granting server,
A is a key distribution center (trusted server).
The keys Kag and Kgs are long term symmetric key whose values are supposed to be known initially only by, A and G, respectively G and S.
L1 and L2 are lifetimes, N1 and N2 are nonces. Tstart, Texpire, T'start, T;expire are time stamps which define the interval of validity of the ticket in which they are contained.
U is a user on behalf of whom the client C communicates. In particular, C initially knows the value of the key Ku.
The key Kcg is freshly generated by A for communication between C and G, and in transmitted to C in message 2, encrypted by Ku, and indirectly to G, in the ticket {U, C, G, Kcg, Tstart, Texpire}Kag which C transmits blindly to G in message 3.
The authentificator {C, T1}Kcg is used by G to check timeliness of the ticket.
The key Kcs is freshly generated by G for communication between C and G, and in transmitted to C in message 4, encrypted by Kcg, and indirectly to S, in the ticket {U, C, S, Kcs, T'start, T'expire}Kgs which C transmits blindly to S in message 5.

Informal Specification

  1. C -> A : U, G, L1, N1
  2. A -> C : U, Tcg, E(Ku: G, Kcg, Tstart, Texpire, N1)
  3. C -> G : S, L2, N2, Tcg, Acg
  4. G -> C : U, Tcs, E(Kcg: S, Kcs, T'start, T'expire, N2)
  5. C -> S : Tcs, Acs
  6. S -> C : E(Kcs : T')

See Commonly Used Representations

MSR Specification

Click here to download 
--- Author: rishav
--- Date: 6 August 2007
--- Kerberos version 5 Protocol
---     C -> A : U, G, L1, N1
---     A -> C : U, Tcg, E(Ku: G, Kcg, Tstart, Texpire, N1) 
---     C -> G : S, L2, N2, Tcg, Acg
---     G -> C : U, Tcs, E(Kcg: S, Kcs, T'start, T'expire, N2)
---     C -> S : Tcs, Acs
---     S -> C : E(Kcs : T')


(reset)
(
module KERB
export * .

client : type.				client <: princ.
server : type.                         server <: princ.
TGS : type.                             TGS <: server.
KDC : type.                             KDC <: server.
key : type.
ltk : princ -> princ -> type.          ltk A B <: key.
stk : princ -> princ -> type.          stk A B <: key.      stk A B <: msg.
ltks : princ -> type.		       ltks S <: key.       ltks S <: msg.
enc : key -> msg -> msg.
time : type.                           time <: msg.
nonce : type.                          nonce <: msg.
net : msg -> state.
clock : time -> state.

TGT : princ -> time -> time -> {C : client} {G : TGS} stk C G -> {A : KDC} {G : TGS} ltk A G -> state.
TGT' : princ -> time -> time -> {C : client} {S : server} stk C S -> state.


initiatorClient:
forall C : client.
{
			exists LC : princ -> TGS -> nonce -> state.
KRule1:
  forall U : princ.
  forall G : TGS.
  empty
  => exists L1 : time.
     exists N1 : nonce.
     net(U & G & L1 & N1), LC U G N1.

KRule3:
  forall A : KDC.
  forall U : princ.
  forall G : TGS.
  forall Kcg : stk C G.
  forall Ku : ltks U.
  forall Tcg : msg.
  forall N1 : nonce.
  forall Tstart : time.
  forall Texpire : time.
  forall Kag : ltk A G.
   net(U & Tcg & enc Ku (G & Kcg & Tstart & Texpire & N1)), LC U G N1
  => TGT U Tstart Texpire C G Kcg A G Kag.

}


keyDistributionCentre:
forall A : KDC.
{

KRule2:
  forall U : princ.
  forall G : TGS.
  forall Tstart : time.
  forall Texpire : time.
  forall Ku : ltks U.
  forall N1 : nonce.
    net(U & G & L1 & N1)
   => exists Kcg : stk C G.
      net(U & enc Kag (U & C & G & Kcg & Tstart & Texpire) & enc Ku (G & Kcg & Tstart & Texpire & N1)).

}

initiatorClient2:
forall C : client.
{
			exists LC2 : KDC -> princ -> server -> {G : TGS} stk C G -> nonce -> state.
KRule4:
  forall A : KDC.
  forall U : princ.
  forall G : TGS.
  forall S : server.
  forall Kcg : stk C G.
  forall Kag : ltk A G.
  forall Tcg : msg.
  forall Tstart : time.
  forall T : time.
  forall Texpire : time.
  TGT U Tstart Texpire C G Kcg A G Kag
  => exists L2 : time.
     exists N2 : nonce.
     net(S & Tcg & enc Kcg (C & T) & L2 & N2), LC2 A U S G Kcg N2.

KRUle6: 
  forall A : KDC.
  forall U : princ.
  forall S : server.
--- forall G needed for LC2 or else gives unsolved constraints error
  forall G : TGS. 
  forall Kcg : stk C G.
  forall Kcs : stk C S.
  forall T'start : time.
  forall T'expire : time.
  forall N2 : nonce.
    net(U & enc Kcg (U & C & G & S & Kcs & T'start & T'expire) & enc Kcg (S & Kcs & T'start & T'expire & N2)), LC2 A U S G Kcg N2
  => TGT' U T'start T'expire C S Kcs.
}


ticketGrantingServer:
forall G : TGS.
{
---needs everything to be declared>>> weird as reconstruction is supposed to work..for eg time.
KRule5:
  forall C : princ.
  forall A : KDC.
  forall U : princ.
  forall S : server.
  forall Kcg : stk C G.
  forall T : time.
  forall Tstart : time.
  forall Texpire : time.
  forall T'start : time.
  forall T'expire : time.
  forall L2 : time.
  forall N2 : nonce.
    net(S & enc Kag (U & C & G & Kcg & Tstart & Texpire) & enc Kcg (C & T) & L2 & N2)
   => exists Kcs : stk C S.
      net(U & enc Kcg (U & C & G & S & Kcs & T'start & T'expire) & enc Kcg (S & Kcs & T'start & T'expire & N2)) if clock T.

}

initiatorClient3:
forall C : client.
{
			exists C3 : {S : server} stk C S -> time -> state.
KRule7:
  forall U : princ.
  forall G : TGS.
  forall S : server.
  forall Kcg : stk C G.
  forall T'start : time.
  forall T' : time.
  forall Kcs : stk C S.
  forall T'expire : time.
  TGT' U T'start T'expire C S Kcs
  => net(enc Kcg (U & C & G & S & Kcs & T'start & T'expire) & enc Kcs (C & T')), C3 S Kcs T' if clock T'.

KRUle8: 
  forall S : server.
  forall Kcs : stk C S.
  forall T' : time.
    net(enc Kcs T'), C3 S Kcs T'
  => empty.
}

server:
forall S : server.
{

KRule9:
  
  forall U : princ.
  forall G : TGS.
  forall S : server.
  forall Kcg : stk C G.
  forall T'start : time.
  forall T' : time.
  forall Kcs : stk C S.
  forall T'expire : time.
  forall C : client.
   net(enc Kcg (U & C & G & S & Kcs & T'start & T'expire) & enc Kcs (C & T'))
  => net(enc Kcs T').
}
)
 

Findings

A very good example of how MSR handles repetition. It took time to only understand the concept. But once cleared, representing kerberos didn't take much time.