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