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