(*  Title:      HOL/Auth/Kerberos_BAN

     ID:         $Id$

     Author:     Giampaolo Bella, Cambridge University Computer Laboratory

     Copyright   1998  University of Cambridge

 The Kerberos protocol, BAN version.

 From page 251 of

   Burrows, Abadi and Needham.  A Logic of Authentication.

   Proc. Royal Soc. 426 (1989)

 *)

 Kerberos_BAN = Shared + 

 (* Temporal modelization: session keys can be leaked 

                           ONLY when they have expired *)

 syntax

     CT :: event list=>nat

     Expired :: [nat, event list] => bool

     RecentAuth :: [nat, event list] => bool

 consts

     (*Duration of the session key*)

     SesKeyLife   :: nat

     (*Duration of the authenticator*)

     AutLife :: nat

 rules

     (*The ticket should remain fresh for two journeys on the network at least*)

     SesKeyLife_LB "# 2 <= SesKeyLife"

     (*The authenticator only for one journey*)

     AutLife_LB    "Suc 0 <= AutLife"

 translations

    "CT" == "length"

    "Expired T evs" == "SesKeyLife + T < CT evs"

    "RecentAuth T evs" == "CT evs <= AutLife + T"

 consts  kerberos_ban   :: event list set

 inductive "kerberos_ban"

   intrs 

     Nil  "[] \\<in> kerberos_ban"

     Fake "[| evsf \\<in> kerberos_ban;  X \\<in> synth (analz (spies evsf)) |]

           ==> Says Spy B X # evsf \\<in> kerberos_ban"

     Kb1  "[| evs1 \\<in> kerberos_ban |]

           ==> Says A Server {|Agent A, Agent B|} # evs1

                 \\<in>  kerberos_ban"

     Kb2  "[| evs2 \\<in> kerberos_ban;  Key KAB \\<notin> used evs2;

              Says A' Server {|Agent A, Agent B|} \\<in> set evs2 |]

           ==> Says Server A 

                 (Crypt (shrK A)

                    {|Number (CT evs2), Agent B, Key KAB,  

                     (Crypt (shrK B) {|Number (CT evs2), Agent A, Key KAB|})|}) 

                 # evs2 \\<in> kerberos_ban"

     Kb3  "[| evs3 \\<in> kerberos_ban;  

              Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) 

                \\<in> set evs3;

              Says A Server {|Agent A, Agent B|} \\<in> set evs3;

              ~ Expired Ts evs3 |]

           ==> Says A B {|X, Crypt K {|Agent A, Number (CT evs3)|} |} 

                # evs3 \\<in> kerberos_ban"

     Kb4  "[| evs4 \\<in> kerberos_ban;  

              Says A' B {|(Crypt (shrK B) {|Number Ts, Agent A, Key K|}), 

 		         (Crypt K {|Agent A, Number Ta|}) |}: set evs4;

              ~ Expired Ts evs4;  RecentAuth Ta evs4 |]

           ==> Says B A (Crypt K (Number Ta)) # evs4

                 \\<in> kerberos_ban"

          (*Old session keys may become compromised*)

     Oops "[| evso \\<in> kerberos_ban;  

              Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})

                \\<in> set evso;

              Expired Ts evso |]

           ==> Notes Spy {|Number Ts, Key K|} # evso \\<in> kerberos_ban"

 end