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