(reset)
(
--- === An extended model of Kerberos 5 in MSR === ---

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

--- Principals

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

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

--- Encryption types

etype: type.
etype <: msg.

--- Keys

key: etype -> type.
dbK: etype -> tcs -> type.
shK: etype -> client -> ts -> type.

dbK E A <: key E [dbK-key].
shK E C A <: key E [shK-key].
shK E C A <: msg [shK-msg].

--- Timestamps

time: type.
time <: msg.

--- Options

Opt, KOpt, TOpt, SOpt: type.
Opt <: msg.
KOpt <: Opt.
TOpt <: Opt.
SOpt <: Opt.

--- Flags

Flag, TFlag, SFlag: type.
Flag <: msg.
TFlag <: Flag.
SFlag <: Flag.

--- Encryption

encrypt: key E -> msg -> msg.

--- Message digest

digest: key E -> msg -> msg.

--- Message tags

KRB_ERROR: msg.

--- Option predicates (?)

Mutual: SOpt -> state.

--- Memory predicates

Auth:    {C : client} msg -> TFlag -> {T : TGS} shK E C T -> state.
ASError: {C : client} msg -> time -> msg -> KAS -> state.
Service: {C : client} msg -> SFlag -> {S : server} shK E C S -> state.
Clock:   tcs -> time -> state.
Mem:     {S : server} {C : client} shK E C S -> time -> state.
DoneMut: {C : client} {S : server} shK E C S -> state.
TGSError: client -> TGS -> time -> msg -> 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 -> KOpt -> TGS -> nonce -> etype -> state.
  
  req:
    forall e: etype.
    forall T: TGS.
    forall KOpts: KOpt.
    START-ASE C T
    =>
    exists n1: nonce.
    KOpts & C & T & n1 & e,
    L C KOpts T n1 e.
    
  resp:
    forall e: etype.
    forall T: TGS.
    forall kC: dbK e C.
    forall AKey: shK e C T.
    forall X: msg.
    forall n1: nonce.
    forall TFlags: TFlag.
    forall KOpts: KOpt.
    C & X & encrypt kC (AKey & n1 & TFlags & T),
    L C KOpts T n1 e
    =>
    Auth C X TFlags T AKey.
  
  error:
    forall e: etype.
    forall T: TGS.
    forall K: KAS.
    forall ErrorCode: msg.
    forall t: time.
    forall n1: nonce.
    forall KOpts: KOpt.
    KRB_ERROR & t & ErrorCode & C & K,
    L C KOpts T n1 e
    =>
    ASError C KRB_ERROR t ErrorCode K.
})

--- authentication server's role in Authentication Service Exchange
(serverASE: forall K: KAS. {
  answer:
    forall C: client.
    forall T: TGS.
    forall n1: nonce.
    forall e: etype.
    forall kC: dbK e C.
    forall kT: dbK e T.
    forall KOpts: KOpt.
    forall TFlags: TFlag.
    KOpts & C & T & n1 & e
    --- Valid
    --- SetAuthFlags KOpts TFlags
    =>
    exists AKey: shK e C T.
    C & encrypt kT (TFlags & AKey & C) & encrypt kC (AKey & n1 & TFlags & T).
    
  error:
    forall C: client.
    forall T: TGS.
    forall n1: nonce.
    forall ErrorCode: msg.
    forall t: time.
    forall KOpts: KOpt.
    forall e: etype.
    KOpts & C & T & n1 & e
    --- Invalid
    --- Clock
    =>
    KRB_ERROR & t & ErrorCode & C & K.
})

--- client's role in Ticket Granting Exchange
(clientTGE: forall C: client. {
  exists L: client -> TOpt -> server -> TGS -> nonce -> time -> etype -> state.
  
  req:
    forall e: etype.
    forall T: TGS.
    forall S: server.
    forall AKey: shK e C T.
    forall X: msg.
    forall t_req: time.
    forall TFlags: TFlag.
    forall TOpts: TOpt.
    START-TGE C,
    Auth C X TFlags T AKey,
    Clock C t_req
    =>
    exists n2: nonce.
    Auth C X TFlags T AKey,
    X & encrypt AKey (C & encrypt AKey (TOpts & C & S & n2 & e) & t_req) & TOpts & C & S & n2 & e,
    L C TOpts S T n2 t_req e.
    
  resp:
    forall e: etype.
    forall T: TGS.
    forall S: server.
    forall SKey: shK e C S.
    forall AKey: shK e C T.
    forall Y: msg.
    forall n2: nonce.
    forall t_req: time.
    forall SFlags: SFlag.
    forall TOpts: TOpt.
    C & Y & encrypt AKey (SKey & n2 & SFlags & S),
    L C TOpts S T n2 t_req e
    =>
    Service C Y SFlags S SKey.
    
  error:
    forall t_req: time.
    forall t_err: time.
    forall ErrorCode: msg.
    forall T: TGS.
    forall TOpts: TOpt.
    forall S: server.
    forall n2: nonce.
    forall e: etype.
    KRB_ERROR & t_req & t_err & ErrorCode & C & T,
    L C TOpts S T n2 t_req e
    =>
    TGSError C T t_err ErrorCode.
})

--- ticket granting server's role in Ticket Granting Exchange
(serverTGE: forall T: TGS. {
  answer:
    forall e: etype.
    forall C: client.
    forall S: server.
    forall AKey: shK e C T.
    forall kT: dbK e T.
    forall kS: dbK e S.
    forall n2: nonce.
    forall TFlags: TFlag.
    forall t_req: time.
    forall TOpts: TOpt.
    forall SFlags: SFlag.
    encrypt kT (TFlags & AKey & C) & encrypt AKey (C &
      ***(ck) encrypt AKey (TOpts & C & S & n2 & e)
      & t_req) & TOpts & C & S & n2 & e
    --- Valid
    --- SetServFlags
    =>
    exists SKey: shK e C S.
    C & encrypt kS (SFlags & SKey & C) & encrypt AKey (SKey & n2 & SFlags & S).
    
  error:
    forall t_req: time.
    forall t_err: time.
    forall ErrorCode: msg.
    forall C: client.
    forall S: server.
    forall T: TGS.
    forall TOpts: TOpt.
    forall n2: nonce.
    forall e: etype.
    forall kT: dbK e T.
    forall AKey: shK e C T.
    forall TFlags: TFlag.
    encrypt kT (TFlags & AKey & C) & encrypt AKey (C &
      ***(ck) encrypt AKey (TOpts & C & S & n2 & e)
      & t_req) & TOpts & C & S & n2 & e,
    --- Invalid
    Clock T t_err
    =>
    KRB_ERROR & t_req & t_err & ErrorCode & C & T.
    
})

--- client's role in Client/Server exchange
(clientCSE: forall C: client. {
  exists L: {C : client} SOpt -> {S : server} shK C S -> time -> msg -> state.
  
  req:
    forall e: etype.
    forall S: server.
    forall SKey: shK e C S.
    forall t: time.
    forall Y: msg.
    forall SFlags: SFlag.
    forall SOpts: SOpt.
    START-CSE C,
    Service C Y SFlags S SKey,
    Clock C t
    Mutual SOpts
    =>
    Service C Y SFlags S SKey,
    SOpts & Y & encrypt SKey (C & encrypt SKey ... & t),
    L C SOpts 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.
)

***(occ)