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