Tidied using more default rules
authorpaulson
Tue Dec 23 11:43:48 1997 +0100 (1997-12-23)
changeset 4470af3239def3d4
parent 4469 399868bf8444
child 4471 0abf9d3f4391
Tidied using more default rules
src/HOL/Auth/NS_Public.ML
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/WooLam.ML
     1.1 --- a/src/HOL/Auth/NS_Public.ML	Tue Dec 23 11:41:12 1997 +0100
     1.2 +++ b/src/HOL/Auth/NS_Public.ML	Tue Dec 23 11:43:48 1997 +0100
     1.3 @@ -5,6 +5,9 @@
     1.4  
     1.5  Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
     1.6  Version incorporating Lowe's fix (inclusion of B's identify in round 2).
     1.7 +
     1.8 +This version is experimental.  It adds many more rules to the claset and even
     1.9 +replaces Fake_parts_insert_tac by Blast_tac.
    1.10  *)
    1.11  
    1.12  open NS_Public;
    1.13 @@ -12,6 +15,10 @@
    1.14  set proof_timing;
    1.15  HOL_quantifiers := false;
    1.16  
    1.17 +AddEs spies_partsEs;
    1.18 +AddDs [impOfSubs analz_subset_parts];
    1.19 +AddDs [impOfSubs Fake_parts_insert];
    1.20 +
    1.21  AddIffs [Spy_in_bad];
    1.22  
    1.23  (*A "possibility property": there are traces that reach the end*)
    1.24 @@ -53,27 +60,18 @@
    1.25  goal thy 
    1.26   "!!A. evs: ns_public ==> (Key (priK A) : parts (spies evs)) = (A : bad)";
    1.27  by (parts_induct_tac 1);
    1.28 -by (Fake_parts_insert_tac 1);
    1.29 +by (Blast_tac 1);
    1.30  qed "Spy_see_priK";
    1.31  Addsimps [Spy_see_priK];
    1.32  
    1.33 -AddDs [impOfSubs analz_subset_parts];
    1.34 -AddDs [Says_imp_spies RS parts.Inj];
    1.35 -AddDs [impOfSubs Fake_parts_insert];
    1.36 -
    1.37  goal thy 
    1.38   "!!A. evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
    1.39  by (Auto_tac());
    1.40  qed "Spy_analz_priK";
    1.41  Addsimps [Spy_analz_priK];
    1.42  
    1.43 -goal thy  "!!A. [| Key (priK A) : parts (spies evs);       \
    1.44 -\                  evs : ns_public |] ==> A:bad";
    1.45 -by (blast_tac (claset() addDs [Spy_see_priK]) 1);
    1.46 -qed "Spy_see_priK_D";
    1.47 -
    1.48 -bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
    1.49 -AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
    1.50 +AddSDs [Spy_see_priK RSN (2, rev_iffD1), 
    1.51 +	Spy_analz_priK RSN (2, rev_iffD1)];
    1.52  
    1.53  
    1.54  (**** Authenticity properties obtained from NS2 ****)
    1.55 @@ -88,13 +86,12 @@
    1.56  by (etac rev_mp 1);
    1.57  by (etac rev_mp 1);
    1.58  by (parts_induct_tac 1);
    1.59 -(*NS3*)
    1.60 -by (blast_tac (claset() addSEs partsEs) 3);
    1.61 -(*NS2*)
    1.62 -by (blast_tac (claset() addSEs partsEs) 2);
    1.63 -by (Fake_parts_insert_tac 1);
    1.64 +by (ALLGOALS Blast_tac);
    1.65  qed "no_nonce_NS1_NS2";
    1.66  
    1.67 +(*Adding it to the claset slows down proofs...*)
    1.68 +val nonce_NS1_NS2_E = no_nonce_NS1_NS2 RSN (2, rev_notE);
    1.69 +
    1.70  
    1.71  (*Unicity for NS1: nonce NA identifies agents A and B*)
    1.72  goal thy 
    1.73 @@ -105,13 +102,14 @@
    1.74  by (etac rev_mp 1);
    1.75  by (parts_induct_tac 1);
    1.76  by (ALLGOALS
    1.77 -    (asm_simp_tac (simpset() addsimps [all_conj_distrib, parts_insert_spies])));
    1.78 +    (asm_simp_tac (simpset() addsimps [all_conj_distrib,
    1.79 +				       parts_insert_spies])));
    1.80  (*NS1*)
    1.81 -by (expand_case_tac "NA = ?y" 2 THEN blast_tac (claset() addSEs partsEs) 2);
    1.82 +by (expand_case_tac "NA = ?y" 2 THEN Blast_tac 2);
    1.83  (*Fake*)
    1.84  by (Clarify_tac 1);
    1.85  by (ex_strip_tac 1);
    1.86 -by (Fake_parts_insert_tac 1);
    1.87 +by (Blast_tac 1);
    1.88  val lemma = result();
    1.89  
    1.90  goal thy 
    1.91 @@ -127,8 +125,7 @@
    1.92  (*Tactic for proving secrecy theorems*)
    1.93  fun analz_induct_tac i = 
    1.94      etac ns_public.induct i   THEN
    1.95 -    ALLGOALS (asm_simp_tac 
    1.96 -              (simpset() addsplits [expand_if]));
    1.97 +    ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]));
    1.98  
    1.99  
   1.100  (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
   1.101 @@ -139,12 +136,11 @@
   1.102  by (etac rev_mp 1);
   1.103  by (analz_induct_tac 1);
   1.104  (*NS3*)
   1.105 -by (blast_tac (claset() addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
   1.106 +by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 4);
   1.107  (*NS2*)
   1.108 -by (blast_tac (claset() addSEs [MPair_parts]
   1.109 -		        addDs  [parts.Body, unique_NA]) 3);
   1.110 +by (blast_tac (claset() addDs [unique_NA]) 3);
   1.111  (*NS1*)
   1.112 -by (blast_tac (claset() addSEs spies_partsEs) 2);
   1.113 +by (Blast_tac 2);
   1.114  (*Fake*)
   1.115  by (spy_analz_tac 1);
   1.116  qed "Spy_not_see_NA";
   1.117 @@ -165,7 +161,7 @@
   1.118  by (etac ns_public.induct 1);
   1.119  by (ALLGOALS Asm_simp_tac);
   1.120  (*NS1*)
   1.121 -by (blast_tac (claset() addSEs spies_partsEs) 2);
   1.122 +by (Blast_tac 2);
   1.123  (*Fake*)
   1.124  by (blast_tac (claset() addDs [Spy_not_see_NA]) 1);
   1.125  qed "A_trusts_NS2";
   1.126 @@ -179,7 +175,7 @@
   1.127  by (etac rev_mp 1);
   1.128  by (etac rev_mp 1);
   1.129  by (parts_induct_tac 1);
   1.130 -by (Fake_parts_insert_tac 1);
   1.131 +by (Blast_tac 1);
   1.132  qed "B_trusts_NS1";
   1.133  
   1.134  
   1.135 @@ -200,11 +196,11 @@
   1.136      (asm_simp_tac (simpset() addsimps [all_conj_distrib, 
   1.137  				       parts_insert_spies])));
   1.138  (*NS2*)
   1.139 -by (expand_case_tac "NB = ?y" 2 THEN blast_tac (claset() addSEs partsEs) 2);
   1.140 +by (expand_case_tac "NB = ?y" 2 THEN Blast_tac 2);
   1.141  (*Fake*)
   1.142  by (Clarify_tac 1);
   1.143  by (ex_strip_tac 1);
   1.144 -by (Fake_parts_insert_tac 1);
   1.145 +by (Blast_tac 1);
   1.146  val lemma = result();
   1.147  
   1.148  goal thy 
   1.149 @@ -218,6 +214,8 @@
   1.150  by (prove_unique_tac lemma 1);
   1.151  qed "unique_NB";
   1.152  
   1.153 +AddDs [unique_NB];
   1.154 +
   1.155  
   1.156  (*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*)
   1.157  goal thy 
   1.158 @@ -228,12 +226,11 @@
   1.159  by (etac rev_mp 1);
   1.160  by (analz_induct_tac 1);
   1.161  (*NS3*)
   1.162 -by (blast_tac (claset() addDs [unique_NB]) 4);
   1.163 +by (Blast_tac 4);
   1.164  (*NS2: by freshness and unicity of NB*)
   1.165 -by (blast_tac (claset() addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]
   1.166 -                        addEs partsEs) 3);
   1.167 +by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 3);
   1.168  (*NS1*)
   1.169 -by (blast_tac (claset() addSEs spies_partsEs) 2);
   1.170 +by (Blast_tac 2);
   1.171  (*Fake*)
   1.172  by (spy_analz_tac 1);
   1.173  qed "Spy_not_see_NB";
   1.174 @@ -254,12 +251,7 @@
   1.175  by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
   1.176  by (parts_induct_tac 1);
   1.177  by (ALLGOALS Clarify_tac);
   1.178 -(*NS3: because NB determines A*)
   1.179 -by (blast_tac (claset() addDs [unique_NB]) 3);
   1.180 -(*NS1: by freshness*)
   1.181 -by (blast_tac (claset() addSEs spies_partsEs) 2);
   1.182 -(*Fake*)
   1.183 -by (Blast_tac 1);
   1.184 +by (ALLGOALS Blast_tac);
   1.185  qed "B_trusts_NS3";
   1.186  
   1.187  
   1.188 @@ -284,11 +276,7 @@
   1.189  by (etac ns_public.induct 1);
   1.190  by (ALLGOALS Asm_simp_tac);
   1.191  by (ALLGOALS Clarify_tac);
   1.192 -(*NS3: because NB determines A and NA*)
   1.193 -by (blast_tac (claset() addDs [unique_NB]) 3);
   1.194 -(*NS1*)
   1.195 -by (blast_tac (claset() addSEs spies_partsEs) 2);
   1.196 -(*Fake*)
   1.197 -by (Blast_tac 1);
   1.198 +(*NS3 holds because NB determines A and NA*)
   1.199 +by (ALLGOALS Blast_tac);
   1.200  qed "B_trusts_protocol";
   1.201  
     2.1 --- a/src/HOL/Auth/NS_Shared.ML	Tue Dec 23 11:41:12 1997 +0100
     2.2 +++ b/src/HOL/Auth/NS_Shared.ML	Tue Dec 23 11:43:48 1997 +0100
     2.3 @@ -15,6 +15,10 @@
     2.4  set proof_timing;
     2.5  HOL_quantifiers := false;
     2.6  
     2.7 +AddEs spies_partsEs;
     2.8 +AddDs [impOfSubs analz_subset_parts];
     2.9 +AddDs [impOfSubs Fake_parts_insert];
    2.10 +
    2.11  
    2.12  (*A "possibility property": there are traces that reach the end*)
    2.13  goal thy 
    2.14 @@ -49,13 +53,13 @@
    2.15  (*For reasoning about the encrypted portion of message NS3*)
    2.16  goal thy "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set evs \
    2.17  \                ==> X : parts (spies evs)";
    2.18 -by (blast_tac (claset() addSEs spies_partsEs) 1);
    2.19 +by (Blast_tac 1);
    2.20  qed "NS3_msg_in_parts_spies";
    2.21                                
    2.22  goal thy
    2.23      "!!evs. Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set evs \
    2.24  \           ==> K : parts (spies evs)";
    2.25 -by (blast_tac (claset() addSEs spies_partsEs) 1);
    2.26 +by (Blast_tac 1);
    2.27  qed "Oops_parts_spies";
    2.28  
    2.29  (*For proving the easier theorems about X ~: parts (spies evs).*)
    2.30 @@ -74,24 +78,18 @@
    2.31  goal thy 
    2.32   "!!evs. evs : ns_shared ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    2.33  by (parts_induct_tac 1);
    2.34 -by (Fake_parts_insert_tac 1);
    2.35  by (ALLGOALS Blast_tac);
    2.36  qed "Spy_see_shrK";
    2.37  Addsimps [Spy_see_shrK];
    2.38  
    2.39  goal thy 
    2.40   "!!evs. evs : ns_shared ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
    2.41 -by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
    2.42 +by (Auto_tac());
    2.43  qed "Spy_analz_shrK";
    2.44  Addsimps [Spy_analz_shrK];
    2.45  
    2.46 -goal thy  "!!A. [| Key (shrK A) : parts (spies evs);       \
    2.47 -\                  evs : ns_shared |] ==> A:bad";
    2.48 -by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
    2.49 -qed "Spy_see_shrK_D";
    2.50 -
    2.51 -bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
    2.52 -AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
    2.53 +AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
    2.54 +	Spy_analz_shrK RSN (2, rev_iffD1)];
    2.55  
    2.56  
    2.57  (*Nobody can have used non-existent keys!*)
    2.58 @@ -105,7 +103,7 @@
    2.59                  addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    2.60                  addss  (simpset())) 1);
    2.61  (*NS2, NS4, NS5*)
    2.62 -by (ALLGOALS (blast_tac (claset() addSEs spies_partsEs)));
    2.63 +by (ALLGOALS (Blast_tac));
    2.64  qed_spec_mp "new_keys_not_used";
    2.65  
    2.66  bind_thm ("new_keys_not_analzd",
    2.67 @@ -138,7 +136,7 @@
    2.68  \               : set evs";
    2.69  by (etac rev_mp 1);
    2.70  by (parts_induct_tac 1);
    2.71 -by (Fake_parts_insert_tac 1);
    2.72 +by (Blast_tac 1);
    2.73  qed "A_trusts_NS2";
    2.74  
    2.75  
    2.76 @@ -162,7 +160,7 @@
    2.77  by (case_tac "A : bad" 1);
    2.78  by (fast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]
    2.79                         addss (simpset())) 1);
    2.80 -by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj, cert_A_form]) 1);
    2.81 +by (blast_tac (claset() addSDs [cert_A_form]) 1);
    2.82  qed "Says_S_message_form";
    2.83  
    2.84  
    2.85 @@ -191,7 +189,7 @@
    2.86  \           (Crypt KAB X) : parts (spies evs) &         \
    2.87  \           Key K : parts {X} --> Key K : parts (spies evs)";
    2.88  by (parts_induct_tac 1);
    2.89 -(*Deals with Faked messages*)
    2.90 +(*Fake*)
    2.91  by (blast_tac (claset() addSEs partsEs
    2.92                          addDs [impOfSubs parts_insert_subset_Un]) 1);
    2.93  (*Base, NS4 and NS5*)
    2.94 @@ -242,8 +240,7 @@
    2.95  (*NS2: it can't be a new key*)
    2.96  by (expand_case_tac "K = ?y" 1);
    2.97  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
    2.98 -by (blast_tac (claset() delrules [conjI]   (*prevent splitup into 4 subgoals*)
    2.99 -                        addSEs spies_partsEs) 1);
   2.100 +by (Blast_tac 1);
   2.101  val lemma = result();
   2.102  
   2.103  (*In messages of this form, the session key uniquely identifies the rest*)
   2.104 @@ -278,9 +275,7 @@
   2.105  (*NS3, replay sub-case*) 
   2.106  by (Blast_tac 4);
   2.107  (*NS2*)
   2.108 -by (blast_tac (claset() addSEs spies_partsEs
   2.109 -                        addIs  [parts_insertI, 
   2.110 -			        impOfSubs analz_subset_parts]) 2);
   2.111 +by (Blast_tac 2);
   2.112  (*Fake*) 
   2.113  by (spy_analz_tac 1);
   2.114  (*NS3, Server sub-case*) (**LEVEL 6 **)
   2.115 @@ -288,7 +283,7 @@
   2.116  by (forward_tac [Says_imp_spies RS parts.Inj RS A_trusts_NS2] 1);
   2.117  by (assume_tac 2);
   2.118  by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS
   2.119 -			      Crypt_Spy_analz_bad]) 1);
   2.120 +			       Crypt_Spy_analz_bad]) 1);
   2.121  by (blast_tac (claset() addDs [unique_session_keys]) 1);
   2.122  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   2.123  
   2.124 @@ -320,8 +315,6 @@
   2.125  \             : set evs";
   2.126  by (etac rev_mp 1);
   2.127  by (parts_induct_tac 1);
   2.128 -by (Fake_parts_insert_tac 1);
   2.129 -(*Fake case*)
   2.130  by (ALLGOALS Blast_tac);
   2.131  qed "B_trusts_NS3";
   2.132  
   2.133 @@ -339,7 +332,7 @@
   2.134  by (parts_induct_tac 1);
   2.135  (*NS3*)
   2.136  by (Blast_tac 3);
   2.137 -by (Fake_parts_insert_tac 1);
   2.138 +by (Blast_tac 1);
   2.139  (*NS2: contradiction from the assumptions  
   2.140    Key K ~: used evs2  and Crypt K (Nonce NB) : parts (spies evs2) *)
   2.141  by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)]
   2.142 @@ -348,8 +341,7 @@
   2.143  (*NS4*)
   2.144  by (Clarify_tac 1);
   2.145  by (not_bad_tac "Ba" 1);
   2.146 -by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS B_trusts_NS3, 
   2.147 -			       unique_session_keys]) 1);
   2.148 +by (blast_tac (claset() addDs [B_trusts_NS3, unique_session_keys]) 1);
   2.149  qed "A_trusts_NS4_lemma";
   2.150  
   2.151  
   2.152 @@ -381,7 +373,7 @@
   2.153  by (parts_induct_tac 1);
   2.154  by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
   2.155  by (ALLGOALS Clarify_tac);
   2.156 -by (Fake_parts_insert_tac 1);
   2.157 +by (Blast_tac 1);
   2.158  (**LEVEL 7**)
   2.159  (*NS2*)
   2.160  by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)]
   2.161 @@ -407,19 +399,18 @@
   2.162  \            Says A B (Crypt K {|Nonce NB, Nonce NB|}) : set evs";
   2.163  by (parts_induct_tac 1);
   2.164  (*NS4*)
   2.165 -by (blast_tac (claset() addSEs spies_partsEs) 4);
   2.166 +by (Blast_tac 4);
   2.167  (*NS3*)
   2.168 -by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj, cert_A_form]) 3);
   2.169 +by (blast_tac (claset() addSDs [cert_A_form]) 3);
   2.170  (*NS2*)
   2.171  by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)]
   2.172  			addSDs [Crypt_imp_keysFor]) 2);
   2.173 -by (Fake_parts_insert_tac 1);
   2.174 +by (Blast_tac 1);
   2.175  (**LEVEL 5**)
   2.176  (*NS5*)
   2.177  by (Clarify_tac 1);
   2.178  by (not_bad_tac "Aa" 1);
   2.179 -by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS A_trusts_NS2, 
   2.180 -			       unique_session_keys]) 1);
   2.181 +by (blast_tac (claset() addDs [A_trusts_NS2, unique_session_keys]) 1);
   2.182  val lemma = result();
   2.183  
   2.184  
     3.1 --- a/src/HOL/Auth/OtwayRees.ML	Tue Dec 23 11:41:12 1997 +0100
     3.2 +++ b/src/HOL/Auth/OtwayRees.ML	Tue Dec 23 11:43:48 1997 +0100
     3.3 @@ -17,6 +17,10 @@
     3.4  set proof_timing;
     3.5  HOL_quantifiers := false;
     3.6  
     3.7 +AddEs spies_partsEs;
     3.8 +AddDs [impOfSubs analz_subset_parts];
     3.9 +AddDs [impOfSubs Fake_parts_insert];
    3.10 +
    3.11  
    3.12  (*A "possibility property": there are traces that reach the end*)
    3.13  goal thy 
    3.14 @@ -45,17 +49,19 @@
    3.15  
    3.16  goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \
    3.17  \                ==> X : analz (spies evs)";
    3.18 -by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
    3.19 +bd (Says_imp_spies RS analz.Inj) 1;
    3.20 +by (Blast_tac 1);
    3.21  qed "OR2_analz_spies";
    3.22  
    3.23  goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
    3.24  \                ==> X : analz (spies evs)";
    3.25 -by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
    3.26 +bd (Says_imp_spies RS analz.Inj) 1;
    3.27 +by (Blast_tac 1);
    3.28  qed "OR4_analz_spies";
    3.29  
    3.30  goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
    3.31  \                 ==> K : parts (spies evs)";
    3.32 -by (blast_tac (claset() addSEs spies_partsEs) 1);
    3.33 +by (Blast_tac 1);
    3.34  qed "Oops_parts_spies";
    3.35  
    3.36  (*OR2_analz... and OR4_analz... let us treat those cases using the same 
    3.37 @@ -85,7 +91,6 @@
    3.38  goal thy 
    3.39   "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    3.40  by (parts_induct_tac 1);
    3.41 -by (Fake_parts_insert_tac 1);
    3.42  by (ALLGOALS Blast_tac);
    3.43  qed "Spy_see_shrK";
    3.44  Addsimps [Spy_see_shrK];
    3.45 @@ -96,12 +101,8 @@
    3.46  qed "Spy_analz_shrK";
    3.47  Addsimps [Spy_analz_shrK];
    3.48  
    3.49 -goal thy  "!!A. [| Key (shrK A) : parts (spies evs); evs : otway |] ==> A:bad";
    3.50 -by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
    3.51 -qed "Spy_see_shrK_D";
    3.52 -
    3.53 -bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
    3.54 -AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
    3.55 +AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
    3.56 +	Spy_analz_shrK RSN (2, rev_iffD1)];
    3.57  
    3.58  
    3.59  (*Nobody can have used non-existent keys!*)
    3.60 @@ -111,9 +112,9 @@
    3.61  (*Fake*)
    3.62  by (best_tac
    3.63        (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    3.64 -               addIs  [impOfSubs analz_subset_parts]
    3.65 -               addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    3.66 -               addss  (simpset())) 1);
    3.67 +		addIs  [impOfSubs analz_subset_parts]
    3.68 +		addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    3.69 +		addss  (simpset())) 1);
    3.70  by (ALLGOALS Blast_tac);
    3.71  qed_spec_mp "new_keys_not_used";
    3.72  
    3.73 @@ -201,8 +202,7 @@
    3.74  by (expand_case_tac "K = ?y" 1);
    3.75  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
    3.76  (*...we assume X is a recent message, and handle this case by contradiction*)
    3.77 -by (blast_tac (claset() addSEs spies_partsEs
    3.78 -                       delrules [conjI] (*no split-up into 4 subgoals*)) 1);
    3.79 +by (Blast_tac 1);
    3.80  val lemma = result();
    3.81  
    3.82  goal thy 
    3.83 @@ -224,7 +224,7 @@
    3.84  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
    3.85  \             : set evs";
    3.86  by (parts_induct_tac 1);
    3.87 -by (Fake_parts_insert_tac 1);
    3.88 +by (Blast_tac 1);
    3.89  qed_spec_mp "Crypt_imp_OR1";
    3.90  
    3.91  
    3.92 @@ -236,11 +236,11 @@
    3.93  \        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) \
    3.94  \        --> B = B'";
    3.95  by (parts_induct_tac 1);
    3.96 -by (Fake_parts_insert_tac 1);
    3.97 +by (Blast_tac 1);
    3.98  by (simp_tac (simpset() addsimps [all_conj_distrib]) 1); 
    3.99  (*OR1: creation of new Nonce.  Move assertion into global context*)
   3.100  by (expand_case_tac "NA = ?y" 1);
   3.101 -by (blast_tac (claset() addSEs spies_partsEs) 1);
   3.102 +by (Blast_tac 1);
   3.103  val lemma = result();
   3.104  
   3.105  goal thy 
   3.106 @@ -261,11 +261,10 @@
   3.107  \            Crypt (shrK A) {|NA', NA, Agent A', Agent A|}  \
   3.108  \             ~: parts (spies evs)";
   3.109  by (parts_induct_tac 1);
   3.110 -by (Fake_parts_insert_tac 1);
   3.111 -by (REPEAT (blast_tac (claset() addSEs spies_partsEs
   3.112 -                               addSDs  [impOfSubs parts_insert_subset_Un]) 1));
   3.113 +by (ALLGOALS Blast_tac);
   3.114  qed_spec_mp"no_nonce_OR1_OR2";
   3.115  
   3.116 +val nonce_OR1_OR2_E = no_nonce_OR1_OR2 RSN (2, rev_notE);
   3.117  
   3.118  (*Crucial property: If the encrypted message appears, and A has used NA
   3.119    to start a run, then it originated with the Server!*)
   3.120 @@ -281,24 +280,19 @@
   3.121  \                   Crypt (shrK B) {|NB, Key K|}|}                     \
   3.122  \                   : set evs)";
   3.123  by (parts_induct_tac 1);
   3.124 -by (Fake_parts_insert_tac 1);
   3.125 +by (Blast_tac 1);
   3.126  (*OR1: it cannot be a new Nonce, contradiction.*)
   3.127 -by (blast_tac (claset() addSIs [parts_insertI] addSEs spies_partsEs) 1);
   3.128 +by (Blast_tac 1);
   3.129  (*OR3 and OR4*)
   3.130  by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
   3.131  by (rtac conjI 1);
   3.132  by (ALLGOALS Clarify_tac);
   3.133  (*OR4*)
   3.134 -by (blast_tac (claset() addSIs [Crypt_imp_OR1]
   3.135 -                       addEs  spies_partsEs) 3);
   3.136 -(*OR3, two cases*)  (** LEVEL 5 **)
   3.137 -by (blast_tac (claset() addSEs [MPair_parts]
   3.138 -                       addSDs [Says_imp_spies RS parts.Inj]
   3.139 -                       addEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
   3.140 -                       delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
   3.141 -by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj]
   3.142 -                       addSEs [MPair_parts]
   3.143 -                       addIs  [unique_NA]) 1);
   3.144 +by (blast_tac (claset() addSIs [Crypt_imp_OR1]) 3);
   3.145 +(*OR3, two cases*)  (** LEVEL 7 **)
   3.146 +by (blast_tac (claset() addSEs  [nonce_OR1_OR2_E]
   3.147 +                        delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
   3.148 +by (blast_tac (claset() addIs  [unique_NA]) 1);
   3.149  qed_spec_mp "NA_Crypt_imp_Server_msg";
   3.150  
   3.151  
   3.152 @@ -316,8 +310,7 @@
   3.153  \                       Crypt (shrK A) {|NA, Key K|},              \
   3.154  \                       Crypt (shrK B) {|NB, Key K|}|}             \
   3.155  \                       : set evs";
   3.156 -by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]
   3.157 -                       addEs  spies_partsEs) 1);
   3.158 +by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]) 1);
   3.159  qed "A_trusts_OR4";
   3.160  
   3.161  
   3.162 @@ -343,8 +336,7 @@
   3.163  (*OR4*) 
   3.164  by (Blast_tac 3);
   3.165  (*OR3*)
   3.166 -by (blast_tac (claset() addSEs spies_partsEs
   3.167 -                       addIs [impOfSubs analz_subset_parts]) 2);
   3.168 +by (Blast_tac 2);
   3.169  (*Fake*) 
   3.170  by (spy_analz_tac 1);
   3.171  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   3.172 @@ -374,7 +366,6 @@
   3.173  \               Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   3.174  \             : set evs)";
   3.175  by (parts_induct_tac 1);
   3.176 -by (Fake_parts_insert_tac 1);
   3.177  by (ALLGOALS Blast_tac);
   3.178  bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE);
   3.179  
   3.180 @@ -387,11 +378,11 @@
   3.181  \      Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs) \
   3.182  \      --> NA = NA' & A = A'";
   3.183  by (parts_induct_tac 1);
   3.184 -by (Fake_parts_insert_tac 1);
   3.185 +by (Blast_tac 1);
   3.186  by (simp_tac (simpset() addsimps [all_conj_distrib]) 1); 
   3.187  (*OR2: creation of new Nonce.  Move assertion into global context*)
   3.188  by (expand_case_tac "NB = ?y" 1);
   3.189 -by (blast_tac (claset() addSEs spies_partsEs) 1);
   3.190 +by (Blast_tac 1);
   3.191  val lemma = result();
   3.192  
   3.193  goal thy 
   3.194 @@ -417,20 +408,20 @@
   3.195  \                        Crypt (shrK B) {|NB, Key K|}|}                  \
   3.196  \                   : set evs)";
   3.197  by (parts_induct_tac 1);
   3.198 -by (Fake_parts_insert_tac 1);
   3.199 +by (Blast_tac 1);
   3.200  (*OR1: it cannot be a new Nonce, contradiction.*)
   3.201 -by (blast_tac (claset() addSIs [parts_insertI] addSEs spies_partsEs) 1);
   3.202 +by (Blast_tac 1);
   3.203  (*OR4*)
   3.204 -by (blast_tac (claset() addSEs [MPair_parts, Crypt_imp_OR2]) 2);
   3.205 +by (blast_tac (claset() addSEs [Crypt_imp_OR2]) 2);
   3.206  (*OR3*)
   3.207 +(*Provable in 38s by the single command
   3.208 +    by (blast_tac (claset() addDs  [unique_NB] addEs[nonce_OR1_OR2_E]) 1);
   3.209 +*)
   3.210  by (safe_tac (claset() delrules [disjCI, impCE]));
   3.211 -by (blast_tac (claset() delrules [conjI] (*stop split-up*)) 3); 
   3.212 -by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj]
   3.213 -                       addSEs [MPair_parts]
   3.214 -                       addDs  [unique_NB]) 2);
   3.215 -by (blast_tac (claset() addSEs [MPair_parts, no_nonce_OR1_OR2 RSN (2, rev_notE)]
   3.216 -                       addSDs [Says_imp_spies RS parts.Inj]
   3.217 -                       delrules [conjI, impCE] (*stop split-up*)) 1);
   3.218 +by (Blast_tac 3); 
   3.219 +by (blast_tac (claset() addDs  [unique_NB]) 2);
   3.220 +by (blast_tac (claset() addSEs [nonce_OR1_OR2_E]
   3.221 +                        delrules [conjI] (*stop split-up*)) 1);
   3.222  qed_spec_mp "NB_Crypt_imp_Server_msg";
   3.223  
   3.224  
   3.225 @@ -447,8 +438,7 @@
   3.226  \                   Crypt (shrK A) {|NA, Key K|},                  \
   3.227  \                   Crypt (shrK B) {|NB, Key K|}|}                 \
   3.228  \                   : set evs";
   3.229 -by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]
   3.230 -                       addSEs spies_partsEs) 1);
   3.231 +by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]) 1);
   3.232  qed "B_trusts_OR3";
   3.233  
   3.234  
   3.235 @@ -465,8 +455,7 @@
   3.236  \            : set evs)";
   3.237  by (etac otway.induct 1);
   3.238  by (ALLGOALS Asm_simp_tac);
   3.239 -by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj]
   3.240 -		       addSEs [MPair_parts, Crypt_imp_OR2]) 3);
   3.241 +by (blast_tac (claset() addSEs [Crypt_imp_OR2]) 3);
   3.242  by (ALLGOALS Blast_tac);
   3.243  bind_thm ("OR3_imp_OR2", result() RSN (2,rev_mp) RS exE);
   3.244  
   3.245 @@ -482,6 +471,6 @@
   3.246  \        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,              \
   3.247  \                              Crypt (shrK B)  {|NA, NB, Agent A, Agent B|} |}\
   3.248  \            : set evs";
   3.249 -by (blast_tac (claset() addSDs  [A_trusts_OR4]
   3.250 -                       addSEs [OR3_imp_OR2]) 1);
   3.251 +by (blast_tac (claset() addSDs [A_trusts_OR4]
   3.252 +                        addSEs [OR3_imp_OR2]) 1);
   3.253  qed "A_auths_B";
     4.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Tue Dec 23 11:41:12 1997 +0100
     4.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Tue Dec 23 11:43:48 1997 +0100
     4.3 @@ -17,6 +17,10 @@
     4.4  set proof_timing;
     4.5  HOL_quantifiers := false;
     4.6  
     4.7 +AddEs spies_partsEs;
     4.8 +AddDs [impOfSubs analz_subset_parts];
     4.9 +AddDs [impOfSubs Fake_parts_insert];
    4.10 +
    4.11  
    4.12  (*A "possibility property": there are traces that reach the end*)
    4.13  goal thy 
    4.14 @@ -45,12 +49,13 @@
    4.15  
    4.16  goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \
    4.17  \                X : analz (spies evs)";
    4.18 -by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
    4.19 +bd (Says_imp_spies RS analz.Inj) 1;
    4.20 +by (Blast_tac 1);
    4.21  qed "OR4_analz_spies";
    4.22  
    4.23  goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
    4.24  \                  : set evs ==> K : parts (spies evs)";
    4.25 -by (blast_tac (claset() addSEs spies_partsEs) 1);
    4.26 +by (Blast_tac 1);
    4.27  qed "Oops_parts_spies";
    4.28  
    4.29  (*OR4_analz_spies lets us treat those cases using the same 
    4.30 @@ -75,7 +80,6 @@
    4.31  goal thy 
    4.32   "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    4.33  by (parts_induct_tac 1);
    4.34 -by (Fake_parts_insert_tac 1);
    4.35  by (ALLGOALS Blast_tac);
    4.36  qed "Spy_see_shrK";
    4.37  Addsimps [Spy_see_shrK];
    4.38 @@ -86,12 +90,8 @@
    4.39  qed "Spy_analz_shrK";
    4.40  Addsimps [Spy_analz_shrK];
    4.41  
    4.42 -goal thy  "!!A. [| Key (shrK A) : parts (spies evs); evs : otway |] ==> A:bad";
    4.43 -by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
    4.44 -qed "Spy_see_shrK_D";
    4.45 -
    4.46 -bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
    4.47 -AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
    4.48 +AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
    4.49 +	Spy_analz_shrK RSN (2, rev_iffD1)];
    4.50  
    4.51  
    4.52  (*Nobody can have used non-existent keys!*)
    4.53 @@ -101,9 +101,9 @@
    4.54  (*Fake*)
    4.55  by (best_tac
    4.56        (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    4.57 -               addIs  [impOfSubs analz_subset_parts]
    4.58 -               addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    4.59 -               addss  (simpset())) 1);
    4.60 +		addIs  [impOfSubs analz_subset_parts]
    4.61 +		addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    4.62 +		addss  (simpset())) 1);
    4.63  (*OR3*)
    4.64  by (Blast_tac 1);
    4.65  qed_spec_mp "new_keys_not_used";
    4.66 @@ -195,8 +195,7 @@
    4.67  by (expand_case_tac "K = ?y" 1);
    4.68  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
    4.69  (*...we assume X is a recent message and handle this case by contradiction*)
    4.70 -by (blast_tac (claset() addSEs spies_partsEs
    4.71 -                       delrules[conjI] (*prevent splitup into 4 subgoals*)) 1);
    4.72 +by (Blast_tac 1);
    4.73  val lemma = result();
    4.74  
    4.75  
    4.76 @@ -227,7 +226,7 @@
    4.77  \                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
    4.78  \                  : set evs)";
    4.79  by (parts_induct_tac 1);
    4.80 -by (Fake_parts_insert_tac 1);
    4.81 +by (Blast_tac 1);
    4.82  by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
    4.83  (*OR3*)
    4.84  by (Blast_tac 1);
    4.85 @@ -244,8 +243,7 @@
    4.86  \                    {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},  \
    4.87  \                      Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
    4.88  \                   : set evs";
    4.89 -by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]
    4.90 -                      addEs  spies_partsEs) 1);
    4.91 +by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]) 1);
    4.92  qed "A_trusts_OR4";
    4.93  
    4.94  
    4.95 @@ -272,8 +270,7 @@
    4.96  (*OR4*) 
    4.97  by (Blast_tac 3);
    4.98  (*OR3*)
    4.99 -by (blast_tac (claset() addSEs spies_partsEs
   4.100 -                       addIs [impOfSubs analz_subset_parts]) 2);
   4.101 +by (Blast_tac 2);
   4.102  (*Fake*) 
   4.103  by (spy_analz_tac 1);
   4.104  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   4.105 @@ -302,7 +299,7 @@
   4.106  \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   4.107  \                     : set evs)";
   4.108  by (parts_induct_tac 1);
   4.109 -by (Fake_parts_insert_tac 1);
   4.110 +by (Blast_tac 1);
   4.111  by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
   4.112  (*OR3*)
   4.113  by (Blast_tac 1);
   4.114 @@ -319,6 +316,5 @@
   4.115  \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   4.116  \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   4.117  \                     : set evs";
   4.118 -by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]
   4.119 -                       addEs  spies_partsEs) 1);
   4.120 +by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]) 1);
   4.121  qed "B_trusts_OR3";
     5.1 --- a/src/HOL/Auth/WooLam.ML	Tue Dec 23 11:41:12 1997 +0100
     5.2 +++ b/src/HOL/Auth/WooLam.ML	Tue Dec 23 11:43:48 1997 +0100
     5.3 @@ -15,6 +15,10 @@
     5.4  set proof_timing;
     5.5  HOL_quantifiers := false;
     5.6  
     5.7 +AddEs spies_partsEs;
     5.8 +AddDs [impOfSubs analz_subset_parts];
     5.9 +AddDs [impOfSubs Fake_parts_insert];
    5.10 +
    5.11  
    5.12  (*A "possibility property": there are traces that reach the end*)
    5.13  goal thy 
    5.14 @@ -62,23 +66,18 @@
    5.15  goal thy 
    5.16   "!!evs. evs : woolam ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    5.17  by (parts_induct_tac 1);
    5.18 -by (Fake_parts_insert_tac 1);
    5.19 +by (Blast_tac 1);
    5.20  qed "Spy_see_shrK";
    5.21  Addsimps [Spy_see_shrK];
    5.22  
    5.23  goal thy 
    5.24   "!!evs. evs : woolam ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
    5.25 -by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
    5.26 +by (Auto_tac());
    5.27  qed "Spy_analz_shrK";
    5.28  Addsimps [Spy_analz_shrK];
    5.29  
    5.30 -goal thy  "!!A. [| Key (shrK A) : parts (spies evs);       \
    5.31 -\                  evs : woolam |] ==> A:bad";
    5.32 -by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
    5.33 -qed "Spy_see_shrK_D";
    5.34 -
    5.35 -bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
    5.36 -AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
    5.37 +AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
    5.38 +	Spy_analz_shrK RSN (2, rev_iffD1)];
    5.39  
    5.40  
    5.41  (**** Autheticity properties for Woo-Lam ****)
    5.42 @@ -88,61 +87,53 @@
    5.43  
    5.44  (*If the encrypted message appears then it originated with Alice*)
    5.45  goal thy 
    5.46 - "!!evs. [| A ~: bad;  evs : woolam |]                        \
    5.47 -\        ==> Crypt (shrK A) (Nonce NB) : parts (spies evs)  \
    5.48 -\            --> (EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs)";
    5.49 + "!!evs. [| Crypt (shrK A) (Nonce NB) : parts (spies evs);  \
    5.50 +\           A ~: bad;  evs : woolam |]                      \
    5.51 +\        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
    5.52 +by (etac rev_mp 1);
    5.53  by (parts_induct_tac 1);
    5.54 -by (Fake_parts_insert_tac 1);
    5.55 -by (Blast_tac 1);
    5.56 -qed_spec_mp "NB_Crypt_imp_Alice_msg";
    5.57 +by (ALLGOALS Blast_tac);
    5.58 +qed "NB_Crypt_imp_Alice_msg";
    5.59  
    5.60  (*Guarantee for Server: if it gets a message containing a certificate from 
    5.61    Alice, then she originated that certificate.  But we DO NOT know that B
    5.62    ever saw it: the Spy may have rerouted the message to the Server.*)
    5.63  goal thy 
    5.64 - "!!evs. [| A ~: bad;  evs : woolam;                      \
    5.65 -\           Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \
    5.66 -\            : set evs |]                                  \
    5.67 + "!!evs. [| Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \
    5.68 +\             : set evs;                                                   \
    5.69 +\           A ~: bad;  evs : woolam |]                                     \
    5.70  \        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
    5.71 -by (blast_tac (claset() addSIs [NB_Crypt_imp_Alice_msg]
    5.72 -                      addSEs [MPair_parts]
    5.73 -                      addDs  [Says_imp_spies RS parts.Inj]) 1);
    5.74 +by (blast_tac (claset() addSIs [NB_Crypt_imp_Alice_msg]) 1);
    5.75  qed "Server_trusts_WL4";
    5.76  
    5.77 +AddDs [Server_trusts_WL4];
    5.78 +
    5.79  
    5.80  (*** WL5 ***)
    5.81  
    5.82  (*Server sent WL5 only if it received the right sort of message*)
    5.83  goal thy 
    5.84 - "!!evs. evs : woolam ==>                                                   \
    5.85 -\        Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs           \
    5.86 -\        --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \
    5.87 -\               : set evs)";
    5.88 + "!!evs. [| Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs;      \
    5.89 +\           evs : woolam |]                                                \
    5.90 +\        ==> EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \
    5.91 +\               : set evs";
    5.92 +by (etac rev_mp 1);
    5.93  by (parts_induct_tac 1);
    5.94 -by (Fake_parts_insert_tac 1);
    5.95  by (ALLGOALS Blast_tac);
    5.96 -bind_thm ("Server_sent_WL5", result() RSN (2, rev_mp));
    5.97 +qed "Server_sent_WL5";
    5.98  
    5.99 +AddDs [Server_sent_WL5];
   5.100  
   5.101  (*If the encrypted message appears then it originated with the Server!*)
   5.102  goal thy 
   5.103 - "!!evs. [| B ~: bad;  evs : woolam |]                             \
   5.104 -\        ==> Crypt (shrK B) {|Agent A, NB|} : parts (spies evs)  \
   5.105 -\        --> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs";
   5.106 + "!!evs. [| Crypt (shrK B) {|Agent A, NB|} : parts (spies evs);  \
   5.107 +\           B ~: bad;  evs : woolam |]                           \
   5.108 +\        ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs";
   5.109 +by (etac rev_mp 1);
   5.110  by (parts_induct_tac 1);
   5.111 -by (Fake_parts_insert_tac 1);
   5.112 +by (Blast_tac 1);
   5.113  qed_spec_mp "NB_Crypt_imp_Server_msg";
   5.114  
   5.115 -(*Partial guarantee for B: if it gets a message of correct form then the Server
   5.116 -  sent the same message.*)
   5.117 -goal thy 
   5.118 - "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, NB|}) : set evs;         \
   5.119 -\           B ~: bad;  evs : woolam |]                                  \
   5.120 -\        ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs";
   5.121 -by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]
   5.122 -                      addDs  [Says_imp_spies RS parts.Inj]) 1);
   5.123 -qed "B_got_WL5";
   5.124 -
   5.125  (*Guarantee for B.  If B gets the Server's certificate then A has encrypted
   5.126    the nonce using her key.  This event can be no older than the nonce itself.
   5.127    But A may have sent the nonce to some other agent and it could have reached
   5.128 @@ -151,20 +142,18 @@
   5.129   "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs; \
   5.130  \           A ~: bad;  B ~: bad;  evs : woolam  |]                  \
   5.131  \        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
   5.132 -by (blast_tac (claset() addIs  [Server_trusts_WL4]
   5.133 -                      addSDs [B_got_WL5 RS Server_sent_WL5]) 1);
   5.134 +by (blast_tac (claset() addSDs [NB_Crypt_imp_Server_msg]) 1);
   5.135  qed "B_trusts_WL5";
   5.136  
   5.137  
   5.138 -(*B only issues challenges in response to WL1.  Useful??*)
   5.139 +(*B only issues challenges in response to WL1.  Not used.*)
   5.140  goal thy 
   5.141 - "!!evs. [| B ~= Spy;  evs : woolam |]        \
   5.142 -\    ==> Says B A (Nonce NB) : set evs        \
   5.143 -\        --> (EX A'. Says A' B (Agent A) : set evs)";
   5.144 + "!!evs. [| Says B A (Nonce NB) : set evs;  B ~= Spy;  evs : woolam |]  \
   5.145 +\        ==> EX A'. Says A' B (Agent A) : set evs";
   5.146 +by (etac rev_mp 1);
   5.147  by (parts_induct_tac 1);
   5.148 -by (Fake_parts_insert_tac 1);
   5.149  by (ALLGOALS Blast_tac);
   5.150 -bind_thm ("B_said_WL2", result() RSN (2, rev_mp));
   5.151 +qed "B_said_WL2";
   5.152  
   5.153  
   5.154  (**CANNOT be proved because A doesn't know where challenges come from...
   5.155 @@ -174,7 +163,6 @@
   5.156  \        Says B A (Nonce NB) : set evs                       \
   5.157  \        --> Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
   5.158  by (parts_induct_tac 1);
   5.159 -by (Fake_parts_insert_tac 1);
   5.160 +by (Blast_tac 1);
   5.161  by Safe_tac;
   5.162 -by (blast_tac (claset() addSEs partsEs) 1);
   5.163  **)