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