src/HOL/Auth/Event.ML
author paulson
Wed Aug 21 13:22:23 1996 +0200 (1996-08-21)
changeset 1933 8b24773de6db
parent 1930 cdf9bcd53749
child 1942 6c9c1a42a869
permissions -rw-r--r--
Addition of message NS5
     1 (*  Title:      HOL/Auth/Message
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Datatype of events;
     7 inductive relation "traces" for Needham-Schroeder (shared keys)
     8 
     9 Rewrites should not refer to	 initState (Friend i)    -- not in normal form
    10 *)
    11 
    12 Addsimps [parts_cut_eq];
    13 
    14 
    15 (*INSTALLED ON NAT.ML*)
    16 goalw Nat.thy [le_def] "(m <= n) = (m < Suc n)";
    17 by (rtac not_less_eq 1);
    18 qed "le_eq_less_Suc";
    19 
    20 proof_timing:=true;
    21 
    22 (*FOR LIST.ML??*)
    23 goal List.thy "x : set_of_list (x#xs)";
    24 by (Simp_tac 1);
    25 qed "set_of_list_I1";
    26 
    27 goal List.thy "!!x. xs = x#xs' ==> x : set_of_list xs";
    28 by (Asm_simp_tac 1);
    29 qed "set_of_list_eqI1";
    30 
    31 goal List.thy "set_of_list l <= set_of_list (x#l)";
    32 by (Simp_tac 1);
    33 by (Fast_tac 1);
    34 qed "set_of_list_subset_Cons";
    35 
    36 (*Not for Addsimps -- it can cause goals to blow up!*)
    37 goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
    38 by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
    39 qed "mem_if";
    40 
    41 (*FUN.ML??  WE NEED A NOTION OF INVERSE IMAGE, OR GRAPH!!*)
    42 goal Set.thy "!!f. B <= range f = (B = f`` {x. f x: B})";
    43 by (fast_tac (!claset addEs [equalityE]) 1);
    44 val subset_range_iff = result();
    45 
    46 
    47 open Event;
    48 
    49 Addsimps [Un_insert_left, Un_insert_right];
    50 
    51 (*By default only o_apply is built-in.  But in the presence of eta-expansion
    52   this means that some terms displayed as (f o g) will be rewritten, and others
    53   will not!*)
    54 Addsimps [o_def];
    55 
    56 (*** Basic properties of serverKey and newK ***)
    57 
    58 (* invKey (serverKey A) = serverKey A *)
    59 bind_thm ("invKey_serverKey", rewrite_rule [isSymKey_def] isSym_serverKey);
    60 
    61 (* invKey (newK evs) = newK evs *)
    62 bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK);
    63 Addsimps [invKey_serverKey, invKey_newK];
    64 
    65 
    66 (*New keys and nonces are fresh*)
    67 val serverKey_inject = inj_serverKey RS injD;
    68 val newN_inject = inj_newN RS injD
    69 and newK_inject = inj_newK RS injD;
    70 AddSEs [serverKey_inject, newN_inject, newK_inject,
    71 	fresh_newK RS notE, fresh_newN RS notE];
    72 Addsimps [inj_serverKey RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq];
    73 Addsimps [fresh_newN, fresh_newK];
    74 
    75 goal thy "newK evs ~= serverKey B";
    76 by (subgoal_tac "newK evs = serverKey B --> \
    77 \                Key (newK evs) : parts (initState B)" 1);
    78 by (Fast_tac 1);
    79 by (agent.induct_tac "B" 1);
    80 by (auto_tac (!claset addIs [range_eqI], !simpset));
    81 qed "newK_neq_serverKey";
    82 
    83 Addsimps [newK_neq_serverKey, newK_neq_serverKey RS not_sym];
    84 
    85 (*Good for talking about Server's initial state*)
    86 goal thy "!!H. H <= Key``E ==> parts H = H";
    87 by (Auto_tac ());
    88 be parts.induct 1;
    89 by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    90 qed "parts_image_subset";
    91 
    92 bind_thm ("parts_image_Key", subset_refl RS parts_image_subset);
    93 
    94 goal thy "!!H. H <= Key``E ==> analz H = H";
    95 by (Auto_tac ());
    96 be analz.induct 1;
    97 by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    98 qed "analz_image_subset";
    99 
   100 bind_thm ("analz_image_Key", subset_refl RS analz_image_subset);
   101 
   102 Addsimps [parts_image_Key, analz_image_Key];
   103 
   104 goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
   105 by (agent.induct_tac "C" 1);
   106 by (auto_tac (!claset addIs [range_eqI] delrules partsEs, !simpset));
   107 qed "keysFor_parts_initState";
   108 Addsimps [keysFor_parts_initState];
   109 
   110 goalw thy [keysFor_def] "keysFor (Key``E) = {}";
   111 by (Auto_tac ());
   112 qed "keysFor_image_Key";
   113 Addsimps [keysFor_image_Key];
   114 
   115 goal thy "serverKey A ~: newK``E";
   116 by (agent.induct_tac "A" 1);
   117 by (Auto_tac ());
   118 qed "serverKey_notin_image_newK";
   119 Addsimps [serverKey_notin_image_newK];
   120 
   121 
   122 (*Agents see their own serverKeys!*)
   123 goal thy "Key (serverKey A) : analz (sees A evs)";
   124 by (list.induct_tac "evs" 1);
   125 by (asm_simp_tac (!simpset addsimps [impOfSubs(Un_upper2 RS analz_mono)]) 2);
   126 by (agent.induct_tac "A" 1);
   127 by (auto_tac (!claset addIs [range_eqI], !simpset));
   128 qed "analz_own_serverKey";
   129 
   130 bind_thm ("parts_own_serverKey",
   131 	  [analz_subset_parts, analz_own_serverKey] MRS subsetD);
   132 
   133 Addsimps [analz_own_serverKey, parts_own_serverKey];
   134 
   135 
   136 
   137 (**** Inductive relation "traces" -- basic properties ****)
   138 
   139 val mk_cases = traces.mk_cases (list.simps @ agent.simps @ event.simps);
   140 
   141 val Says_tracesE        = mk_cases "Says A B X # evs: traces";
   142 val Says_Server_tracesE = mk_cases "Says Server B X # evs: traces";
   143 val Says_Enemy_tracesE  = mk_cases "Says Enemy B X # evs: traces";
   144 val Says_to_Server_tracesE = mk_cases "Says A Server X # evs: traces";
   145 val Notes_tracesE       = mk_cases "Notes A X # evs: traces";
   146 
   147 (*The tail of a trace is a trace*)
   148 goal thy "!!ev evs. ev#evs : traces ==> evs : traces";
   149 by (fast_tac (!claset addEs [mk_cases "ev#evs:traces"]) 1);
   150 qed "traces_ConsE";
   151 
   152 goal thy "!!ev evs. [| evs = ev#evs'; evs : traces |] ==> evs' : traces";
   153 by (fast_tac (!claset addEs [mk_cases "ev#evs:traces"]) 1);
   154 qed "traces_eq_ConsE";
   155 
   156 
   157 (** Specialized rewrite rules for (sees A (Says...#evs)) **)
   158 
   159 goal thy "sees A (Says A B X # evs) = insert X (sees A evs)";
   160 by (Simp_tac 1);
   161 qed "sees_own";
   162 
   163 goal thy "!!A. Server ~= A ==> \
   164 \              sees Server (Says A B X # evs) = sees Server evs";
   165 by (Asm_simp_tac 1);
   166 qed "sees_Server";
   167 
   168 goal thy "!!A. Friend i ~= A ==> \
   169 \              sees (Friend i) (Says A B X # evs) = sees (Friend i) evs";
   170 by (Asm_simp_tac 1);
   171 qed "sees_Friend";
   172 
   173 goal thy "sees Enemy (Says A B X # evs) = insert X (sees Enemy evs)";
   174 by (Simp_tac 1);
   175 qed "sees_Enemy";
   176 
   177 goal thy "sees A (Says A' B X # evs) <= insert X (sees A evs)";
   178 by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
   179 by (Fast_tac 1);
   180 qed "sees_Says_subset_insert";
   181 
   182 goal thy "sees A evs <= sees A (Says A' B X # evs)";
   183 by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
   184 by (Fast_tac 1);
   185 qed "sees_subset_sees_Says";
   186 
   187 (*Pushing Unions into parts; one of the A's equals B, and thus sees Y*)
   188 goal thy "(UN A. parts (sees A (Says B C Y # evs))) = \
   189 \         parts {Y} Un (UN A. parts (sees A evs))";
   190 by (Step_tac 1);
   191 be rev_mp 1;	(*for some reason, split_tac does not work on assumptions*)
   192 val ss = (!simpset addsimps [parts_Un, sees_Cons] 
   193 	           setloop split_tac [expand_if]);
   194 by (ALLGOALS (fast_tac (!claset addss ss)));
   195 qed "UN_parts_sees_Says";
   196 
   197 goal thy "Says A B X : set_of_list evs --> X : sees Enemy evs";
   198 by (list.induct_tac "evs" 1);
   199 by (Auto_tac ());
   200 qed_spec_mp "Says_imp_sees_Enemy";
   201 
   202 Addsimps [Says_imp_sees_Enemy];
   203 AddIs    [Says_imp_sees_Enemy];
   204 
   205 goal thy "initState C <= Key `` range serverKey";
   206 by (agent.induct_tac "C" 1);
   207 by (Auto_tac ());
   208 qed "initState_subset";
   209 
   210 goal thy "X : sees C evs --> \
   211 \          (EX A B. Says A B X : set_of_list evs) | \
   212 \          (EX A. Notes A X : set_of_list evs) | \
   213 \          (EX A. X = Key (serverKey A))";
   214 by (list.induct_tac "evs" 1);
   215 by (ALLGOALS Asm_simp_tac);
   216 by (fast_tac (!claset addDs [impOfSubs initState_subset]) 1);
   217 br conjI 1;
   218 by (Fast_tac 2);
   219 by (event.induct_tac "a" 1);
   220 by (ALLGOALS (asm_simp_tac (!simpset addsimps [mem_if])));
   221 by (ALLGOALS Fast_tac);
   222 qed_spec_mp "seesD";
   223 
   224 
   225 Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Enemy];
   226 Delsimps [sees_Cons];	(**** NOTE REMOVAL -- laws above are cleaner ****)
   227 
   228 
   229 (**** Inductive proofs about traces ****)
   230 
   231 (*The Enemy can see more than anybody else, except for their initial state*)
   232 goal thy 
   233  "!!evs. evs : traces ==> \
   234 \     sees A evs <= initState A Un sees Enemy evs";
   235 be traces.induct 1;
   236 by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
   237 			        addss (!simpset))));
   238 qed "sees_agent_subset_sees_Enemy";
   239 
   240 
   241 (*Nobody sends themselves messages*)
   242 goal thy "!!evs. evs : traces ==> ALL A X. Says A A X ~: set_of_list evs";
   243 be traces.induct 1;
   244 by (Auto_tac());
   245 qed_spec_mp "not_Says_to_self";
   246 Addsimps [not_Says_to_self];
   247 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
   248 
   249 goal thy "!!evs. evs : traces ==> Notes A X ~: set_of_list evs";
   250 be traces.induct 1;
   251 by (Auto_tac());
   252 qed "not_Notes";
   253 Addsimps [not_Notes];
   254 AddSEs   [not_Notes RSN (2, rev_notE)];
   255 
   256 
   257 goal thy "!!evs. (Says S A (Crypt {|N, B, K, X|} KA)) : set_of_list evs ==> \
   258 \                X : parts (sees Enemy evs)";
   259 by (fast_tac (!claset addSEs partsEs
   260 	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
   261 qed "NS3_msg_in_parts_sees_Enemy";
   262 			      
   263 
   264 (*** Server keys are not betrayed ***)
   265 
   266 (*Enemy never sees another agent's server key!*)
   267 goal thy 
   268  "!!evs. [| evs : traces; A ~= Enemy |] ==> \
   269 \        Key (serverKey A) ~: parts (sees Enemy evs)";
   270 be traces.induct 1;
   271 bd NS3_msg_in_parts_sees_Enemy 5;
   272 by (Auto_tac());
   273 (*Deals with Fake message*)
   274 by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   275 			     impOfSubs synth_analz_parts_insert_subset_Un]) 1);
   276 qed "Enemy_not_see_serverKey";
   277 
   278 bind_thm ("Enemy_not_analz_serverKey",
   279 	  [analz_subset_parts, Enemy_not_see_serverKey] MRS contra_subsetD);
   280 
   281 Addsimps [Enemy_not_see_serverKey, 
   282 	  not_sym RSN (2, Enemy_not_see_serverKey), 
   283 	  Enemy_not_analz_serverKey, 
   284 	  not_sym RSN (2, Enemy_not_analz_serverKey)];
   285 
   286 (*We go to some trouble to preserve R in the 3rd subgoal*)
   287 val major::prems = 
   288 goal thy  "[| Key (serverKey A) : parts (sees Enemy evs);    \
   289 \             evs : traces;                                  \
   290 \             A=Enemy ==> R                                  \
   291 \           |] ==> R";
   292 br ccontr 1;
   293 br ([major, Enemy_not_see_serverKey] MRS rev_notE) 1;
   294 by (swap_res_tac prems 2);
   295 by (ALLGOALS (fast_tac (!claset addIs prems)));
   296 qed "Enemy_see_serverKey_E";
   297 
   298 bind_thm ("Enemy_analz_serverKey_E", 
   299 	  analz_subset_parts RS subsetD RS Enemy_see_serverKey_E);
   300 
   301 (*Classical reasoner doesn't need the not_sym versions (with swapped ~=) *)
   302 AddSEs [Enemy_see_serverKey_E, Enemy_analz_serverKey_E];
   303 
   304 
   305 (*No Friend will ever see another agent's server key 
   306   (excluding the Enemy, who might transmit his).
   307   The Server, of course, knows all server keys.*)
   308 goal thy 
   309  "!!evs. [| evs : traces; A ~= Enemy;  A ~= Friend j |] ==> \
   310 \        Key (serverKey A) ~: parts (sees (Friend j) evs)";
   311 br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1;
   312 by (ALLGOALS Asm_simp_tac);
   313 qed "Friend_not_see_serverKey";
   314 
   315 
   316 (*Not for Addsimps -- it can cause goals to blow up!*)
   317 goal thy  
   318  "!!evs. evs : traces ==>                                  \
   319 \        (Key (serverKey A) \
   320 \           : analz (insert (Key (serverKey B)) (sees Enemy evs))) =  \
   321 \        (A=B | A=Enemy)";
   322 by (best_tac (!claset addDs [impOfSubs analz_subset_parts]
   323 		      addIs [impOfSubs (subset_insertI RS analz_mono)]
   324 	              addss (!simpset)) 1);
   325 qed "serverKey_mem_analz";
   326 
   327 
   328 
   329 
   330 (*** Future keys can't be seen or used! ***)
   331 
   332 (*Nobody can have SEEN keys that will be generated in the future.
   333   This has to be proved anew for each protocol description,
   334   but should go by similar reasoning every time.  Hardest case is the
   335   standard Fake rule.  
   336       The length comparison, and Union over C, are essential for the 
   337   induction! *)
   338 goal thy "!!evs. evs : traces ==> \
   339 \                length evs <= length evs' --> \
   340 \                          Key (newK evs') ~: (UN C. parts (sees C evs))";
   341 be traces.induct 1;
   342 bd NS3_msg_in_parts_sees_Enemy 5;
   343 (*auto_tac does not work here, as it performs safe_tac first*)
   344 by (ALLGOALS Asm_simp_tac);
   345 by (ALLGOALS (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   346 				       impOfSubs parts_insert_subset_Un,
   347 				       Suc_leD]
   348 			        addss (!simpset))));
   349 val lemma = result();
   350 
   351 (*Variant needed for the main theorem below*)
   352 goal thy 
   353  "!!evs. [| evs : traces;  length evs <= length evs' |] ==> \
   354 \        Key (newK evs') ~: parts (sees C evs)";
   355 by (fast_tac (!claset addDs [lemma]) 1);
   356 qed "new_keys_not_seen";
   357 Addsimps [new_keys_not_seen];
   358 
   359 (*Another variant: old messages must contain old keys!*)
   360 goal thy 
   361  "!!evs. [| Says A B X : set_of_list evs;  \
   362 \           Key (newK evt) : parts {X};    \
   363 \           evs : traces                 \
   364 \        |] ==> length evt < length evs";
   365 br ccontr 1;
   366 by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy]
   367 	              addIs [impOfSubs parts_mono, leI]) 1);
   368 qed "Says_imp_old_keys";
   369 
   370 
   371 goal thy "!!K. newK evs = invKey K ==> newK evs = K";
   372 br (invKey_eq RS iffD1) 1;
   373 by (Simp_tac 1);
   374 val newK_invKey = result();
   375 
   376 
   377 val keysFor_parts_mono = parts_mono RS keysFor_mono;
   378 
   379 (*Nobody can have USED keys that will be generated in the future.
   380   ...very like new_keys_not_seen*)
   381 goal thy "!!evs. evs : traces ==> \
   382 \                length evs <= length evs' --> \
   383 \                newK evs' ~: keysFor (UN C. parts (sees C evs))";
   384 be traces.induct 1;
   385 bd NS3_msg_in_parts_sees_Enemy 5;
   386 by (ALLGOALS Asm_simp_tac);
   387 (*NS1 and NS2*)
   388 map (by o fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [3,2];
   389 (*Fake and NS3*)
   390 map (by o best_tac
   391      (!claset addSDs [newK_invKey]
   392 	      addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   393 		     impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   394 		     Suc_leD]
   395 	      addEs [new_keys_not_seen RS not_parts_not_analz RSN (2,rev_notE)]
   396 	      addss (!simpset)))
   397     [2,1];
   398 (*NS4 and NS5: nonce exchange*)
   399 by (ALLGOALS (deepen_tac (!claset addSDs [newK_invKey, Says_imp_old_keys]
   400 	                          addIs  [less_SucI, impOfSubs keysFor_mono]
   401 		                  addss (!simpset addsimps [le_def])) 0));
   402 val lemma = result();
   403 
   404 goal thy 
   405  "!!evs. [| evs : traces;  length evs <= length evs' |] ==> \
   406 \        newK evs' ~: keysFor (parts (sees C evs))";
   407 by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
   408 qed "new_keys_not_used";
   409 
   410 bind_thm ("new_keys_not_analzd",
   411 	  [analz_subset_parts RS keysFor_mono,
   412 	   new_keys_not_used] MRS contra_subsetD);
   413 
   414 Addsimps [new_keys_not_used, new_keys_not_analzd];
   415 
   416 
   417 (** Rewrites to push in Key and Crypt messages, so that other messages can
   418     be pulled out using the analz_insert rules **)
   419 
   420 fun insComm x y = read_instantiate_sg (sign_of thy) [("x",x), ("y",y)] 
   421                       insert_commute;
   422 
   423 val pushKeys = map (insComm "Key ?K") 
   424                   ["Agent ?C", "Nonce ?N", "MPair ?X ?Y", "Crypt ?X ?K'"];
   425 
   426 val pushCrypts = map (insComm "Crypt ?X ?K") 
   427                     ["Agent ?C", "Nonce ?N", "MPair ?X' ?Y"];
   428 
   429 (*Cannot be added with Addsimps -- we don't always want to re-order messages*)
   430 val pushes = pushKeys@pushCrypts;
   431 
   432 val pushKey_newK = insComm "Key (newK ?evs)"  "Key (serverKey ?C)";
   433 
   434 
   435 (** Lemmas concerning the form of items passed in messages **)
   436 
   437 (*Describes the form *and age* of K, and the form of X,
   438   when the following message is sent*)
   439 goal thy 
   440  "!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') : set_of_list evs; \
   441 \           evs : traces    \
   442 \        |] ==> (EX evt:traces. \
   443 \                         K = Key(newK evt) & \
   444 \                         X = (Crypt {|K, Agent A|} (serverKey B)) & \
   445 \                         K' = serverKey A & \
   446 \                         length evt < length evs)";
   447 be rev_mp 1;
   448 be traces.induct 1;
   449 by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
   450 qed "Says_Server_message_form";
   451 
   452 (* c ~: keysFor (parts H) ==> c ~: keysFor (analz H) *)
   453 bind_thm ("not_parts_not_keysFor_analz", 
   454 	  analz_subset_parts RS keysFor_mono RS contra_subsetD);
   455 
   456 
   457 
   458 (*USELESS for NS3, case 1, as the ind hyp says the same thing!
   459 goal thy 
   460  "!!evs. [| evs = Says Server (Friend i) \
   461 \                 (Crypt {|N, Agent(Friend j), K, X|} K') # evs';  \
   462 \           evs : traces;  i~=k                                    \
   463 \        |] ==>                                                    \
   464 \     K ~: analz (insert (Key (serverKey (Friend k))) (sees Enemy evs))";
   465 be rev_mp 1;
   466 be traces.induct 1;
   467 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes)));
   468 by (Step_tac 1);
   469 by (asm_full_simp_tac (!simpset addsimps[analz_subset_parts RS contra_subsetD]) 1);
   470 val Enemy_not_see_encrypted_key_lemma = result();
   471 *)
   472 
   473 
   474 (*Describes the form of X when the following message is sent*)
   475 goal thy
   476  "!!evs. evs : traces ==>                             \
   477 \        ALL A NA B K X.                            \
   478 \            (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
   479 \            : parts (sees Enemy evs) & A ~= Enemy  -->   \
   480 \          (EX evt:traces. K = newK evt & \
   481 \                          X = (Crypt {|Key K, Agent A|} (serverKey B)))";
   482 be traces.induct 1;
   483 bd NS3_msg_in_parts_sees_Enemy 5;
   484 by (Step_tac 1);
   485 by (ALLGOALS Asm_full_simp_tac);
   486 (*Remaining cases are Fake and NS2*)
   487 by (fast_tac (!claset addSDs [spec]) 2);
   488 (*Now for the Fake case*)
   489 by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   490 			     impOfSubs synth_analz_parts_insert_subset_Un]
   491 	              addss (!simpset)) 1);
   492 qed_spec_mp "encrypted_form";
   493 
   494 
   495 (*For eliminating the A ~= Enemy condition from the previous result*)
   496 goal thy 
   497  "!!evs. evs : traces ==>                             \
   498 \        ALL S A NA B K X.                            \
   499 \            Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
   500 \            : set_of_list evs  -->   \
   501 \        S = Server | S = Enemy";
   502 be traces.induct 1;
   503 by (ALLGOALS Asm_simp_tac);
   504 (*We are left with NS3*)
   505 by (subgoal_tac "S = Server | S = Enemy" 1);
   506 (*First justify this assumption!*)
   507 by (fast_tac (!claset addSEs [allE, mp] addss (!simpset)) 2);
   508 by (Step_tac 1);
   509 bd Says_Server_message_form 1;
   510 by (ALLGOALS Full_simp_tac);
   511 (*Final case.  Clear out needless quantifiers to speed the following step*)
   512 by (eres_inst_tac [("V","ALL x. ?P(x)")] thin_rl 1);
   513 bd encrypted_form 1;
   514 br (parts.Inj RS conjI) 1;
   515 auto();
   516 qed_spec_mp "Server_or_Enemy";
   517 
   518 
   519 (*Describes the form of X when the following message is sent;
   520   use Says_Server_message_form if applicable*)
   521 goal thy 
   522  "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
   523 \            : set_of_list evs;                              \
   524 \           evs : traces               \
   525 \        |] ==> (EX evt:traces. K = newK evt & length evt < length evs & \
   526 \                               X = (Crypt {|Key K, Agent A|} (serverKey B)))";
   527 by (forward_tac [Server_or_Enemy] 1);
   528 ba 1;
   529 by (Step_tac 1);
   530 by (fast_tac (!claset addSDs [Says_Server_message_form] addss (!simpset)) 1);
   531 by (forward_tac [encrypted_form] 1);
   532 br (parts.Inj RS conjI) 1;
   533 by (auto_tac (!claset addIs [Says_imp_old_keys], !simpset));
   534 qed "Says_S_message_form";
   535 
   536 (*Currently unused.  Needed only to reason about the VERY LAST message.*)
   537 goal thy 
   538  "!!evs. [| evs = Says S A (Crypt {|Nonce NA, Agent B, Key K, X|}   \
   539 \                           (serverKey A)) # evs';                  \
   540 \           evs : traces                                           \
   541 \        |] ==> (EX evt:traces. evs' : traces & length evt < length evs & \
   542 \                               K = newK evt & \
   543 \                               X = (Crypt {|Key K, Agent A|} (serverKey B)))";
   544 by (forward_tac [traces_eq_ConsE] 1);
   545 by (dtac (set_of_list_eqI1 RS Says_S_message_form) 2);
   546 by (Auto_tac());	
   547 qed "Says_S_message_form_eq";
   548 
   549 
   550 
   551 (****
   552  The following is to prove theorems of the form
   553 
   554           Key K : analz (insert (Key (newK evt)) 
   555 	                   (insert (Key (serverKey C)) (sees Enemy evs))) ==>
   556           Key K : analz (insert (Key (serverKey C)) (sees Enemy evs))
   557 
   558  A more general formula must be proved inductively.
   559 
   560 ****)
   561 
   562 
   563 (*NOT useful in this form, but it says that session keys are not used
   564   to encrypt messages containing other keys, in the actual protocol.
   565   We require that agents should behave like this subsequently also.*)
   566 goal thy 
   567  "!!evs. evs : traces ==> \
   568 \        (Crypt X (newK evt)) : parts (sees Enemy evs) & \
   569 \        Key K : parts {X} --> Key K : parts (sees Enemy evs)";
   570 be traces.induct 1;
   571 bd NS3_msg_in_parts_sees_Enemy 5;
   572 by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
   573 (*Deals with Faked messages*)
   574 by (best_tac (!claset addSEs partsEs
   575 		      addDs [impOfSubs analz_subset_parts,
   576                              impOfSubs parts_insert_subset_Un]
   577                       addss (!simpset)) 1);
   578 (*NS4 and NS5*)
   579 by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   580 result();
   581 
   582 
   583 (** Specialized rewriting for this proof **)
   584 
   585 Delsimps [image_insert];
   586 Addsimps [image_insert RS sym];
   587 
   588 goal thy "insert (Key (newK x)) (sees A evs) = \
   589 \         Key `` (newK``{x}) Un (sees A evs)";
   590 by (Fast_tac 1);
   591 val insert_Key_singleton = result();
   592 
   593 goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
   594 \         Key `` (f `` (insert x E)) Un C";
   595 by (Fast_tac 1);
   596 val insert_Key_image = result();
   597 
   598 
   599 (** Session keys are not used to encrypt other session keys **)
   600 
   601 goal thy  
   602  "!!evs. evs : traces ==> \
   603 \  ALL K E. (Key K : analz (insert (Key (serverKey C)) \
   604 \                             (Key``(newK``E) Un (sees Enemy evs)))) = \
   605 \           (K : newK``E |  \
   606 \            Key K : analz (insert (Key (serverKey C)) \
   607 \                             (sees Enemy evs)))";
   608 be traces.induct 1;
   609 by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);	
   610 by (REPEAT ((eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac) 5));
   611 by (ALLGOALS 
   612     (asm_simp_tac 
   613      (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   614 			 @ pushes)
   615                setloop split_tac [expand_if])));
   616 (*Cases NS2 and NS3!!  Simple, thanks to auto case splits*)
   617 by (REPEAT (Fast_tac 3));
   618 (*Base case*)
   619 by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   620 (** LEVEL 7 **)
   621 (*Fake case*)
   622 by (REPEAT (Safe_step_tac 1));
   623 by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 2);
   624 by (subgoal_tac 
   625     "Key K : analz \
   626 \             (synth \
   627 \              (analz (insert (Key (serverKey C)) \
   628 \                        (Key``(newK``E) Un (sees Enemy evsa)))))" 1);
   629 (*First, justify this subgoal*)
   630 (*Discard formulae for better speed*)
   631 by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
   632 by (eres_inst_tac [("V","?Q ~: ?QQ")] thin_rl 2);
   633 by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)]
   634                       addSEs [impOfSubs analz_mono]) 2);
   635 by (Asm_full_simp_tac 1);
   636 by (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1);
   637 qed_spec_mp "analz_image_newK";
   638 
   639 
   640 goal thy  
   641  "!!evs. evs : traces ==>                                  \
   642 \        Key K : analz (insert (Key (newK evt))            \
   643 \                         (insert (Key (serverKey C))      \
   644 \                          (sees Enemy evs))) =            \
   645 \             (K = newK evt |                              \
   646 \              Key K : analz (insert (Key (serverKey C))   \
   647 \                               (sees Enemy evs)))";
   648 by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   649 				   insert_Key_singleton]) 1);
   650 by (Fast_tac 1);
   651 qed "analz_insert_Key_newK";
   652 
   653 
   654 
   655 (*This says that the Key, K, uniquely identifies the message.
   656     But if C=Enemy then he could send all sorts of nonsense.*)
   657 goal thy 
   658  "!!evs. evs : traces ==>                      \
   659 \      EX X'. ALL C S A Y N B X.               \
   660 \         C ~= Enemy -->                       \
   661 \         Says S A Y : set_of_list evs -->     \
   662 \         ((Crypt {|N, Agent B, Key K, X|} (serverKey C)) : parts{Y} --> \
   663 \       (X = X'))";
   664 be traces.induct 1;
   665 by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);	
   666 by (ALLGOALS 
   667     (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib])));
   668 (*NS2: Case split propagates some context to other subgoal...*)
   669 by (excluded_middle_tac "K = newK evsa" 2);
   670 by (Asm_simp_tac 2);
   671 (*...we assume X is a very new message, and handle this case by contradiction*)
   672 by (fast_tac (!claset addIs [impOfSubs (subset_insertI RS parts_mono)]
   673 		      addSEs partsEs
   674 		      addEs [Says_imp_old_keys RS less_irrefl]
   675 	              addss (!simpset)) 2);
   676 (*NS3: No relevant messages*)
   677 by (fast_tac (!claset addSEs [exI] addss (!simpset)) 2);
   678 (*Fake*)
   679 by (Step_tac 1);
   680 br exI 1;
   681 br conjI 1;
   682 ba 2;
   683 by (Step_tac 1);
   684 (** LEVEL 12 **)
   685 by (subgoal_tac "Crypt {|N, Agent Ba, Key K, Xa|} (serverKey C) \
   686 \                  : parts (sees Enemy evsa)" 1);
   687 by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
   688 by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
   689 	              addDs [impOfSubs parts_insert_subset_Un]
   690                       addss (!simpset)) 2);
   691 by (eres_inst_tac [("V","?aa : parts {X}")] thin_rl 1);
   692 bd parts_singleton 1;
   693 by (Step_tac 1);
   694 bd seesD 1;
   695 by (Step_tac 1);
   696 by (Full_simp_tac 2);
   697 by (fast_tac (!claset addSDs [spec]) 1);
   698 val lemma = result();
   699 
   700 
   701 (*In messages of this form, the session key uniquely identifies the rest*)
   702 goal thy 
   703  "!!evs. [| Says S A          \
   704 \             (Crypt {|N, Agent B, Key K, X|} (serverKey C))     \
   705 \                  : set_of_list evs; \
   706  \          Says S' A'                                         \
   707 \             (Crypt {|N', Agent B', Key K, X'|} (serverKey C')) \
   708 \                  : set_of_list evs;                         \
   709 \           evs : traces;  C ~= Enemy;  C' ~= Enemy    |] ==> X = X'";
   710 bd lemma 1;
   711 be exE 1;
   712 by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   713 by (Fast_tac 1);
   714 qed "unique_session_keys";
   715 
   716 
   717 
   718 (*Crucial security property: Enemy does not see the keys sent in msg NS2
   719    -- even if another key is compromised*)
   720 goal thy 
   721  "!!evs. [| Says Server (Friend i) \
   722 \            (Crypt {|N, Agent(Friend j), K, X|} K') : set_of_list evs;  \
   723 \           evs : traces;  Friend i ~= C;  Friend j ~= C              \
   724 \        |] ==>                                                       \
   725 \     K ~: analz (insert (Key (serverKey C)) (sees Enemy evs))";
   726 be rev_mp 1;
   727 be traces.induct 1;
   728 by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
   729 (*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
   730 by (REPEAT_FIRST (resolve_tac [conjI, impI]));
   731 by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac));
   732 by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac));
   733 by (ALLGOALS 
   734     (asm_full_simp_tac 
   735      (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   736 			  analz_insert_Key_newK] @ pushes)
   737                setloop split_tac [expand_if])));
   738 (*NS2*)
   739 by (fast_tac (!claset addSEs [less_irrefl]) 2);
   740 (** LEVEL 8 **)
   741 (*Now for the Fake case*)
   742 br notI 1;
   743 by (subgoal_tac 
   744     "Key (newK evt) : \
   745 \    analz (synth (analz (insert (Key (serverKey C)) \
   746 \                                  (sees Enemy evsa))))" 1);
   747 be (impOfSubs analz_mono) 2;
   748 by (deepen_tac (!claset addIs [analz_mono RS synth_mono RSN (2,rev_subsetD),
   749 			       impOfSubs synth_increasing,
   750 			       impOfSubs analz_increasing]) 0 2);
   751 (*Proves the Fake goal*)
   752 by (fast_tac (!claset addss (!simpset)) 1);
   753 
   754 (**LEVEL 13**)
   755 (*NS3: that message from the Server was sent earlier*)
   756 by (mp_tac 1);
   757 by (forward_tac [Says_S_message_form] 1 THEN assume_tac 1);
   758 by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac));
   759 by (asm_full_simp_tac
   760     (!simpset addsimps (mem_if::analz_insert_Key_newK::pushes)) 1);
   761 by (Step_tac 1);
   762 (**LEVEL 18 **)
   763 bd unique_session_keys 1;
   764 by (REPEAT_FIRST assume_tac);
   765 by (ALLGOALS Full_simp_tac);
   766 by (Step_tac 1);
   767 by (asm_full_simp_tac (!simpset addsimps [serverKey_mem_analz]) 1);
   768 qed "Enemy_not_see_encrypted_key";
   769 
   770 
   771 
   772 
   773 XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX;
   774 
   775 
   776 goals_limit:=4;
   777 
   778 
   779 
   780 goal thy 
   781  "!!evs. [| Says Server (Friend i) \
   782 \             (Crypt {|N, Agent B, K|} K') : set_of_list evs;  \
   783 \           evs : traces;  i~=j    \
   784 \         |] ==> K ~: analz (sees (Friend j) evs)";
   785 br (sees_agent_subset_sees_Enemy RS analz_mono RS contra_subsetD) 1;
   786 by (ALLGOALS (asm_simp_tac (!simpset addsimps [Enemy_not_see_encrypted_key])));
   787 qed "Friend_not_see_encrypted_key";
   788 
   789 goal thy 
   790  "!!evs. [| Says Server (Friend i) \
   791 \             (Crypt {|N, Agent B, K|} K') : set_of_list evs;  \
   792 \           A ~: {Friend i, Server};  \
   793 \           evs : traces    \
   794 \        |] ==>  K ~: analz (sees A evs)";
   795 by (eres_inst_tac [("P", "A~:?X")] rev_mp 1);
   796 by (agent.induct_tac "A" 1);
   797 by (ALLGOALS Simp_tac);
   798 by (asm_simp_tac (!simpset addsimps [eq_sym_conv, 
   799 				     Friend_not_see_encrypted_key]) 1);
   800 br ([analz_mono, Enemy_not_see_encrypted_key] MRS contra_subsetD) 1;
   801 (*  hyp_subst_tac would deletes the equality assumption... *)
   802 by (ALLGOALS (rtac n_not_Suc_n ORELSE' Fast_tac));
   803 qed "Agent_not_see_encrypted_key";
   804 
   805 
   806 (*Neatly packaged, perhaps in a useless form*)
   807 goalw thy [knownBy_def]
   808  "!!evs. [| Says Server (Friend i) \
   809 \             (Crypt {|N, Agent B, K|} K') : set_of_list evs;  \
   810 \           evs : traces    \
   811 \        |] ==>  knownBy evs K <= {Friend i, Server}";
   812 
   813 by (Step_tac 1);
   814 br ccontr 1;
   815 by (fast_tac (!claset addDs [Agent_not_see_encrypted_key]) 1);
   816 qed "knownBy_encrypted_key";
   817 
   818 
   819 
   820 
   821 
   822 
   823 
   824 push_proof();
   825 goal thy 
   826  "!!evs. [| evs = Says S (Friend i) \
   827 \                 (Crypt {|N, Agent(Friend j), K, X|} K') # evs';  \
   828 \           evs : traces;  i~=k                                    \
   829 \        |] ==>                                                    \
   830 \     K ~: analz (insert (Key (serverKey (Friend k))) (sees Enemy evs))";
   831 be rev_mp 1;
   832 be traces.induct 1;
   833 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes)));
   834 by (Step_tac 1);
   835 by (asm_full_simp_tac (!simpset addsimps[analz_subset_parts RS contra_subsetD]) 1);
   836 val Enemy_not_see_encrypted_key_lemma = result();
   837 
   838 
   839 
   840 
   841 
   842 
   843 
   844 (*Precisely formulated as needed below.  Perhaps redundant, as simplification
   845   with the aid of  analz_subset_parts RS contra_subsetD  might do the
   846   same thing.*)
   847 goal thy 
   848  "!!evs. [| evs : traces; A ~= Enemy;  A ~= Friend j |] ==> \
   849 \        Key (serverKey A) ~:                               \
   850 \          analz (insert (Key (serverKey (Friend j))) (sees Enemy evs))";
   851 br (analz_subset_parts RS contra_subsetD) 1;
   852 by (Asm_simp_tac 1);
   853 qed "insert_not_analz_serverKey";
   854 
   855 
   856 
   857 
   858 XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX;
   859 proof_timing:=true;
   860 
   861 
   862 
   863 YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY;
   864 
   865 
   866 
   867 (*If a message is sent, encrypted with a Friend's server key, then either
   868   that Friend or the Server originally sent it.*)
   869 goal thy 
   870  "!!evs. evs : traces ==>                             \
   871 \    ALL A B X i. Says A B (Crypt X (serverKey (Friend i))) \
   872 \        : set_of_list evs  -->   \
   873 \    (EX B'. Says Server B' (Crypt X (serverKey (Friend i))) : set_of_list evs | \
   874 \            Says (Friend i) B' (Crypt X (serverKey (Friend i))) : set_of_list evs)";
   875 be traces.induct 1;
   876 by (Step_tac 1);
   877 by (ALLGOALS Asm_full_simp_tac);
   878 (*Remaining cases are Fake, NS2 and NS3*)
   879 by (Fast_tac 2);	(*Proves the NS2 case*)
   880 
   881 by (REPEAT (dtac spec 2));
   882 fe conjE;
   883 bd mp 2;
   884 
   885 by (REPEAT (resolve_tac [refl, conjI] 2));
   886 by (ALLGOALS Asm_full_simp_tac);
   887 
   888 
   889 
   890 
   891 by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
   892 be conjE 2;
   893 by ((dtac spec THEN' dtac spec THEN' dtac spec THEN' dtac spec)2);
   894 
   895 (*The NS3 case needs the induction hypothesis twice!
   896     One application is to the X component of the most recent message.*)
   897 by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent A|} (serverKey B)" 2);
   898 by (Fast_tac 3);
   899 by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
   900 be conjE 2;
   901 (*DELETE the first quantified formula: it's now useless*)
   902 by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
   903 by (fast_tac (!claset addss (!simpset)) 2);
   904 (*Now for the Fake case*)
   905 be disjE 1;
   906 (*The subcase of Fake, where the message in question is NOT the most recent*)
   907 by (Best_tac 2);
   908 
   909 by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac));
   910 be Crypt_synth 1;
   911 be Key_synth 2;
   912 
   913 (*Split up the possibilities of that message being synthd...*)
   914 by (Step_tac 1);
   915 by (Best_tac 6);
   916 
   917 
   918 
   919 
   920 
   921 (*NEEDED??*)
   922 
   923 goal thy "!!A. X ~= Y ==> (X : sees A (Says B C Y # evs)) = (X : sees A evs)";
   924 by (asm_simp_tac (!simpset addsimps [sees_Cons] 
   925                            setloop split_tac [expand_if]) 1); 
   926 qed "in_sees_Says";
   927 
   928 goal thy "!!A. X ~: parts {Y} ==> \
   929 \              (X : parts (sees A (Says B C Y # evs))) = \
   930 \              (X : parts (sees A evs))";
   931 by (asm_simp_tac (!simpset addsimps [sees_Cons] 
   932                            setloop split_tac [expand_if]) 1); 
   933 by (asm_simp_tac (!simpset addsimps [parts_Un]) 1); 
   934 qed "in_parts_sees_Says";
   935 
   936 goal thy "!!evs. length evs < length evs' ==> newK  evs ~= newK (A',evs')";
   937 by (fast_tac (!claset addSEs [less_irrefl]) 1);
   938 qed "length_less_newK_neq";
   939 
   940 
   941 
   942 
   943 
   944 
   945 YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY;
   946 
   947 goalw thy [keysFor_def]
   948     "!!X. Crypt X K: H ==> invKey K : keysFor H";
   949 by (Fast_tac 1);
   950 qed "keysFor_I";
   951 AddSIs [keysFor_I];
   952 
   953 goalw thy [keysFor_def]
   954     "!!K. K : keysFor H ==> EX X K'. K=invKey K' & Crypt X K': H";
   955 by (Fast_tac 1);
   956 qed "keysFor_D";
   957 AddSDs [keysFor_D];
   958 
   959