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