src/HOL/Auth/OtwayRees_AN.ML
changeset 2516 4d68fbe6378b
parent 2454 92f43ed48935
child 2637 e9b203f854ae
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Fri Jan 17 11:50:09 1997 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Fri Jan 17 12:49:31 1997 +0100
     1.3 @@ -26,9 +26,7 @@
     1.4  \             : set_of_list evs";
     1.5  by (REPEAT (resolve_tac [exI,bexI] 1));
     1.6  by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
     1.7 -by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
     1.8 -by (REPEAT_FIRST (resolve_tac [refl, conjI]));
     1.9 -by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver))));
    1.10 +by possibility_tac;
    1.11  result();
    1.12  
    1.13  
    1.14 @@ -54,15 +52,14 @@
    1.15  
    1.16  (** For reasoning about the encrypted portion of messages **)
    1.17  
    1.18 -goal thy "!!evs. Says S B {|X, X'|} : set_of_list evs ==> \
    1.19 +goal thy "!!evs. Says S B {|X, Crypt(shrK B) X'|} : set_of_list evs ==> \
    1.20  \                X : analz (sees lost Spy evs)";
    1.21  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    1.22  qed "OR4_analz_sees_Spy";
    1.23  
    1.24  goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
    1.25  \                  : set_of_list evs ==> K : parts (sees lost Spy evs)";
    1.26 -by (fast_tac (!claset addSEs partsEs
    1.27 -                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    1.28 +by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
    1.29  qed "Oops_parts_sees_Spy";
    1.30  
    1.31  (*OR4_analz_sees_Spy lets us treat those cases using the same 
    1.32 @@ -81,9 +78,9 @@
    1.33  (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    1.34  fun parts_induct_tac i = SELECT_GOAL
    1.35      (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN
    1.36 -	     (*Fake message*)
    1.37 -	     TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    1.38 -					   impOfSubs Fake_parts_insert]
    1.39 +             (*Fake message*)
    1.40 +             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    1.41 +                                           impOfSubs Fake_parts_insert]
    1.42                                      addss (!simpset)) 2)) THEN
    1.43       (*Base case*)
    1.44       fast_tac (!claset addss (!simpset)) 1 THEN
    1.45 @@ -117,49 +114,18 @@
    1.46  AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
    1.47  
    1.48  
    1.49 -(*** Future keys can't be seen or used! ***)
    1.50 -
    1.51 -(*Nobody can have SEEN keys that will be generated in the future. *)
    1.52 -goal thy "!!i. evs : otway lost ==>             \
    1.53 -\              length evs <= i --> Key(newK i) ~: parts (sees lost Spy evs)";
    1.54 +(*Nobody can have used non-existent keys!*)
    1.55 +goal thy "!!evs. evs : otway lost ==>          \
    1.56 +\         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
    1.57  by (parts_induct_tac 1);
    1.58 -by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
    1.59 -				    addDs [impOfSubs analz_subset_parts,
    1.60 -                                           impOfSubs parts_insert_subset_Un,
    1.61 -                                           Suc_leD]
    1.62 -                                    addss (!simpset))));
    1.63 -qed_spec_mp "new_keys_not_seen";
    1.64 -Addsimps [new_keys_not_seen];
    1.65 -
    1.66 -(*Variant: old messages must contain old keys!*)
    1.67 -goal thy 
    1.68 - "!!evs. [| Says A B X : set_of_list evs;          \
    1.69 -\           Key (newK i) : parts {X};              \
    1.70 -\           evs : otway lost                       \
    1.71 -\        |] ==> i < length evs";
    1.72 -by (rtac ccontr 1);
    1.73 -by (dtac leI 1);
    1.74 -by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
    1.75 -                      addIs  [impOfSubs parts_mono]) 1);
    1.76 -qed "Says_imp_old_keys";
    1.77 -
    1.78 -
    1.79 -(*Nobody can have USED keys that will be generated in the future.
    1.80 -  ...very like new_keys_not_seen*)
    1.81 -goal thy "!!i. evs : otway lost ==>          \
    1.82 -\           length evs <= i --> newK i ~: keysFor (parts (sees lost Spy evs))";
    1.83 -by (parts_induct_tac 1);
    1.84 -(*Fake, OR4: these messages send unknown (X) components*)
    1.85 -by (EVERY
    1.86 -    (map 
    1.87 -     (best_tac
    1.88 -      (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
    1.89 -                      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
    1.90 -                      Suc_leD]
    1.91 -               addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
    1.92 -               addss (!simpset))) [5,1]));
    1.93 -(*Remaining subgoals*)
    1.94 -by (REPEAT (fast_tac (!claset addDs [Suc_leD] addss (!simpset)) 1));
    1.95 +(*Fake*)
    1.96 +by (best_tac
    1.97 +      (!claset addIs [impOfSubs analz_subset_parts]
    1.98 +               addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
    1.99 +                      impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
   1.100 +               addss (!simpset)) 1);
   1.101 +(*OR3*)
   1.102 +by (fast_tac (!claset addss (!simpset)) 1);
   1.103  qed_spec_mp "new_keys_not_used";
   1.104  
   1.105  bind_thm ("new_keys_not_analzd",
   1.106 @@ -174,12 +140,12 @@
   1.107  
   1.108  (*Describes the form of K and NA when the Server sends this message.*)
   1.109  goal thy 
   1.110 - "!!evs. [| Says Server B \
   1.111 -\           {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                     \
   1.112 -\             Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs; \
   1.113 -\           evs : otway lost |]                                               \
   1.114 -\        ==> (EX n. K = Key(newK n)) &                                        \
   1.115 -\            (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
   1.116 + "!!evs. [| Says Server B                                           \
   1.117 +\              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
   1.118 +\                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
   1.119 +\             : set_of_list evs;                                    \
   1.120 +\           evs : otway lost |]                                     \
   1.121 +\        ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
   1.122  by (etac rev_mp 1);
   1.123  by (etac otway.induct 1);
   1.124  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   1.125 @@ -190,18 +156,17 @@
   1.126  val analz_Fake_tac = 
   1.127      dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
   1.128      forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
   1.129 -    assume_tac 7 THEN Full_simp_tac 7 THEN
   1.130 +    assume_tac 7 THEN
   1.131      REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
   1.132  
   1.133  
   1.134  (****
   1.135   The following is to prove theorems of the form
   1.136  
   1.137 -  Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
   1.138 +  Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
   1.139    Key K : analz (sees lost Spy evs)
   1.140  
   1.141   A more general formula must be proved inductively.
   1.142 -
   1.143  ****)
   1.144  
   1.145  
   1.146 @@ -210,31 +175,28 @@
   1.147  (*The equality makes the induction hypothesis easier to apply*)
   1.148  goal thy  
   1.149   "!!evs. evs : otway lost ==>                                         \
   1.150 -\  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
   1.151 -\           (K : newK``E | Key K : analz (sees lost Spy evs))";
   1.152 +\  ALL K KK. KK <= Compl (range shrK) -->                      \
   1.153 +\            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
   1.154 +\            (K : KK | Key K : analz (sees lost Spy evs))";
   1.155  by (etac otway.induct 1);
   1.156  by analz_Fake_tac;
   1.157 -by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
   1.158 -by (ALLGOALS (*Takes 18 secs*)
   1.159 -    (asm_simp_tac 
   1.160 -     (!simpset addsimps [Un_assoc RS sym, 
   1.161 -			 insert_Key_singleton, insert_Key_image, pushKey_newK]
   1.162 -               setloop split_tac [expand_if])));
   1.163 +by (REPEAT_FIRST (resolve_tac [allI, impI]));
   1.164 +by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
   1.165 +(*14 seconds*)
   1.166 +by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   1.167  (*OR4, Fake*) 
   1.168 -by (EVERY (map spy_analz_tac [4,2]));
   1.169 -(*Oops, OR3, Base*)
   1.170 -by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
   1.171 -qed_spec_mp "analz_image_newK";
   1.172 +by (EVERY (map spy_analz_tac [3,2]));
   1.173 +(*Base*)
   1.174 +by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   1.175 +qed_spec_mp "analz_image_freshK";
   1.176  
   1.177  
   1.178  goal thy
   1.179 - "!!evs. evs : otway lost ==>                                          \
   1.180 -\        Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \
   1.181 -\        (K = newK i | Key K : analz (sees lost Spy evs))";
   1.182 -by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   1.183 -                                   insert_Key_singleton]) 1);
   1.184 -by (Fast_tac 1);
   1.185 -qed "analz_insert_Key_newK";
   1.186 + "!!evs. [| evs : otway lost;  KAB ~: range shrK |] ==>             \
   1.187 +\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
   1.188 +\        (K = KAB | Key K : analz (sees lost Spy evs))";
   1.189 +by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   1.190 +qed "analz_insert_freshK";
   1.191  
   1.192  
   1.193  (*** The Key K uniquely identifies the Server's  message. **)
   1.194 @@ -254,8 +216,8 @@
   1.195  by (Fast_tac 2);
   1.196  by (expand_case_tac "K = ?y" 1);
   1.197  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   1.198 -(*...we assume X is a very new message, and handle this case by contradiction*)
   1.199 -by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   1.200 +(*...we assume X is a recent message and handle this case by contradiction*)
   1.201 +by (fast_tac (!claset addSEs sees_Spy_partsEs
   1.202                        delrules [conjI]    (*prevent split-up into 4 subgoals*)
   1.203                        addss (!simpset addsimps [parts_insertI])) 1);
   1.204  val lemma = result();
   1.205 @@ -306,8 +268,7 @@
   1.206  \                      Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   1.207  \                   : set_of_list evs";
   1.208  by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   1.209 -                      addEs  partsEs
   1.210 -                      addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   1.211 +                      addEs  sees_Spy_partsEs) 1);
   1.212  qed "A_trusts_OR4";
   1.213  
   1.214  
   1.215 @@ -326,38 +287,43 @@
   1.216  by (etac otway.induct 1);
   1.217  by analz_Fake_tac;
   1.218  by (ALLGOALS
   1.219 -    (asm_simp_tac (!simpset addsimps [not_parts_not_analz,
   1.220 -				      analz_insert_Key_newK]
   1.221 -		            setloop split_tac [expand_if])));
   1.222 +    (asm_simp_tac (!simpset addcongs [conj_cong] 
   1.223 +                            addsimps [not_parts_not_analz,
   1.224 +                                      analz_insert_freshK]
   1.225 +                            setloop split_tac [expand_if])));
   1.226  (*OR3*)
   1.227 -by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   1.228 +by (fast_tac (!claset delrules [impCE]
   1.229 +                      addSEs sees_Spy_partsEs
   1.230 +                      addIs [impOfSubs analz_subset_parts]
   1.231                        addss (!simpset addsimps [parts_insert2])) 2);
   1.232 +(*Oops*) 
   1.233 +by (best_tac (!claset addDs [unique_session_keys] addss (!simpset)) 3);
   1.234  (*OR4, Fake*) 
   1.235  by (REPEAT_FIRST spy_analz_tac);
   1.236 -(*Oops*) 
   1.237 -by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
   1.238  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   1.239  
   1.240  goal thy 
   1.241 - "!!evs. [| Says Server B                                                     \
   1.242 -\            {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                    \
   1.243 -\              Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs;\
   1.244 -\           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                      \
   1.245 -\           A ~: lost;  B ~: lost;  evs : otway lost |]                       \
   1.246 -\        ==> K ~: analz (sees lost Spy evs)";
   1.247 + "!!evs. [| Says Server B                                           \
   1.248 +\              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
   1.249 +\                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
   1.250 +\             : set_of_list evs;                                    \
   1.251 +\           Says B Spy {|NA, NB, Key K|} ~: set_of_list evs;        \
   1.252 +\           A ~: lost;  B ~: lost;  evs : otway lost |]             \
   1.253 +\        ==> Key K ~: analz (sees lost Spy evs)";
   1.254  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.255  by (fast_tac (!claset addSEs [lemma]) 1);
   1.256  qed "Spy_not_see_encrypted_key";
   1.257  
   1.258  
   1.259  goal thy 
   1.260 - "!!evs. [| C ~: {A,B,Server};                                                \
   1.261 -\           Says Server B                                                     \
   1.262 -\            {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                    \
   1.263 -\              Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs;\
   1.264 -\           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                 \
   1.265 -\           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   1.266 -\        ==> K ~: analz (sees lost C evs)";
   1.267 + "!!evs. [| C ~: {A,B,Server};                                      \
   1.268 +\           Says Server B                                           \
   1.269 +\              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
   1.270 +\                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
   1.271 +\             : set_of_list evs;                                    \
   1.272 +\           Says B Spy {|NA, NB, Key K|} ~: set_of_list evs;        \
   1.273 +\           A ~: lost;  B ~: lost;  evs : otway lost |]             \
   1.274 +\        ==> Key K ~: analz (sees lost C evs)";
   1.275  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   1.276  by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   1.277  by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   1.278 @@ -394,6 +360,5 @@
   1.279  \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   1.280  \                     : set_of_list evs";
   1.281  by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   1.282 -                      addEs  partsEs
   1.283 -                      addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   1.284 +                      addEs  sees_Spy_partsEs) 1);
   1.285  qed "B_trusts_OR3";