(reset)
(
--- === A simplified model of Kerberos 5 in MSR === ---

--- nonce, msg, princ are predefined in MSR prelude 

--- Principals

KAS: type. %enum
server: type. %enum
tcs, ts, TGS, client: type.

KAS <: princ.
tcs <: princ.
ts <: tcs.
TGS <: ts.
server <: ts.
client <: tcs.

--- Keys

key: type.
dbK: tcs -> type. %enum
shK: client -> ts -> type.

dbK A <: key.
shK C A <: key.
shK C A <: msg.

--- Timestamps

time: type.
time <: msg.

--- Encryption

encrypt: key -> msg -> msg.

--- Memory predicates

Auth:    {C : client} msg -> {T : TGS} shK C T -> state.
Service: {C : client} msg -> {S : server} shK C S -> state.
--- Clock:   {C : client} time -> state.
Mem:     {S : server} {C : client} shK C S -> time -> state.
DoneMut: {C : client} {S : server} shK C S -> state.

--- Start/end tags
START-ASE: client -> TGS -> state.
START-TGE: client -> state.
START-CSE: client -> state.

--- client's role in Authentication Service Exchange
clientASE: forall C: client. {
  exists L: client -> TGS -> nonce -> state.
  
  req:
    forall T: TGS.
    START-ASE C T
    =>
    exists n1: nonce.
    C & T & n1, L C T n1.
    
  resp:
    forall T: TGS.
    forall kC: dbK C.
    forall AKey: shK C T.
    forall n1: nonce.
    C & X & encrypt kC (AKey & n1 & T), L C T n1
    =>
    Auth C X T AKey.
}

--- authentication server's role in Authentication Service Exchange
serverASE: forall K: KAS. {
  answer:
    forall C: client.
    forall T: TGS.
    forall n1: nonce.
    forall kC: dbK C.
    forall kT: dbK T.
    C & T & n1
    =>
    exists AKey: shK C T.
    C & encrypt kT (AKey & C) & encrypt kC (AKey & n1 & T).
}

--- client's role in Ticket Granting Exchange
clientTGE: forall C: client. {
  exists L: client -> server -> TGS -> nonce -> state.
  
  req:
    forall T: TGS.
    forall S: server.
    forall AKey: shK C T.
    forall X: msg.
    Auth C X T AKey;
    START-TGE C
    =>
    exists n2: nonce.
    X & encrypt AKey C & C & S & n2,
    L C S T n2.
    
  resp:
    forall T: TGS.
    forall S: server.
    forall SKey: shK C S.
    forall AKey: shK C T.
    forall Y: msg.
    forall n2: nonce.
    C & Y & encrypt AKey (SKey & n2 & S),
    L C S T n2
    =>
    Service C Y S SKey.
}

--- ticket granting server's role in Ticket Granting Exchange
serverTGE: forall T: TGS. {
  answer:
    forall C: client.
    forall S: server.
    forall AKey: shK C T.
    forall kT: dbK T.
    forall kS: dbK S.
    forall n2: nonce.
    encrypt kT (AKey & C) & encrypt AKey C & C & S & n2
    =>
    exists SKey: shK C S.
    C & encrypt kS (SKey & C) & encrypt AKey (SKey & n2 & S).
}

--- client's role in Client/Server exchange
clientCSE: forall C: client. {
  exists L: {C : client} {S : server} shK C S -> time -> msg -> state.
  
  req:
    forall S: server.
    forall SKey: shK C S.
    --- forall t: time.
    forall Y: msg.
    START-CSE C,
    Service C Y S SKey ***(,
    Clock C t)
    =>
    exists t: time.
    Service C Y S SKey,
    Y & encrypt SKey (C & t),
    L C S SKey t Y.
    
  resp:
    forall S: server.
    forall SKey: shK C S.
    forall t: time.
    forall Y: msg.
    encrypt SKey t,
    L C S SKey t Y
    =>
    DoneMut C S SKey.
}

--- server's role in Client/Server exchange
serverCSE: forall S: server. {
  answer:
    forall C: client.
    forall SKey: shK C S.
    forall t: time.
    forall kS: dbK S.
    forall X: msg.
    encrypt kS X & encrypt SKey (C & t)
    =>
    encrypt SKey t,
    Mem S C SKey t.
}

--- Example configuration

C: client.
AS: KAS.
TS: TGS.
S: server.
kC: dbK C.
kTS: dbK TS.
kS: dbK S.

config START-ASE C TS, START-TGE C, START-CSE C.    
)