src/HOL/Auth/Kerberos_BAN.thy
changeset 5434 9b4bed3f394c
parent 5053 75d20f367e94
child 11185 1b737b4c2108
     1.1 --- a/src/HOL/Auth/Kerberos_BAN.thy	Tue Sep 08 14:54:21 1998 +0200
     1.2 +++ b/src/HOL/Auth/Kerberos_BAN.thy	Tue Sep 08 15:17:11 1998 +0200
     1.3 @@ -48,18 +48,16 @@
     1.4  
     1.5      Nil  "[]: kerberos_ban"
     1.6  
     1.7 -
     1.8 -    Fake "[| evs: kerberos_ban;  B ~= Spy;  
     1.9 -             X: synth (analz (spies evs)) |]
    1.10 +    Fake "[| evs: kerberos_ban;  X: synth (analz (spies evs)) |]
    1.11            ==> Says Spy B X # evs : kerberos_ban"
    1.12  
    1.13  
    1.14 -    Kb1  "[| evs1: kerberos_ban;  A ~= Server |]
    1.15 +    Kb1  "[| evs1: kerberos_ban |]
    1.16            ==> Says A Server {|Agent A, Agent B|} # evs1
    1.17                  :  kerberos_ban"
    1.18  
    1.19  
    1.20 -    Kb2  "[| evs2: kerberos_ban;  A ~= B;  A ~= Server;  Key KAB ~: used evs2;
    1.21 +    Kb2  "[| evs2: kerberos_ban;  Key KAB ~: used evs2;
    1.22               Says A' Server {|Agent A, Agent B|} : set evs2 |]
    1.23            ==> Says Server A 
    1.24                  (Crypt (shrK A)
    1.25 @@ -68,7 +66,7 @@
    1.26                  # evs2 : kerberos_ban"
    1.27  
    1.28  
    1.29 -    Kb3  "[| evs3: kerberos_ban;  A ~= B; 
    1.30 +    Kb3  "[| evs3: kerberos_ban;  
    1.31               Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) 
    1.32                 : set evs3;
    1.33               Says A Server {|Agent A, Agent B|} : set evs3;
    1.34 @@ -77,21 +75,19 @@
    1.35                 # evs3 : kerberos_ban"
    1.36  
    1.37  
    1.38 -    Kb4  "[| evs4: kerberos_ban;  A ~= B;  
    1.39 +    Kb4  "[| evs4: kerberos_ban;  
    1.40               Says A' B {|(Crypt (shrK B) {|Number Ts, Agent A, Key K|}), 
    1.41  		         (Crypt K {|Agent A, Number Ta|}) |}: set evs4;
    1.42 -             ~ Expired Ts evs4; 
    1.43 -             RecentAuth Ta evs4|]
    1.44 +             ~ Expired Ts evs4;  RecentAuth Ta evs4 |]
    1.45            ==> Says B A (Crypt K (Number Ta)) # evs4
    1.46                  : kerberos_ban"
    1.47  
    1.48 -
    1.49 -(*The session key has EXPIRED when it gets lost *)
    1.50 -    Oops "[| evso: kerberos_ban;  A ~= Spy;
    1.51 +         (*Old session keys may become compromised*)
    1.52 +    Oops "[| evso: kerberos_ban;  
    1.53               Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
    1.54                 : set evso;
    1.55               Expired Ts evso |]
    1.56 -          ==> Says A Spy {|Number Ts, Key K|} # evso : kerberos_ban"
    1.57 +          ==> Notes Spy {|Number Ts, Key K|} # evso : kerberos_ban"
    1.58  
    1.59  
    1.60  end