src/HOL/Auth/Yahalom.ML

 (** For reasoning about the encrypted portion of messages **)
 
 (*Lets us treat YM4 using a similar argument as for the Fake case.*)
 goal thy "!!evs. Says S A {|Crypt (shrK A) Y, X|} : set evs ==> \
 \                X : analz (spies evs)";
-by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1);
+by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
 qed "YM4_analz_spies";
 
 bind_thm ("YM4_parts_spies",
           YM4_analz_spies RS (impOfSubs analz_subset_parts));
 
 (*Relates to both YM4 and Oops*)
 goal thy "!!evs. Says S A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} : set evs ==> \
 \                K : parts (spies evs)";
-by (blast_tac (!claset addSEs partsEs
+by (blast_tac (claset() addSEs partsEs
                       addSDs [Says_imp_spies RS parts.Inj]) 1);
 qed "YM4_Key_parts_spies";
 
 (*For proving the easier theorems about X ~: parts (spies evs).*)
 fun parts_spies_tac i = 

 qed "Spy_see_shrK";
 Addsimps [Spy_see_shrK];
 
 goal thy 
  "!!evs. evs : yahalom ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
-by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
+by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
 qed "Spy_analz_shrK";
 Addsimps [Spy_analz_shrK];
 
 goal thy  "!!A. [| Key (shrK A) : parts (spies evs);       \
 \                  evs : yahalom |] ==> A:bad";
-by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
+by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
 qed "Spy_see_shrK_D";
 
 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
 

 goal thy "!!evs. evs : yahalom ==>          \
 \         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
 by (parts_induct_tac 1);
 (*Fake*)
 by (best_tac
-      (!claset addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
+      (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
                addIs  [impOfSubs analz_subset_parts]
                addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
-               addss  (!simpset)) 1);
+               addss  (simpset())) 1);
 (*YM2-4: Because Key K is not fresh, etc.*)
-by (REPEAT (blast_tac (!claset addSEs spies_partsEs) 1));
+by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1));
 qed_spec_mp "new_keys_not_used";
 
 bind_thm ("new_keys_not_analzd",
           [analz_subset_parts RS keysFor_mono,
            new_keys_not_used] MRS contra_subsetD);

 \      EX A' B' na' nb' X'. ALL A B na nb X.                        \
 \          Says Server A                                            \
 \           {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}        \
 \          : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
 by (etac yahalom.induct 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
 by (ALLGOALS Clarify_tac);
 by (ex_strip_tac 2);
 by (Blast_tac 2);
 (*Remaining case: YM3*)
 by (expand_case_tac "K = ?y" 1);
 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
 (*...we assume X is a recent message and handle this case by contradiction*)
-by (blast_tac (!claset addSEs spies_partsEs
+by (blast_tac (claset() addSEs spies_partsEs
                        delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
 val lemma = result();
 
 goal thy 
 "!!evs. [| Says Server A                                                 \

 \            Key K ~: analz (spies evs)";
 by (etac yahalom.induct 1);
 by analz_spies_tac;
 by (ALLGOALS
     (asm_simp_tac 
-     (!simpset addsimps (expand_ifs@pushes)
+     (simpset() addsimps (expand_ifs@pushes)
 	       addsimps [analz_insert_eq, analz_insert_freshK])));
 (*Oops*)
-by (blast_tac (!claset addDs [unique_session_keys]) 3);
+by (blast_tac (claset() addDs [unique_session_keys]) 3);
 (*YM3*)
-by (blast_tac (!claset delrules [impCE]
+by (blast_tac (claset() delrules [impCE]
                        addSEs spies_partsEs
                        addIs [impOfSubs analz_subset_parts]) 2);
 (*Fake*) 
 by (spy_analz_tac 1);
 val lemma = result() RS mp RS mp RSN(2,rev_notE);

 \             : set evs;                                          \
 \           Says A Spy {|na, nb, Key K|} ~: set evs;              \
 \           A ~: bad;  B ~: bad;  evs : yahalom |]         \
 \        ==> Key K ~: analz (spies evs)";
 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
-by (blast_tac (!claset addSEs [lemma]) 1);
+by (blast_tac (claset() addSEs [lemma]) 1);
 qed "Spy_not_see_encrypted_key";
 
 
 (** Security Guarantee for A upon receiving YM3 **)
 

 by (Fake_parts_insert_tac 1);
 (*YM4*)
 (*A is uncompromised because NB is secure*)
 by (not_bad_tac "A" 1);
 (*A's certificate guarantees the existence of the Server message*)
-by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS
+by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS
 			      A_trusts_YM3]) 1);
 bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp));
 
 
 (**** Towards proving secrecy of Nonce NB ****)

 
 (*A fresh key cannot be associated with any nonce 
   (with respect to a given trace). *)
 goalw thy [KeyWithNonce_def]
  "!!evs. Key K ~: used evs ==> ~ KeyWithNonce K NB evs";
-by (blast_tac (!claset addSEs spies_partsEs) 1);
+by (blast_tac (claset() addSEs spies_partsEs) 1);
 qed "fresh_not_KeyWithNonce";
 
 (*The Server message associates K with NB' and therefore not with any 
   other nonce NB.*)
 goalw thy [KeyWithNonce_def]
  "!!evs. [| Says Server A                                                \
 \                {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|} \
 \             : set evs;                                                 \
 \           NB ~= NB';  evs : yahalom |]                            \
 \        ==> ~ KeyWithNonce K NB evs";
-by (blast_tac (!claset addDs [unique_session_keys]) 1);
+by (blast_tac (claset() addDs [unique_session_keys]) 1);
 qed "Says_Server_KeyWithNonce";
 
 
 (*The only nonces that can be found with the help of session keys are
   those distributed as nonce NB by the Server.  The form of the theorem

 (*As with analz_image_freshK, we take some pains to express the property
   as a logical equivalence so that the simplifier can apply it.*)
 goal thy  
  "!!evs. P --> (X : analz (G Un H)) --> (X : analz H)  ==> \
 \        P --> (X : analz (G Un H)) = (X : analz H)";
-by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
+by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
 val Nonce_secrecy_lemma = result();
 
 goal thy 
  "!!evs. evs : yahalom ==>                                         \
 \        (ALL KK. KK <= Compl (range shrK) -->                          \

 by (spy_analz_tac 1);
 (*YM4*)  (** LEVEL 7 **)
 by (not_bad_tac "A" 1);
 by (dtac (Says_imp_spies RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
     THEN REPEAT (assume_tac 1));
-by (blast_tac (!claset addIs [KeyWithNonceI]) 1);
+by (blast_tac (claset() addIs [KeyWithNonceI]) 1);
 qed_spec_mp "Nonce_secrecy";
 
 
 (*Version required below: if NB can be decrypted using a session key then it
   was distributed with that key.  The more general form above is required

 \      --> B ~: bad --> NA = NA' & A = A' & B = B'";
 by (parts_induct_tac 1);
 (*Fake*)
 by (REPEAT (etac (exI RSN (2,exE)) 1)   (*stripping EXs makes proof faster*)
     THEN Fake_parts_insert_tac 1);
-by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
+by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1); 
 (*YM2: creation of new Nonce.  Move assertion into global context*)
 by (expand_case_tac "nb = ?y" 1);
 by (REPEAT (resolve_tac [exI, conjI, impI, refl] 1));
-by (blast_tac (!claset addSEs spies_partsEs) 1);
+by (blast_tac (claset() addSEs spies_partsEs) 1);
 val lemma = result();
 
 goal thy 
  "!!evs.[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts (spies evs); \
 \          Crypt (shrK B') {|Agent A', Nonce NA', nb|} : parts (spies evs); \

 \          Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|} \
 \            : set evs;                                                   \
 \          nb ~: analz (spies evs);  evs : yahalom |]        \
 \        ==> NA' = NA & A' = A & B' = B";
 by (not_bad_tac "B'" 1);
-by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
+by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj]
                        addSEs [MPair_parts]
                        addDs  [unique_NB]) 1);
 qed "Says_unique_NB";
 
 

 \ ==> Nonce NB ~: analz (spies evs) -->           \
 \     Crypt (shrK B') {|Agent A', Nonce NB, nb'|} : parts(spies evs) --> \
 \     Crypt (shrK B)  {|Agent A, Nonce NA, Nonce NB|} ~: parts(spies evs)";
 by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
-by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj]
+by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]
                        addSIs [parts_insertI]
                        addSEs partsEs) 1);
 bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE));
 
 (*The Server sends YM3 only in response to YM2.*)

 \     Nonce NB ~: analz (spies evs)";
 by (etac yahalom.induct 1);
 by analz_spies_tac;
 by (ALLGOALS
     (asm_simp_tac 
-     (!simpset addsimps (expand_ifs@pushes)
+     (simpset() addsimps (expand_ifs@pushes)
 	       addsimps [analz_insert_eq, analz_insert_freshK])));
 (*Prove YM3 by showing that no NB can also be an NA*)
-by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj]
+by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj]
 	               addSEs [MPair_parts]
 		       addDs  [no_nonce_YM1_YM2, Says_unique_NB]) 4
     THEN flexflex_tac);
 (*YM2: similar freshness reasoning*) 
-by (blast_tac (!claset addSEs partsEs
+by (blast_tac (claset() addSEs partsEs
 		       addDs  [Says_imp_spies RS analz.Inj,
 			       impOfSubs analz_subset_parts]) 3);
 (*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*)
-by (blast_tac (!claset addSIs [parts_insertI]
+by (blast_tac (claset() addSIs [parts_insertI]
                        addSEs spies_partsEs) 2);
 (*Fake*)
 by (spy_analz_tac 1);
 (** LEVEL 7: YM4 and Oops remain **)
 by (ALLGOALS Clarify_tac);

 by (dtac (Says_imp_spies RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
 by (forward_tac [Says_Server_message_form] 3);
 by (forward_tac [Says_Server_imp_YM2] 4);
 by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, exE, disjE]));
 (*  use Says_unique_NB to identify message components: Aa=A, Ba=B, NAa=NA *)
-by (blast_tac (!claset addDs [Says_unique_NB, Spy_not_see_encrypted_key,
+by (blast_tac (claset() addDs [Says_unique_NB, Spy_not_see_encrypted_key,
 			      impOfSubs Fake_analz_insert]) 1);
 (** LEVEL 14 **)
 (*Oops case: if the nonce is betrayed now, show that the Oops event is 
   covered by the quantified Oops assumption.*)
-by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
+by (full_simp_tac (simpset() addsimps [all_conj_distrib]) 1);
 by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
 by (expand_case_tac "NB = NBa" 1);
 (*If NB=NBa then all other components of the Oops message agree*)
-by (blast_tac (!claset addDs [Says_unique_NB]) 1 THEN flexflex_tac);
+by (blast_tac (claset() addDs [Says_unique_NB]) 1 THEN flexflex_tac);
 (*case NB ~= NBa*)
-by (asm_simp_tac (!simpset addsimps [single_Nonce_secrecy]) 1);
-by (blast_tac (!claset addSEs [MPair_parts]
+by (asm_simp_tac (simpset() addsimps [single_Nonce_secrecy]) 1);
+by (blast_tac (claset() addSEs [MPair_parts]
 		       addDs  [Says_imp_spies RS parts.Inj, 
 			       no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1);
 bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp));
 
 

     dtac B_trusts_YM4_shrK 1);
 by (dtac B_trusts_YM4_newK 3);
 by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
 by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1);
 by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1));
-by (blast_tac (!claset addDs [Says_unique_NB]) 1);
+by (blast_tac (claset() addDs [Says_unique_NB]) 1);
 qed "B_trusts_YM4";
 
 
 
 (*** Authenticating B to A ***)

 by (etac yahalom.induct 1);
 by (ALLGOALS Asm_simp_tac);
 (*YM4*)
 by (Blast_tac 2);
 (*YM3*)
-by (best_tac (!claset addSDs [B_Said_YM2, Says_imp_spies RS parts.Inj]
+by (best_tac (claset() addSDs [B_Said_YM2, Says_imp_spies RS parts.Inj]
 		      addSEs [MPair_parts]) 1);
 val lemma = result() RSN (2, rev_mp) RS mp |> standard;
 
 (*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
 goal thy
  "!!evs. [| Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
 \             : set evs;                                                    \
 \           A ~: bad;  B ~: bad;  evs : yahalom |]                        \
 \   ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
 \         : set evs";
-by (blast_tac (!claset addSDs [A_trusts_YM3, lemma]
+by (blast_tac (claset() addSDs [A_trusts_YM3, lemma]
 		       addEs spies_partsEs) 1);
 qed "YM3_auth_B_to_A";
 
 
 (*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)

 \            (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
 by (parts_induct_tac 1);
 (*Fake*)
 by (Fake_parts_insert_tac 1);
 (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
-by (fast_tac (!claset addSDs [Crypt_imp_invKey_keysFor] addss (!simpset)) 1); 
+by (fast_tac (claset() addSDs [Crypt_imp_invKey_keysFor] addss (simpset())) 1); 
 (*YM4: was Crypt K (Nonce NB) the very last message?  If not, use ind. hyp.*)
-by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
+by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
 (*yes: apply unicity of session keys*)
 by (not_bad_tac "Aa" 1);
-by (blast_tac (!claset addSEs [MPair_parts]
+by (blast_tac (claset() addSEs [MPair_parts]
                        addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
 		       addDs  [Says_imp_spies RS parts.Inj,
 			       unique_session_keys]) 1);
 val lemma = normalize_thm [RSspec, RSmp] (result()) |> standard;
 

 by (REPEAT_FIRST (eresolve_tac [asm_rl, spec]));
 by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1);
 by (rtac lemma 1);
 by (rtac Spy_not_see_encrypted_key 2);
 by (REPEAT_FIRST assume_tac);
-by (blast_tac (!claset addSEs [MPair_parts]
+by (blast_tac (claset() addSEs [MPair_parts]
 	       	       addDs [Says_imp_spies RS parts.Inj]) 1);
 qed_spec_mp "YM4_imp_A_Said_YM3";