1.1 --- a/src/HOL/Auth/Shared.ML Fri Jan 17 11:50:09 1997 +0100
1.2 +++ b/src/HOL/Auth/Shared.ML Fri Jan 17 12:49:31 1997 +0100
1.3 @@ -28,18 +28,16 @@
1.4
1.5 (*Injectiveness and freshness of new keys and nonces*)
1.6 AddIffs [inj_shrK RS inj_eq, inj_newN RS inj_eq,
1.7 - inj_newK RS inj_eq, inj_nPair RS inj_eq];
1.8 + inj_newK RS inj_eq, inj_nPair RS inj_eq];
1.9
1.10 (* invKey (shrK A) = shrK A *)
1.11 -bind_thm ("invKey_shrK", rewrite_rule [isSymKey_def] isSym_shrK);
1.12 +bind_thm ("invKey_id", rewrite_rule [isSymKey_def] isSym_keys);
1.13
1.14 -(* invKey (newK i) = newK i *)
1.15 -bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK);
1.16 -Addsimps [invKey_shrK, invKey_newK];
1.17 +Addsimps [invKey_id];
1.18
1.19 goal thy "!!K. newK i = invKey K ==> newK i = K";
1.20 by (rtac (invKey_eq RS iffD1) 1);
1.21 -by (Simp_tac 1);
1.22 +by (Full_simp_tac 1);
1.23 val newK_invKey = result();
1.24
1.25 AddSDs [newK_invKey, sym RS newK_invKey];
1.26 @@ -54,12 +52,7 @@
1.27 by (Auto_tac ());
1.28 qed "newK_notin_initState";
1.29
1.30 -goal thy "Nonce (newN i) ~: parts (initState lost B)";
1.31 -by (agent.induct_tac "B" 1);
1.32 -by (Auto_tac ());
1.33 -qed "newN_notin_initState";
1.34 -
1.35 -AddIffs [newK_notin_initState, newN_notin_initState];
1.36 +AddIffs [newK_notin_initState];
1.37
1.38 goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}";
1.39 by (agent.induct_tac "C" 1);
1.40 @@ -156,6 +149,10 @@
1.41 by (Auto_tac ());
1.42 qed_spec_mp "Says_imp_sees_Spy";
1.43
1.44 +(*Use with addSEs to derive contradictions from old Says events containing
1.45 + items known to be fresh*)
1.46 +val sees_Spy_partsEs = make_elim (Says_imp_sees_Spy RS parts.Inj):: partsEs;
1.47 +
1.48 goal thy
1.49 "!!evs. [| Says A B (Crypt (shrK C) X) : set_of_list evs; C : lost |] \
1.50 \ ==> X : analz (sees lost Spy evs)";
1.51 @@ -194,6 +191,181 @@
1.52 Delsimps [sees_Cons]; (**** NOTE REMOVAL -- laws above are cleaner ****)
1.53
1.54
1.55 +(*** Fresh nonces ***)
1.56 +
1.57 +goal thy "Nonce N ~: parts (initState lost B)";
1.58 +by (agent.induct_tac "B" 1);
1.59 +by (Auto_tac ());
1.60 +qed "Nonce_notin_initState";
1.61 +
1.62 +AddIffs [Nonce_notin_initState];
1.63 +
1.64 +goalw thy [used_def] "!!X. X: parts (sees lost B evs) ==> X: used evs";
1.65 +by (etac (impOfSubs parts_mono) 1);
1.66 +by (Fast_tac 1);
1.67 +qed "usedI";
1.68 +
1.69 +AddIs [usedI];
1.70 +
1.71 +(** Fresh keys never clash with long-term shared keys **)
1.72 +
1.73 +goal thy "Key (shrK A) : used evs";
1.74 +by (Best_tac 1);
1.75 +qed "shrK_in_used";
1.76 +AddIffs [shrK_in_used];
1.77 +
1.78 +(*Used in parts_Fake_tac and analz_Fake_tac to distinguish session keys
1.79 + from long-term shared keys*)
1.80 +goal thy "!!K. Key K ~: used evs ==> K ~: range shrK";
1.81 +by (Best_tac 1);
1.82 +qed "Key_not_used";
1.83 +
1.84 +(*A session key cannot clash with a long-term shared key*)
1.85 +goal thy "!!K. K ~: range shrK ==> shrK B ~= K";
1.86 +by (Fast_tac 1);
1.87 +qed "shrK_neq";
1.88 +
1.89 +Addsimps [Key_not_used, shrK_neq, shrK_neq RS not_sym];
1.90 +
1.91 +
1.92 +goal thy "used (Says A B X # evs) = parts{X} Un used evs";
1.93 +by (simp_tac (!simpset addsimps [used_def, UN_parts_sees_Says]) 1);
1.94 +qed "used_Says";
1.95 +Addsimps [used_Says];
1.96 +
1.97 +goal thy "used [] <= used l";
1.98 +by (list.induct_tac "l" 1);
1.99 +by (event.induct_tac "a" 2);
1.100 +by (ALLGOALS Asm_simp_tac);
1.101 +by (Best_tac 1);
1.102 +qed "used_nil_subset";
1.103 +
1.104 +goal thy "used l <= used (l@l')";
1.105 +by (list.induct_tac "l" 1);
1.106 +by (simp_tac (!simpset addsimps [used_nil_subset]) 1);
1.107 +by (event.induct_tac "a" 1);
1.108 +by (Asm_simp_tac 1);
1.109 +by (Best_tac 1);
1.110 +qed "used_subset_append";
1.111 +
1.112 +
1.113 +(*** Supply fresh nonces for possibility theorems. ***)
1.114 +
1.115 +goalw thy [used_def] "EX N. ALL n. N<=n --> Nonce n ~: used evs";
1.116 +by (list.induct_tac "evs" 1);
1.117 +by (res_inst_tac [("x","0")] exI 1);
1.118 +by (Step_tac 1);
1.119 +by (Full_simp_tac 1);
1.120 +(*Inductive step*)
1.121 +by (event.induct_tac "a" 1);
1.122 +by (full_simp_tac (!simpset addsimps [UN_parts_sees_Says]) 1);
1.123 +by (msg.induct_tac "msg" 1);
1.124 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [exI, parts_insert2])));
1.125 +by (Step_tac 1);
1.126 +(*MPair case*)
1.127 +by (res_inst_tac [("x","Na+Nb")] exI 2);
1.128 +by (fast_tac (!claset addSEs [add_leE]) 2);
1.129 +(*Nonce case*)
1.130 +by (res_inst_tac [("x","N + Suc nat")] exI 1);
1.131 +by (fast_tac (!claset addSEs [add_leE] addafter (TRYALL trans_tac)) 1);
1.132 +val lemma = result();
1.133 +
1.134 +goal thy "EX N. Nonce N ~: used evs";
1.135 +by (rtac (lemma RS exE) 1);
1.136 +by (Fast_tac 1);
1.137 +qed "Nonce_supply1";
1.138 +
1.139 +goal thy "EX N N'. Nonce N ~: used evs & Nonce N' ~: used evs' & N ~= N'";
1.140 +by (cut_inst_tac [("evs","evs")] lemma 1);
1.141 +by (cut_inst_tac [("evs","evs'")] lemma 1);
1.142 +by (Step_tac 1);
1.143 +by (res_inst_tac [("x","N")] exI 1);
1.144 +by (res_inst_tac [("x","Suc (N+Na)")] exI 1);
1.145 +by (asm_simp_tac (!simpset addsimps [less_not_refl2 RS not_sym,
1.146 + le_add2, le_add1,
1.147 + le_eq_less_Suc RS sym]) 1);
1.148 +qed "Nonce_supply2";
1.149 +
1.150 +goal thy "EX N N' N''. Nonce N ~: used evs & Nonce N' ~: used evs' & \
1.151 +\ Nonce N'' ~: used evs'' & N ~= N' & N' ~= N'' & N ~= N''";
1.152 +by (cut_inst_tac [("evs","evs")] lemma 1);
1.153 +by (cut_inst_tac [("evs","evs'")] lemma 1);
1.154 +by (cut_inst_tac [("evs","evs''")] lemma 1);
1.155 +by (Step_tac 1);
1.156 +by (res_inst_tac [("x","N")] exI 1);
1.157 +by (res_inst_tac [("x","Suc (N+Na)")] exI 1);
1.158 +by (res_inst_tac [("x","Suc (Suc (N+Na+Nb))")] exI 1);
1.159 +by (asm_simp_tac (!simpset addsimps [less_not_refl2 RS not_sym,
1.160 + le_add2, le_add1,
1.161 + le_eq_less_Suc RS sym]) 1);
1.162 +by (rtac (less_trans RS less_not_refl2 RS not_sym) 1);
1.163 +by (stac (le_eq_less_Suc RS sym) 1);
1.164 +by (asm_simp_tac (!simpset addsimps [le_eq_less_Suc RS sym]) 2);
1.165 +by (REPEAT (rtac le_add1 1));
1.166 +qed "Nonce_supply3";
1.167 +
1.168 +goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
1.169 +by (rtac (lemma RS exE) 1);
1.170 +by (rtac selectI 1);
1.171 +by (Fast_tac 1);
1.172 +qed "Nonce_supply";
1.173 +
1.174 +(*** Supply fresh keys for possibility theorems. ***)
1.175 +
1.176 +goal thy "EX K. Key K ~: used evs";
1.177 +by (rtac (Fin.emptyI RS Key_supply_ax RS exE) 1);
1.178 +by (Fast_tac 1);
1.179 +qed "Key_supply1";
1.180 +
1.181 +val Fin_UNIV_insertI = UNIV_I RS Fin.insertI;
1.182 +
1.183 +goal thy "EX K K'. Key K ~: used evs & Key K' ~: used evs' & K ~= K'";
1.184 +by (cut_inst_tac [("evs","evs")] (Fin.emptyI RS Key_supply_ax) 1);
1.185 +by (etac exE 1);
1.186 +by (cut_inst_tac [("evs","evs'")]
1.187 + (Fin.emptyI RS Fin_UNIV_insertI RS Key_supply_ax) 1);
1.188 +by (Auto_tac());
1.189 +qed "Key_supply2";
1.190 +
1.191 +goal thy "EX K K' K''. Key K ~: used evs & Key K' ~: used evs' & \
1.192 +\ Key K'' ~: used evs'' & K ~= K' & K' ~= K'' & K ~= K''";
1.193 +by (cut_inst_tac [("evs","evs")] (Fin.emptyI RS Key_supply_ax) 1);
1.194 +by (etac exE 1);
1.195 +by (cut_inst_tac [("evs","evs'")]
1.196 + (Fin.emptyI RS Fin_UNIV_insertI RS Key_supply_ax) 1);
1.197 +by (etac exE 1);
1.198 +by (cut_inst_tac [("evs","evs''")]
1.199 + (Fin.emptyI RS Fin_UNIV_insertI RS Fin_UNIV_insertI RS Key_supply_ax) 1);
1.200 +by (Step_tac 1);
1.201 +by (Full_simp_tac 1);
1.202 +by (fast_tac (!claset addSEs [allE]) 1);
1.203 +qed "Key_supply3";
1.204 +
1.205 +goal thy "Key (@ K. Key K ~: used evs) ~: used evs";
1.206 +by (rtac (Fin.emptyI RS Key_supply_ax RS exE) 1);
1.207 +by (rtac selectI 1);
1.208 +by (Fast_tac 1);
1.209 +qed "Key_supply";
1.210 +
1.211 +(*** Tactics for possibility theorems ***)
1.212 +
1.213 +val possibility_tac =
1.214 + REPEAT (*omit used_Says so that Nonces, Keys start from different traces!*)
1.215 + (ALLGOALS (simp_tac
1.216 + (!simpset delsimps [used_Says] setsolver safe_solver))
1.217 + THEN
1.218 + REPEAT_FIRST (eq_assume_tac ORELSE'
1.219 + resolve_tac [refl, conjI, Nonce_supply, Key_supply]));
1.220 +
1.221 +(*For harder protocols (such as Recur) where we have to set up some
1.222 + nonces and keys initially*)
1.223 +val basic_possibility_tac =
1.224 + REPEAT
1.225 + (ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver))
1.226 + THEN
1.227 + REPEAT_FIRST (resolve_tac [refl, conjI]));
1.228 +
1.229 +
1.230 (** Power of the Spy **)
1.231
1.232 (*The Spy can see more than anybody else, except for their initial state*)
1.233 @@ -227,25 +399,35 @@
1.234 (*Push newK applications in, allowing other keys to be pulled out*)
1.235 val pushKey_newK = insComm thy "Key (newK ?evs)" "Key (shrK ?C)";
1.236
1.237 -Delsimps [image_insert];
1.238 -Addsimps [image_insert RS sym];
1.239 -
1.240 -Delsimps [image_Un];
1.241 -Addsimps [image_Un RS sym];
1.242 -
1.243 -goal thy "insert (Key (newK x)) H = Key `` (newK``{x}) Un H";
1.244 +goal thy "!!A. A <= Compl (range shrK) ==> shrK x ~: A";
1.245 by (Fast_tac 1);
1.246 -qed "insert_Key_singleton";
1.247 +qed "subset_Compl_range";
1.248
1.249 goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
1.250 \ Key `` (f `` (insert x E)) Un C";
1.251 by (Fast_tac 1);
1.252 qed "insert_Key_image";
1.253
1.254 +goal thy "insert (Key K) H = Key `` {K} Un H";
1.255 +by (Fast_tac 1);
1.256 +qed "insert_Key_singleton";
1.257 +
1.258 +goal thy "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
1.259 +by (Fast_tac 1);
1.260 +qed "insert_Key_image'";
1.261 +
1.262 +val analz_image_freshK_ss =
1.263 + !simpset delsimps [image_insert, image_Un]
1.264 + addsimps ([image_insert RS sym, image_Un RS sym,
1.265 + Key_not_used,
1.266 + insert_Key_singleton, subset_Compl_range,
1.267 + insert_Key_image', Un_assoc RS sym]
1.268 + @disj_comms)
1.269 + setloop split_tac [expand_if];
1.270
1.271 (*Lemma for the trivial direction of the if-and-only-if*)
1.272 goal thy
1.273 "!!evs. (Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H) ==> \
1.274 \ (Key K : analz (Key``nE Un H)) = (K : nE | Key K : analz H)";
1.275 by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
1.276 -qed "analz_image_newK_lemma";
1.277 +qed "analz_image_freshK_lemma";