src/HOL/Auth/OtwayRees_AN.ML
changeset 3683 aafe719dff14
parent 3674 65ec38fbb265
child 3730 6933d20f335f
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Wed Sep 17 16:40:52 1997 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Thu Sep 18 13:24:04 1997 +0200
     1.3 @@ -44,36 +44,36 @@
     1.4  (** For reasoning about the encrypted portion of messages **)
     1.5  
     1.6  goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \
     1.7 -\                X : analz (sees Spy evs)";
     1.8 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
     1.9 -qed "OR4_analz_sees_Spy";
    1.10 +\                X : analz (spies evs)";
    1.11 +by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1);
    1.12 +qed "OR4_analz_spies";
    1.13  
    1.14  goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
    1.15 -\                  : set evs ==> K : parts (sees Spy evs)";
    1.16 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
    1.17 -qed "Oops_parts_sees_Spy";
    1.18 +\                  : set evs ==> K : parts (spies evs)";
    1.19 +by (blast_tac (!claset addSEs spies_partsEs) 1);
    1.20 +qed "Oops_parts_spies";
    1.21  
    1.22 -(*OR4_analz_sees_Spy lets us treat those cases using the same 
    1.23 +(*OR4_analz_spies lets us treat those cases using the same 
    1.24    argument as for the Fake case.  This is possible for most, but not all,
    1.25    proofs, since Fake messages originate from the Spy. *)
    1.26  
    1.27 -bind_thm ("OR4_parts_sees_Spy",
    1.28 -          OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    1.29 +bind_thm ("OR4_parts_spies",
    1.30 +          OR4_analz_spies RS (impOfSubs analz_subset_parts));
    1.31  
    1.32 -(*For proving the easier theorems about X ~: parts (sees Spy evs).*)
    1.33 +(*For proving the easier theorems about X ~: parts (spies evs).*)
    1.34  fun parts_induct_tac i = 
    1.35      etac otway.induct i			THEN 
    1.36 -    forward_tac [Oops_parts_sees_Spy] (i+6) THEN
    1.37 -    forward_tac [OR4_parts_sees_Spy]  (i+5) THEN
    1.38 +    forward_tac [Oops_parts_spies] (i+6) THEN
    1.39 +    forward_tac [OR4_parts_spies]  (i+5) THEN
    1.40      prove_simple_subgoals_tac  i;
    1.41  
    1.42  
    1.43 -(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
    1.44 +(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
    1.45      sends messages containing X! **)
    1.46  
    1.47 -(*Spy never sees another agent's shared key! (unless it's lost at start)*)
    1.48 +(*Spy never sees another agent's shared key! (unless it's bad at start)*)
    1.49  goal thy 
    1.50 - "!!evs. evs : otway ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
    1.51 + "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    1.52  by (parts_induct_tac 1);
    1.53  by (Fake_parts_insert_tac 1);
    1.54  by (Blast_tac 1);
    1.55 @@ -81,13 +81,12 @@
    1.56  Addsimps [Spy_see_shrK];
    1.57  
    1.58  goal thy 
    1.59 - "!!evs. evs : otway ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
    1.60 + "!!evs. evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
    1.61  by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
    1.62  qed "Spy_analz_shrK";
    1.63  Addsimps [Spy_analz_shrK];
    1.64  
    1.65 -goal thy  "!!A. [| Key (shrK A) : parts (sees Spy evs);       \
    1.66 -\                  evs : otway |] ==> A:lost";
    1.67 +goal thy  "!!A. [| Key (shrK A) : parts (spies evs); evs : otway |] ==> A:bad";
    1.68  by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
    1.69  qed "Spy_see_shrK_D";
    1.70  
    1.71 @@ -97,7 +96,7 @@
    1.72  
    1.73  (*Nobody can have used non-existent keys!*)
    1.74  goal thy "!!evs. evs : otway ==>          \
    1.75 -\         Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
    1.76 +\         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
    1.77  by (parts_induct_tac 1);
    1.78  (*Fake*)
    1.79  by (best_tac
    1.80 @@ -135,8 +134,8 @@
    1.81  
    1.82  
    1.83  (*For proofs involving analz.*)
    1.84 -val analz_sees_tac = 
    1.85 -    dtac OR4_analz_sees_Spy 6 THEN
    1.86 +val analz_spies_tac = 
    1.87 +    dtac OR4_analz_spies 6 THEN
    1.88      forward_tac [Says_Server_message_form] 7 THEN
    1.89      assume_tac 7 THEN
    1.90      REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
    1.91 @@ -145,8 +144,8 @@
    1.92  (****
    1.93   The following is to prove theorems of the form
    1.94  
    1.95 -  Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
    1.96 -  Key K : analz (sees Spy evs)
    1.97 +  Key K : analz (insert (Key KAB) (spies evs)) ==>
    1.98 +  Key K : analz (spies evs)
    1.99  
   1.100   A more general formula must be proved inductively.
   1.101  ****)
   1.102 @@ -158,10 +157,10 @@
   1.103  goal thy  
   1.104   "!!evs. evs : otway ==>                                    \
   1.105  \  ALL K KK. KK <= Compl (range shrK) -->                   \
   1.106 -\            (Key K : analz (Key``KK Un (sees Spy evs))) =  \
   1.107 -\            (K : KK | Key K : analz (sees Spy evs))";
   1.108 +\            (Key K : analz (Key``KK Un (spies evs))) =  \
   1.109 +\            (K : KK | Key K : analz (spies evs))";
   1.110  by (etac otway.induct 1);
   1.111 -by analz_sees_tac;
   1.112 +by analz_spies_tac;
   1.113  by (REPEAT_FIRST (resolve_tac [allI, impI]));
   1.114  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
   1.115  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   1.116 @@ -174,8 +173,8 @@
   1.117  
   1.118  goal thy
   1.119   "!!evs. [| evs : otway;  KAB ~: range shrK |] ==>          \
   1.120 -\        Key K : analz (insert (Key KAB) (sees Spy evs)) =  \
   1.121 -\        (K = KAB | Key K : analz (sees Spy evs))";
   1.122 +\        Key K : analz (insert (Key KAB) (spies evs)) =  \
   1.123 +\        (K = KAB | Key K : analz (spies evs))";
   1.124  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   1.125  qed "analz_insert_freshK";
   1.126  
   1.127 @@ -198,7 +197,7 @@
   1.128  by (expand_case_tac "K = ?y" 1);
   1.129  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   1.130  (*...we assume X is a recent message and handle this case by contradiction*)
   1.131 -by (blast_tac (!claset addSEs sees_Spy_partsEs
   1.132 +by (blast_tac (!claset addSEs spies_partsEs
   1.133                         delrules[conjI] (*prevent splitup into 4 subgoals*)) 1);
   1.134  val lemma = result();
   1.135  
   1.136 @@ -223,9 +222,8 @@
   1.137  
   1.138  (*If the encrypted message appears then it originated with the Server!*)
   1.139  goal thy 
   1.140 - "!!evs. [| A ~: lost;  evs : otway |]                 \
   1.141 -\ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}   \
   1.142 -\      : parts (sees Spy evs)                          \
   1.143 + "!!evs. [| A ~: bad;  evs : otway |]                 \
   1.144 +\ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} : parts (spies evs) \
   1.145  \     --> (EX NB. Says Server B                                          \
   1.146  \                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   1.147  \                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   1.148 @@ -243,13 +241,13 @@
   1.149  goal thy 
   1.150   "!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
   1.151  \            : set evs;                                                 \
   1.152 -\           A ~: lost;  evs : otway |]                                  \
   1.153 +\           A ~: bad;  evs : otway |]                                  \
   1.154  \        ==> EX NB. Says Server B                                       \
   1.155  \                    {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},  \
   1.156  \                      Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   1.157  \                   : set evs";
   1.158  by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   1.159 -                      addEs  sees_Spy_partsEs) 1);
   1.160 +                      addEs  spies_partsEs) 1);
   1.161  qed "A_trusts_OR4";
   1.162  
   1.163  
   1.164 @@ -258,15 +256,15 @@
   1.165      the premises, e.g. by having A=Spy **)
   1.166  
   1.167  goal thy 
   1.168 - "!!evs. [| A ~: lost;  B ~: lost;  evs : otway |]                 \
   1.169 + "!!evs. [| A ~: bad;  B ~: bad;  evs : otway |]                 \
   1.170  \        ==> Says Server B                                         \
   1.171  \             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
   1.172  \               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
   1.173  \            : set evs -->                                         \
   1.174  \            Says B Spy {|NA, NB, Key K|} ~: set evs -->           \
   1.175 -\            Key K ~: analz (sees Spy evs)";
   1.176 +\            Key K ~: analz (spies evs)";
   1.177  by (etac otway.induct 1);
   1.178 -by analz_sees_tac;
   1.179 +by analz_spies_tac;
   1.180  by (ALLGOALS
   1.181      (asm_simp_tac (!simpset addcongs [conj_cong, if_weak_cong] 
   1.182                              addsimps [analz_insert_eq, analz_insert_freshK]
   1.183 @@ -276,7 +274,7 @@
   1.184  (*OR4*) 
   1.185  by (Blast_tac 3);
   1.186  (*OR3*)
   1.187 -by (blast_tac (!claset addSEs sees_Spy_partsEs
   1.188 +by (blast_tac (!claset addSEs spies_partsEs
   1.189                         addIs [impOfSubs analz_subset_parts]) 2);
   1.190  (*Fake*) 
   1.191  by (spy_analz_tac 1);
   1.192 @@ -288,8 +286,8 @@
   1.193  \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
   1.194  \             : set evs;                                            \
   1.195  \           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
   1.196 -\           A ~: lost;  B ~: lost;  evs : otway |]                  \
   1.197 -\        ==> Key K ~: analz (sees Spy evs)";
   1.198 +\           A ~: bad;  B ~: bad;  evs : otway |]                  \
   1.199 +\        ==> Key K ~: analz (spies evs)";
   1.200  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.201  by (blast_tac (!claset addSEs [lemma]) 1);
   1.202  qed "Spy_not_see_encrypted_key";
   1.203 @@ -299,9 +297,8 @@
   1.204  
   1.205  (*If the encrypted message appears then it originated with the Server!*)
   1.206  goal thy 
   1.207 - "!!evs. [| B ~: lost;  evs : otway |]                                 \
   1.208 -\    ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}                \
   1.209 -\         : parts (sees Spy evs)                                       \
   1.210 + "!!evs. [| B ~: bad;  evs : otway |]                                 \
   1.211 +\    ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} : parts (spies evs) \
   1.212  \        --> (EX NA. Says Server B                                          \
   1.213  \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   1.214  \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   1.215 @@ -317,7 +314,7 @@
   1.216  (*Guarantee for B: if it gets a well-formed certificate then the Server
   1.217    has sent the correct message in round 3.*)
   1.218  goal thy 
   1.219 - "!!evs. [| B ~: lost;  evs : otway;                                        \
   1.220 + "!!evs. [| B ~: bad;  evs : otway;                                        \
   1.221  \           Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   1.222  \            : set evs |]                                                   \
   1.223  \        ==> EX NA. Says Server B                                           \
   1.224 @@ -325,5 +322,5 @@
   1.225  \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   1.226  \                     : set evs";
   1.227  by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   1.228 -                       addEs  sees_Spy_partsEs) 1);
   1.229 +                       addEs  spies_partsEs) 1);
   1.230  qed "B_trusts_OR3";