src/HOL/Auth/Yahalom.ML
changeset 4091 771b1f6422a8
parent 3961 6a8996fb7d99
child 4238 679a233fb206
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Mon Nov 03 12:22:43 1997 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Mon Nov 03 12:24:13 1997 +0100
     1.3 @@ -45,7 +45,7 @@
     1.4  (*Lets us treat YM4 using a similar argument as for the Fake case.*)
     1.5  goal thy "!!evs. Says S A {|Crypt (shrK A) Y, X|} : set evs ==> \
     1.6  \                X : analz (spies evs)";
     1.7 -by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1);
     1.8 +by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
     1.9  qed "YM4_analz_spies";
    1.10  
    1.11  bind_thm ("YM4_parts_spies",
    1.12 @@ -54,7 +54,7 @@
    1.13  (*Relates to both YM4 and Oops*)
    1.14  goal thy "!!evs. Says S A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} : set evs ==> \
    1.15  \                K : parts (spies evs)";
    1.16 -by (blast_tac (!claset addSEs partsEs
    1.17 +by (blast_tac (claset() addSEs partsEs
    1.18                        addSDs [Says_imp_spies RS parts.Inj]) 1);
    1.19  qed "YM4_Key_parts_spies";
    1.20  
    1.21 @@ -88,13 +88,13 @@
    1.22  
    1.23  goal thy 
    1.24   "!!evs. evs : yahalom ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
    1.25 -by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
    1.26 +by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
    1.27  qed "Spy_analz_shrK";
    1.28  Addsimps [Spy_analz_shrK];
    1.29  
    1.30  goal thy  "!!A. [| Key (shrK A) : parts (spies evs);       \
    1.31  \                  evs : yahalom |] ==> A:bad";
    1.32 -by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
    1.33 +by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
    1.34  qed "Spy_see_shrK_D";
    1.35  
    1.36  bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
    1.37 @@ -107,12 +107,12 @@
    1.38  by (parts_induct_tac 1);
    1.39  (*Fake*)
    1.40  by (best_tac
    1.41 -      (!claset addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    1.42 +      (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    1.43                 addIs  [impOfSubs analz_subset_parts]
    1.44                 addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    1.45 -               addss  (!simpset)) 1);
    1.46 +               addss  (simpset())) 1);
    1.47  (*YM2-4: Because Key K is not fresh, etc.*)
    1.48 -by (REPEAT (blast_tac (!claset addSEs spies_partsEs) 1));
    1.49 +by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1));
    1.50  qed_spec_mp "new_keys_not_used";
    1.51  
    1.52  bind_thm ("new_keys_not_analzd",
    1.53 @@ -187,7 +187,7 @@
    1.54  \           {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}        \
    1.55  \          : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
    1.56  by (etac yahalom.induct 1);
    1.57 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
    1.58 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
    1.59  by (ALLGOALS Clarify_tac);
    1.60  by (ex_strip_tac 2);
    1.61  by (Blast_tac 2);
    1.62 @@ -195,7 +195,7 @@
    1.63  by (expand_case_tac "K = ?y" 1);
    1.64  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
    1.65  (*...we assume X is a recent message and handle this case by contradiction*)
    1.66 -by (blast_tac (!claset addSEs spies_partsEs
    1.67 +by (blast_tac (claset() addSEs spies_partsEs
    1.68                         delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
    1.69  val lemma = result();
    1.70  
    1.71 @@ -224,12 +224,12 @@
    1.72  by analz_spies_tac;
    1.73  by (ALLGOALS
    1.74      (asm_simp_tac 
    1.75 -     (!simpset addsimps (expand_ifs@pushes)
    1.76 +     (simpset() addsimps (expand_ifs@pushes)
    1.77  	       addsimps [analz_insert_eq, analz_insert_freshK])));
    1.78  (*Oops*)
    1.79 -by (blast_tac (!claset addDs [unique_session_keys]) 3);
    1.80 +by (blast_tac (claset() addDs [unique_session_keys]) 3);
    1.81  (*YM3*)
    1.82 -by (blast_tac (!claset delrules [impCE]
    1.83 +by (blast_tac (claset() delrules [impCE]
    1.84                         addSEs spies_partsEs
    1.85                         addIs [impOfSubs analz_subset_parts]) 2);
    1.86  (*Fake*) 
    1.87 @@ -247,7 +247,7 @@
    1.88  \           A ~: bad;  B ~: bad;  evs : yahalom |]         \
    1.89  \        ==> Key K ~: analz (spies evs)";
    1.90  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
    1.91 -by (blast_tac (!claset addSEs [lemma]) 1);
    1.92 +by (blast_tac (claset() addSEs [lemma]) 1);
    1.93  qed "Spy_not_see_encrypted_key";
    1.94  
    1.95  
    1.96 @@ -307,7 +307,7 @@
    1.97  (*A is uncompromised because NB is secure*)
    1.98  by (not_bad_tac "A" 1);
    1.99  (*A's certificate guarantees the existence of the Server message*)
   1.100 -by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS
   1.101 +by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS
   1.102  			      A_trusts_YM3]) 1);
   1.103  bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp));
   1.104  
   1.105 @@ -337,7 +337,7 @@
   1.106    (with respect to a given trace). *)
   1.107  goalw thy [KeyWithNonce_def]
   1.108   "!!evs. Key K ~: used evs ==> ~ KeyWithNonce K NB evs";
   1.109 -by (blast_tac (!claset addSEs spies_partsEs) 1);
   1.110 +by (blast_tac (claset() addSEs spies_partsEs) 1);
   1.111  qed "fresh_not_KeyWithNonce";
   1.112  
   1.113  (*The Server message associates K with NB' and therefore not with any 
   1.114 @@ -348,7 +348,7 @@
   1.115  \             : set evs;                                                 \
   1.116  \           NB ~= NB';  evs : yahalom |]                            \
   1.117  \        ==> ~ KeyWithNonce K NB evs";
   1.118 -by (blast_tac (!claset addDs [unique_session_keys]) 1);
   1.119 +by (blast_tac (claset() addDs [unique_session_keys]) 1);
   1.120  qed "Says_Server_KeyWithNonce";
   1.121  
   1.122  
   1.123 @@ -362,7 +362,7 @@
   1.124  goal thy  
   1.125   "!!evs. P --> (X : analz (G Un H)) --> (X : analz H)  ==> \
   1.126  \        P --> (X : analz (G Un H)) = (X : analz H)";
   1.127 -by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
   1.128 +by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
   1.129  val Nonce_secrecy_lemma = result();
   1.130  
   1.131  goal thy 
   1.132 @@ -394,7 +394,7 @@
   1.133  by (not_bad_tac "A" 1);
   1.134  by (dtac (Says_imp_spies RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
   1.135      THEN REPEAT (assume_tac 1));
   1.136 -by (blast_tac (!claset addIs [KeyWithNonceI]) 1);
   1.137 +by (blast_tac (claset() addIs [KeyWithNonceI]) 1);
   1.138  qed_spec_mp "Nonce_secrecy";
   1.139  
   1.140  
   1.141 @@ -424,11 +424,11 @@
   1.142  (*Fake*)
   1.143  by (REPEAT (etac (exI RSN (2,exE)) 1)   (*stripping EXs makes proof faster*)
   1.144      THEN Fake_parts_insert_tac 1);
   1.145 -by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   1.146 +by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1); 
   1.147  (*YM2: creation of new Nonce.  Move assertion into global context*)
   1.148  by (expand_case_tac "nb = ?y" 1);
   1.149  by (REPEAT (resolve_tac [exI, conjI, impI, refl] 1));
   1.150 -by (blast_tac (!claset addSEs spies_partsEs) 1);
   1.151 +by (blast_tac (claset() addSEs spies_partsEs) 1);
   1.152  val lemma = result();
   1.153  
   1.154  goal thy 
   1.155 @@ -450,7 +450,7 @@
   1.156  \          nb ~: analz (spies evs);  evs : yahalom |]        \
   1.157  \        ==> NA' = NA & A' = A & B' = B";
   1.158  by (not_bad_tac "B'" 1);
   1.159 -by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
   1.160 +by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj]
   1.161                         addSEs [MPair_parts]
   1.162                         addDs  [unique_NB]) 1);
   1.163  qed "Says_unique_NB";
   1.164 @@ -465,7 +465,7 @@
   1.165  \     Crypt (shrK B)  {|Agent A, Nonce NA, Nonce NB|} ~: parts(spies evs)";
   1.166  by (parts_induct_tac 1);
   1.167  by (Fake_parts_insert_tac 1);
   1.168 -by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj]
   1.169 +by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]
   1.170                         addSIs [parts_insertI]
   1.171                         addSEs partsEs) 1);
   1.172  bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE));
   1.173 @@ -497,19 +497,19 @@
   1.174  by analz_spies_tac;
   1.175  by (ALLGOALS
   1.176      (asm_simp_tac 
   1.177 -     (!simpset addsimps (expand_ifs@pushes)
   1.178 +     (simpset() addsimps (expand_ifs@pushes)
   1.179  	       addsimps [analz_insert_eq, analz_insert_freshK])));
   1.180  (*Prove YM3 by showing that no NB can also be an NA*)
   1.181 -by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj]
   1.182 +by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj]
   1.183  	               addSEs [MPair_parts]
   1.184  		       addDs  [no_nonce_YM1_YM2, Says_unique_NB]) 4
   1.185      THEN flexflex_tac);
   1.186  (*YM2: similar freshness reasoning*) 
   1.187 -by (blast_tac (!claset addSEs partsEs
   1.188 +by (blast_tac (claset() addSEs partsEs
   1.189  		       addDs  [Says_imp_spies RS analz.Inj,
   1.190  			       impOfSubs analz_subset_parts]) 3);
   1.191  (*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*)
   1.192 -by (blast_tac (!claset addSIs [parts_insertI]
   1.193 +by (blast_tac (claset() addSIs [parts_insertI]
   1.194                         addSEs spies_partsEs) 2);
   1.195  (*Fake*)
   1.196  by (spy_analz_tac 1);
   1.197 @@ -522,19 +522,19 @@
   1.198  by (forward_tac [Says_Server_imp_YM2] 4);
   1.199  by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, exE, disjE]));
   1.200  (*  use Says_unique_NB to identify message components: Aa=A, Ba=B, NAa=NA *)
   1.201 -by (blast_tac (!claset addDs [Says_unique_NB, Spy_not_see_encrypted_key,
   1.202 +by (blast_tac (claset() addDs [Says_unique_NB, Spy_not_see_encrypted_key,
   1.203  			      impOfSubs Fake_analz_insert]) 1);
   1.204  (** LEVEL 14 **)
   1.205  (*Oops case: if the nonce is betrayed now, show that the Oops event is 
   1.206    covered by the quantified Oops assumption.*)
   1.207 -by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
   1.208 +by (full_simp_tac (simpset() addsimps [all_conj_distrib]) 1);
   1.209  by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
   1.210  by (expand_case_tac "NB = NBa" 1);
   1.211  (*If NB=NBa then all other components of the Oops message agree*)
   1.212 -by (blast_tac (!claset addDs [Says_unique_NB]) 1 THEN flexflex_tac);
   1.213 +by (blast_tac (claset() addDs [Says_unique_NB]) 1 THEN flexflex_tac);
   1.214  (*case NB ~= NBa*)
   1.215 -by (asm_simp_tac (!simpset addsimps [single_Nonce_secrecy]) 1);
   1.216 -by (blast_tac (!claset addSEs [MPair_parts]
   1.217 +by (asm_simp_tac (simpset() addsimps [single_Nonce_secrecy]) 1);
   1.218 +by (blast_tac (claset() addSEs [MPair_parts]
   1.219  		       addDs  [Says_imp_spies RS parts.Inj, 
   1.220  			       no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1);
   1.221  bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp));
   1.222 @@ -565,7 +565,7 @@
   1.223  by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
   1.224  by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1);
   1.225  by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1));
   1.226 -by (blast_tac (!claset addDs [Says_unique_NB]) 1);
   1.227 +by (blast_tac (claset() addDs [Says_unique_NB]) 1);
   1.228  qed "B_trusts_YM4";
   1.229  
   1.230  
   1.231 @@ -596,7 +596,7 @@
   1.232  (*YM4*)
   1.233  by (Blast_tac 2);
   1.234  (*YM3*)
   1.235 -by (best_tac (!claset addSDs [B_Said_YM2, Says_imp_spies RS parts.Inj]
   1.236 +by (best_tac (claset() addSDs [B_Said_YM2, Says_imp_spies RS parts.Inj]
   1.237  		      addSEs [MPair_parts]) 1);
   1.238  val lemma = result() RSN (2, rev_mp) RS mp |> standard;
   1.239  
   1.240 @@ -607,7 +607,7 @@
   1.241  \           A ~: bad;  B ~: bad;  evs : yahalom |]                        \
   1.242  \   ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
   1.243  \         : set evs";
   1.244 -by (blast_tac (!claset addSDs [A_trusts_YM3, lemma]
   1.245 +by (blast_tac (claset() addSDs [A_trusts_YM3, lemma]
   1.246  		       addEs spies_partsEs) 1);
   1.247  qed "YM3_auth_B_to_A";
   1.248  
   1.249 @@ -628,12 +628,12 @@
   1.250  (*Fake*)
   1.251  by (Fake_parts_insert_tac 1);
   1.252  (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
   1.253 -by (fast_tac (!claset addSDs [Crypt_imp_invKey_keysFor] addss (!simpset)) 1); 
   1.254 +by (fast_tac (claset() addSDs [Crypt_imp_invKey_keysFor] addss (simpset())) 1); 
   1.255  (*YM4: was Crypt K (Nonce NB) the very last message?  If not, use ind. hyp.*)
   1.256 -by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
   1.257 +by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
   1.258  (*yes: apply unicity of session keys*)
   1.259  by (not_bad_tac "Aa" 1);
   1.260 -by (blast_tac (!claset addSEs [MPair_parts]
   1.261 +by (blast_tac (claset() addSEs [MPair_parts]
   1.262                         addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
   1.263  		       addDs  [Says_imp_spies RS parts.Inj,
   1.264  			       unique_session_keys]) 1);
   1.265 @@ -657,6 +657,6 @@
   1.266  by (rtac lemma 1);
   1.267  by (rtac Spy_not_see_encrypted_key 2);
   1.268  by (REPEAT_FIRST assume_tac);
   1.269 -by (blast_tac (!claset addSEs [MPair_parts]
   1.270 +by (blast_tac (claset() addSEs [MPair_parts]
   1.271  	       	       addDs [Says_imp_spies RS parts.Inj]) 1);
   1.272  qed_spec_mp "YM4_imp_A_Said_YM3";