Auth proofs work up to the XXX...
authorpaulson
Fri Jul 26 12:19:46 1996 +0200 (1996-07-26)
changeset 1885a18a6dc14f76
parent 1884 5a1f81da3e12
child 1886 0922b597b53d
Auth proofs work up to the XXX...
src/HOL/Auth/Event.ML
src/HOL/Auth/Event.thy
src/HOL/Auth/Message.ML
     1.1 --- a/src/HOL/Auth/Event.ML	Fri Jul 26 12:18:50 1996 +0200
     1.2 +++ b/src/HOL/Auth/Event.ML	Fri Jul 26 12:19:46 1996 +0200
     1.3 @@ -10,11 +10,53 @@
     1.4  *)
     1.5  
     1.6  
     1.7 +proof_timing:=true;
     1.8 +
     1.9 +Delrules [less_SucE];	(*Perhaps avoid inserting this in Arith.ML????*)
    1.10 +
    1.11 +(*FOR LIST.ML??*)
    1.12 +goal List.thy "x : setOfList (x#xs)";
    1.13 +by (Simp_tac 1);
    1.14 +qed "setOfList_I1";
    1.15 +
    1.16 +goal List.thy "!!x. xs = x#xs' ==> x : setOfList xs";
    1.17 +by (Asm_simp_tac 1);
    1.18 +qed "setOfList_eqI1";
    1.19 +
    1.20 +(*Not for Addsimps -- it can cause goals to blow up!*)
    1.21 +goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
    1.22 +by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
    1.23 +qed "mem_if";
    1.24 +
    1.25 +(*DELETE, AS ALREADY IN SET.ML*)
    1.26 +goalw Set.thy [Bex_def] "(? x:A. False) = False";
    1.27 +by (Simp_tac 1);
    1.28 +qed "bex_False";
    1.29 +Addsimps [bex_False];
    1.30 +goal Set.thy "!!x. x:A ==> insert (f x) (f``A) = f``A";
    1.31 +by (Fast_tac 1);
    1.32 +qed "insert_image";
    1.33 +Addsimps [insert_image];
    1.34 +
    1.35 +
    1.36 +(*FUN.ML??  WE NEED A NOTION OF INVERSE IMAGE!!*)
    1.37 +goal Set.thy "!!f. B <= range f = (B = f`` {x. f x: B})";
    1.38 +by (fast_tac (!claset addEs [equalityE]) 1);
    1.39 +val subset_range_iff = result();
    1.40 +
    1.41 +
    1.42  open Event;
    1.43  
    1.44 -(*Rewrite using   {a} Un A = insert a A *)
    1.45 -Addsimps [insert_is_Un RS sym];
    1.46 +goal Set.thy "A Un (insert a B) = insert a (A Un B)";
    1.47 +by (Fast_tac 1);
    1.48 +qed "Un_insert_right";
    1.49  
    1.50 +Addsimps [Un_insert_left, Un_insert_right];
    1.51 +
    1.52 +(*By default only o_apply is built-in.  But in the presence of eta-expansion
    1.53 +  this means that some terms displayed as (f o g) will be rewritten, and others
    1.54 +  will not!*)
    1.55 +Addsimps [o_def];
    1.56  
    1.57  (*** Basic properties of serverKey and newK ***)
    1.58  
    1.59 @@ -46,19 +88,23 @@
    1.60  Addsimps [newK_neq_serverKey, newK_neq_serverKey RS not_sym];
    1.61  
    1.62  (*Good for talking about Server's initial state*)
    1.63 -goal thy "parts (range (Key o f)) = range (Key o f)";
    1.64 -by (auto_tac (!claset addIs [range_eqI], !simpset));
    1.65 +goal thy "!!H. H <= Key``E ==> parts H = H";
    1.66 +by (Auto_tac ());
    1.67  be parts.induct 1;
    1.68  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    1.69 -qed "parts_range_Key";
    1.70 +qed "parts_image_subset";
    1.71  
    1.72 -goal thy "analyze (range (Key o f)) = range (Key o f)";
    1.73 -by (auto_tac (!claset addIs [range_eqI], !simpset));
    1.74 +bind_thm ("parts_image_Key", subset_refl RS parts_image_subset);
    1.75 +
    1.76 +goal thy "!!H. H <= Key``E ==> analyze H = H";
    1.77 +by (Auto_tac ());
    1.78  be analyze.induct 1;
    1.79  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    1.80 -qed "analyze_range_Key";
    1.81 +qed "analyze_image_subset";
    1.82  
    1.83 -Addsimps [parts_range_Key, analyze_range_Key];
    1.84 +bind_thm ("analyze_image_Key", subset_refl RS analyze_image_subset);
    1.85 +
    1.86 +Addsimps [parts_image_Key, analyze_image_Key];
    1.87  
    1.88  goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
    1.89  by (agent.induct_tac "C" 1);
    1.90 @@ -66,6 +112,32 @@
    1.91  qed "keysFor_parts_initState";
    1.92  Addsimps [keysFor_parts_initState];
    1.93  
    1.94 +goalw thy [keysFor_def] "keysFor (Key``E) = {}";
    1.95 +by (Auto_tac ());
    1.96 +qed "keysFor_image_Key";
    1.97 +Addsimps [keysFor_image_Key];
    1.98 +
    1.99 +goal thy "serverKey A ~: newK``E";
   1.100 +by (agent.induct_tac "A" 1);
   1.101 +by (Auto_tac ());
   1.102 +qed "serverKey_notin_image_newK";
   1.103 +Addsimps [serverKey_notin_image_newK];
   1.104 +
   1.105 +
   1.106 +(*Agents see their own serverKeys!*)
   1.107 +goal thy "Key (serverKey A) : analyze (sees A evs)";
   1.108 +by (list.induct_tac "evs" 1);
   1.109 +by (asm_simp_tac (!simpset addsimps [impOfSubs(Un_upper2 RS analyze_mono)]) 2);
   1.110 +by (agent.induct_tac "A" 1);
   1.111 +by (auto_tac (!claset addIs [range_eqI], !simpset));
   1.112 +qed "analyze_own_serverKey";
   1.113 +
   1.114 +bind_thm ("parts_own_serverKey",
   1.115 +	  [analyze_subset_parts, analyze_own_serverKey] MRS subsetD);
   1.116 +
   1.117 +Addsimps [analyze_own_serverKey, parts_own_serverKey];
   1.118 +
   1.119 +
   1.120  
   1.121  (**** Inductive relation "traces" -- basic properties ****)
   1.122  
   1.123 @@ -83,6 +155,11 @@
   1.124  by (fast_tac (!claset addEs [mk_cases "ev#evs:traces"]) 1);
   1.125  qed "traces_ConsE";
   1.126  
   1.127 +goal thy "!!ev evs. [| evs = ev#evs'; evs : traces |] ==> evs' : traces";
   1.128 +by (fast_tac (!claset addEs [mk_cases "ev#evs:traces"]) 1);
   1.129 +qed "traces_eq_ConsE";
   1.130 +
   1.131 +
   1.132  (** Specialized rewrite rules for (sees A (Says...#evs)) **)
   1.133  
   1.134  goal thy "sees A (Says A B X # evs) = insert X (sees A evs)";
   1.135 @@ -123,6 +200,13 @@
   1.136  by (ALLGOALS (fast_tac (!claset addss ss)));
   1.137  qed "UN_parts_sees_Says";
   1.138  
   1.139 +goal thy "Says A B X : setOfList evs --> X : sees Enemy evs";
   1.140 +by (list.induct_tac "evs" 1);
   1.141 +by (Auto_tac ());
   1.142 +qed_spec_mp "Says_imp_sees_Enemy";
   1.143 +
   1.144 +Addsimps [Says_imp_sees_Enemy];
   1.145 +AddIs    [Says_imp_sees_Enemy];
   1.146  
   1.147  Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Enemy];
   1.148  Delsimps [sees_Cons];	(**** NOTE REMOVAL -- laws above are cleaner ****)
   1.149 @@ -142,6 +226,7 @@
   1.150  qed "sees_agent_subset_sees_Enemy";
   1.151  
   1.152  
   1.153 +(*Nobody sends themselves messages*)
   1.154  goal thy "!!evs. evs : traces ==> ALL A X. Says A A X ~: setOfList evs";
   1.155  be traces.induct 1;
   1.156  by (Auto_tac());
   1.157 @@ -168,11 +253,15 @@
   1.158  bind_thm ("Enemy_not_analyze_serverKey",
   1.159  	  [analyze_subset_parts, Enemy_not_see_serverKey] MRS contra_subsetD);
   1.160  
   1.161 -Addsimps [Enemy_not_see_serverKey, Enemy_not_analyze_serverKey];
   1.162 +Addsimps [Enemy_not_see_serverKey, 
   1.163 +	  not_sym RSN (2, Enemy_not_see_serverKey), 
   1.164 +	  Enemy_not_analyze_serverKey, 
   1.165 +	  not_sym RSN (2, Enemy_not_analyze_serverKey)];
   1.166  
   1.167  
   1.168  (*No Friend will ever see another agent's server key 
   1.169 -  (excluding the Enemy, who might transmit his).*)
   1.170 +  (excluding the Enemy, who might transmit his).
   1.171 +  The Server, of course, knows all server keys.*)
   1.172  goal thy 
   1.173   "!!evs. [| evs : traces; A ~= Enemy;  A ~= Friend j |] ==> \
   1.174  \        Key (serverKey A) ~: parts (sees (Friend j) evs)";
   1.175 @@ -181,6 +270,20 @@
   1.176  qed "Friend_not_see_serverKey";
   1.177  
   1.178  
   1.179 +(*Not for Addsimps -- it can cause goals to blow up!*)
   1.180 +goal thy  
   1.181 + "!!evs. evs : traces ==>                                  \
   1.182 +\        (Key (serverKey A) \
   1.183 +\           : analyze (insert (Key (serverKey B)) (sees Enemy evs))) =  \
   1.184 +\        (A=B | A=Enemy)";
   1.185 +by (best_tac (!claset addDs [impOfSubs analyze_subset_parts]
   1.186 +		      addIs [impOfSubs (subset_insertI RS analyze_mono)]
   1.187 +	              addss (!simpset)) 1);
   1.188 +qed "serverKey_mem_analyze";
   1.189 +
   1.190 +
   1.191 +
   1.192 +
   1.193  (*** Future keys can't be seen or used! ***)
   1.194  
   1.195  (*Nobody can have SEEN keys that will be generated in the future.
   1.196 @@ -218,6 +321,8 @@
   1.197  by (fast_tac (!claset addDs [lemma]) 1);
   1.198  qed "new_keys_not_seen";
   1.199  
   1.200 +Addsimps [new_keys_not_seen];
   1.201 +
   1.202  goal thy "!!K. newK evs = invKey K ==> newK evs = K";
   1.203  br (invKey_eq RS iffD1) 1;
   1.204  by (Simp_tac 1);
   1.205 @@ -265,60 +370,897 @@
   1.206  \        newK evs' ~: keysFor (parts (sees C evs))";
   1.207  by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
   1.208  qed "new_keys_not_used";
   1.209 -Addsimps [new_keys_not_used];
   1.210  
   1.211  bind_thm ("new_keys_not_analyzed",
   1.212  	  [analyze_subset_parts RS keysFor_mono,
   1.213  	   new_keys_not_used] MRS contra_subsetD);
   1.214  
   1.215 -
   1.216 -(*Maybe too specific to be of much use...*)
   1.217 -goal thy 
   1.218 - "!!evs. [| Says Server A (Crypt {|Nonce NA, Agent B, Key K, X|} \
   1.219 -\                                (serverKey A))                  \
   1.220 -\               : setOfList evs;                                 \
   1.221 -\           evs : traces    \
   1.222 -\        |] ==> (EX evs'. X = (Crypt {|Key(newK evs'), Agent A|} (serverKey B)))";
   1.223 -be rev_mp 1;
   1.224 -be traces.induct 1;
   1.225 -be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
   1.226 -be subst 5;	(*NS3: discard evsa = Says S Aa... as irrelevant!*)
   1.227 -by (ALLGOALS Asm_full_simp_tac);
   1.228 -by (Fast_tac 1);	(*Proves the NS2 case*)
   1.229 -qed "Says_Server_imp_X_eq_Crypt";
   1.230 +Addsimps [new_keys_not_used, new_keys_not_analyzed];
   1.231  
   1.232  
   1.233 -(*Pushes Crypt events in so that others might be pulled out*)
   1.234 -goal thy "insert (Crypt X K) (insert y evs) = \
   1.235 -\         insert y (insert (Crypt X K) evs)";
   1.236 -by (Fast_tac 1);
   1.237 -qed "insert_Crypt_delay";
   1.238 +(** Rewrites to push in Key and Crypt messages, so that other messages can
   1.239 +    be pulled out using the analyze_insert rules **)
   1.240 +
   1.241 +fun insComm x y = read_instantiate_sg (sign_of thy) [("x",x), ("y",y)] 
   1.242 +                      insert_commute;
   1.243  
   1.244 -goal thy "insert (Key K) (insert y evs) = \
   1.245 -\         insert y (insert (Key K) evs)";
   1.246 -by (Fast_tac 1);
   1.247 -qed "insert_Key_delay";
   1.248 +val pushKeys = map (insComm "Key ?K") 
   1.249 +                  ["Agent ?C", "Nonce ?N", "MPair ?X ?Y", "Crypt ?X ?K'"];
   1.250 +
   1.251 +val pushCrypts = map (insComm "Crypt ?X ?K") 
   1.252 +                    ["Agent ?C", "Nonce ?N", "MPair ?X' ?Y"];
   1.253 +
   1.254 +(*Cannot be added with Addsimps -- we don't always want to re-order messages*)
   1.255 +val pushes = pushKeys@pushCrypts;
   1.256 +
   1.257 +val pushKey_newK = insComm "Key (newK ?evs)"  "Key (serverKey ?C)";
   1.258  
   1.259  
   1.260  (** Lemmas concerning the form of items passed in messages **)
   1.261  
   1.262 -(*Describes the form *and age* of K when the following message is sent*)
   1.263 +(*Describes the form *and age* of K, and the form of X,
   1.264 +  when the following message is sent*)
   1.265  goal thy 
   1.266 - "!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') \
   1.267 -\               : setOfList evs;  \
   1.268 -\           evs : traces          \
   1.269 -\        |] ==> (EX evs'. K = Key (newK evs') & length evs' < length evs)";
   1.270 + "!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') : setOfList evs; \
   1.271 +\           evs : traces    \
   1.272 +\        |] ==> (EX evs':traces. K = Key(newK evs') & length evs' < length evs & \
   1.273 +\                         X = (Crypt {|K, Agent A|} (serverKey B)))";
   1.274  be rev_mp 1;
   1.275  be traces.induct 1;
   1.276  be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
   1.277  by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
   1.278 -qed "Says_Server_imp_Key_newK";
   1.279 +qed "Says_Server_message_form";
   1.280  
   1.281  (* c ~: keysFor (parts H) ==> c ~: keysFor (analyze H) *)
   1.282  bind_thm ("not_parts_not_keysFor_analyze", 
   1.283  	  analyze_subset_parts RS keysFor_mono RS contra_subsetD);
   1.284  
   1.285  
   1.286 +
   1.287 +(*USELESS for NS3, case 1, as the ind hyp says the same thing!
   1.288 +goal thy 
   1.289 + "!!evs. [| evs = Says Server (Friend i) \
   1.290 +\                 (Crypt {|N, Agent(Friend j), K, X|} K') # evs';  \
   1.291 +\           evs : traces;  i~=k                                    \
   1.292 +\        |] ==>                                                    \
   1.293 +\     K ~: analyze (insert (Key (serverKey (Friend k))) (sees Enemy evs))";
   1.294 +be rev_mp 1;
   1.295 +be traces.induct 1;
   1.296 +be subst 4;	(*NS2: discard evsa = Says A Server... as irrelevant!*)
   1.297 +by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes)));
   1.298 +by (Step_tac 1);
   1.299 +by (asm_full_simp_tac (!simpset addsimps[analyze_subset_parts RS contra_subsetD]) 1);
   1.300 +val Enemy_not_see_encrypted_key_lemma = result();
   1.301 +*)
   1.302 +
   1.303 +
   1.304 +(*Describes the form of X when the following message is sent*)
   1.305 +goal thy
   1.306 + "!!evs. evs : traces ==>                             \
   1.307 +\        ALL A NA B K X.                            \
   1.308 +\            (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
   1.309 +\            : parts (sees Enemy evs) & A ~= Enemy  -->   \
   1.310 +\          (EX evt:traces. K = newK evt & \
   1.311 +\                          X = (Crypt {|Key K, Agent A|} (serverKey B)))";
   1.312 +be traces.induct 1;
   1.313 +be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
   1.314 +by (Step_tac 1);
   1.315 +by (ALLGOALS Asm_full_simp_tac);
   1.316 +(*Remaining cases are Fake, NS2 and NS3*)
   1.317 +by (fast_tac (!claset addSDs [spec]) 2);
   1.318 +(*The NS3 case needs the induction hypothesis twice!
   1.319 +    One application is to the X component of the most recent message.*)
   1.320 +by (full_simp_tac (!simpset addsimps [conj_disj_distribR, all_conj_distrib]) 2);
   1.321 +be conjE 2;
   1.322 +by (subgoal_tac "? evs':traces. K = newK evs' & \
   1.323 +\                     X = Crypt {|Key K, Agent (Friend i)|} (serverKey B)" 2);
   1.324 +(*DELETE the second quantified formula for speed*)
   1.325 +by (eres_inst_tac [("V","ALL A NA B K Xa. ?f A NA B K Xa : ?H X & ?P(A) --> \
   1.326 +\                                         ?Q K Xa A B")] thin_rl 3);
   1.327 +by (fast_tac (!claset addSEs [allE, mp] addss (!simpset)) 3);
   1.328 +(*DELETE the first quantified formula: it's now useless*)
   1.329 +by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
   1.330 +by (fast_tac (!claset addss (!simpset)) 2);
   1.331 +(*Now for the Fake case*)
   1.332 +by (subgoal_tac 
   1.333 +    "Crypt {|Nonce NA, Agent Ba, Key K, Xa|} (serverKey A) : \
   1.334 +\    parts (synthesize (analyze (sees Enemy evsa)) Un (sees Enemy evsa))" 1);
   1.335 +by (fast_tac (!claset addSEs [impOfSubs parts_mono]) 2);
   1.336 +by (best_tac (!claset addDs [impOfSubs analyze_subset_parts]
   1.337 +	              addss (!simpset)) 1);
   1.338 +val encrypted_form = result();
   1.339 +
   1.340 +
   1.341 +(*For eliminating the A ~= Enemy condition from the previous result*)
   1.342 +goal thy 
   1.343 + "!!evs. evs : traces ==>                             \
   1.344 +\        ALL S A NA B K X.                            \
   1.345 +\            Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
   1.346 +\            : setOfList evs  -->   \
   1.347 +\        S = Server | S = Enemy";
   1.348 +be traces.induct 1;
   1.349 +be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
   1.350 +by (ALLGOALS Asm_full_simp_tac);
   1.351 +(*We are left with NS3*)
   1.352 +by (subgoal_tac "S = Server | S = Enemy" 1);
   1.353 +(*First justify this assumption!*)
   1.354 +by (fast_tac (!claset addSEs [allE, mp] addss (!simpset)) 2);
   1.355 +by (Step_tac 1);
   1.356 +bd (setOfList_I1 RS Says_Server_message_form) 1;
   1.357 +by (ALLGOALS Full_simp_tac);
   1.358 +(*Final case.  Clear out needless quantifiers to speed the following step*)
   1.359 +by (eres_inst_tac [("V","ALL x. ?P(x)")] thin_rl 1);
   1.360 +bd (normalize_thm [RSspec,RSmp] encrypted_form) 1;
   1.361 +br (parts.Inj RS conjI) 1;
   1.362 +auto();
   1.363 +qed_spec_mp "Server_or_Enemy";
   1.364 +
   1.365 +
   1.366 +
   1.367 +(*Describes the form of X when the following message is sent;
   1.368 +  use Says_Server_message_form if applicable*)
   1.369 +goal thy 
   1.370 + "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
   1.371 +\            : setOfList evs;                              \
   1.372 +\           evs : traces               \
   1.373 +\        |] ==> (EX evt:traces. K = newK evt & \
   1.374 +\                               X = (Crypt {|Key K, Agent A|} (serverKey B)))";
   1.375 +by (forward_tac [Server_or_Enemy] 1);
   1.376 +ba 1;
   1.377 +by (Step_tac 1);
   1.378 +by (fast_tac (!claset addSDs [Says_Server_message_form] addss (!simpset)) 1);
   1.379 +by (forward_tac [normalize_thm [RSspec,RSmp] encrypted_form] 1);
   1.380 +br (parts.Inj RS conjI) 1;
   1.381 +by (Auto_tac());
   1.382 +qed "Says_S_message_form";
   1.383 +
   1.384 +goal thy 
   1.385 + "!!evs. [| evs = Says S A (Crypt {|Nonce NA, Agent B, Key K, X|}   \
   1.386 +\                           (serverKey A)) # evs';                  \
   1.387 +\           evs : traces                                           \
   1.388 +\        |] ==> (EX evt:traces. evs' : traces &                    \
   1.389 +\                               K = newK evt & \
   1.390 +\                               X = (Crypt {|Key K, Agent A|} (serverKey B)))";
   1.391 +by (forward_tac [traces_eq_ConsE] 1);
   1.392 +by (dtac (setOfList_eqI1 RS Says_S_message_form) 2);
   1.393 +by (Auto_tac());	
   1.394 +qed "Says_S_message_form_eq";
   1.395 +
   1.396 +
   1.397 +
   1.398 +
   1.399 +(****
   1.400 + The following is to prove theorems of the form
   1.401 +
   1.402 +          Key K : analyze (insert (Key (newK evt)) 
   1.403 +	                   (insert (Key (serverKey C)) (sees Enemy evs))) ==>
   1.404 +          Key K : analyze (insert (Key (serverKey C)) (sees Enemy evs))
   1.405 +
   1.406 + A more general formula must be proved inductively.
   1.407 +
   1.408 +****)
   1.409 +
   1.410 +
   1.411 +(*Not useful in this form, but it says that session keys are not used
   1.412 +  to encrypt messages containing other keys, in the actual protocol.
   1.413 +  We require that agents should behave like this subsequently also.*)
   1.414 +goal thy 
   1.415 + "!!evs. evs : traces ==> \
   1.416 +\        (Crypt X (newK evt)) : parts (sees Enemy evs) & \
   1.417 +\        Key K : parts {X} --> Key K : parts (sees Enemy evs)";
   1.418 +be traces.induct 1;
   1.419 +be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
   1.420 +by (hyp_subst_tac 5);	(*NS3: apply evsa = Says S A (Crypt ...) # ... *)
   1.421 +by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes)));
   1.422 +(*Case NS3*)
   1.423 +by (res_inst_tac [("x1","Xa")] (insert_commute RS ssubst) 2);
   1.424 +by (Asm_full_simp_tac 2);
   1.425 +(*Deals with Faked messages*)
   1.426 +by (best_tac (!claset addDs [impOfSubs analyze_subset_parts,
   1.427 +			     impOfSubs parts_insert_subset_Un]
   1.428 +	              addss (!simpset)) 1);
   1.429 +result();
   1.430 +
   1.431 +
   1.432 +(** Specialized rewrites for this proof **)
   1.433 +
   1.434 +Delsimps [image_insert];
   1.435 +Addsimps [image_insert RS sym];
   1.436 +
   1.437 +goal thy "insert (Key (newK x)) (sees A evs) = \
   1.438 +\         Key `` (newK``{x}) Un (sees A evs)";
   1.439 +by (Fast_tac 1);
   1.440 +val insert_Key_singleton = result();
   1.441 +
   1.442 +goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
   1.443 +\         Key `` (f `` (insert x E)) Un C";
   1.444 +by (Fast_tac 1);
   1.445 +val insert_Key_image = result();
   1.446 +
   1.447 +
   1.448 +goal thy  
   1.449 + "!!evs. evs : traces ==> \
   1.450 +\  ALL K E. (Key K : analyze (insert (Key (serverKey C)) \
   1.451 +\                             (Key``(newK``E) Un (sees Enemy evs)))) = \
   1.452 +\           (K : newK``E |  \
   1.453 +\            Key K : analyze (insert (Key (serverKey C)) \
   1.454 +\                             (sees Enemy evs)))";
   1.455 +be traces.induct 1;
   1.456 +be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
   1.457 +by (dtac Says_S_message_form_eq 5 THEN assume_tac 5);	
   1.458 +by (REPEAT ((eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac) 5));
   1.459 +by (ALLGOALS 
   1.460 +    (asm_full_simp_tac 
   1.461 +     (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   1.462 +			 @ pushes)
   1.463 +               setloop split_tac [expand_if])));
   1.464 +(*Cases NS2 and NS3!!  Simple, thanks to auto case splits*)
   1.465 +by (REPEAT (Fast_tac 3));
   1.466 +(*Base case*)
   1.467 +by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   1.468 +(** LEVEL 7 **)
   1.469 +(*Fake case*)
   1.470 +by (REPEAT (Safe_step_tac 1));
   1.471 +by (fast_tac (!claset addSEs [impOfSubs (analyze_mono)]) 2);
   1.472 +by (subgoal_tac 
   1.473 +    "Key K : analyze \
   1.474 +\             (synthesize \
   1.475 +\              (analyze (insert (Key (serverKey C)) \
   1.476 +\                        (Key``(newK``E) Un (sees Enemy evsa)))))" 1);
   1.477 +(*First, justify this subgoal*)
   1.478 +(*Discard the quantified formula for better speed*)
   1.479 +by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
   1.480 +by (eres_inst_tac [("V","?Q ~: ?QQ")] thin_rl 2);
   1.481 +by (best_tac (!claset addIs [impOfSubs (analyze_mono RS synthesize_mono)]
   1.482 +                      addSEs [impOfSubs analyze_mono]) 2);
   1.483 +by (Asm_full_simp_tac 1);
   1.484 +by (deepen_tac (!claset addIs [impOfSubs analyze_mono]) 0 1);
   1.485 +qed_spec_mp "analyze_image_newK";
   1.486 +
   1.487 +
   1.488 +goal thy  
   1.489 + "!!evs. evs : traces ==>                                  \
   1.490 +\        Key K : analyze (insert (Key (newK evt))          \
   1.491 +\                         (insert (Key (serverKey C))      \
   1.492 +\                          (sees Enemy evs))) =            \
   1.493 +\             (K = newK evt |                              \
   1.494 +\              Key K : analyze (insert (Key (serverKey C)) \
   1.495 +\                               (sees Enemy evs)))";
   1.496 +by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analyze_image_newK, 
   1.497 +				   insert_Key_singleton]) 1);
   1.498 +by (Fast_tac 1);
   1.499 +qed "analyze_insert_Key_newK";
   1.500 +
   1.501 +
   1.502 +
   1.503 +
   1.504 +XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX;
   1.505 +
   1.506 +
   1.507 +goal thy 
   1.508 + "!!evs. [| evs = Says Server (Friend i) \
   1.509 +\                 (Crypt {|N, Agent(Friend j), K, X|} K') # evs';  \
   1.510 +\           evs : traces;  i~=k                                    \
   1.511 +\        |] ==>                                                    \
   1.512 +\     K = newK evs'";  ????????????????
   1.513 +
   1.514 +
   1.515 +goals_limit:=2;
   1.516 +goal thy 
   1.517 + "!!evs. [| Says S A          \
   1.518 +\            (Crypt {|N, Agent B, Key K, X|} (serverKey A)) : setOfList evs; \
   1.519 +\           evs : traces                                                 \
   1.520 +\        |] ==>                                                          \
   1.521 +\               ALL A' N' B' X'.                                       \
   1.522 +\                 Says Server A'                                         \
   1.523 +\                  (Crypt {|N', Agent B', Key K, X'|} (serverKey A')) :  \
   1.524 +\                 setOfList evs --> X = X'";
   1.525 +be rev_mp 1;
   1.526 +be traces.induct 1;
   1.527 +be subst 4;	(*NS2: discard evsa = Says A Server... as irrelevant!*)
   1.528 +by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes)));
   1.529 +by (REPEAT_FIRST (resolve_tac [conjI, impI, allI] ORELSE' etac conjE
   1.530 +		  ORELSE' hyp_subst_tac));
   1.531 +
   1.532 +by (ALLGOALS (full_simp_tac (!simpset addsimps [not_Cons_self])));
   1.533 +by (Step_tac 1);
   1.534 +fe Crypt_synthesize;
   1.535 +by (fast_tac (!claset addss (!simpset)) 2);
   1.536 +
   1.537 +
   1.538 +
   1.539 +by (Step_tac 1);
   1.540 +by (asm_full_simp_tac (!simpset addsimps[analyze_subset_parts RS contra_subsetD]) 1);
   1.541 +val Enemy_not_see_encrypted_key_lemma = result();
   1.542 +
   1.543 +
   1.544 +
   1.545 +
   1.546 +AddSEs [less_irrefl];
   1.547 +
   1.548 +(*Crucial security property: Enemy does not see the keys sent in msg NS2
   1.549 +   -- even if another key is compromised*)
   1.550 +goal thy 
   1.551 + "!!evs. [| Says Server (Friend i) \
   1.552 +\            (Crypt {|N, Agent(Friend j), K, X|} K') : setOfList evs;  \
   1.553 +\           evs : traces;  Friend i ~= C;  Friend j ~= C              \
   1.554 +\        |] ==>                                                       \
   1.555 +\     K ~: analyze (insert (Key (serverKey C)) (sees Enemy evs))";
   1.556 +be rev_mp 1;
   1.557 +be traces.induct 1;
   1.558 +be subst 4;	(*NS2: discard evsa = Says A Server... as irrelevant!*)
   1.559 +by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes)));
   1.560 +(*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
   1.561 +by (REPEAT_FIRST (resolve_tac [conjI, impI]));
   1.562 +by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac));
   1.563 +by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac));
   1.564 +by (ALLGOALS 
   1.565 +    (asm_full_simp_tac 
   1.566 +     (!simpset addsimps ([analyze_subset_parts RS contra_subsetD,
   1.567 +			  analyze_insert_Key_newK] @ pushes)
   1.568 +               setloop split_tac [expand_if])));
   1.569 +
   1.570 +(*NS2*)
   1.571 +by (Fast_tac 2);
   1.572 +(** LEVEL 9 **)
   1.573 +(*Now for the Fake case*)
   1.574 +br notI 1;
   1.575 +by (subgoal_tac 
   1.576 +    "Key (newK evs') : \
   1.577 +\    analyze (synthesize (analyze (insert (Key (serverKey C)) \
   1.578 +\                                  (sees Enemy evsa))))" 1);
   1.579 +be (impOfSubs analyze_mono) 2;
   1.580 +by (deepen_tac (!claset addIs [analyze_mono RS synthesize_mono RSN 
   1.581 +			     (2,rev_subsetD),
   1.582 +			     impOfSubs synthesize_increasing,
   1.583 +			     impOfSubs analyze_increasing]) 0 2);
   1.584 +(*Proves the Fake goal*)
   1.585 +by (fast_tac (!claset addss (!simpset)) 1);
   1.586 +
   1.587 +(**LEVEL 16**)
   1.588 +(*Now for NS3*)
   1.589 +(*NS3, case 1: that message from the Server was just sent*)
   1.590 +by (ALLGOALS (forward_tac [traces_ConsE]));
   1.591 +by (forward_tac [setOfList_I1 RS Says_Server_message_form] 1);
   1.592 +by (Full_simp_tac 1);
   1.593 +by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac));
   1.594 +(*Can simplify the Crypt messages: their key is secure*)
   1.595 +by (dres_inst_tac [("psi", "?X ~: ?H")] asm_rl 1);
   1.596 +by (asm_full_simp_tac
   1.597 +    (!simpset addsimps (pushes @ [analyze_insert_Crypt,
   1.598 +				  analyze_subset_parts RS contra_subsetD])) 1);
   1.599 +
   1.600 +(**LEVEL 20, one subgoal left! **)
   1.601 +(*NS3, case 2: that message from the Server was sent earlier*)
   1.602 +
   1.603 +(*simplify the good implication*)
   1.604 +by (Asm_full_simp_tac 1);       
   1.605 +by (eres_inst_tac [("V","?P-->?Q")] thin_rl 1); (*delete the bad implication*)
   1.606 +by ((forward_tac [Says_Server_message_form] THEN' assume_tac) 1);
   1.607 +by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac));
   1.608 +by (Full_simp_tac 1);
   1.609 +
   1.610 +(**LEVEL 25 **)
   1.611 +
   1.612 +by ((forward_tac [setOfList_I1 RS Says_S_message_form]) 1);
   1.613 +by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac));
   1.614 +by (asm_full_simp_tac (!simpset addsimps (analyze_insert_Key_newK::pushes)) 1);
   1.615 +by (step_tac (!claset delrules [impCE]) 1);
   1.616 +by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes)));
   1.617 +
   1.618 +
   1.619 +by (Step_tac 1);
   1.620 +by (Fast_tac 1); 
   1.621 +
   1.622 +(*May do this once we have proved that the keys coincide*)
   1.623 +by (subgoal_tac "i = ia & N = Nonce NA & Friend j = C & K' = serverKey (Friend ia)" 1);
   1.624 +by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac));
   1.625 +
   1.626 +(**LEVEL 29 **)
   1.627 +
   1.628 +by (asm_full_simp_tac (!simpset addsimps (pushes)) 1);
   1.629 +
   1.630 +
   1.631 +(*ALL THAT REMAINS IS TO PROVE THE SUBGOAL!*)
   1.632 +
   1.633 +
   1.634 +
   1.635 +
   1.636 +
   1.637 +by (Step_tac 1);
   1.638 +by (Fast_tac 1); 
   1.639 +
   1.640 +
   1.641 +
   1.642 +
   1.643 +by (forward_tac [setOfList_I1 RSN (2, Server_or_Enemy)] 1);
   1.644 +
   1.645 +
   1.646 +    (!simpset addsimps ([analyze_subset_parts RS keysFor_mono RS contra_subsetD])) 1);
   1.647 +
   1.648 +
   1.649 +by (excluded_middle_tac "evs'a=evt" 1);
   1.650 +(*Keys agree?  Then should have B = Friend j, so encrypted msg is secure*)
   1.651 +by (subgoal_tac "B = Friend j" 2);
   1.652 +by (REPEAT_FIRST hyp_subst_tac);
   1.653 +by (asm_full_simp_tac
   1.654 +    (!simpset addsimps ([analyze_subset_parts RS contra_subsetD])) 2);
   1.655 +(*Keys differ?  Then they cannot clash*)
   1.656 +
   1.657 +br notI 1;
   1.658 +bd (impOfSubs analyze_insert_Crypt_subset) 1;
   1.659 +
   1.660 +
   1.661 +????????????????????????????????????????????????????????????????;
   1.662 +
   1.663 +(**LEVEL 35 **)
   1.664 +
   1.665 +(*In this case, the Key in X (newK evs') is younger than 
   1.666 +  the Key we are worried about (newK evs'a).  And nobody has used the
   1.667 +  new Key yet, so it can be pulled out of the "analyze".*)
   1.668 +by (asm_full_simp_tac
   1.669 +    (!simpset addsimps ([analyze_subset_parts RS keysFor_mono RS contra_subsetD])) 1);
   1.670 +by (Fast_tac 1); 
   1.671 +(*In this case, Enemy has seen the (encrypted!) message at hand...*)
   1.672 +by (dres_inst_tac [("psi", "?X ~: ?H")] asm_rl 1);
   1.673 +by (asm_full_simp_tac (!simpset addsimps ([insert_absorb]@pushes)) 1);
   1.674 +
   1.675 +(**LEVEL 39 **)
   1.676 +
   1.677 +br notI 1;
   1.678 +bd (impOfSubs analyze_insert_Crypt_subset) 1;
   1.679 +by (asm_full_simp_tac
   1.680 +    (!simpset addsimps ([analyze_subset_parts RS keysFor_mono RS contra_subsetD])) 1);
   1.681 +
   1.682 +
   1.683 +by (excluded_middle_tac "evs'a=evt" 1);
   1.684 +(*Keys agree?  Then should have B = Friend j, so encrypted msg is secure*)
   1.685 +by (subgoal_tac "B = Friend j" 2);
   1.686 +by (REPEAT_FIRST hyp_subst_tac);
   1.687 +by (asm_full_simp_tac
   1.688 +    (!simpset addsimps ([analyze_subset_parts RS contra_subsetD])) 2);
   1.689 +(*Keys differ?  Then they cannot clash*)
   1.690 +
   1.691 +br notI 1;
   1.692 +bd (impOfSubs analyze_insert_Crypt_subset) 1;
   1.693 +
   1.694 +
   1.695 +
   1.696 +
   1.697 +
   1.698 +
   1.699 +
   1.700 +(**LEVEL 28 OLD VERSION, with extra case split on ia=k **)
   1.701 +
   1.702 +by (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1);
   1.703 +by (excluded_middle_tac "ia=k" 1);
   1.704 +(*Case where the key is compromised*)
   1.705 +by (hyp_subst_tac 2);
   1.706 +by (asm_full_simp_tac (!simpset addsimps pushes) 2);
   1.707 +by (full_simp_tac (!simpset addsimps [insert_commute]) 2);
   1.708 +
   1.709 +(**LEVEL 33 **)
   1.710 +
   1.711 +XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX;
   1.712 +proof_timing:=true;
   1.713 +AddSEs [less_irrefl];
   1.714 +
   1.715 +
   1.716 +(*Case where the key is secure*)
   1.717 +by (dres_inst_tac [("psi", "?X ~: ?H")] asm_rl 1);
   1.718 +
   1.719 +(*pretend we have the right lemma!*)
   1.720 +(*EITHER the message was just sent by the Server, OR is a replay from the Enemy
   1.721 +  -- in either case it has the right form, only the age differs
   1.722 +*)
   1.723 +by (subgoal_tac "EX evt. K = newK evt & X = (Crypt {|Key K, Agent(Friend ia)|} (serverKey B)) & (evt = evs' | (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey (Friend ia))) : sees Enemy evs')" 1);
   1.724 +by (REPEAT_FIRST (eresolve_tac [exE, disjE, conjE] ORELSE' hyp_subst_tac));
   1.725 +by (asm_full_simp_tac (!simpset addsimps pushes) 1);
   1.726 +by (res_inst_tac [("x1","Crypt ?U (?K ia)")] (insert_commute RS ssubst) 1);
   1.727 +br notI 1;
   1.728 +
   1.729 +bd (impOfSubs analyze_insert_Crypt_subset) 1;
   1.730 +
   1.731 +(**LEVEL 40 **)
   1.732 +
   1.733 +(*In this case, the Key in X (newK evs') is younger than 
   1.734 +  the Key we are worried about (newK evs'a).  And nobody has used the
   1.735 +  new Key yet, so it can be pulled out of the "analyze".*)
   1.736 +by (asm_full_simp_tac
   1.737 +    (!simpset addsimps ([analyze_subset_parts RS keysFor_mono RS contra_subsetD])) 1);
   1.738 +by (Fast_tac 1); 
   1.739 +(*In this case, Enemy already knows about the message at hand...*)
   1.740 +by (dres_inst_tac [("psi", "?X ~: ?H")] asm_rl 1);
   1.741 +by (asm_full_simp_tac (!simpset addsimps ([insert_absorb]@pushes)) 1);
   1.742 +
   1.743 +(**LEVEL 44 **)
   1.744 +
   1.745 +by (excluded_middle_tac "evs'a=evt" 1);
   1.746 +(*Keys agree?  Then should have B = Friend j, so encrypted msg is secure*)
   1.747 +by (subgoal_tac "B = Friend j" 2);
   1.748 +by (REPEAT_FIRST hyp_subst_tac);
   1.749 +by (asm_full_simp_tac
   1.750 +    (!simpset addsimps ([analyze_subset_parts RS contra_subsetD])) 2);
   1.751 +(*Keys differ?  Then they cannot clash*)
   1.752 +
   1.753 +br notI 1;
   1.754 +bd (impOfSubs analyze_insert_Crypt_subset) 1;
   1.755 +
   1.756 +by (asm_full_simp_tac
   1.757 +    (!simpset addsimps (pushes@[analyze_subset_parts RS keysFor_mono RS contra_subsetD])) 1);
   1.758 +by (Fast_tac 1); 
   1.759 +
   1.760 +
   1.761 +
   1.762 +by (excluded_middle_tac "evs'a=evt" 1);
   1.763 +(*Keys agree?  Then should have B = Friend j, so encrypted msg is secure*)
   1.764 +by (subgoal_tac "B = Friend j & ia=i" 2);
   1.765 +by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac));
   1.766 +by (asm_full_simp_tac
   1.767 +    (!simpset addsimps ([analyze_subset_parts RS contra_subsetD])) 2);
   1.768 +(*Keys differ?  Then they cannot clash*)
   1.769 +
   1.770 +br notI 1;
   1.771 +bd (impOfSubs analyze_insert_Crypt_subset) 1;
   1.772 +
   1.773 +by (asm_full_simp_tac
   1.774 +    (!simpset addsimps (pushes@[analyze_subset_parts RS keysFor_mono RS contra_subsetD])) 1);
   1.775 +by (Fast_tac 1); 
   1.776 +
   1.777 +
   1.778 +Level 51
   1.779 +!!evs. [| Says Server (Friend i) (Crypt {|N, Agent (Friend j), K, X|} K') :
   1.780 +          setOfList evs;
   1.781 +          evs : traces; i ~= k; j ~= k |] ==>
   1.782 +       K ~: analyze (insert (Key (serverKey (Friend k))) (sees Enemy evs))
   1.783 + 1. !!evs A B K NA S X evsa evs' ia evs'a evt.
   1.784 +       [| i ~= k; j ~= k;
   1.785 +          Says S (Friend ia)
   1.786 +           (Crypt
   1.787 +             {|Nonce NA, Agent B, Key (newK evt),
   1.788 +              Crypt {|Key (newK evt), Agent (Friend ia)|} (serverKey B)|}
   1.789 +             (serverKey (Friend ia))) #
   1.790 +          evs' :
   1.791 +          traces;
   1.792 +          Friend ia ~= B;
   1.793 +          Says (Friend ia) Server {|Agent (Friend ia), Agent B, Nonce NA|} :
   1.794 +          setOfList evs';
   1.795 +          Says Server (Friend i)
   1.796 +           (Crypt
   1.797 +             {|N, Agent (Friend j), Key (newK evs'a),
   1.798 +              Crypt {|Key (newK evs'a), Agent (Friend i)|}
   1.799 +               (serverKey (Friend j))|}
   1.800 +             K') :
   1.801 +          setOfList evs';
   1.802 +          evs' : traces; length evs'a < length evs'; ia ~= k;
   1.803 +          Crypt
   1.804 +           {|Nonce NA, Agent B, Key (newK evt),
   1.805 +            Crypt {|Key (newK evt), Agent (Friend ia)|} (serverKey B)|}
   1.806 +           (serverKey (Friend ia)) :
   1.807 +          sees Enemy evs';
   1.808 +          Key (newK evs'a) ~:
   1.809 +          analyze (insert (Key (serverKey (Friend k))) (sees Enemy evs'));
   1.810 +          evs'a ~= evt;
   1.811 +          Key (newK evs'a) :
   1.812 +          analyze
   1.813 +           (insert (Key (newK evt))
   1.814 +             (insert (Key (serverKey (Friend k))) (sees Enemy evs'))) |] ==>
   1.815 +       False
   1.816 +
   1.817 +
   1.818 +
   1.819 +
   1.820 +YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY;
   1.821 +
   1.822 +
   1.823 +push_proof();
   1.824 +goal thy 
   1.825 + "!!evs. [| evs = Says S (Friend i) \
   1.826 +\                 (Crypt {|N, Agent(Friend j), K, X|} K') # evs';  \
   1.827 +\           evs : traces;  i~=k                                    \
   1.828 +\        |] ==>                                                    \
   1.829 +\     K ~: analyze (insert (Key (serverKey (Friend k))) (sees Enemy evs))";
   1.830 +be rev_mp 1;
   1.831 +be traces.induct 1;
   1.832 +be subst 4;	(*NS2: discard evsa = Says A Server... as irrelevant!*)
   1.833 +by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes)));
   1.834 +by (Step_tac 1);
   1.835 +by (asm_full_simp_tac (!simpset addsimps[analyze_subset_parts RS contra_subsetD]) 1);
   1.836 +val Enemy_not_see_encrypted_key_lemma = result();
   1.837 +
   1.838 +
   1.839 +
   1.840 +
   1.841 +by (asm_full_simp_tac
   1.842 +    (!simpset addsimps (pushes @
   1.843 +			[analyze_subset_parts RS contra_subsetD,
   1.844 +			 traces_ConsE RS Enemy_not_see_serverKey])) 1);
   1.845 +
   1.846 +by (asm_full_simp_tac
   1.847 +    (!simpset addsimps [analyze_subset_parts  RS keysFor_mono RS contra_subsetD,
   1.848 +			traces_ConsE RS new_keys_not_used]) 1);
   1.849 +by (Fast_tac 1); 
   1.850 +
   1.851 +
   1.852 +
   1.853 +
   1.854 +(*Precisely formulated as needed below.  Perhaps redundant, as simplification
   1.855 +  with the aid of  analyze_subset_parts RS contra_subsetD  might do the
   1.856 +  same thing.*)
   1.857 +goal thy 
   1.858 + "!!evs. [| evs : traces; A ~= Enemy;  A ~= Friend j |] ==> \
   1.859 +\        Key (serverKey A) ~:                               \
   1.860 +\          analyze (insert (Key (serverKey (Friend j))) (sees Enemy evs))";
   1.861 +br (analyze_subset_parts RS contra_subsetD) 1;
   1.862 +by (Asm_simp_tac 1);
   1.863 +qed "insert_not_analyze_serverKey";
   1.864 +
   1.865 +
   1.866 +
   1.867 +
   1.868 +by (asm_full_simp_tac
   1.869 +    (!simpset addsimps (pushes @
   1.870 +			[insert_not_analyze_serverKey, 
   1.871 +			 traces_ConsE RS insert_not_analyze_serverKey])) 1);
   1.872 +
   1.873 +
   1.874 +by (stac analyze_insert_Crypt 1);
   1.875 +
   1.876 +
   1.877 +
   1.878 +
   1.879 +
   1.880 +
   1.881 +
   1.882 +
   1.883 +
   1.884 +
   1.885 +
   1.886 +
   1.887 +(*NS3, case 1: that message from the Server was just sent*)
   1.888 +by (asm_full_simp_tac (!simpset addsimps pushes) 1);
   1.889 +
   1.890 +(*NS3, case 2: that message from the Server was sent earlier*)
   1.891 +by (REPEAT_FIRST (eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac));
   1.892 +by (mp_tac 1);
   1.893 +by (asm_full_simp_tac (!simpset addsimps pushes) 1);
   1.894 +
   1.895 +by (Step_tac 1);
   1.896 +by (asm_full_simp_tac
   1.897 +    (!simpset addsimps [traces_ConsE RS insert_not_analyze_serverKey]) 1);
   1.898 +
   1.899 +
   1.900 +
   1.901 +(*pretend we have the right lemma!*)
   1.902 +by (subgoal_tac "(EX evt. X = (Crypt {|Key(newK evt), Agent(Friend ia)|} (serverKey B)))" 1);
   1.903 +by (REPEAT_FIRST (eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac));
   1.904 +by (asm_full_simp_tac (!simpset addsimps pushes) 1);
   1.905 +
   1.906 +by (excluded_middle_tac "ia=k" 1);
   1.907 +(*Case where the key is compromised*)
   1.908 +by (hyp_subst_tac 2);
   1.909 +by (stac insert_commute 2);   (*Pushes in the "insert X" for simplification*)
   1.910 +by (Asm_full_simp_tac 2);
   1.911 +
   1.912 +
   1.913 +
   1.914 +by (asm_full_simp_tac (!simpset addsimps pushes) 1);
   1.915 +
   1.916 +by (REPEAT_FIRST Safe_step_tac);
   1.917 +by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes)));
   1.918 +
   1.919 +
   1.920 +by (REPEAT (Safe_step_tac 1));
   1.921 +
   1.922 +
   1.923 +
   1.924 +by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes)));
   1.925 +
   1.926 +by (REPEAT_FIRST (eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac));
   1.927 +
   1.928 +by (eres_inst_tac [("V","?P-->?Q")] thin_rl 1);	(*deletes the bad implication*)
   1.929 +by ((forward_tac [Says_Server_message_form] THEN' 
   1.930 +     fast_tac (!claset addSEs [traces_ConsE])) 1);
   1.931 +by (REPEAT_FIRST (eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac));
   1.932 +
   1.933 +
   1.934 +
   1.935 +XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX;
   1.936 +proof_timing:=true;
   1.937 +
   1.938 +(*Case where the key is secure*)
   1.939 +by (dres_inst_tac [("psi", "?X ~: ?H")] asm_rl 1);
   1.940 +by (asm_full_simp_tac
   1.941 +    (!simpset addsimps [traces_ConsE RS insert_not_analyze_serverKey]) 1);
   1.942 +
   1.943 +
   1.944 +
   1.945 +by (full_simp_tac (!simpset addsimps [insert_Key_Agent_delay,
   1.946 +				      insert_Key_Crypt_delay]) 1);
   1.947 +
   1.948 +by (forward_tac [setOfList_I1 RS Says_Server_message_form] 1);
   1.949 +by (REPEAT_FIRST (eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac));
   1.950 +
   1.951 +
   1.952 +by (asm_full_simp_tac
   1.953 +    (!simpset addsimps [traces_ConsE RS insert_not_analyze_serverKey]) 1);
   1.954 +
   1.955 +
   1.956 +by (stac insert_commute 1);   (*Pushes in the "insert X" for simplification*)
   1.957 +by (stac analyze_insert_Crypt 1);
   1.958 +
   1.959 +by (asm_full_simp_tac
   1.960 +    (!simpset addsimps [insert_not_analyze_serverKey, 
   1.961 +			traces_ConsE RS insert_not_analyze_serverKey]) 1);
   1.962 +
   1.963 +
   1.964 + 1. !!evs A B K NA S X evsa evs' ia evs'a.
   1.965 +       [| i ~= k; j ~= k;
   1.966 +          Says S (Friend ia)
   1.967 +           (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey (Friend ia))) #
   1.968 +          evs' :
   1.969 +          traces;
   1.970 +          Friend ia ~= B;
   1.971 +          Says (Friend ia) Server {|Agent (Friend ia), Agent B, Nonce NA|} :
   1.972 +          setOfList evs';
   1.973 +          Says Server (Friend i)
   1.974 +           (Crypt
   1.975 +             {|N, Agent (Friend j), Key (newK evs'a),
   1.976 +              Crypt {|Key (newK evs'a), Agent (Friend i)|}
   1.977 +               (serverKey (Friend j))|}
   1.978 +             K') :
   1.979 +          setOfList evs';
   1.980 +          Key (newK evs'a) ~:
   1.981 +          analyze
   1.982 +           (insert
   1.983 +             (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey (Friend ia)))
   1.984 +             (insert (Key (serverKey (Friend k))) (sees Enemy evs')));
   1.985 +          length evs'a < length evs' |] ==>
   1.986 +       Key (newK evs'a) ~:
   1.987 +       analyze
   1.988 +        (insert X
   1.989 +          (insert
   1.990 +            (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey (Friend ia)))
   1.991 +            (insert (Key (serverKey (Friend k))) (sees Enemy evs'))))
   1.992 +
   1.993 +
   1.994 +by (Asm_full_simp_tac 1);
   1.995 +
   1.996 +
   1.997 +by (Simp_tac 2);
   1.998 +
   1.999 +
  1.1000 +by (Simp_tac 2);
  1.1001 +
  1.1002 +by (simp_tac (HOL_ss addsimps [insert_commute]) 2);
  1.1003 +
  1.1004 +
  1.1005 +by (simp_tac (HOL_ss addsimps [analyze_insert_insert]) 2);
  1.1006 +by (Asm_full_simp_tac 2);
  1.1007 +by (simp_tac (!simpset addsimps [insert_absorb]) 2);
  1.1008 +
  1.1009 +
  1.1010 +by (stac analyze_insert_Decrypt 2);
  1.1011 +
  1.1012 +
  1.1013 +goal thy "analyze (insert X (insert Y H)) = analyze (insert X (analyze (insert Y H)))";
  1.1014 +br analyze_insert_cong 1;
  1.1015 +by (Simp_tac 1);
  1.1016 +qed "analyze_insert_insert";
  1.1017 +
  1.1018 +
  1.1019 +
  1.1020 +
  1.1021 +
  1.1022 +
  1.1023 +
  1.1024 + 1. !!evs A B K NA S X evsa evs' ia evs'a.
  1.1025 +       [| i ~= k; j ~= k;
  1.1026 +          Says S (Friend ia)
  1.1027 +           (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey (Friend ia))) #
  1.1028 +          evs' :
  1.1029 +          traces;
  1.1030 +          Friend ia ~= B;
  1.1031 +          Says (Friend ia) Server {|Agent (Friend ia), Agent B, Nonce NA|} :
  1.1032 +          setOfList evs';
  1.1033 +          Says Server (Friend i)
  1.1034 +           (Crypt
  1.1035 +             {|N, Agent (Friend j), Key (newK evs'a),
  1.1036 +              Crypt {|Key (newK evs'a), Agent (Friend i)|}
  1.1037 +               (serverKey (Friend j))|}
  1.1038 +             K') :
  1.1039 +          setOfList evs';
  1.1040 +          length evs'a < length evs'; ia ~= k;
  1.1041 +          Key (newK evs'a) ~:
  1.1042 +          analyze (insert (Key (serverKey (Friend k))) (sees Enemy evs')) |] ==>
  1.1043 +       Key (newK evs'a) ~:
  1.1044 +       analyze
  1.1045 +        (insert X
  1.1046 +          (insert
  1.1047 +            (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey (Friend ia)))
  1.1048 +            (insert (Key (serverKey (Friend k))) (sees Enemy evs'))))
  1.1049 +
  1.1050 +
  1.1051 +by (ALLGOALS Asm_full_simp_tac);
  1.1052 +
  1.1053 +by (Asm_full_simp_tac 1);
  1.1054 +
  1.1055 +by (asm_simp_tac (!simpset addsimps [insert_not_analyze_serverKey]) 1);
  1.1056 +fr insert_not_analyze_serverKey;
  1.1057 +by (fast_tac (!claset addSEs [traces_ConsE]) 1);
  1.1058 +
  1.1059 +by (forward_tac [traces_ConsE] 1);
  1.1060 +
  1.1061 +
  1.1062 +
  1.1063 +by (asm_full_simp_tac (!simpset addsimps [analyze_subset_parts RS contra_subsetD]) 1);
  1.1064 +
  1.1065 +
  1.1066 +
  1.1067 +auto();
  1.1068 +
  1.1069 +by (REPEAT_FIRST (resolve_tac [conjI, impI]   (*DELETE NEXT TWO LINES??*)
  1.1070 +          ORELSE' eresolve_tac [conjE]
  1.1071 +          ORELSE' hyp_subst_tac));
  1.1072 +
  1.1073 +by (forward_tac [Says_Server_message_form] 2);
  1.1074 +
  1.1075 +bd Says_Server_message_form 2;
  1.1076 +by (fast_tac (!claset addSEs [traces_ConsE]) 2);
  1.1077 +auto();
  1.1078 +by (ALLGOALS (full_simp_tac (!simpset addsimps [insert_Key_delay])));
  1.1079 +
  1.1080 +(*SUBGOAL 1: use analyze_insert_Crypt to pull out
  1.1081 +       Crypt{|...|} (serverKey (Friend i))
  1.1082 +  SUBGOAL 2: cannot do this, as we don't seem to have ia~=j
  1.1083 +*)
  1.1084 +
  1.1085 +
  1.1086 +
  1.1087 +qed "Enemy_not_see_encrypted_key";
  1.1088 +
  1.1089 +
  1.1090 +goal thy 
  1.1091 + "!!evs. [| Says Server (Friend i) \
  1.1092 +\             (Crypt {|N, Agent B, K|} K') : setOfList evs;  \
  1.1093 +\           evs : traces;  i~=j    \
  1.1094 +\         |] ==> K ~: analyze (sees (Friend j) evs)";
  1.1095 +br (sees_agent_subset_sees_Enemy RS analyze_mono RS contra_subsetD) 1;
  1.1096 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [Enemy_not_see_encrypted_key])));
  1.1097 +qed "Friend_not_see_encrypted_key";
  1.1098 +
  1.1099 +goal thy 
  1.1100 + "!!evs. [| Says Server (Friend i) \
  1.1101 +\             (Crypt {|N, Agent B, K|} K') : setOfList evs;  \
  1.1102 +\           A ~: {Friend i, Server};  \
  1.1103 +\           evs : traces    \
  1.1104 +\        |] ==>  K ~: analyze (sees A evs)";
  1.1105 +by (eres_inst_tac [("P", "A~:?X")] rev_mp 1);
  1.1106 +by (agent.induct_tac "A" 1);
  1.1107 +by (ALLGOALS Simp_tac);
  1.1108 +by (asm_simp_tac (!simpset addsimps [eq_sym_conv, 
  1.1109 +				     Friend_not_see_encrypted_key]) 1);
  1.1110 +br ([analyze_mono, Enemy_not_see_encrypted_key] MRS contra_subsetD) 1;
  1.1111 +(*  hyp_subst_tac would deletes the equality assumption... *)
  1.1112 +by (ALLGOALS (rtac n_not_Suc_n ORELSE' Fast_tac));
  1.1113 +qed "Agent_not_see_encrypted_key";
  1.1114 +
  1.1115 +
  1.1116 +(*Neatly packaged, perhaps in a useless form*)
  1.1117 +goalw thy [knownBy_def]
  1.1118 + "!!evs. [| Says Server (Friend i) \
  1.1119 +\             (Crypt {|N, Agent B, K|} K') : setOfList evs;  \
  1.1120 +\           evs : traces    \
  1.1121 +\        |] ==>  knownBy evs K <= {Friend i, Server}";
  1.1122 +
  1.1123 +by (Step_tac 1);
  1.1124 +br ccontr 1;
  1.1125 +by (fast_tac (!claset addDs [Agent_not_see_encrypted_key]) 1);
  1.1126 +qed "knownBy_encrypted_key";
  1.1127 +
  1.1128 +
  1.1129 +
  1.1130 +
  1.1131  XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX;
  1.1132  
  1.1133  ZZZZZZZZZZZZZZZZ;
  1.1134 @@ -520,101 +1462,6 @@
  1.1135  WWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWW;
  1.1136  
  1.1137  
  1.1138 -Addsimps [new_keys_not_seen];
  1.1139 -
  1.1140 -(*Crucial security property: Enemy does not see the keys sent in msg NS2
  1.1141 -   -- even if another friend's key is compromised*)
  1.1142 -goal thy 
  1.1143 - "!!evs. [| Says Server (Friend i) \
  1.1144 -\          (Crypt {|N, Agent B, K, X|} K') : setOfList evs;  \
  1.1145 -\          evs : traces;  i~=j |] ==> \
  1.1146 -\       \
  1.1147 -\     K ~: analyze (insert (Key (serverKey (Friend j))) (sees Enemy evs))";
  1.1148 -be rev_mp 1;
  1.1149 -be traces.induct 1;
  1.1150 -be subst 4;	(*NS2: discard evsa = Says A Server... as irrelevant!*)
  1.1151 -by (ALLGOALS Asm_full_simp_tac);
  1.1152 -(*The two simplifications cannot be combined -- they loop!*)
  1.1153 -by (ALLGOALS (full_simp_tac (!simpset addsimps [insert_Key_delay])));
  1.1154 -(*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
  1.1155 -br conjI 3;
  1.1156 -by (REPEAT_FIRST (resolve_tac [impI]));
  1.1157 -by (TRYALL (forward_tac [Says_Server_imp_Key_newK] THEN' assume_tac));
  1.1158 -(*NS1, subgoal concerns "(Says A Server
  1.1159 -                          {|Agent A, Agent B, Nonce (newN evsa)|}"*)
  1.1160 -(*... thus it cannot equal any components of A's message above.*)
  1.1161 -by (fast_tac (!claset addss (!simpset)) 2);
  1.1162 -(*NS2, the subcase where that message was the most recently sent;
  1.1163 -  it holds because here K' = serverKey(Friend i), which Enemies can't see,
  1.1164 -  AND because nobody can know about a brand new key*)
  1.1165 -by (fast_tac (!claset addss (!simpset addsimps [not_parts_not_analyze])) 2);
  1.1166 -(*NS2, other subcase.  K is an old key, and thus not in the latest message.*)
  1.1167 -by (fast_tac 
  1.1168 -    (!claset addSEs [less_irrefl]
  1.1169 -             addDs [impOfSubs analyze_insert_Crypt_subset]
  1.1170 -	     addss (!simpset addsimps [not_parts_not_keysFor_analyze])) 2);
  1.1171 -(*Now for the Fake case*)
  1.1172 -be exE 1;
  1.1173 -br notI 1;
  1.1174 -by (REPEAT (etac conjE 1));
  1.1175 -by (REPEAT (hyp_subst_tac 1));
  1.1176 -by (subgoal_tac 
  1.1177 -    "Key (newK evs') : \
  1.1178 -\    analyze (synthesize (analyze (insert (Key (serverKey (Friend j))) \
  1.1179 -\                                  (sees Enemy evsa))))" 1);
  1.1180 -be (impOfSubs analyze_mono) 2;
  1.1181 -by (best_tac (!claset addIs [analyze_mono RS synthesize_mono RSN 
  1.1182 -			     (2,rev_subsetD),
  1.1183 -			     impOfSubs synthesize_increasing,
  1.1184 -			     impOfSubs analyze_increasing]) 2);
  1.1185 -(*Proves the Fake goal*)
  1.1186 -by (Auto_tac());
  1.1187 -qed "Enemy_not_see_encrypted_key";
  1.1188 -
  1.1189 -
  1.1190 -goal thy 
  1.1191 - "!!evs. [| Says Server (Friend i) \
  1.1192 -\             (Crypt {|N, Agent B, K|} K') : setOfList evs;  \
  1.1193 -\           evs : traces;  i~=j    \
  1.1194 -\         |] ==> K ~: analyze (sees (Friend j) evs)";
  1.1195 -br (sees_agent_subset_sees_Enemy RS analyze_mono RS contra_subsetD) 1;
  1.1196 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [Enemy_not_see_encrypted_key])));
  1.1197 -qed "Friend_not_see_encrypted_key";
  1.1198 -
  1.1199 -goal thy 
  1.1200 - "!!evs. [| Says Server (Friend i) \
  1.1201 -\             (Crypt {|N, Agent B, K|} K') : setOfList evs;  \
  1.1202 -\           A ~: {Friend i, Server};  \
  1.1203 -\           evs : traces    \
  1.1204 -\        |] ==>  K ~: analyze (sees A evs)";
  1.1205 -by (eres_inst_tac [("P", "A~:?X")] rev_mp 1);
  1.1206 -by (agent.induct_tac "A" 1);
  1.1207 -by (ALLGOALS Simp_tac);
  1.1208 -by (asm_simp_tac (!simpset addsimps [eq_sym_conv, 
  1.1209 -				     Friend_not_see_encrypted_key]) 1);
  1.1210 -br ([analyze_mono, Enemy_not_see_encrypted_key] MRS contra_subsetD) 1;
  1.1211 -(*  hyp_subst_tac would deletes the equality assumption... *)
  1.1212 -by (ALLGOALS (rtac n_not_Suc_n ORELSE' Fast_tac));
  1.1213 -qed "Agent_not_see_encrypted_key";
  1.1214 -
  1.1215 -
  1.1216 -(*Neatly packaged, perhaps in a useless form*)
  1.1217 -goalw thy [knownBy_def]
  1.1218 - "!!evs. [| Says Server (Friend i) \
  1.1219 -\             (Crypt {|N, Agent B, K|} K') : setOfList evs;  \
  1.1220 -\           evs : traces    \
  1.1221 -\        |] ==>  knownBy evs K <= {Friend i, Server}";
  1.1222 -
  1.1223 -by (Step_tac 1);
  1.1224 -br ccontr 1;
  1.1225 -by (fast_tac (!claset addDs [Agent_not_see_encrypted_key]) 1);
  1.1226 -qed "knownBy_encrypted_key";
  1.1227 -
  1.1228 -
  1.1229 -
  1.1230 -
  1.1231 -XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX;
  1.1232 -
  1.1233  
  1.1234  
  1.1235  
  1.1236 @@ -651,10 +1498,6 @@
  1.1237  
  1.1238  
  1.1239  
  1.1240 -goal thy "insert (Crypt x) (insert {|X,Y|} evs) = \
  1.1241 -\         insert {|X,Y|} (insert (Crypt x) evs)";
  1.1242 -by (Fast_tac 1);
  1.1243 -qed "insert_Crypt_MPair_delay";
  1.1244  
  1.1245  
  1.1246  
     2.1 --- a/src/HOL/Auth/Event.thy	Fri Jul 26 12:18:50 1996 +0200
     2.2 +++ b/src/HOL/Auth/Event.thy	Fri Jul 26 12:19:46 1996 +0200
     2.3 @@ -26,7 +26,7 @@
     2.4  
     2.5  primrec initState agent
     2.6          (*Server knows all keys; other agents know only their own*)
     2.7 -  initState_Server  "initState Server     = range (Key o serverKey)"
     2.8 +  initState_Server  "initState Server     = Key `` range serverKey"
     2.9    initState_Friend  "initState (Friend i) = {Key (serverKey (Friend i))}"
    2.10    initState_Enemy   "initState Enemy  = {Key (serverKey Enemy)}"
    2.11  
    2.12 @@ -111,7 +111,7 @@
    2.13                     (serverKey A))) # evs : traces"
    2.14  
    2.15             (*We can't assume S=Server.  Agent A "remembers" her nonce.
    2.16 -             May assume WLOG that she is NOT the Enemy, as the Fake rule.
    2.17 +             May assume WLOG that she is NOT the Enemy: the Fake rule
    2.18               covers this case.  Can inductively show A ~= Server*)
    2.19      NS3  "[| evs: traces;  A ~= B;
    2.20               evs = (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|}
     3.1 --- a/src/HOL/Auth/Message.ML	Fri Jul 26 12:18:50 1996 +0200
     3.2 +++ b/src/HOL/Auth/Message.ML	Fri Jul 26 12:19:46 1996 +0200
     3.3 @@ -268,6 +268,8 @@
     3.4  AddSEs [MPair_analyze];
     3.5  AddDs  [analyze.Decrypt];
     3.6  
     3.7 +Addsimps [analyze.Inj];
     3.8 +
     3.9  goal thy "H <= analyze(H)";
    3.10  by (Fast_tac 1);
    3.11  qed "analyze_increasing";
    3.12 @@ -289,6 +291,13 @@
    3.13  qed "parts_analyze";
    3.14  Addsimps [parts_analyze];
    3.15  
    3.16 +goal thy "analyze (parts H) = parts H";
    3.17 +by (Auto_tac());
    3.18 +be analyze.induct 1;
    3.19 +by (Auto_tac());
    3.20 +qed "analyze_parts";
    3.21 +Addsimps [analyze_parts];
    3.22 +
    3.23  (*Monotonicity; Lemma 1 of Lowe*)
    3.24  goalw thy analyze.defs "!!G H. G<=H ==> analyze(G) <= analyze(H)";
    3.25  by (rtac lfp_mono 1);
    3.26 @@ -342,6 +351,17 @@
    3.27  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    3.28  qed "analyze_insert_Key";
    3.29  
    3.30 +goal thy "analyze (insert {|X,Y|} H) = \
    3.31 +\         insert {|X,Y|} (analyze (insert X (insert Y H)))";
    3.32 +br equalityI 1;
    3.33 +br subsetI 1;
    3.34 +be analyze.induct 1;
    3.35 +by (Auto_tac());
    3.36 +be analyze.induct 1;
    3.37 +by (ALLGOALS (deepen_tac (!claset addIs [analyze.Fst, analyze.Snd, analyze.Decrypt]) 0));
    3.38 +qed "analyze_insert_MPair";
    3.39 +
    3.40 +(*Can pull out enCrypted message if the Key is not known*)
    3.41  goal thy "!!H. Key (invKey K) ~: analyze H ==>  \
    3.42  \              analyze (insert (Crypt X K) H) = \
    3.43  \              insert (Crypt X K) (analyze H)";
    3.44 @@ -375,70 +395,31 @@
    3.45  by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1));
    3.46  qed "analyze_insert_Decrypt";
    3.47  
    3.48 +(*Case analysis: either the message is secure, or it is not!
    3.49 +  Use with expand_if;  apparently split_tac does not cope with patterns
    3.50 +  such as "analyze (insert (Crypt X' K) H)" *)
    3.51 +goal thy "analyze (insert (Crypt X' K) H) = \
    3.52 +\         (if (Key (invKey K)  : analyze H) then    \
    3.53 +\               insert (Crypt X' K) (analyze (insert X' H)) \
    3.54 +\          else insert (Crypt X' K) (analyze H))";
    3.55 +by (excluded_middle_tac "Key (invKey K)  : analyze H " 1);
    3.56 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [analyze_insert_Crypt, 
    3.57 +					       analyze_insert_Decrypt])));
    3.58 +qed "analyze_Crypt_if";
    3.59 +
    3.60  Addsimps [analyze_insert_Agent, analyze_insert_Nonce, 
    3.61 -	  analyze_insert_Key, analyze_insert_Crypt,
    3.62 -	  analyze_insert_Decrypt];
    3.63 -
    3.64 +	  analyze_insert_Key, analyze_insert_MPair, 
    3.65 +	  analyze_Crypt_if];
    3.66  
    3.67  (*This rule supposes "for the sake of argument" that we have the key.*)
    3.68  goal thy  "analyze (insert (Crypt X K) H) <=  \
    3.69 -\         insert (Crypt X K) (analyze (insert X H))";
    3.70 +\          insert (Crypt X K) (analyze (insert X H))";
    3.71  br subsetI 1;
    3.72  be analyze.induct 1;
    3.73  by (Auto_tac());
    3.74  qed "analyze_insert_Crypt_subset";
    3.75  
    3.76  
    3.77 -(** Rewrite rules for pulling out atomic parts of messages **)
    3.78 -
    3.79 -goal thy "analyze (insert X H) <= analyze (insert {|X,Y|} H)";
    3.80 -br subsetI 1;
    3.81 -be analyze.induct 1;
    3.82 -by (ALLGOALS (best_tac (!claset addIs [analyze.Fst]))); 
    3.83 -qed "analyze_insert_subset_MPair1";
    3.84 -
    3.85 -goal thy "analyze (insert Y H) <= analyze (insert {|X,Y|} H)";
    3.86 -br subsetI 1;
    3.87 -be analyze.induct 1;
    3.88 -by (ALLGOALS (best_tac (!claset addIs [analyze.Snd]))); 
    3.89 -qed "analyze_insert_subset_MPair2";
    3.90 -
    3.91 -goal thy "analyze (insert {|Agent agt,Y|} H) = \
    3.92 -\         insert {|Agent agt,Y|} (insert (Agent agt) (analyze (insert Y H)))";
    3.93 -by (rtac equalityI 1);
    3.94 -by (best_tac (!claset addIs [analyze.Fst,
    3.95 -			     impOfSubs analyze_insert_subset_MPair2]) 2); 
    3.96 -br subsetI 1;
    3.97 -be analyze.induct 1;
    3.98 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    3.99 -qed "analyze_insert_Agent_MPair";
   3.100 -
   3.101 -goal thy "analyze (insert {|Nonce N,Y|} H) = \
   3.102 -\         insert {|Nonce N,Y|} (insert (Nonce N) (analyze (insert Y H)))";
   3.103 -by (rtac equalityI 1);
   3.104 -by (best_tac (!claset addIs [analyze.Fst,
   3.105 -			     impOfSubs analyze_insert_subset_MPair2]) 2); 
   3.106 -br subsetI 1;
   3.107 -be analyze.induct 1;
   3.108 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   3.109 -qed "analyze_insert_Nonce_MPair";
   3.110 -
   3.111 -(*Can only pull out Keys if they are not needed to decrypt the rest*)
   3.112 -goalw thy [keysFor_def]
   3.113 -    "!!K. K ~: keysFor (analyze (insert Y H)) ==>  \
   3.114 -\         analyze (insert {|Key K, Y|} H) = \
   3.115 -\         insert {|Key K, Y|} (insert (Key K) (analyze (insert Y H)))";
   3.116 -by (rtac equalityI 1);
   3.117 -by (best_tac (!claset addIs [analyze.Fst,
   3.118 -			     impOfSubs analyze_insert_subset_MPair2]) 2); 
   3.119 -br subsetI 1;
   3.120 -be analyze.induct 1;
   3.121 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   3.122 -qed "analyze_insert_Key_MPair";
   3.123 -
   3.124 -Addsimps [analyze_insert_Agent_MPair, analyze_insert_Nonce_MPair,
   3.125 -	  analyze_insert_Key_MPair];
   3.126 -
   3.127  (** Idempotence and transitivity **)
   3.128  
   3.129  goal thy "!!H. X: analyze (analyze H) ==> X: analyze H";
   3.130 @@ -467,6 +448,29 @@
   3.131     "!!H. Y: analyze (insert X H) ==> X: analyze H --> Y: analyze H"
   3.132  *)
   3.133  
   3.134 +
   3.135 +(** A congruence rule for "analyze" **)
   3.136 +
   3.137 +goal thy "!!H. [| analyze G <= analyze G'; analyze H <= analyze H' \
   3.138 +\              |] ==> analyze (G Un H) <= analyze (G' Un H')";
   3.139 +by (Step_tac 1);
   3.140 +be analyze.induct 1;
   3.141 +by (ALLGOALS (best_tac (!claset addIs [analyze_mono RS subsetD])));
   3.142 +qed "analyze_subset_cong";
   3.143 +
   3.144 +goal thy "!!H. [| analyze G = analyze G'; analyze H = analyze H' \
   3.145 +\              |] ==> analyze (G Un H) = analyze (G' Un H')";
   3.146 +by (REPEAT_FIRST (ares_tac [equalityI, analyze_subset_cong]
   3.147 +	  ORELSE' etac equalityE));
   3.148 +qed "analyze_cong";
   3.149 +
   3.150 +
   3.151 +goal thy "!!H. analyze H = analyze H'  ==>    \
   3.152 +\              analyze (insert X H) = analyze (insert X H')";
   3.153 +by (asm_simp_tac (!simpset addsimps [insert_def] 
   3.154 +		           setloop (rtac analyze_cong)) 1);
   3.155 +qed "analyze_insert_cong";
   3.156 +
   3.157  (*If there are no pairs or encryptions then analyze does nothing*)
   3.158  goal thy "!!H. [| ALL X Y. {|X,Y|} ~: H;  ALL X K. Crypt X K ~: H |] ==> \
   3.159  \         analyze H = H";
   3.160 @@ -510,6 +514,10 @@
   3.161  by (REPEAT (ares_tac [Un_least, synthesize_mono, Un_upper1, Un_upper2] 1));
   3.162  qed "synthesize_Un";
   3.163  
   3.164 +goal thy "insert X (synthesize H) <= synthesize(insert X H)";
   3.165 +by (fast_tac (!claset addEs [impOfSubs synthesize_mono]) 1);
   3.166 +qed "synthesize_insert";
   3.167 +
   3.168  (** Idempotence and transitivity **)
   3.169  
   3.170  goal thy "!!H. X: synthesize (synthesize H) ==> X: synthesize H";
   3.171 @@ -539,6 +547,7 @@
   3.172    but can synthesize a pair or encryption from its components...*)
   3.173  val mk_cases = synthesize.mk_cases msg.simps;
   3.174  
   3.175 +(*NO Agent_synthesize, as any Agent name can be synthesized*)
   3.176  val Nonce_synthesize = mk_cases "Nonce n : synthesize H";
   3.177  val Key_synthesize   = mk_cases "Key K : synthesize H";
   3.178  val MPair_synthesize = mk_cases "{|X,Y|} : synthesize H";
   3.179 @@ -566,14 +575,6 @@
   3.180  
   3.181  (*** Combinations of parts, analyze and synthesize ***)
   3.182  
   3.183 -(*Not that useful, in view of the following one...*)
   3.184 -goal thy "parts (synthesize H) <= synthesize (parts H)";
   3.185 -by (Step_tac 1);
   3.186 -be parts.induct 1;
   3.187 -be (parts_increasing RS synthesize_mono RS subsetD) 1;
   3.188 -by (ALLGOALS Fast_tac);
   3.189 -qed "parts_synthesize_subset";
   3.190 -
   3.191  goal thy "parts (synthesize H) = parts H Un synthesize H";
   3.192  br equalityI 1;
   3.193  br subsetI 1;