Working version of NS, messages 1-3, WITH INTERLEAVING
authorpaulson
Tue Aug 20 17:46:24 1996 +0200 (1996-08-20)
changeset 1929f0839bab4b00
parent 1928 3d1d73e3d185
child 1930 cdf9bcd53749
Working version of NS, messages 1-3, WITH INTERLEAVING
src/HOL/Auth/Event.ML
src/HOL/Auth/Event.thy
src/HOL/Auth/Message.ML
     1.1 --- a/src/HOL/Auth/Event.ML	Tue Aug 20 12:40:17 1996 +0200
     1.2 +++ b/src/HOL/Auth/Event.ML	Tue Aug 20 17:46:24 1996 +0200
     1.3 @@ -9,11 +9,16 @@
     1.4  Rewrites should not refer to	 initState (Friend i)    -- not in normal form
     1.5  *)
     1.6  
     1.7 +Addsimps [parts_cut_eq];
     1.8 +
     1.9 +
    1.10 +(*INSTALLED ON NAT.ML*)
    1.11 +goalw Nat.thy [le_def] "(m <= n) = (m < Suc n)";
    1.12 +by (rtac not_less_eq 1);
    1.13 +qed "le_eq_less_Suc";
    1.14  
    1.15  proof_timing:=true;
    1.16  
    1.17 -Delrules [less_SucE];	(*Perhaps avoid inserting this in Arith.ML????*)
    1.18 -
    1.19  (*FOR LIST.ML??*)
    1.20  goal List.thy "x : set_of_list (x#xs)";
    1.21  by (Simp_tac 1);
    1.22 @@ -98,7 +103,7 @@
    1.23  
    1.24  goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
    1.25  by (agent.induct_tac "C" 1);
    1.26 -by (auto_tac (!claset addIs [range_eqI], !simpset));
    1.27 +by (auto_tac (!claset addIs [range_eqI] delrules partsEs, !simpset));
    1.28  qed "keysFor_parts_initState";
    1.29  Addsimps [keysFor_parts_initState];
    1.30  
    1.31 @@ -228,8 +233,6 @@
    1.32   "!!evs. evs : traces ==> \
    1.33  \     sees A evs <= initState A Un sees Enemy evs";
    1.34  be traces.induct 1;
    1.35 -be subst 4;	(*NS2: discard evsa = Says A Server... as irrelevant!*)
    1.36 -be subst 5;	(*NS3: discard evsa = Says S Aa... as irrelevant!*)
    1.37  by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
    1.38  			        addss (!simpset))));
    1.39  qed "sees_agent_subset_sees_Enemy";
    1.40 @@ -251,6 +254,13 @@
    1.41  AddSEs   [not_Notes RSN (2, rev_notE)];
    1.42  
    1.43  
    1.44 +goal thy "!!evs. (Says S A (Crypt {|N, B, K, X|} KA)) : set_of_list evs ==> \
    1.45 +\                X : parts (sees Enemy evs)";
    1.46 +by (fast_tac (!claset addSEs partsEs
    1.47 +	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
    1.48 +qed "NS3_msg_in_parts_sees_Enemy";
    1.49 +			      
    1.50 +
    1.51  (*** Server keys are not betrayed ***)
    1.52  
    1.53  (*Enemy never sees another agent's server key!*)
    1.54 @@ -258,12 +268,11 @@
    1.55   "!!evs. [| evs : traces; A ~= Enemy |] ==> \
    1.56  \        Key (serverKey A) ~: parts (sees Enemy evs)";
    1.57  be traces.induct 1;
    1.58 -be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
    1.59 -by (auto_tac(!claset, !simpset addsimps [parts_insert2]));
    1.60 -(*Deals with Faked messages*)
    1.61 +bd NS3_msg_in_parts_sees_Enemy 5;
    1.62 +by (Auto_tac());
    1.63 +(*Deals with Fake message*)
    1.64  by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    1.65 -			     impOfSubs parts_insert_subset_Un]
    1.66 -	              addss (!simpset)) 1);
    1.67 +			     impOfSubs synth_analz_parts_insert_subset_Un]) 1);
    1.68  qed "Enemy_not_see_serverKey";
    1.69  
    1.70  bind_thm ("Enemy_not_analz_serverKey",
    1.71 @@ -330,21 +339,13 @@
    1.72  \                length evs <= length evs' --> \
    1.73  \                          Key (newK evs') ~: (UN C. parts (sees C evs))";
    1.74  be traces.induct 1;
    1.75 -be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
    1.76 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [Suc_le_eq])));
    1.77 -(*Initial state?  New keys cannot clash*)
    1.78 -by (Fast_tac 1);
    1.79 -(*Rule NS1 in protocol*)
    1.80 -by (fast_tac (!claset addDs [less_imp_le]) 2);
    1.81 -(*Rule NS2 in protocol*)
    1.82 -by (fast_tac (!claset addIs [less_imp_le] addss (!simpset)) 2);
    1.83 -(*Rule NS3 in protocol*)
    1.84 -by (fast_tac (!claset addIs [less_imp_le] addss (!simpset)) 2);
    1.85 -(*Rule Fake: where an Enemy agent can say practically anything*)
    1.86 -by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    1.87 -			     impOfSubs parts_insert_subset_Un,
    1.88 -			     less_imp_le]
    1.89 -	              addss (!simpset)) 1);
    1.90 +bd NS3_msg_in_parts_sees_Enemy 5;
    1.91 +(*auto_tac does not work here, as it performs safe_tac first*)
    1.92 +by (ALLGOALS Asm_simp_tac);
    1.93 +by (ALLGOALS (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    1.94 +				       impOfSubs parts_insert_subset_Un,
    1.95 +				       Suc_leD]
    1.96 +			        addss (!simpset))));
    1.97  val lemma = result();
    1.98  
    1.99  (*Variant needed for the main theorem below*)
   1.100 @@ -381,31 +382,16 @@
   1.101  \                length evs <= length evs' --> \
   1.102  \                newK evs' ~: keysFor (UN C. parts (sees C evs))";
   1.103  be traces.induct 1;
   1.104 -be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
   1.105 -by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [Suc_le_eq])));
   1.106 -(*Rule NS1 in protocol*)
   1.107 -by (fast_tac (!claset addDs [less_imp_le]) 2);
   1.108 -(*Rule NS2 in protocol*)
   1.109 -by (fast_tac (!claset addDs [less_imp_le]) 2);
   1.110 -(*Rule Fake: where an Enemy agent can say practically anything*)
   1.111 -by (best_tac 
   1.112 -    (!claset addSDs [newK_invKey]
   1.113 -	     addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   1.114 -		    impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   1.115 -		    less_imp_le]
   1.116 -             addEs [new_keys_not_seen RS not_parts_not_analz RSN (2,rev_notE)]
   1.117 -	     addss (!simpset)) 1);
   1.118 -(*Rule NS3: quite messy...*)
   1.119 -by (hyp_subst_tac 1);
   1.120 -by (full_simp_tac (!simpset addcongs [conj_cong]) 1);
   1.121 -br impI 1;
   1.122 -bd mp 1;
   1.123 -by (fast_tac (!claset addDs [less_imp_le]) 1);
   1.124 -by (best_tac (!claset addIs 
   1.125 -	      [impOfSubs (sees_subset_sees_Says RS keysFor_parts_mono),
   1.126 -	       impOfSubs (sees_own RS equalityD2 RS keysFor_parts_mono),
   1.127 -	       impOfSubs (empty_subsetI RS insert_mono RS keysFor_parts_mono)]
   1.128 -              addss (!simpset)) 1);
   1.129 +bd NS3_msg_in_parts_sees_Enemy 5;
   1.130 +by (ALLGOALS Asm_simp_tac);
   1.131 +by (ALLGOALS
   1.132 +    (best_tac 
   1.133 +     (!claset addSDs [newK_invKey]
   1.134 +	      addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   1.135 +		     impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   1.136 +		     Suc_leD]
   1.137 +	      addEs [new_keys_not_seen RS not_parts_not_analz RSN (2,rev_notE)]
   1.138 +	      addss (!simpset))));
   1.139  val lemma = result();
   1.140  
   1.141  goal thy 
   1.142 @@ -453,7 +439,6 @@
   1.143  \                         length evt < length evs)";
   1.144  be rev_mp 1;
   1.145  be traces.induct 1;
   1.146 -be subst 4;	(*NS2: discard evsa = Says A Server...#evs' as irrelevant!*)
   1.147  by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
   1.148  qed "Says_Server_message_form";
   1.149  
   1.150 @@ -472,7 +457,6 @@
   1.151  \     K ~: analz (insert (Key (serverKey (Friend k))) (sees Enemy evs))";
   1.152  be rev_mp 1;
   1.153  be traces.induct 1;
   1.154 -be subst 4;	(*NS2: discard evsa = Says A Server... as irrelevant!*)
   1.155  by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes)));
   1.156  by (Step_tac 1);
   1.157  by (asm_full_simp_tac (!simpset addsimps[analz_subset_parts RS contra_subsetD]) 1);
   1.158 @@ -489,33 +473,16 @@
   1.159  \          (EX evt:traces. K = newK evt & \
   1.160  \                          X = (Crypt {|Key K, Agent A|} (serverKey B)))";
   1.161  be traces.induct 1;
   1.162 -be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
   1.163 +bd NS3_msg_in_parts_sees_Enemy 5;
   1.164  by (Step_tac 1);
   1.165  by (ALLGOALS Asm_full_simp_tac);
   1.166 -(*Remaining cases are Fake, NS2 and NS3*)
   1.167 +(*Remaining cases are Fake and NS2*)
   1.168  by (fast_tac (!claset addSDs [spec]) 2);
   1.169 -(*The NS3 case needs the induction hypothesis twice!
   1.170 -    One application is to the X component of the most recent message.*)
   1.171 -by (full_simp_tac (!simpset addsimps [conj_disj_distribR, 
   1.172 -				      all_conj_distrib]) 2);
   1.173 -be conjE 2;
   1.174 -by (subgoal_tac "? evs':traces. K = newK evs' & \
   1.175 -\                     X = Crypt {|Key K, Agent (Friend i)|} (serverKey B)" 2);
   1.176 -(*DELETE the second quantified formula for speed*)
   1.177 -by (eres_inst_tac [("V","ALL A NA B K Xa. ?f A NA B K Xa : ?H X & ?P(A) --> \
   1.178 -\                                         ?Q K Xa A B")] thin_rl 3);
   1.179 -by (fast_tac (!claset addSEs [allE, mp] addss (!simpset)) 3);
   1.180 -(*DELETE the first quantified formula: it's now useless*)
   1.181 -by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
   1.182 -by (fast_tac (!claset addss (!simpset)) 2);
   1.183  (*Now for the Fake case*)
   1.184 -by (subgoal_tac 
   1.185 -    "Crypt {|Nonce NA, Agent Ba, Key K, Xa|} (serverKey A) : \
   1.186 -\    parts (synth (analz (sees Enemy evsa)) Un (sees Enemy evsa))" 1);
   1.187 -by (fast_tac (!claset addSEs [impOfSubs parts_mono]) 2);
   1.188 -by (best_tac (!claset addDs [impOfSubs analz_subset_parts]
   1.189 +by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.190 +			     impOfSubs synth_analz_parts_insert_subset_Un]
   1.191  	              addss (!simpset)) 1);
   1.192 -val encrypted_form = result();
   1.193 +qed_spec_mp "encrypted_form";
   1.194  
   1.195  
   1.196  (*For eliminating the A ~= Enemy condition from the previous result*)
   1.197 @@ -526,18 +493,17 @@
   1.198  \            : set_of_list evs  -->   \
   1.199  \        S = Server | S = Enemy";
   1.200  be traces.induct 1;
   1.201 -be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
   1.202  by (ALLGOALS Asm_simp_tac);
   1.203  (*We are left with NS3*)
   1.204  by (subgoal_tac "S = Server | S = Enemy" 1);
   1.205  (*First justify this assumption!*)
   1.206  by (fast_tac (!claset addSEs [allE, mp] addss (!simpset)) 2);
   1.207  by (Step_tac 1);
   1.208 -bd (set_of_list_I1 RS Says_Server_message_form) 1;
   1.209 +bd Says_Server_message_form 1;
   1.210  by (ALLGOALS Full_simp_tac);
   1.211  (*Final case.  Clear out needless quantifiers to speed the following step*)
   1.212  by (eres_inst_tac [("V","ALL x. ?P(x)")] thin_rl 1);
   1.213 -bd (normalize_thm [RSspec,RSmp] encrypted_form) 1;
   1.214 +bd encrypted_form 1;
   1.215  br (parts.Inj RS conjI) 1;
   1.216  auto();
   1.217  qed_spec_mp "Server_or_Enemy";
   1.218 @@ -555,7 +521,7 @@
   1.219  ba 1;
   1.220  by (Step_tac 1);
   1.221  by (fast_tac (!claset addSDs [Says_Server_message_form] addss (!simpset)) 1);
   1.222 -by (forward_tac [normalize_thm [RSspec,RSmp] encrypted_form] 1);
   1.223 +by (forward_tac [encrypted_form] 1);
   1.224  br (parts.Inj RS conjI) 1;
   1.225  by (auto_tac (!claset addIs [Says_imp_old_keys], !simpset));
   1.226  qed "Says_S_message_form";
   1.227 @@ -595,16 +561,13 @@
   1.228  \        (Crypt X (newK evt)) : parts (sees Enemy evs) & \
   1.229  \        Key K : parts {X} --> Key K : parts (sees Enemy evs)";
   1.230  be traces.induct 1;
   1.231 -be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
   1.232 -by (hyp_subst_tac 5);	(*NS3: apply evsa = Says S A (Crypt ...) # ... *)
   1.233 +bd NS3_msg_in_parts_sees_Enemy 5;
   1.234  by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
   1.235 -(*Case NS3*)
   1.236 -by (res_inst_tac [("x1","Xa")] (insert_commute RS ssubst) 2);
   1.237 -by (Asm_full_simp_tac 2);
   1.238  (*Deals with Faked messages*)
   1.239 -by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.240 -			     impOfSubs parts_insert_subset_Un]
   1.241 -	              addss (!simpset)) 1);
   1.242 +by (best_tac (!claset addSEs partsEs
   1.243 +		      addDs [impOfSubs analz_subset_parts,
   1.244 +                             impOfSubs parts_insert_subset_Un]
   1.245 +                      addss (!simpset)) 1);
   1.246  result();
   1.247  
   1.248  
   1.249 @@ -634,8 +597,7 @@
   1.250  \            Key K : analz (insert (Key (serverKey C)) \
   1.251  \                             (sees Enemy evs)))";
   1.252  be traces.induct 1;
   1.253 -be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
   1.254 -by (dtac Says_S_message_form_eq 5 THEN assume_tac 5);	
   1.255 +by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);	
   1.256  by (REPEAT ((eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac) 5));
   1.257  by (ALLGOALS 
   1.258      (asm_simp_tac 
   1.259 @@ -649,14 +611,14 @@
   1.260  (** LEVEL 7 **)
   1.261  (*Fake case*)
   1.262  by (REPEAT (Safe_step_tac 1));
   1.263 -by (fast_tac (!claset addSEs [impOfSubs (analz_mono)]) 2);
   1.264 +by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 2);
   1.265  by (subgoal_tac 
   1.266      "Key K : analz \
   1.267  \             (synth \
   1.268  \              (analz (insert (Key (serverKey C)) \
   1.269  \                        (Key``(newK``E) Un (sees Enemy evsa)))))" 1);
   1.270  (*First, justify this subgoal*)
   1.271 -(*Discard the quantified formula for better speed*)
   1.272 +(*Discard formulae for better speed*)
   1.273  by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
   1.274  by (eres_inst_tac [("V","?Q ~: ?QQ")] thin_rl 2);
   1.275  by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)]
   1.276 @@ -668,11 +630,11 @@
   1.277  
   1.278  goal thy  
   1.279   "!!evs. evs : traces ==>                                  \
   1.280 -\        Key K : analz (insert (Key (newK evt))          \
   1.281 +\        Key K : analz (insert (Key (newK evt))            \
   1.282  \                         (insert (Key (serverKey C))      \
   1.283  \                          (sees Enemy evs))) =            \
   1.284  \             (K = newK evt |                              \
   1.285 -\              Key K : analz (insert (Key (serverKey C)) \
   1.286 +\              Key K : analz (insert (Key (serverKey C))   \
   1.287  \                               (sees Enemy evs)))";
   1.288  by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   1.289  				   insert_Key_singleton]) 1);
   1.290 @@ -681,17 +643,17 @@
   1.291  
   1.292  
   1.293  
   1.294 -(*If C=Enemy then of course he could make up all sorts of nonsense.*)
   1.295 +(*This says that the Key, K, uniquely identifies the message.
   1.296 +    But if C=Enemy then he could send all sorts of nonsense.*)
   1.297  goal thy 
   1.298   "!!evs. evs : traces ==>                      \
   1.299  \      EX X'. ALL C S A Y N B X.               \
   1.300  \         C ~= Enemy -->                       \
   1.301 -\         Says S A Y : set_of_list evs -->       \
   1.302 +\         Says S A Y : set_of_list evs -->     \
   1.303  \         ((Crypt {|N, Agent B, Key K, X|} (serverKey C)) : parts{Y} --> \
   1.304  \       (X = X'))";
   1.305  be traces.induct 1;
   1.306 -be subst 4;	(*NS2: discard evsa = Says A Server... as irrelevant!*)
   1.307 -by (dtac Says_S_message_form_eq 5 THEN assume_tac 5);	
   1.308 +by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);	
   1.309  by (ALLGOALS 
   1.310      (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib])));
   1.311  (*NS2: Case split propagates some context to other subgoal...*)
   1.312 @@ -699,6 +661,7 @@
   1.313  by (Asm_simp_tac 2);
   1.314  (*...we assume X is a very new message, and handle this case by contradiction*)
   1.315  by (fast_tac (!claset addIs [impOfSubs (subset_insertI RS parts_mono)]
   1.316 +		      addSEs partsEs
   1.317  		      addEs [Says_imp_old_keys RS less_irrefl]
   1.318  	              addss (!simpset)) 2);
   1.319  (*NS3: No relevant messages*)
   1.320 @@ -709,7 +672,7 @@
   1.321  br conjI 1;
   1.322  ba 2;
   1.323  by (Step_tac 1);
   1.324 -(** LEVEL 13 **)
   1.325 +(** LEVEL 12 **)
   1.326  by (subgoal_tac "Crypt {|N, Agent Ba, Key K, Xa|} (serverKey C) \
   1.327  \                  : parts (sees Enemy evsa)" 1);
   1.328  by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
   1.329 @@ -729,11 +692,12 @@
   1.330  (*In messages of this form, the session key uniquely identifies the rest*)
   1.331  goal thy 
   1.332   "!!evs. [| Says S A          \
   1.333 -\         (Crypt {|N, Agent B, Key K, X|} (serverKey C)) : set_of_list evs; \
   1.334 - \      Says S' A'                                         \
   1.335 -\         (Crypt {|N', Agent B', Key K, X'|} (serverKey C')) : set_of_list evs;                         \
   1.336 -\     \
   1.337 -\   evs : traces;  C ~= Enemy;  C' ~= Enemy    |] ==> X = X'";
   1.338 +\             (Crypt {|N, Agent B, Key K, X|} (serverKey C))     \
   1.339 +\                  : set_of_list evs; \
   1.340 + \          Says S' A'                                         \
   1.341 +\             (Crypt {|N', Agent B', Key K, X'|} (serverKey C')) \
   1.342 +\                  : set_of_list evs;                         \
   1.343 +\           evs : traces;  C ~= Enemy;  C' ~= Enemy    |] ==> X = X'";
   1.344  bd lemma 1;
   1.345  be exE 1;
   1.346  by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   1.347 @@ -752,7 +716,6 @@
   1.348  \     K ~: analz (insert (Key (serverKey C)) (sees Enemy evs))";
   1.349  be rev_mp 1;
   1.350  be traces.induct 1;
   1.351 -be subst 4;	(*NS2: discard evsa = Says A Server... as irrelevant!*)
   1.352  by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
   1.353  (*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
   1.354  by (REPEAT_FIRST (resolve_tac [conjI, impI]));
   1.355 @@ -765,7 +728,7 @@
   1.356                 setloop split_tac [expand_if])));
   1.357  (*NS2*)
   1.358  by (fast_tac (!claset addSEs [less_irrefl]) 2);
   1.359 -(** LEVEL 9 **)
   1.360 +(** LEVEL 8 **)
   1.361  (*Now for the Fake case*)
   1.362  br notI 1;
   1.363  by (subgoal_tac 
   1.364 @@ -773,49 +736,25 @@
   1.365  \    analz (synth (analz (insert (Key (serverKey C)) \
   1.366  \                                  (sees Enemy evsa))))" 1);
   1.367  be (impOfSubs analz_mono) 2;
   1.368 -by (deepen_tac (!claset addIs [analz_mono RS synth_mono RSN 
   1.369 -			     (2,rev_subsetD),
   1.370 -			     impOfSubs synth_increasing,
   1.371 -			     impOfSubs analz_increasing]) 0 2);
   1.372 +by (deepen_tac (!claset addIs [analz_mono RS synth_mono RSN (2,rev_subsetD),
   1.373 +			       impOfSubs synth_increasing,
   1.374 +			       impOfSubs analz_increasing]) 0 2);
   1.375  (*Proves the Fake goal*)
   1.376  by (fast_tac (!claset addss (!simpset)) 1);
   1.377  
   1.378 -(**LEVEL 14**)
   1.379 -(*Now for NS3*)
   1.380 -(*NS3, case 1: that message from the Server was just sent*)
   1.381 -by (ALLGOALS (forward_tac [traces_ConsE]));
   1.382 -by (forward_tac [set_of_list_I1 RS Says_Server_message_form] 1);
   1.383 -by (Full_simp_tac 1);
   1.384 -by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac));
   1.385 -(*Can simplify the Crypt messages: their key is secure*)
   1.386 -by (dres_inst_tac [("psi", "?X ~: ?H")] asm_rl 1);
   1.387 -by (asm_full_simp_tac
   1.388 -    (!simpset addsimps (pushes @ [analz_insert_Crypt,
   1.389 -				  analz_subset_parts RS contra_subsetD])) 1);
   1.390 -
   1.391 -(**LEVEL 20, one subgoal left! **)
   1.392 -(*NS3, case 2: that message from the Server was sent earlier*)
   1.393 -
   1.394 -(*simplify the good implication*)
   1.395 -by (Asm_full_simp_tac 1);       
   1.396 -(*delete the bad implication*)
   1.397 -by (eres_inst_tac [("V","?P-->?Q")] thin_rl 1); 
   1.398 -by ((forward_tac [Says_Server_message_form] THEN' assume_tac) 1);
   1.399 -by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac));
   1.400 -
   1.401 -(**LEVEL 24 **)
   1.402 -
   1.403 -by ((forward_tac [set_of_list_I1 RS Says_S_message_form]) 1);
   1.404 +(**LEVEL 13**)
   1.405 +(*NS3: that message from the Server was sent earlier*)
   1.406 +by (mp_tac 1);
   1.407 +by (forward_tac [Says_S_message_form] 1 THEN assume_tac 1);
   1.408  by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac));
   1.409  by (asm_full_simp_tac
   1.410      (!simpset addsimps (mem_if::analz_insert_Key_newK::pushes)) 1);
   1.411 -by (step_tac (!claset delrules [impCE]) 1);
   1.412 -
   1.413 -(**LEVEL 28 **)
   1.414 -bd ([impOfSubs set_of_list_subset_Cons, set_of_list_I1] MRS unique_session_keys) 1;
   1.415 -ba 1;
   1.416 +by (Step_tac 1);
   1.417 +(**LEVEL 18 **)
   1.418 +bd unique_session_keys 1;
   1.419 +by (REPEAT_FIRST assume_tac);
   1.420  by (ALLGOALS Full_simp_tac);
   1.421 -by (REPEAT_FIRST (eresolve_tac [conjE] ORELSE' hyp_subst_tac));
   1.422 +by (Step_tac 1);
   1.423  by (asm_full_simp_tac (!simpset addsimps [serverKey_mem_analz]) 1);
   1.424  qed "Enemy_not_see_encrypted_key";
   1.425  
   1.426 @@ -882,7 +821,6 @@
   1.427  \     K ~: analz (insert (Key (serverKey (Friend k))) (sees Enemy evs))";
   1.428  be rev_mp 1;
   1.429  be traces.induct 1;
   1.430 -be subst 4;	(*NS2: discard evsa = Says A Server... as irrelevant!*)
   1.431  by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes)));
   1.432  by (Step_tac 1);
   1.433  by (asm_full_simp_tac (!simpset addsimps[analz_subset_parts RS contra_subsetD]) 1);
   1.434 @@ -926,7 +864,6 @@
   1.435  \    (EX B'. Says Server B' (Crypt X (serverKey (Friend i))) : set_of_list evs | \
   1.436  \            Says (Friend i) B' (Crypt X (serverKey (Friend i))) : set_of_list evs)";
   1.437  be traces.induct 1;
   1.438 -be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
   1.439  by (Step_tac 1);
   1.440  by (ALLGOALS Asm_full_simp_tac);
   1.441  (*Remaining cases are Fake, NS2 and NS3*)
     2.1 --- a/src/HOL/Auth/Event.thy	Tue Aug 20 12:40:17 1996 +0200
     2.2 +++ b/src/HOL/Auth/Event.thy	Tue Aug 20 17:46:24 1996 +0200
     2.3 @@ -82,10 +82,8 @@
     2.4    isSym_newK "isSymKey (newK evs)"
     2.5  
     2.6  
     2.7 -(*NS1 AND NS2 DON'T ALLOW INTERLEAVING -- that is, they only respond to the
     2.8 -  MOST RECENT message.  Does this mean we can't model middleperson attacks?
     2.9 -  We don't need the most recent restriction in order to handle interception
    2.10 -  by the Enemy, as agents are not forced to respond anyway.*)
    2.11 +(*NS3 DOESN'T ALLOW INTERLEAVING -- that is, it only responds to the
    2.12 +  MOST RECENT message.*)
    2.13  
    2.14  consts  traces   :: "event list set"
    2.15  inductive traces
    2.16 @@ -102,9 +100,11 @@
    2.17            |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN evs)|}) 
    2.18                   # evs : traces"
    2.19  
    2.20 -          (*We can't trust the sender field, hence the A' in it  *)
    2.21 +          (*We can't trust the sender field, hence the A' in it.
    2.22 +            This allows the Server to respond more than once to A's
    2.23 +            request...*)
    2.24      NS2  "[| evs: traces;  A ~= B;  A ~= Server;
    2.25 -             evs = (Says A' Server {|Agent A, Agent B, Nonce NA|}) # evs'
    2.26 +             (Says A' Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs
    2.27            |] ==> (Says Server A 
    2.28                    (Crypt {|Nonce NA, Agent B, Key (newK evs),   
    2.29                             (Crypt {|Key (newK evs), Agent A|} (serverKey B))|}
    2.30 @@ -114,11 +114,10 @@
    2.31               May assume WLOG that she is NOT the Enemy: the Fake rule
    2.32               covers this case.  Can inductively show A ~= Server*)
    2.33      NS3  "[| evs: traces;  A ~= B;
    2.34 -             evs = (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|}
    2.35 -                              (serverKey A))) 
    2.36 -                   # evs';
    2.37 +             (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A))) 
    2.38 +               : set_of_list evs;
    2.39               A = Friend i;
    2.40 -             (Says A Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs'
    2.41 +             (Says A Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs
    2.42            |] ==> (Says A B X) # evs : traces"
    2.43  
    2.44  (*Initial version of NS2 had 
     3.1 --- a/src/HOL/Auth/Message.ML	Tue Aug 20 12:40:17 1996 +0200
     3.2 +++ b/src/HOL/Auth/Message.ML	Tue Aug 20 17:46:24 1996 +0200
     3.3 @@ -81,8 +81,13 @@
     3.4  qed "MPair_parts";
     3.5  
     3.6  AddIs  [parts.Inj];
     3.7 -AddSEs [MPair_parts];
     3.8 -AddDs  [parts.Body];
     3.9 +
    3.10 +val partsEs = [MPair_parts, make_elim parts.Body];
    3.11 +
    3.12 +AddSEs partsEs;
    3.13 +(*NB These two rules are UNSAFE in the formal sense, as they discard the
    3.14 +     compound message.  They work well on THIS FILE, perhaps because its
    3.15 +     proofs concern only atomic messages.*)
    3.16  
    3.17  goal thy "H <= parts(H)";
    3.18  by (Fast_tac 1);
    3.19 @@ -161,12 +166,6 @@
    3.20  by (fast_tac (!claset addEs [impOfSubs parts_mono]) 1);
    3.21  qed "parts_insert_subset";
    3.22  
    3.23 -(*Especially for reasoning about the Fake rule in traces*)
    3.24 -goal thy "!!Y. X: G ==> parts(insert X H) <= parts G Un parts H";
    3.25 -br ([parts_mono, parts_Un_subset2] MRS subset_trans) 1;
    3.26 -by (Fast_tac 1);
    3.27 -qed "parts_insert_subset_Un";
    3.28 -
    3.29  (** Idempotence and transitivity **)
    3.30  
    3.31  goal thy "!!H. X: parts (parts H) ==> X: parts H";
    3.32 @@ -191,6 +190,11 @@
    3.33  by (Fast_tac 1);
    3.34  qed "parts_cut";
    3.35  
    3.36 +goal thy "!!H. X: parts H ==> parts (insert X H) = parts H";
    3.37 +by (fast_tac (!claset addSEs [parts_cut]
    3.38 +                      addIs [impOfSubs (subset_insertI RS parts_mono)]) 1);
    3.39 +qed "parts_cut_eq";
    3.40 +
    3.41  
    3.42  (** Rewrite rules for pulling out atomic messages **)
    3.43  
    3.44 @@ -598,3 +602,23 @@
    3.45  			addIs  [analz.Decrypt]) 0 1);
    3.46  qed "analz_UN1_synth";
    3.47  Addsimps [analz_UN1_synth];
    3.48 +
    3.49 +(*Especially for reasoning about the Fake rule in traces*)
    3.50 +goal thy "!!Y. X: G ==> parts(insert X H) <= parts G Un parts H";
    3.51 +br ([parts_mono, parts_Un_subset2] MRS subset_trans) 1;
    3.52 +by (Fast_tac 1);
    3.53 +qed "parts_insert_subset_Un";
    3.54 +
    3.55 +(*Also for the Fake rule, but more specific*)
    3.56 +goal thy "!!H. X: synth (analz H) ==> \
    3.57 +\              parts (insert X H) <= synth (analz H) Un parts H";
    3.58 +bd parts_insert_subset_Un 1;
    3.59 +by (Full_simp_tac 1);
    3.60 +by (Fast_tac 1);
    3.61 +qed "synth_analz_parts_insert_subset_Un";
    3.62 +
    3.63 +
    3.64 +
    3.65 +(*We do NOT want Crypt... messages broken up in protocols!!*)
    3.66 +Delrules partsEs;
    3.67 +