src/HOL/Auth/Message.ML
author paulson
Mon Dec 16 10:41:26 1996 +0100 (1996-12-16)
changeset 2415 46de4b035f00
parent 2373 490ffa16952e
child 2484 596a5b5a68ff
permissions -rw-r--r--
New tactic: prove_unique_tac
     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 Datatypes of agents and messages;
     7 Inductive relations "parts", "analz" and "synth"
     8 *)
     9 
    10 val prems = goal HOL.thy "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)";
    11 by (case_tac "P" 1);
    12 by (ALLGOALS (asm_simp_tac (!simpset addsimps prems)));
    13 val expand_case = result();
    14 
    15 fun expand_case_tac P i =
    16     res_inst_tac [("P",P)] expand_case i THEN
    17     Simp_tac (i+1) THEN 
    18     Simp_tac i;
    19 
    20 
    21 
    22 (*GOALS.ML??*)
    23 fun prlim n = (goals_limit:=n; pr());
    24 
    25 (*FUN.ML??  WE NEED A NOTION OF INVERSE IMAGE, OR GRAPH!!*)
    26 goal Set.thy "!!f. B <= range f = (B = f`` {x. f x: B})";
    27 by (fast_tac (!claset addEs [equalityE]) 1);
    28 val subset_range_iff = result();
    29 
    30 
    31 open Message;
    32 
    33 AddIffs (msg.inject);
    34 
    35 (** Inverse of keys **)
    36 
    37 goal thy "!!K K'. (invKey K = invKey K') = (K=K')";
    38 by (Step_tac 1);
    39 by (rtac box_equals 1);
    40 by (REPEAT (rtac invKey 2));
    41 by (Asm_simp_tac 1);
    42 qed "invKey_eq";
    43 
    44 Addsimps [invKey, invKey_eq];
    45 
    46 
    47 (**** keysFor operator ****)
    48 
    49 goalw thy [keysFor_def] "keysFor {} = {}";
    50 by (Fast_tac 1);
    51 qed "keysFor_empty";
    52 
    53 goalw thy [keysFor_def] "keysFor (H Un H') = keysFor H Un keysFor H'";
    54 by (Fast_tac 1);
    55 qed "keysFor_Un";
    56 
    57 goalw thy [keysFor_def] "keysFor (UN i. H i) = (UN i. keysFor (H i))";
    58 by (Fast_tac 1);
    59 qed "keysFor_UN";
    60 
    61 (*Monotonicity*)
    62 goalw thy [keysFor_def] "!!G H. G<=H ==> keysFor(G) <= keysFor(H)";
    63 by (Fast_tac 1);
    64 qed "keysFor_mono";
    65 
    66 goalw thy [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H";
    67 by (fast_tac (!claset addss (!simpset)) 1);
    68 qed "keysFor_insert_Agent";
    69 
    70 goalw thy [keysFor_def] "keysFor (insert (Nonce N) H) = keysFor H";
    71 by (fast_tac (!claset addss (!simpset)) 1);
    72 qed "keysFor_insert_Nonce";
    73 
    74 goalw thy [keysFor_def] "keysFor (insert (Key K) H) = keysFor H";
    75 by (fast_tac (!claset addss (!simpset)) 1);
    76 qed "keysFor_insert_Key";
    77 
    78 goalw thy [keysFor_def] "keysFor (insert (Hash X) H) = keysFor H";
    79 by (fast_tac (!claset addss (!simpset)) 1);
    80 qed "keysFor_insert_Hash";
    81 
    82 goalw thy [keysFor_def] "keysFor (insert {|X,Y|} H) = keysFor H";
    83 by (fast_tac (!claset addss (!simpset)) 1);
    84 qed "keysFor_insert_MPair";
    85 
    86 goalw thy [keysFor_def]
    87     "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)";
    88 by (Auto_tac());
    89 qed "keysFor_insert_Crypt";
    90 
    91 Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, 
    92           keysFor_insert_Agent, keysFor_insert_Nonce, keysFor_insert_Key, 
    93 	  keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt];
    94 
    95 goalw thy [keysFor_def] "!!H. Crypt K X : H ==> invKey K : keysFor H";
    96 by (Fast_tac 1);
    97 qed "Crypt_imp_invKey_keysFor";
    98 
    99 
   100 (**** Inductive relation "parts" ****)
   101 
   102 val major::prems = 
   103 goal thy "[| {|X,Y|} : parts H;       \
   104 \            [| X : parts H; Y : parts H |] ==> P  \
   105 \         |] ==> P";
   106 by (cut_facts_tac [major] 1);
   107 by (resolve_tac prems 1);
   108 by (REPEAT (eresolve_tac [asm_rl, parts.Fst, parts.Snd] 1));
   109 qed "MPair_parts";
   110 
   111 AddIs  [parts.Inj];
   112 
   113 val partsEs = [MPair_parts, make_elim parts.Body];
   114 
   115 AddSEs partsEs;
   116 (*NB These two rules are UNSAFE in the formal sense, as they discard the
   117      compound message.  They work well on THIS FILE, perhaps because its
   118      proofs concern only atomic messages.*)
   119 
   120 goal thy "H <= parts(H)";
   121 by (Fast_tac 1);
   122 qed "parts_increasing";
   123 
   124 (*Monotonicity*)
   125 goalw thy parts.defs "!!G H. G<=H ==> parts(G) <= parts(H)";
   126 by (rtac lfp_mono 1);
   127 by (REPEAT (ares_tac basic_monos 1));
   128 qed "parts_mono";
   129 
   130 val parts_insertI = impOfSubs (subset_insertI RS parts_mono);
   131 
   132 goal thy "parts{} = {}";
   133 by (Step_tac 1);
   134 by (etac parts.induct 1);
   135 by (ALLGOALS Fast_tac);
   136 qed "parts_empty";
   137 Addsimps [parts_empty];
   138 
   139 goal thy "!!X. X: parts{} ==> P";
   140 by (Asm_full_simp_tac 1);
   141 qed "parts_emptyE";
   142 AddSEs [parts_emptyE];
   143 
   144 (*WARNING: loops if H = {Y}, therefore must not be repeated!*)
   145 goal thy "!!H. X: parts H ==> EX Y:H. X: parts {Y}";
   146 by (etac parts.induct 1);
   147 by (ALLGOALS Fast_tac);
   148 qed "parts_singleton";
   149 
   150 
   151 (** Unions **)
   152 
   153 goal thy "parts(G) Un parts(H) <= parts(G Un H)";
   154 by (REPEAT (ares_tac [Un_least, parts_mono, Un_upper1, Un_upper2] 1));
   155 val parts_Un_subset1 = result();
   156 
   157 goal thy "parts(G Un H) <= parts(G) Un parts(H)";
   158 by (rtac subsetI 1);
   159 by (etac parts.induct 1);
   160 by (ALLGOALS Fast_tac);
   161 val parts_Un_subset2 = result();
   162 
   163 goal thy "parts(G Un H) = parts(G) Un parts(H)";
   164 by (REPEAT (ares_tac [equalityI, parts_Un_subset1, parts_Un_subset2] 1));
   165 qed "parts_Un";
   166 
   167 goal thy "parts (insert X H) = parts {X} Un parts H";
   168 by (stac (read_instantiate [("A","H")] insert_is_Un) 1);
   169 by (simp_tac (HOL_ss addsimps [parts_Un]) 1);
   170 qed "parts_insert";
   171 
   172 (*TWO inserts to avoid looping.  This rewrite is better than nothing.
   173   Not suitable for Addsimps: its behaviour can be strange.*)
   174 goal thy "parts (insert X (insert Y H)) = parts {X} Un parts {Y} Un parts H";
   175 by (simp_tac (!simpset addsimps [Un_assoc]) 1);
   176 by (simp_tac (!simpset addsimps [parts_insert RS sym]) 1);
   177 qed "parts_insert2";
   178 
   179 goal thy "(UN x:A. parts(H x)) <= parts(UN x:A. H x)";
   180 by (REPEAT (ares_tac [UN_least, parts_mono, UN_upper] 1));
   181 val parts_UN_subset1 = result();
   182 
   183 goal thy "parts(UN x:A. H x) <= (UN x:A. parts(H x))";
   184 by (rtac subsetI 1);
   185 by (etac parts.induct 1);
   186 by (ALLGOALS Fast_tac);
   187 val parts_UN_subset2 = result();
   188 
   189 goal thy "parts(UN x:A. H x) = (UN x:A. parts(H x))";
   190 by (REPEAT (ares_tac [equalityI, parts_UN_subset1, parts_UN_subset2] 1));
   191 qed "parts_UN";
   192 
   193 goal thy "parts(UN x. H x) = (UN x. parts(H x))";
   194 by (simp_tac (!simpset addsimps [UNION1_def, parts_UN]) 1);
   195 qed "parts_UN1";
   196 
   197 (*Added to simplify arguments to parts, analz and synth*)
   198 Addsimps [parts_Un, parts_UN, parts_UN1];
   199 
   200 goal thy "insert X (parts H) <= parts(insert X H)";
   201 by (fast_tac (!claset addEs [impOfSubs parts_mono]) 1);
   202 qed "parts_insert_subset";
   203 
   204 (** Idempotence and transitivity **)
   205 
   206 goal thy "!!H. X: parts (parts H) ==> X: parts H";
   207 by (etac parts.induct 1);
   208 by (ALLGOALS Fast_tac);
   209 qed "parts_partsE";
   210 AddSEs [parts_partsE];
   211 
   212 goal thy "parts (parts H) = parts H";
   213 by (Fast_tac 1);
   214 qed "parts_idem";
   215 Addsimps [parts_idem];
   216 
   217 goal thy "!!H. [| X: parts G;  G <= parts H |] ==> X: parts H";
   218 by (dtac parts_mono 1);
   219 by (Fast_tac 1);
   220 qed "parts_trans";
   221 
   222 (*Cut*)
   223 goal thy "!!H. [| Y: parts (insert X G);  X: parts H |] \
   224 \              ==> Y: parts (G Un H)";
   225 by (etac parts_trans 1);
   226 by (Auto_tac());
   227 qed "parts_cut";
   228 
   229 goal thy "!!H. X: parts H ==> parts (insert X H) = parts H";
   230 by (fast_tac (!claset addSDs [parts_cut]
   231                       addIs  [parts_insertI] 
   232                       addss (!simpset)) 1);
   233 qed "parts_cut_eq";
   234 
   235 Addsimps [parts_cut_eq];
   236 
   237 
   238 (** Rewrite rules for pulling out atomic messages **)
   239 
   240 fun parts_tac i =
   241   EVERY [rtac ([subsetI, parts_insert_subset] MRS equalityI) i,
   242 	 etac parts.induct i,
   243 	 REPEAT (fast_tac (!claset addss (!simpset)) i)];
   244 
   245 goal thy "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)";
   246 by (parts_tac 1);
   247 qed "parts_insert_Agent";
   248 
   249 goal thy "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)";
   250 by (parts_tac 1);
   251 qed "parts_insert_Nonce";
   252 
   253 goal thy "parts (insert (Key K) H) = insert (Key K) (parts H)";
   254 by (parts_tac 1);
   255 qed "parts_insert_Key";
   256 
   257 goal thy "parts (insert (Hash X) H) = insert (Hash X) (parts H)";
   258 by (parts_tac 1);
   259 qed "parts_insert_Hash";
   260 
   261 goal thy "parts (insert (Crypt K X) H) = \
   262 \         insert (Crypt K X) (parts (insert X H))";
   263 by (rtac equalityI 1);
   264 by (rtac subsetI 1);
   265 by (etac parts.induct 1);
   266 by (Auto_tac());
   267 by (etac parts.induct 1);
   268 by (ALLGOALS (best_tac (!claset addIs [parts.Body])));
   269 qed "parts_insert_Crypt";
   270 
   271 goal thy "parts (insert {|X,Y|} H) = \
   272 \         insert {|X,Y|} (parts (insert X (insert Y H)))";
   273 by (rtac equalityI 1);
   274 by (rtac subsetI 1);
   275 by (etac parts.induct 1);
   276 by (Auto_tac());
   277 by (etac parts.induct 1);
   278 by (ALLGOALS (best_tac (!claset addIs [parts.Fst, parts.Snd])));
   279 qed "parts_insert_MPair";
   280 
   281 Addsimps [parts_insert_Agent, parts_insert_Nonce, parts_insert_Key, 
   282           parts_insert_Hash, parts_insert_Crypt, parts_insert_MPair];
   283 
   284 
   285 goal thy "parts (Key``N) = Key``N";
   286 by (Auto_tac());
   287 by (etac parts.induct 1);
   288 by (Auto_tac());
   289 qed "parts_image_Key";
   290 
   291 Addsimps [parts_image_Key];
   292 
   293 
   294 (**** Inductive relation "analz" ****)
   295 
   296 val major::prems = 
   297 goal thy "[| {|X,Y|} : analz H;       \
   298 \            [| X : analz H; Y : analz H |] ==> P  \
   299 \         |] ==> P";
   300 by (cut_facts_tac [major] 1);
   301 by (resolve_tac prems 1);
   302 by (REPEAT (eresolve_tac [asm_rl, analz.Fst, analz.Snd] 1));
   303 qed "MPair_analz";
   304 
   305 AddIs  [analz.Inj];
   306 AddSEs [MPair_analz];      (*Perhaps it should NOT be deemed safe!*)
   307 AddDs  [analz.Decrypt];
   308 
   309 Addsimps [analz.Inj];
   310 
   311 goal thy "H <= analz(H)";
   312 by (Fast_tac 1);
   313 qed "analz_increasing";
   314 
   315 goal thy "analz H <= parts H";
   316 by (rtac subsetI 1);
   317 by (etac analz.induct 1);
   318 by (ALLGOALS Fast_tac);
   319 qed "analz_subset_parts";
   320 
   321 bind_thm ("not_parts_not_analz", analz_subset_parts RS contra_subsetD);
   322 
   323 
   324 goal thy "parts (analz H) = parts H";
   325 by (rtac equalityI 1);
   326 by (rtac (analz_subset_parts RS parts_mono RS subset_trans) 1);
   327 by (Simp_tac 1);
   328 by (fast_tac (!claset addDs [analz_increasing RS parts_mono RS subsetD]) 1);
   329 qed "parts_analz";
   330 Addsimps [parts_analz];
   331 
   332 goal thy "analz (parts H) = parts H";
   333 by (Auto_tac());
   334 by (etac analz.induct 1);
   335 by (Auto_tac());
   336 qed "analz_parts";
   337 Addsimps [analz_parts];
   338 
   339 (*Monotonicity; Lemma 1 of Lowe*)
   340 goalw thy analz.defs "!!G H. G<=H ==> analz(G) <= analz(H)";
   341 by (rtac lfp_mono 1);
   342 by (REPEAT (ares_tac basic_monos 1));
   343 qed "analz_mono";
   344 
   345 val analz_insertI = impOfSubs (subset_insertI RS analz_mono);
   346 
   347 (** General equational properties **)
   348 
   349 goal thy "analz{} = {}";
   350 by (Step_tac 1);
   351 by (etac analz.induct 1);
   352 by (ALLGOALS Fast_tac);
   353 qed "analz_empty";
   354 Addsimps [analz_empty];
   355 
   356 (*Converse fails: we can analz more from the union than from the 
   357   separate parts, as a key in one might decrypt a message in the other*)
   358 goal thy "analz(G) Un analz(H) <= analz(G Un H)";
   359 by (REPEAT (ares_tac [Un_least, analz_mono, Un_upper1, Un_upper2] 1));
   360 qed "analz_Un";
   361 
   362 goal thy "insert X (analz H) <= analz(insert X H)";
   363 by (fast_tac (!claset addEs [impOfSubs analz_mono]) 1);
   364 qed "analz_insert";
   365 
   366 (** Rewrite rules for pulling out atomic messages **)
   367 
   368 fun analz_tac i =
   369   EVERY [rtac ([subsetI, analz_insert] MRS equalityI) i,
   370 	 etac analz.induct i,
   371 	 REPEAT (fast_tac (!claset addss (!simpset)) i)];
   372 
   373 goal thy "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)";
   374 by (analz_tac 1);
   375 qed "analz_insert_Agent";
   376 
   377 goal thy "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)";
   378 by (analz_tac 1);
   379 qed "analz_insert_Nonce";
   380 
   381 goal thy "analz (insert (Hash X) H) = insert (Hash X) (analz H)";
   382 by (analz_tac 1);
   383 qed "analz_insert_Hash";
   384 
   385 (*Can only pull out Keys if they are not needed to decrypt the rest*)
   386 goalw thy [keysFor_def]
   387     "!!K. K ~: keysFor (analz H) ==>  \
   388 \         analz (insert (Key K) H) = insert (Key K) (analz H)";
   389 by (analz_tac 1);
   390 qed "analz_insert_Key";
   391 
   392 goal thy "analz (insert {|X,Y|} H) = \
   393 \         insert {|X,Y|} (analz (insert X (insert Y H)))";
   394 by (rtac equalityI 1);
   395 by (rtac subsetI 1);
   396 by (etac analz.induct 1);
   397 by (Auto_tac());
   398 by (etac analz.induct 1);
   399 by (ALLGOALS
   400     (deepen_tac (!claset addIs [analz.Fst, analz.Snd, analz.Decrypt]) 0));
   401 qed "analz_insert_MPair";
   402 
   403 (*Can pull out enCrypted message if the Key is not known*)
   404 goal thy "!!H. Key (invKey K) ~: analz H ==>  \
   405 \              analz (insert (Crypt K X) H) = \
   406 \              insert (Crypt K X) (analz H)";
   407 by (analz_tac 1);
   408 qed "analz_insert_Crypt";
   409 
   410 goal thy "!!H. Key (invKey K) : analz H ==>  \
   411 \              analz (insert (Crypt K X) H) <= \
   412 \              insert (Crypt K X) (analz (insert X H))";
   413 by (rtac subsetI 1);
   414 by (eres_inst_tac [("za","x")] analz.induct 1);
   415 by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   416 val lemma1 = result();
   417 
   418 goal thy "!!H. Key (invKey K) : analz H ==>  \
   419 \              insert (Crypt K X) (analz (insert X H)) <= \
   420 \              analz (insert (Crypt K X) H)";
   421 by (Auto_tac());
   422 by (eres_inst_tac [("za","x")] analz.induct 1);
   423 by (Auto_tac());
   424 by (best_tac (!claset addIs [subset_insertI RS analz_mono RS subsetD,
   425                              analz.Decrypt]) 1);
   426 val lemma2 = result();
   427 
   428 goal thy "!!H. Key (invKey K) : analz H ==>  \
   429 \              analz (insert (Crypt K X) H) = \
   430 \              insert (Crypt K X) (analz (insert X H))";
   431 by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1));
   432 qed "analz_insert_Decrypt";
   433 
   434 (*Case analysis: either the message is secure, or it is not!
   435   Effective, but can cause subgoals to blow up!
   436   Use with expand_if;  apparently split_tac does not cope with patterns
   437   such as "analz (insert (Crypt K X) H)" *)
   438 goal thy "analz (insert (Crypt K X) H) =                \
   439 \         (if (Key (invKey K) : analz H)                \
   440 \          then insert (Crypt K X) (analz (insert X H)) \
   441 \          else insert (Crypt K X) (analz H))";
   442 by (case_tac "Key (invKey K)  : analz H " 1);
   443 by (ALLGOALS (asm_simp_tac (!simpset addsimps [analz_insert_Crypt, 
   444                                                analz_insert_Decrypt])));
   445 qed "analz_Crypt_if";
   446 
   447 Addsimps [analz_insert_Agent, analz_insert_Nonce, analz_insert_Key, 
   448 	  analz_insert_Hash, analz_insert_MPair, analz_Crypt_if];
   449 
   450 (*This rule supposes "for the sake of argument" that we have the key.*)
   451 goal thy  "analz (insert (Crypt K X) H) <=  \
   452 \          insert (Crypt K X) (analz (insert X H))";
   453 by (rtac subsetI 1);
   454 by (etac analz.induct 1);
   455 by (Auto_tac());
   456 qed "analz_insert_Crypt_subset";
   457 
   458 
   459 goal thy "analz (Key``N) = Key``N";
   460 by (Auto_tac());
   461 by (etac analz.induct 1);
   462 by (Auto_tac());
   463 qed "analz_image_Key";
   464 
   465 Addsimps [analz_image_Key];
   466 
   467 
   468 (** Idempotence and transitivity **)
   469 
   470 goal thy "!!H. X: analz (analz H) ==> X: analz H";
   471 by (etac analz.induct 1);
   472 by (ALLGOALS Fast_tac);
   473 qed "analz_analzE";
   474 AddSEs [analz_analzE];
   475 
   476 goal thy "analz (analz H) = analz H";
   477 by (Fast_tac 1);
   478 qed "analz_idem";
   479 Addsimps [analz_idem];
   480 
   481 goal thy "!!H. [| X: analz G;  G <= analz H |] ==> X: analz H";
   482 by (dtac analz_mono 1);
   483 by (Fast_tac 1);
   484 qed "analz_trans";
   485 
   486 (*Cut; Lemma 2 of Lowe*)
   487 goal thy "!!H. [| Y: analz (insert X H);  X: analz H |] ==> Y: analz H";
   488 by (etac analz_trans 1);
   489 by (Fast_tac 1);
   490 qed "analz_cut";
   491 
   492 (*Cut can be proved easily by induction on
   493    "!!H. Y: analz (insert X H) ==> X: analz H --> Y: analz H"
   494 *)
   495 
   496 
   497 (** A congruence rule for "analz" **)
   498 
   499 goal thy "!!H. [| analz G <= analz G'; analz H <= analz H' \
   500 \              |] ==> analz (G Un H) <= analz (G' Un H')";
   501 by (Step_tac 1);
   502 by (etac analz.induct 1);
   503 by (ALLGOALS (best_tac (!claset addIs [analz_mono RS subsetD])));
   504 qed "analz_subset_cong";
   505 
   506 goal thy "!!H. [| analz G = analz G'; analz H = analz H' \
   507 \              |] ==> analz (G Un H) = analz (G' Un H')";
   508 by (REPEAT_FIRST (ares_tac [equalityI, analz_subset_cong]
   509           ORELSE' etac equalityE));
   510 qed "analz_cong";
   511 
   512 
   513 goal thy "!!H. analz H = analz H' ==> analz(insert X H) = analz(insert X H')";
   514 by (asm_simp_tac (!simpset addsimps [insert_def] 
   515                            setloop (rtac analz_cong)) 1);
   516 qed "analz_insert_cong";
   517 
   518 (*If there are no pairs or encryptions then analz does nothing*)
   519 goal thy "!!H. [| ALL X Y. {|X,Y|} ~: H;  ALL X K. Crypt K X ~: H |] ==> \
   520 \         analz H = H";
   521 by (Step_tac 1);
   522 by (etac analz.induct 1);
   523 by (ALLGOALS Fast_tac);
   524 qed "analz_trivial";
   525 
   526 (*Helps to prove Fake cases*)
   527 goal thy "!!X. X: analz (UN i. analz (H i)) ==> X: analz (UN i. H i)";
   528 by (etac analz.induct 1);
   529 by (ALLGOALS (fast_tac (!claset addEs [impOfSubs analz_mono])));
   530 val lemma = result();
   531 
   532 goal thy "analz (UN i. analz (H i)) = analz (UN i. H i)";
   533 by (fast_tac (!claset addIs [lemma]
   534                       addEs [impOfSubs analz_mono]) 1);
   535 qed "analz_UN_analz";
   536 Addsimps [analz_UN_analz];
   537 
   538 
   539 (**** Inductive relation "synth" ****)
   540 
   541 AddIs  synth.intrs;
   542 
   543 (*Can only produce a nonce or key if it is already known,
   544   but can synth a pair or encryption from its components...*)
   545 val mk_cases = synth.mk_cases msg.simps;
   546 
   547 (*NO Agent_synth, as any Agent name can be synthd*)
   548 val Nonce_synth = mk_cases "Nonce n : synth H";
   549 val Key_synth   = mk_cases "Key K : synth H";
   550 val Hash_synth  = mk_cases "Hash X : synth H";
   551 val MPair_synth = mk_cases "{|X,Y|} : synth H";
   552 val Crypt_synth = mk_cases "Crypt K X : synth H";
   553 
   554 AddSEs [Nonce_synth, Key_synth, Hash_synth, MPair_synth, Crypt_synth];
   555 
   556 goal thy "H <= synth(H)";
   557 by (Fast_tac 1);
   558 qed "synth_increasing";
   559 
   560 (*Monotonicity*)
   561 goalw thy synth.defs "!!G H. G<=H ==> synth(G) <= synth(H)";
   562 by (rtac lfp_mono 1);
   563 by (REPEAT (ares_tac basic_monos 1));
   564 qed "synth_mono";
   565 
   566 (** Unions **)
   567 
   568 (*Converse fails: we can synth more from the union than from the 
   569   separate parts, building a compound message using elements of each.*)
   570 goal thy "synth(G) Un synth(H) <= synth(G Un H)";
   571 by (REPEAT (ares_tac [Un_least, synth_mono, Un_upper1, Un_upper2] 1));
   572 qed "synth_Un";
   573 
   574 goal thy "insert X (synth H) <= synth(insert X H)";
   575 by (fast_tac (!claset addEs [impOfSubs synth_mono]) 1);
   576 qed "synth_insert";
   577 
   578 (** Idempotence and transitivity **)
   579 
   580 goal thy "!!H. X: synth (synth H) ==> X: synth H";
   581 by (etac synth.induct 1);
   582 by (ALLGOALS Fast_tac);
   583 qed "synth_synthE";
   584 AddSEs [synth_synthE];
   585 
   586 goal thy "synth (synth H) = synth H";
   587 by (Fast_tac 1);
   588 qed "synth_idem";
   589 
   590 goal thy "!!H. [| X: synth G;  G <= synth H |] ==> X: synth H";
   591 by (dtac synth_mono 1);
   592 by (Fast_tac 1);
   593 qed "synth_trans";
   594 
   595 (*Cut; Lemma 2 of Lowe*)
   596 goal thy "!!H. [| Y: synth (insert X H);  X: synth H |] ==> Y: synth H";
   597 by (etac synth_trans 1);
   598 by (Fast_tac 1);
   599 qed "synth_cut";
   600 
   601 goal thy "Agent A : synth H";
   602 by (Fast_tac 1);
   603 qed "Agent_synth";
   604 
   605 goal thy "(Nonce N : synth H) = (Nonce N : H)";
   606 by (Fast_tac 1);
   607 qed "Nonce_synth_eq";
   608 
   609 goal thy "(Key K : synth H) = (Key K : H)";
   610 by (Fast_tac 1);
   611 qed "Key_synth_eq";
   612 
   613 goal thy "!!K. Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X : H)";
   614 by (Fast_tac 1);
   615 qed "Crypt_synth_eq";
   616 
   617 Addsimps [Agent_synth, Nonce_synth_eq, Key_synth_eq, Crypt_synth_eq];
   618 
   619 
   620 goalw thy [keysFor_def]
   621     "keysFor (synth H) = keysFor H Un invKey``{K. Key K : H}";
   622 by (Fast_tac 1);
   623 qed "keysFor_synth";
   624 Addsimps [keysFor_synth];
   625 
   626 
   627 (*** Combinations of parts, analz and synth ***)
   628 
   629 goal thy "parts (synth H) = parts H Un synth H";
   630 by (rtac equalityI 1);
   631 by (rtac subsetI 1);
   632 by (etac parts.induct 1);
   633 by (ALLGOALS
   634     (best_tac (!claset addIs ((synth_increasing RS parts_mono RS subsetD)
   635                              ::parts.intrs))));
   636 qed "parts_synth";
   637 Addsimps [parts_synth];
   638 
   639 goal thy "analz (analz G Un H) = analz (G Un H)";
   640 by (REPEAT_FIRST (resolve_tac [equalityI, analz_subset_cong]));
   641 by (ALLGOALS Simp_tac);
   642 qed "analz_analz_Un";
   643 
   644 goal thy "analz (synth G Un H) = analz (G Un H) Un synth G";
   645 by (rtac equalityI 1);
   646 by (rtac subsetI 1);
   647 by (etac analz.induct 1);
   648 by (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 5);
   649 (*Strange that best_tac just can't hack this one...*)
   650 by (ALLGOALS (deepen_tac (!claset addIs analz.intrs) 0));
   651 qed "analz_synth_Un";
   652 
   653 goal thy "analz (synth H) = analz H Un synth H";
   654 by (cut_inst_tac [("H","{}")] analz_synth_Un 1);
   655 by (Full_simp_tac 1);
   656 qed "analz_synth";
   657 Addsimps [analz_analz_Un, analz_synth_Un, analz_synth];
   658 
   659 (*Hard to prove; still needed now that there's only one Spy?*)
   660 goal thy "analz (UN i. synth (H i)) = \
   661 \         analz (UN i. H i) Un (UN i. synth (H i))";
   662 by (rtac equalityI 1);
   663 by (rtac subsetI 1);
   664 by (etac analz.induct 1);
   665 by (best_tac
   666     (!claset addEs [impOfSubs synth_increasing,
   667                     impOfSubs analz_mono]) 5);
   668 by (Best_tac 1);
   669 by (deepen_tac (!claset addIs [analz.Fst]) 0 1);
   670 by (deepen_tac (!claset addIs [analz.Snd]) 0 1);
   671 by (deepen_tac (!claset addSEs [analz.Decrypt]
   672                         addIs  [analz.Decrypt]) 0 1);
   673 qed "analz_UN1_synth";
   674 Addsimps [analz_UN1_synth];
   675 
   676 
   677 (** For reasoning about the Fake rule in traces **)
   678 
   679 goal thy "!!Y. X: G ==> parts(insert X H) <= parts G Un parts H";
   680 by (rtac ([parts_mono, parts_Un_subset2] MRS subset_trans) 1);
   681 by (Fast_tac 1);
   682 qed "parts_insert_subset_Un";
   683 
   684 (*More specifically for Fake*)
   685 goal thy "!!H. X: synth (analz G) ==> \
   686 \              parts (insert X H) <= synth (analz G) Un parts G Un parts H";
   687 by (dtac parts_insert_subset_Un 1);
   688 by (Full_simp_tac 1);
   689 by (Deepen_tac 0 1);
   690 qed "Fake_parts_insert";
   691 
   692 goal thy
   693      "!!H. [| Crypt K Y : parts (insert X H);  X: synth (analz G);  \
   694 \             Key K ~: analz G |]                                   \
   695 \          ==> Crypt K Y : parts G Un parts H";
   696 by (dtac (impOfSubs Fake_parts_insert) 1);
   697 by (assume_tac 1);
   698 by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]
   699                       addss (!simpset)) 1);
   700 qed "Crypt_Fake_parts_insert";
   701 
   702 goal thy "!!H. X: synth (analz G) ==> \
   703 \              analz (insert X H) <= synth (analz G) Un analz (G Un H)";
   704 by (rtac subsetI 1);
   705 by (subgoal_tac "x : analz (synth (analz G) Un H)" 1);
   706 by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)]
   707                       addSEs [impOfSubs analz_mono]) 2);
   708 by (Full_simp_tac 1);
   709 by (Fast_tac 1);
   710 qed "Fake_analz_insert";
   711 
   712 (*Needed????????????????*)
   713 goal thy "!!H. [| X: synth (analz G); G <= H |] ==> \
   714 \              analz (insert X H) <= synth (analz H) Un analz H";
   715 by (rtac subsetI 1);
   716 by (subgoal_tac "x : analz (synth (analz H))" 1);
   717 by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)]
   718                       addSEs [impOfSubs analz_mono]) 2);
   719 by (Full_simp_tac 1);
   720 by (Fast_tac 1);
   721 qed "Fake_analz_insert_old";
   722 
   723 goal thy "(X: analz H & X: parts H) = (X: analz H)";
   724 by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]) 1);
   725 val analz_conj_parts = result();
   726 
   727 goal thy "(X: analz H | X: parts H) = (X: parts H)";
   728 by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]) 1);
   729 val analz_disj_parts = result();
   730 
   731 AddIffs [analz_conj_parts, analz_disj_parts];
   732 
   733 (*Without this equation, other rules for synth and analz would yield
   734   redundant cases*)
   735 goal thy "({|X,Y|} : synth (analz H)) = \
   736 \         (X : synth (analz H) & Y : synth (analz H))";
   737 by (Fast_tac 1);
   738 qed "MPair_synth_analz";
   739 
   740 AddIffs [MPair_synth_analz];
   741 
   742 goal thy "!!K. [| Key K : analz H;  Key (invKey K) : analz H |] \
   743 \              ==> (Crypt K X : synth (analz H)) = (X : synth (analz H))";
   744 by (Fast_tac 1);
   745 qed "Crypt_synth_analz";
   746 
   747 
   748 goal thy "!!K. Key K ~: analz H \
   749 \   ==> (Hash{|Key K,X|} : synth (analz H)) = (Hash{|Key K,X|} : analz H)";
   750 by (Fast_tac 1);
   751 qed "Hash_synth_analz";
   752 Addsimps [Hash_synth_analz];
   753 
   754 
   755 (*We do NOT want Crypt... messages broken up in protocols!!*)
   756 Delrules partsEs;
   757 
   758 
   759 (** Rewrites to push in Key and Crypt messages, so that other messages can
   760     be pulled out using the analz_insert rules **)
   761 
   762 fun insComm thy x y = read_instantiate_sg (sign_of thy) [("x",x), ("y",y)] 
   763                           insert_commute;
   764 
   765 val pushKeys = map (insComm thy "Key ?K") 
   766                    ["Agent ?C", "Nonce ?N", "Hash ?X", 
   767 		    "MPair ?X ?Y", "Crypt ?X ?K'"];
   768 
   769 val pushCrypts = map (insComm thy "Crypt ?X ?K") 
   770                      ["Agent ?C", "Nonce ?N", "Hash ?X'", "MPair ?X' ?Y"];
   771 
   772 (*Cannot be added with Addsimps -- we don't always want to re-order messages*)
   773 val pushes = pushKeys@pushCrypts;
   774 
   775 
   776 (*No premature instantiation of variables.  For proving weak liveness.*)
   777 fun safe_solver prems =
   778     match_tac (TrueI::refl::prems) ORELSE' eq_assume_tac
   779     ORELSE' etac FalseE;
   780 
   781 val Fake_insert_tac = 
   782     dresolve_tac [impOfSubs Fake_analz_insert,
   783 		  impOfSubs Fake_parts_insert] THEN'
   784     eresolve_tac [asm_rl, synth.Inj];
   785 
   786 (*Analysis of Fake cases and of messages that forward unknown parts.
   787   Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
   788   DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
   789 fun spy_analz_tac i =
   790   DETERM
   791    (SELECT_GOAL
   792      (EVERY 
   793       [  (*push in occurrences of X...*)
   794        (REPEAT o CHANGED)
   795            (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
   796        (*...allowing further simplifications*)
   797        simp_tac (!simpset setloop split_tac [expand_if]) 1,
   798        REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI])),
   799        DEPTH_SOLVE 
   800          (REPEAT (Fake_insert_tac 1) THEN Asm_full_simp_tac 1
   801 	  THEN
   802 	  IF_UNSOLVED (depth_tac (!claset addIs [impOfSubs analz_mono,
   803 						 impOfSubs analz_subset_parts]) 2 1))
   804        ]) i);
   805 
   806 (** Useful in many uniqueness proofs **)
   807 fun ex_strip_tac i = REPEAT (swap_res_tac [exI, conjI] i) THEN 
   808                      assume_tac (i+1);
   809 
   810 (*Apply the EX-ALL quantifification to prove uniqueness theorems in 
   811   their standard form*)
   812 fun prove_unique_tac lemma = 
   813   EVERY' [dtac lemma,
   814 	  REPEAT o (mp_tac ORELSE' eresolve_tac [asm_rl,exE]),
   815 	  (*Duplicate the assumption*)
   816 	  forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl,
   817 	  fast_tac (!claset addSDs [spec])];
   818 
   819 
   820 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
   821 goal Set.thy "A Un (B Un A) = B Un A";
   822 by (Fast_tac 1);
   823 val Un_absorb3 = result();
   824 Addsimps [Un_absorb3];