src/HOL/Auth/Kerberos_BAN.thy
changeset 5053 75d20f367e94
child 5434 9b4bed3f394c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Auth/Kerberos_BAN.thy	Fri Jun 19 10:34:33 1998 +0200
     1.3 @@ -0,0 +1,97 @@
     1.4 +(*  Title:      HOL/Auth/Kerberos_BAN
     1.5 +    ID:         $Id$
     1.6 +    Author:     Giampaolo Bella, Cambridge University Computer Laboratory
     1.7 +    Copyright   1998  University of Cambridge
     1.8 +
     1.9 +The Kerberos protocol, BAN version.
    1.10 +
    1.11 +From page 251 of
    1.12 +  Burrows, Abadi and Needham.  A Logic of Authentication.
    1.13 +  Proc. Royal Soc. 426 (1989)
    1.14 +*)
    1.15 +
    1.16 +Kerberos_BAN = Shared + 
    1.17 +
    1.18 +(* Temporal modelization: session keys can be leaked 
    1.19 +                          ONLY when they have expired *)
    1.20 +
    1.21 +syntax
    1.22 +    CT :: event list=>nat
    1.23 +    Expired :: [nat, event list] => bool
    1.24 +    RecentAuth :: [nat, event list] => bool
    1.25 +
    1.26 +consts
    1.27 +
    1.28 +    (*Duration of the session key*)
    1.29 +    SesKeyLife   :: nat
    1.30 +
    1.31 +    (*Duration of the authenticator*)
    1.32 +    AutLife :: nat
    1.33 +
    1.34 +rules
    1.35 +    (*The ticket should remain fresh for two journeys on the network at least*)
    1.36 +    SesKeyLife_LB    "2 <= SesKeyLife"
    1.37 +
    1.38 +    (*The authenticator only for one journey*)
    1.39 +    AutLife_LB    "1 <= AutLife"
    1.40 +
    1.41 +translations
    1.42 +   "CT" == "length"
    1.43 +  
    1.44 +   "Expired T evs" == "SesKeyLife + T < CT evs"
    1.45 +
    1.46 +   "RecentAuth T evs" == "CT evs <= AutLife + T"
    1.47 +
    1.48 +consts  kerberos_ban   :: event list set
    1.49 +inductive "kerberos_ban"
    1.50 +  intrs 
    1.51 +
    1.52 +    Nil  "[]: kerberos_ban"
    1.53 +
    1.54 +
    1.55 +    Fake "[| evs: kerberos_ban;  B ~= Spy;  
    1.56 +             X: synth (analz (spies evs)) |]
    1.57 +          ==> Says Spy B X # evs : kerberos_ban"
    1.58 +
    1.59 +
    1.60 +    Kb1  "[| evs1: kerberos_ban;  A ~= Server |]
    1.61 +          ==> Says A Server {|Agent A, Agent B|} # evs1
    1.62 +                :  kerberos_ban"
    1.63 +
    1.64 +
    1.65 +    Kb2  "[| evs2: kerberos_ban;  A ~= B;  A ~= Server;  Key KAB ~: used evs2;
    1.66 +             Says A' Server {|Agent A, Agent B|} : set evs2 |]
    1.67 +          ==> Says Server A 
    1.68 +                (Crypt (shrK A)
    1.69 +                   {|Number (CT evs2), Agent B, Key KAB,  
    1.70 +                    (Crypt (shrK B) {|Number (CT evs2), Agent A, Key KAB|})|}) 
    1.71 +                # evs2 : kerberos_ban"
    1.72 +
    1.73 +
    1.74 +    Kb3  "[| evs3: kerberos_ban;  A ~= B; 
    1.75 +             Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) 
    1.76 +               : set evs3;
    1.77 +             Says A Server {|Agent A, Agent B|} : set evs3;
    1.78 +             ~ Expired Ts evs3 |]
    1.79 +          ==> Says A B {|X, Crypt K {|Agent A, Number (CT evs3)|} |} 
    1.80 +               # evs3 : kerberos_ban"
    1.81 +
    1.82 +
    1.83 +    Kb4  "[| evs4: kerberos_ban;  A ~= B;  
    1.84 +             Says A' B {|(Crypt (shrK B) {|Number Ts, Agent A, Key K|}), 
    1.85 +		         (Crypt K {|Agent A, Number Ta|}) |}: set evs4;
    1.86 +             ~ Expired Ts evs4; 
    1.87 +             RecentAuth Ta evs4|]
    1.88 +          ==> Says B A (Crypt K (Number Ta)) # evs4
    1.89 +                : kerberos_ban"
    1.90 +
    1.91 +
    1.92 +(*The session key has EXPIRED when it gets lost *)
    1.93 +    Oops "[| evso: kerberos_ban;  A ~= Spy;
    1.94 +             Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
    1.95 +               : set evso;
    1.96 +             Expired Ts evso |]
    1.97 +          ==> Says A Spy {|Number Ts, Key K|} # evso : kerberos_ban"
    1.98 +
    1.99 +
   1.100 +end