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";