src/HOL/Auth/OtwayRees_AN.ML
changeset 3102 4d01cdc119d2
parent 2891 d8f254ad1ab9
child 3121 cbb6c0c1c58a
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Mon May 05 12:15:20 1997 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Mon May 05 12:15:53 1997 +0200
     1.3 @@ -54,12 +54,12 @@
     1.4  
     1.5  goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set_of_list evs ==> \
     1.6  \                X : analz (sees lost Spy evs)";
     1.7 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
     1.8 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
     1.9  qed "OR4_analz_sees_Spy";
    1.10  
    1.11  goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
    1.12  \                  : set_of_list evs ==> K : parts (sees lost Spy evs)";
    1.13 -by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
    1.14 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
    1.15  qed "Oops_parts_sees_Spy";
    1.16  
    1.17  (*OR4_analz_sees_Spy lets us treat those cases using the same 
    1.18 @@ -107,7 +107,7 @@
    1.19  
    1.20  goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
    1.21  \                  evs : otway lost |] ==> A:lost";
    1.22 -by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
    1.23 +by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
    1.24  qed "Spy_see_shrK_D";
    1.25  
    1.26  bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
    1.27 @@ -125,7 +125,7 @@
    1.28                        impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    1.29                 unsafe_addss (!simpset)) 1);
    1.30  (*OR3*)
    1.31 -by (fast_tac (!claset addss (!simpset)) 1);
    1.32 +by (Blast_tac 1);
    1.33  qed_spec_mp "new_keys_not_used";
    1.34  
    1.35  bind_thm ("new_keys_not_analzd",
    1.36 @@ -148,7 +148,8 @@
    1.37  \        ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
    1.38  by (etac rev_mp 1);
    1.39  by (etac otway.induct 1);
    1.40 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    1.41 +by (ALLGOALS Asm_simp_tac);
    1.42 +by (Blast_tac 1);
    1.43  qed "Says_Server_message_form";
    1.44  
    1.45  
    1.46 @@ -187,7 +188,7 @@
    1.47  (*OR4, Fake*) 
    1.48  by (EVERY (map spy_analz_tac [3,2]));
    1.49  (*Base*)
    1.50 -by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
    1.51 +by (Blast_tac 1);
    1.52  qed_spec_mp "analz_image_freshK";
    1.53  
    1.54  
    1.55 @@ -213,13 +214,12 @@
    1.56  by (Step_tac 1);
    1.57  (*Remaining cases: OR3 and OR4*)
    1.58  by (ex_strip_tac 2);
    1.59 -by (Fast_tac 2);
    1.60 +by (Blast_tac 2);
    1.61  by (expand_case_tac "K = ?y" 1);
    1.62  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
    1.63  (*...we assume X is a recent message and handle this case by contradiction*)
    1.64 -by (fast_tac (!claset addSEs sees_Spy_partsEs
    1.65 -                      delrules [conjI]    (*prevent split-up into 4 subgoals*)
    1.66 -                      addss (!simpset addsimps [parts_insertI])) 1);
    1.67 +by (blast_tac (!claset addSEs sees_Spy_partsEs
    1.68 +                       delrules[conjI] (*prevent splitup into 4 subgoals*)) 1);
    1.69  val lemma = result();
    1.70  
    1.71  
    1.72 @@ -253,7 +253,7 @@
    1.73  by (parts_induct_tac 1);
    1.74  by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
    1.75  (*OR3*)
    1.76 -by (Fast_tac 1);
    1.77 +by (Blast_tac 1);
    1.78  qed_spec_mp "NA_Crypt_imp_Server_msg";
    1.79  
    1.80  
    1.81 @@ -267,7 +267,7 @@
    1.82  \                    {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},  \
    1.83  \                      Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
    1.84  \                   : set_of_list evs";
    1.85 -by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
    1.86 +by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
    1.87                        addEs  sees_Spy_partsEs) 1);
    1.88  qed "A_trusts_OR4";
    1.89  
    1.90 @@ -292,12 +292,10 @@
    1.91                                        analz_insert_freshK]
    1.92                              setloop split_tac [expand_if])));
    1.93  (*OR3*)
    1.94 -by (fast_tac (!claset delrules [impCE]
    1.95 -                      addSEs sees_Spy_partsEs
    1.96 -                      addIs [impOfSubs analz_subset_parts]
    1.97 -                      addss (!simpset addsimps [parts_insert2])) 2);
    1.98 +by (blast_tac (!claset addSEs sees_Spy_partsEs
    1.99 +                       addIs [impOfSubs analz_subset_parts]) 2);
   1.100  (*Oops*) 
   1.101 -by (best_tac (!claset addDs [unique_session_keys] unsafe_addss (!simpset)) 3);
   1.102 +by (blast_tac (!claset addDs [unique_session_keys]) 3);
   1.103  (*OR4, Fake*) 
   1.104  by (REPEAT_FIRST spy_analz_tac);
   1.105  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   1.106 @@ -345,7 +343,7 @@
   1.107  by (parts_induct_tac 1);
   1.108  by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   1.109  (*OR3*)
   1.110 -by (Fast_tac 1);
   1.111 +by (Blast_tac 1);
   1.112  qed_spec_mp "NB_Crypt_imp_Server_msg";
   1.113  
   1.114  
   1.115 @@ -359,6 +357,6 @@
   1.116  \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   1.117  \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   1.118  \                     : set_of_list evs";
   1.119 -by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   1.120 -                      addEs  sees_Spy_partsEs) 1);
   1.121 +by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   1.122 +                       addEs  sees_Spy_partsEs) 1);
   1.123  qed "B_trusts_OR3";