src/HOL/Auth/Shared.ML
changeset 2516 4d68fbe6378b
parent 2451 ce85a2aafc7a
child 2637 e9b203f854ae
     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";