\||||||||||||||||||/
                   --- Welcome to Maude ---
                     /||||||||||||||||||\
            Maude alpha84c built: Jun 22 2004 15:35:45
             Copyright 1997-2004 SRI International
                   Fri Oct 15 21:40:15 2004

*** 168 tests succeeded - MSR Prototype ready ***

Maude> in examples/kerberos.msr
context reset
context extended: {KAS : type}%enum
context extended: {server : type}%enum
context extended: {tcs : type}
context extended: {ts : type}
context extended: {TGS : type}
context extended: {client : type}
context extended: {KAS-princ : KAS <: princ}
context extended: {tcs-princ : tcs <: princ}
context extended: {ts-tcs : ts <: tcs}
context extended: {TGS-ts : TGS <: ts}
context extended: {server-ts : server <: ts}
context extended: {client-tcs : client <: tcs}
context extended: {key : type}
context extended: {dbK : tcs -> type}%enum
context extended: {shK : client -> ts -> type}
context extended: {dbK-key : {A | tcs} dbK A <: key}
context extended: {shK-key : {C | client} {A | ts} shK C A <: key}
context extended: {shK-msg : {C | client} {A | ts} shK C A <: msg}
context extended: {time : type}
context extended: {time-msg : time <: msg}
context extended: {encrypt : key -> msg -> msg}
context extended: {Auth : {C : client} msg ->{T : TGS} shK C(TGS-ts T)-> state}
context extended: {Service : {C : client} msg ->{S : server} shK C(server-ts S)-> state}
context extended: {Mem : {S : server} {C : client} shK C(server-ts S)-> time -> state}
context extended: {DoneMut : {C : client} {S : server} shK C(server-ts S)-> state}
context extended: {START-ASE : client -> TGS -> state}
context extended: {START-TGE : client -> state}
context extended: {START-CSE : client -> state}

role defined
clientASE : forall C : client . {
 exists L : client -> TGS -> nonce -> state .
 req :
  forall T : TGS .
  START-ASE C T
  => exists n1 : nonce .
     N(princ-msg(tcs-princ(client-tcs C))& princ-msg(tcs-princ(ts-tcs(TGS-ts T)))& nonce-msg n1),L C T n1 .
 resp :
  forall X : msg .
  forall T : TGS .
  forall kC : dbK(client-tcs C).
  forall AKey : shK C(TGS-ts T).
  forall n1 : nonce .
  N(princ-msg(tcs-princ(client-tcs C))& X & encrypt(dbK-key kC)(shK-msg AKey & nonce-msg n1 & princ-msg(tcs-princ(ts-tcs(
    TGS-ts T))))),L C T n1
  => Auth C X T AKey .
}

role defined
serverASE : forall K : KAS . {
 answer :
  forall C : client .
  forall T : TGS .
  forall n1 : nonce .
  forall kC : dbK(client-tcs C).
  forall kT : dbK(ts-tcs(TGS-ts T)).
  N(princ-msg(tcs-princ(client-tcs C))& princ-msg(tcs-princ(ts-tcs(TGS-ts T)))& nonce-msg n1)
  => exists AKey : shK C(TGS-ts T).
     N(princ-msg(tcs-princ(client-tcs C))& encrypt(dbK-key kT)(shK-msg AKey & princ-msg(tcs-princ(client-tcs C)))& encrypt(
    dbK-key kC)(shK-msg AKey & nonce-msg n1 & princ-msg(tcs-princ(ts-tcs(TGS-ts T))))).
}

role defined
clientTGE : forall C : client . {
 exists L : client -> server -> TGS -> nonce -> state .
 req :
  forall T : TGS .
  forall S : server .
  forall AKey : shK C(TGS-ts T).
  forall X : msg .
  Auth C X T AKey ; START-TGE C
  => exists n2 : nonce .
     N(X & encrypt(shK-key AKey)(princ-msg(tcs-princ(client-tcs C)))& princ-msg(tcs-princ(client-tcs C))& princ-msg(
    tcs-princ(ts-tcs(server-ts S)))& nonce-msg n2),L C S T n2 .
 resp :
  forall T : TGS .
  forall S : server .
  forall SKey : shK C(server-ts S).
  forall AKey : shK C(TGS-ts T).
  forall Y : msg .
  forall n2 : nonce .
  N(princ-msg(tcs-princ(client-tcs C))& Y & encrypt(shK-key AKey)(shK-msg SKey & nonce-msg n2 & princ-msg(tcs-princ(ts-tcs(
    server-ts S))))),L C S T n2
  => Service C Y S SKey .
}

role defined
serverTGE : forall T : TGS . {
 answer :
  forall C : client .
  forall S : server .
  forall AKey : shK C(TGS-ts T).
  forall kT : dbK(ts-tcs(TGS-ts T)).
  forall kS : dbK(ts-tcs(server-ts S)).
  forall n2 : nonce .
  N(encrypt(dbK-key kT)(shK-msg AKey & princ-msg(tcs-princ(client-tcs C)))& encrypt(shK-key AKey)(princ-msg(tcs-princ(
    client-tcs C)))& princ-msg(tcs-princ(client-tcs C))& princ-msg(tcs-princ(ts-tcs(server-ts S)))& nonce-msg n2)
  => exists SKey : shK C(server-ts S).
     N(princ-msg(tcs-princ(client-tcs C))& encrypt(dbK-key kS)(shK-msg SKey & princ-msg(tcs-princ(client-tcs C)))& encrypt(
    shK-key AKey)(shK-msg SKey & nonce-msg n2 & princ-msg(tcs-princ(ts-tcs(server-ts S))))).
}

role defined
clientCSE : forall C : client . {
 exists L : {C : client} {S : server} shK C(server-ts S)-> time -> msg -> state .
 req :
  forall S : server .
  forall SKey : shK C(server-ts S).
  forall Y : msg .
  START-CSE C,Service C Y S SKey
  => exists t : time .
     Service C Y S SKey,N(Y & encrypt(shK-key SKey)(princ-msg(tcs-princ(client-tcs C))& time-msg t)),L C S SKey t Y .
 resp :
  forall S : server .
  forall SKey : shK C(server-ts S).
  forall t : time .
  forall Y : msg .
  N(encrypt(shK-key SKey)(time-msg t)),L C S SKey t Y
  => DoneMut C S SKey .
}

role defined
serverCSE : forall S : server . {
 answer :
  forall C : client .
  forall SKey : shK C(server-ts S).
  forall t : time .
  forall kS : dbK(ts-tcs(server-ts S)).
  forall X : msg .
  N(encrypt(dbK-key kS)X & encrypt(shK-key SKey)(princ-msg(tcs-princ(client-tcs C))& time-msg t))
  => N(encrypt(shK-key SKey)(time-msg t)),Mem S C SKey t .
}
context extended: {C : client}
context extended: {AS : KAS}
context extended: {TS : TGS}
context extended: {S : server}
context extended: {kC : dbK(client-tcs C)}
context extended: {kTS : dbK(ts-tcs(TGS-ts TS))}
context extended: {kS : dbK(ts-tcs(server-ts S))}
config: START-ASE C TS,START-TGE C,START-CSE C