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