src/HOL/Auth/OtwayRees.ML
changeset 3102 4d01cdc119d2
parent 2837 dee1c7f1f576
child 3121 cbb6c0c1c58a
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Mon May 05 12:15:20 1997 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Mon May 05 12:15:53 1997 +0200
     1.3 @@ -17,6 +17,10 @@
     1.4  proof_timing:=true;
     1.5  HOL_quantifiers := false;
     1.6  
     1.7 +(*Replacing the variable by a constant improves search speed by 50%!*)
     1.8 +val Says_imp_sees_Spy' = 
     1.9 +    read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
    1.10 +
    1.11  
    1.12  (*A "possibility property": there are traces that reach the end*)
    1.13  goal thy 
    1.14 @@ -36,8 +40,8 @@
    1.15  goal thy "!!evs. lost' <= lost ==> otway lost' <= otway lost";
    1.16  by (rtac subsetI 1);
    1.17  by (etac otway.induct 1);
    1.18 -by (REPEAT_FIRST
    1.19 -    (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
    1.20 +by (ALLGOALS
    1.21 +    (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
    1.22                                :: otway.intrs))));
    1.23  qed "otway_mono";
    1.24  
    1.25 @@ -54,17 +58,17 @@
    1.26  
    1.27  goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs \
    1.28  \                ==> X : analz (sees lost Spy evs)";
    1.29 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    1.30 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
    1.31  qed "OR2_analz_sees_Spy";
    1.32  
    1.33  goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set_of_list evs \
    1.34  \                ==> X : analz (sees lost Spy evs)";
    1.35 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    1.36 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
    1.37  qed "OR4_analz_sees_Spy";
    1.38  
    1.39  goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \
    1.40  \                 ==> K : parts (sees lost Spy evs)";
    1.41 -by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
    1.42 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
    1.43  qed "Oops_parts_sees_Spy";
    1.44  
    1.45  (*OR2_analz... and OR4_analz... let us treat those cases using the same 
    1.46 @@ -118,7 +122,7 @@
    1.47  
    1.48  goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
    1.49  \                  evs : otway lost |] ==> A:lost";
    1.50 -by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
    1.51 +by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
    1.52  qed "Spy_see_shrK_D";
    1.53  
    1.54  bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
    1.55 @@ -135,8 +139,7 @@
    1.56                 addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
    1.57                        impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    1.58                 unsafe_addss (!simpset)) 1);
    1.59 -(*OR1-3*)
    1.60 -by (REPEAT (fast_tac (!claset addss (!simpset)) 1));
    1.61 +by (ALLGOALS Blast_tac);
    1.62  qed_spec_mp "new_keys_not_used";
    1.63  
    1.64  bind_thm ("new_keys_not_analzd",
    1.65 @@ -158,7 +161,8 @@
    1.66  \     ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
    1.67  by (etac rev_mp 1);
    1.68  by (etac otway.induct 1);
    1.69 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    1.70 +by (ALLGOALS Simp_tac);
    1.71 +by (ALLGOALS Blast_tac);
    1.72  qed "Says_Server_message_form";
    1.73  
    1.74  
    1.75 @@ -195,7 +199,7 @@
    1.76  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
    1.77  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
    1.78  (*Base*)
    1.79 -by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
    1.80 +by (Blast_tac 1);
    1.81  (*Fake, OR2, OR4*) 
    1.82  by (REPEAT (spy_analz_tac 1));
    1.83  qed_spec_mp "analz_image_freshK";
    1.84 @@ -221,13 +225,12 @@
    1.85  by (Step_tac 1);
    1.86  (*Remaining cases: OR3 and OR4*)
    1.87  by (ex_strip_tac 2);
    1.88 -by (Fast_tac 2);
    1.89 +by (Best_tac 2);
    1.90  by (expand_case_tac "K = ?y" 1);
    1.91  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
    1.92  (*...we assume X is a recent message, and handle this case by contradiction*)
    1.93 -by (fast_tac (!claset addSEs sees_Spy_partsEs
    1.94 -                      delrules [conjI]    (*prevent split-up into 4 subgoals*)
    1.95 -                      addss (!simpset addsimps [parts_insertI])) 1);
    1.96 +by (blast_tac (!claset addSEs sees_Spy_partsEs
    1.97 +                       delrules [conjI] (*no split-up into 4 subgoals*)) 1);
    1.98  val lemma = result();
    1.99  
   1.100  goal thy 
   1.101 @@ -266,7 +269,7 @@
   1.102  by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   1.103  (*OR1: creation of new Nonce.  Move assertion into global context*)
   1.104  by (expand_case_tac "NA = ?y" 1);
   1.105 -by (best_tac (!claset addSEs sees_Spy_partsEs) 1);
   1.106 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   1.107  val lemma = result();
   1.108  
   1.109  goal thy 
   1.110 @@ -288,9 +291,8 @@
   1.111  \            Crypt (shrK A) {|NA', NA, Agent A', Agent A|}       \
   1.112  \             ~: parts (sees lost Spy evs)";
   1.113  by (parts_induct_tac 1);
   1.114 -by (REPEAT (fast_tac (!claset addSEs sees_Spy_partsEs
   1.115 -                              addSDs  [impOfSubs parts_insert_subset_Un]
   1.116 -                              addss (!simpset)) 1));
   1.117 +by (REPEAT (blast_tac (!claset addSEs sees_Spy_partsEs
   1.118 +                               addSDs  [impOfSubs parts_insert_subset_Un]) 1));
   1.119  qed_spec_mp"no_nonce_OR1_OR2";
   1.120  
   1.121  
   1.122 @@ -309,25 +311,23 @@
   1.123  \                   : set_of_list evs)";
   1.124  by (parts_induct_tac 1);
   1.125  (*OR1: it cannot be a new Nonce, contradiction.*)
   1.126 -by (fast_tac (!claset addSIs [parts_insertI]
   1.127 -                      addSEs sees_Spy_partsEs
   1.128 -                      addss (!simpset)) 1);
   1.129 +by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1);
   1.130  (*OR3 and OR4*) 
   1.131  (*OR4*)
   1.132  by (REPEAT (Safe_step_tac 2));
   1.133 -by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3));
   1.134 +by (REPEAT (blast_tac (!claset addSDs [parts_cut]) 3));
   1.135  by (fast_tac (!claset addSIs [Crypt_imp_OR1]
   1.136                        addEs  sees_Spy_partsEs) 2);
   1.137  (*OR3*)  (** LEVEL 5 **)
   1.138  by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
   1.139  by (step_tac (!claset delrules [disjCI, impCE]) 1);
   1.140 -by (fast_tac (!claset addSEs [MPair_parts]
   1.141 -                      addSDs [Says_imp_sees_Spy RS parts.Inj]
   1.142 +by (blast_tac (!claset addSEs [MPair_parts]
   1.143 +                      addSDs [Says_imp_sees_Spy' RS parts.Inj]
   1.144                        addEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
   1.145                        delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
   1.146 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   1.147 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   1.148                        addSEs [MPair_parts]
   1.149 -                      addEs  [unique_NA]) 1);
   1.150 +                      addIs  [unique_NA]) 1);
   1.151  qed_spec_mp "NA_Crypt_imp_Server_msg";
   1.152  
   1.153  
   1.154 @@ -347,8 +347,8 @@
   1.155  \                       Crypt (shrK A) {|NA, Key K|},              \
   1.156  \                       Crypt (shrK B) {|NB, Key K|}|}             \
   1.157  \                       : set_of_list evs";
   1.158 -by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   1.159 -                      addEs  sees_Spy_partsEs) 1);
   1.160 +by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   1.161 +                       addEs  sees_Spy_partsEs) 1);
   1.162  qed "A_trusts_OR4";
   1.163  
   1.164  
   1.165 @@ -370,15 +370,13 @@
   1.166                              addsimps [not_parts_not_analz, analz_insert_freshK]
   1.167                              setloop split_tac [expand_if])));
   1.168  (*OR3*)
   1.169 -by (fast_tac (!claset delrules [impCE]
   1.170 -                      addSEs sees_Spy_partsEs
   1.171 -                      addIs [impOfSubs analz_subset_parts]
   1.172 -                      addss (!simpset addsimps [parts_insert2])) 3);
   1.173 +by (blast_tac (!claset delrules [impCE]
   1.174 +                       addSEs sees_Spy_partsEs
   1.175 +                       addIs [impOfSubs analz_subset_parts]) 3);
   1.176  (*OR4, OR2, Fake*) 
   1.177  by (REPEAT_FIRST spy_analz_tac);
   1.178  (*Oops*) (** LEVEL 5 **)
   1.179 -by (fast_tac (!claset delrules [disjE]
   1.180 -                      addDs [unique_session_keys] addss (!simpset)) 1);
   1.181 +by (blast_tac (!claset addSDs [unique_session_keys]) 1);
   1.182  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   1.183  
   1.184  goal thy 
   1.185 @@ -389,7 +387,7 @@
   1.186  \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   1.187  \        ==> Key K ~: analz (sees lost Spy evs)";
   1.188  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.189 -by (fast_tac (!claset addSEs [lemma]) 1);
   1.190 +by (blast_tac (!claset addSEs [lemma]) 1);
   1.191  qed "Spy_not_see_encrypted_key";
   1.192  
   1.193  
   1.194 @@ -404,7 +402,7 @@
   1.195  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   1.196  by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   1.197  by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   1.198 -by (REPEAT_FIRST (fast_tac (!claset addIs [otway_mono RS subsetD])));
   1.199 +by (REPEAT_FIRST (blast_tac (!claset addIs [otway_mono RS subsetD])));
   1.200  qed "Agent_not_see_encrypted_key";
   1.201  
   1.202  
   1.203 @@ -421,7 +419,7 @@
   1.204  \               Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   1.205  \             : set_of_list evs)";
   1.206  by (parts_induct_tac 1);
   1.207 -by (auto_tac (!claset, !simpset addcongs [conj_cong]));
   1.208 +by (ALLGOALS Blast_tac);
   1.209  bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE);
   1.210  
   1.211  
   1.212 @@ -436,7 +434,7 @@
   1.213  by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   1.214  (*OR2: creation of new Nonce.  Move assertion into global context*)
   1.215  by (expand_case_tac "NB = ?y" 1);
   1.216 -by (deepen_tac (!claset addSEs sees_Spy_partsEs) 3 1);
   1.217 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   1.218  val lemma = result();
   1.219  
   1.220  goal thy 
   1.221 @@ -465,21 +463,18 @@
   1.222  \                   : set_of_list evs)";
   1.223  by (parts_induct_tac 1);
   1.224  (*OR1: it cannot be a new Nonce, contradiction.*)
   1.225 -by (fast_tac (!claset addSIs [parts_insertI]
   1.226 -                      addSEs sees_Spy_partsEs
   1.227 -                      addss (!simpset)) 1);
   1.228 +by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1);
   1.229  (*OR4*)
   1.230 -by (fast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2);
   1.231 +by (blast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2);
   1.232  (*OR3*)
   1.233  by (step_tac (!claset delrules [disjCI, impCE]) 1);
   1.234 -by (fast_tac (!claset delrules [conjI] (*stop split-up*)) 3); 
   1.235 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   1.236 -                      addSEs [MPair_parts]
   1.237 -                      addDs  [unique_NB]) 2);
   1.238 -by (fast_tac (!claset addSEs [MPair_parts]
   1.239 -                      addSDs [Says_imp_sees_Spy RS parts.Inj]
   1.240 -                      addSEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
   1.241 -                      delrules [conjI, impCE] (*stop split-up*)) 1);
   1.242 +by (blast_tac (!claset delrules [conjI] (*stop split-up*)) 3); 
   1.243 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   1.244 +                       addSEs [MPair_parts]
   1.245 +                       addDs  [unique_NB]) 2);
   1.246 +by (blast_tac (!claset addSEs [MPair_parts, no_nonce_OR1_OR2 RSN (2, rev_notE)]
   1.247 +                       addSDs [Says_imp_sees_Spy' RS parts.Inj]
   1.248 +                       delrules [conjI, impCE] (*stop split-up*)) 1);
   1.249  qed_spec_mp "NB_Crypt_imp_Server_msg";
   1.250  
   1.251  
   1.252 @@ -497,8 +492,8 @@
   1.253  \                   Crypt (shrK A) {|NA, Key K|},                  \
   1.254  \                   Crypt (shrK B) {|NB, Key K|}|}                 \
   1.255  \                   : set_of_list evs";
   1.256 -by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   1.257 -                      addEs  sees_Spy_partsEs) 1);
   1.258 +by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   1.259 +                       addSEs sees_Spy_partsEs) 1);
   1.260  qed "B_trusts_OR3";
   1.261  
   1.262  
   1.263 @@ -514,9 +509,10 @@
   1.264  \                            Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   1.265  \            : set_of_list evs)";
   1.266  by (etac otway.induct 1);
   1.267 -by (Auto_tac());
   1.268 -by (dtac (Says_imp_sees_Spy RS parts.Inj) 1);
   1.269 -by (fast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 1);
   1.270 +by (ALLGOALS Asm_simp_tac);
   1.271 +by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj]
   1.272 +		       addSEs [MPair_parts, Crypt_imp_OR2]) 3);
   1.273 +by (ALLGOALS Blast_tac);
   1.274  bind_thm ("OR3_imp_OR2", result() RSN (2,rev_mp) RS exE);
   1.275  
   1.276  
   1.277 @@ -533,6 +529,6 @@
   1.278  \        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,     \
   1.279  \                              Crypt (shrK B)  {|NA, NB, Agent A, Agent B|} |}\
   1.280  \            : set_of_list evs";
   1.281 -by (fast_tac (!claset addSDs  [A_trusts_OR4]
   1.282 -                      addSEs [OR3_imp_OR2]) 1);
   1.283 +by (blast_tac (!claset addSDs  [A_trusts_OR4]
   1.284 +                       addSEs [OR3_imp_OR2]) 1);
   1.285  qed "A_auths_B";