src/HOL/MetisExamples/Message.thy
author paulson
Thu Jun 21 13:23:33 2007 +0200 (2007-06-21)
changeset 23449 dd874e6a3282
child 23755 1c4672d130b1
permissions -rw-r--r--
integration of Metis prover
     1 (*  Title:      HOL/MetisTest/Message.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4 
     5 Testing the metis method
     6 *)
     7 
     8 theory Message imports Main begin
     9 
    10 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
    11 lemma strange_Un_eq [simp]: "A \<union> (B \<union> A) = B \<union> A"
    12 by blast
    13 
    14 types 
    15   key = nat
    16 
    17 consts
    18   all_symmetric :: bool        --{*true if all keys are symmetric*}
    19   invKey        :: "key=>key"  --{*inverse of a symmetric key*}
    20 
    21 specification (invKey)
    22   invKey [simp]: "invKey (invKey K) = K"
    23   invKey_symmetric: "all_symmetric --> invKey = id"
    24     by (rule exI [of _ id], auto)
    25 
    26 
    27 text{*The inverse of a symmetric key is itself; that of a public key
    28       is the private key and vice versa*}
    29 
    30 constdefs
    31   symKeys :: "key set"
    32   "symKeys == {K. invKey K = K}"
    33 
    34 datatype  --{*We allow any number of friendly agents*}
    35   agent = Server | Friend nat | Spy
    36 
    37 datatype
    38      msg = Agent  agent	    --{*Agent names*}
    39          | Number nat       --{*Ordinary integers, timestamps, ...*}
    40          | Nonce  nat       --{*Unguessable nonces*}
    41          | Key    key       --{*Crypto keys*}
    42 	 | Hash   msg       --{*Hashing*}
    43 	 | MPair  msg msg   --{*Compound messages*}
    44 	 | Crypt  key msg   --{*Encryption, public- or shared-key*}
    45 
    46 
    47 text{*Concrete syntax: messages appear as {|A,B,NA|}, etc...*}
    48 syntax
    49   "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
    50 
    51 syntax (xsymbols)
    52   "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
    53 
    54 translations
    55   "{|x, y, z|}"   == "{|x, {|y, z|}|}"
    56   "{|x, y|}"      == "MPair x y"
    57 
    58 
    59 constdefs
    60   HPair :: "[msg,msg] => msg"                       ("(4Hash[_] /_)" [0, 1000])
    61     --{*Message Y paired with a MAC computed with the help of X*}
    62     "Hash[X] Y == {| Hash{|X,Y|}, Y|}"
    63 
    64   keysFor :: "msg set => key set"
    65     --{*Keys useful to decrypt elements of a message set*}
    66   "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"
    67 
    68 
    69 subsubsection{*Inductive Definition of All Parts" of a Message*}
    70 
    71 consts  parts   :: "msg set => msg set"
    72 inductive "parts H"
    73   intros 
    74     Inj [intro]:               "X \<in> H ==> X \<in> parts H"
    75     Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
    76     Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
    77     Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
    78 
    79 
    80 ML{*ResAtp.problem_name := "Message__parts_mono"*}
    81 lemma parts_mono: "G \<subseteq> H ==> parts(G) \<subseteq> parts(H)"
    82 apply auto
    83 apply (erule parts.induct) 
    84 apply (metis Inj set_mp)
    85 apply (metis Fst)
    86 apply (metis Snd)
    87 apply (metis Body)
    88 done
    89 
    90 
    91 text{*Equations hold because constructors are injective.*}
    92 lemma Friend_image_eq [simp]: "(Friend x \<in> Friend`A) = (x:A)"
    93 by auto
    94 
    95 lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x\<in>A)"
    96 by auto
    97 
    98 lemma Nonce_Key_image_eq [simp]: "(Nonce x \<notin> Key`A)"
    99 by auto
   100 
   101 
   102 subsubsection{*Inverse of keys *}
   103 
   104 ML{*ResAtp.problem_name := "Message__invKey_eq"*}
   105 lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
   106 by (metis invKey)
   107 
   108 
   109 subsection{*keysFor operator*}
   110 
   111 lemma keysFor_empty [simp]: "keysFor {} = {}"
   112 by (unfold keysFor_def, blast)
   113 
   114 lemma keysFor_Un [simp]: "keysFor (H \<union> H') = keysFor H \<union> keysFor H'"
   115 by (unfold keysFor_def, blast)
   116 
   117 lemma keysFor_UN [simp]: "keysFor (\<Union>i\<in>A. H i) = (\<Union>i\<in>A. keysFor (H i))"
   118 by (unfold keysFor_def, blast)
   119 
   120 text{*Monotonicity*}
   121 lemma keysFor_mono: "G \<subseteq> H ==> keysFor(G) \<subseteq> keysFor(H)"
   122 by (unfold keysFor_def, blast)
   123 
   124 lemma keysFor_insert_Agent [simp]: "keysFor (insert (Agent A) H) = keysFor H"
   125 by (unfold keysFor_def, auto)
   126 
   127 lemma keysFor_insert_Nonce [simp]: "keysFor (insert (Nonce N) H) = keysFor H"
   128 by (unfold keysFor_def, auto)
   129 
   130 lemma keysFor_insert_Number [simp]: "keysFor (insert (Number N) H) = keysFor H"
   131 by (unfold keysFor_def, auto)
   132 
   133 lemma keysFor_insert_Key [simp]: "keysFor (insert (Key K) H) = keysFor H"
   134 by (unfold keysFor_def, auto)
   135 
   136 lemma keysFor_insert_Hash [simp]: "keysFor (insert (Hash X) H) = keysFor H"
   137 by (unfold keysFor_def, auto)
   138 
   139 lemma keysFor_insert_MPair [simp]: "keysFor (insert {|X,Y|} H) = keysFor H"
   140 by (unfold keysFor_def, auto)
   141 
   142 lemma keysFor_insert_Crypt [simp]: 
   143     "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"
   144 by (unfold keysFor_def, auto)
   145 
   146 lemma keysFor_image_Key [simp]: "keysFor (Key`E) = {}"
   147 by (unfold keysFor_def, auto)
   148 
   149 lemma Crypt_imp_invKey_keysFor: "Crypt K X \<in> H ==> invKey K \<in> keysFor H"
   150 by (unfold keysFor_def, blast)
   151 
   152 
   153 subsection{*Inductive relation "parts"*}
   154 
   155 lemma MPair_parts:
   156      "[| {|X,Y|} \<in> parts H;        
   157          [| X \<in> parts H; Y \<in> parts H |] ==> P |] ==> P"
   158 by (blast dest: parts.Fst parts.Snd) 
   159 
   160     declare MPair_parts [elim!]  parts.Body [dest!]
   161 text{*NB These two rules are UNSAFE in the formal sense, as they discard the
   162      compound message.  They work well on THIS FILE.  
   163   @{text MPair_parts} is left as SAFE because it speeds up proofs.
   164   The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*}
   165 
   166 lemma parts_increasing: "H \<subseteq> parts(H)"
   167 by blast
   168 
   169 lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD, standard]
   170 
   171 lemma parts_empty [simp]: "parts{} = {}"
   172 apply safe
   173 apply (erule parts.induct)
   174 apply blast+
   175 done
   176 
   177 lemma parts_emptyE [elim!]: "X\<in> parts{} ==> P"
   178 by simp
   179 
   180 text{*WARNING: loops if H = {Y}, therefore must not be repeated!*}
   181 lemma parts_singleton: "X\<in> parts H ==> \<exists>Y\<in>H. X\<in> parts {Y}"
   182 apply (erule parts.induct)
   183 apply blast+
   184 done
   185 
   186 
   187 subsubsection{*Unions *}
   188 
   189 lemma parts_Un_subset1: "parts(G) \<union> parts(H) \<subseteq> parts(G \<union> H)"
   190 by (intro Un_least parts_mono Un_upper1 Un_upper2)
   191 
   192 lemma parts_Un_subset2: "parts(G \<union> H) \<subseteq> parts(G) \<union> parts(H)"
   193 apply (rule subsetI)
   194 apply (erule parts.induct, blast+)
   195 done
   196 
   197 lemma parts_Un [simp]: "parts(G \<union> H) = parts(G) \<union> parts(H)"
   198 by (intro equalityI parts_Un_subset1 parts_Un_subset2)
   199 
   200 lemma parts_insert: "parts (insert X H) = parts {X} \<union> parts H"
   201 apply (subst insert_is_Un [of _ H])
   202 apply (simp only: parts_Un)
   203 done
   204 
   205 ML{*ResAtp.problem_name := "Message__parts_insert_two"*}
   206 lemma parts_insert2:
   207      "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
   208 by (metis Un_commute Un_empty_left Un_empty_right Un_insert_left Un_insert_right insert_commute parts_Un)
   209 
   210 
   211 lemma parts_UN_subset1: "(\<Union>x\<in>A. parts(H x)) \<subseteq> parts(\<Union>x\<in>A. H x)"
   212 by (intro UN_least parts_mono UN_upper)
   213 
   214 lemma parts_UN_subset2: "parts(\<Union>x\<in>A. H x) \<subseteq> (\<Union>x\<in>A. parts(H x))"
   215 apply (rule subsetI)
   216 apply (erule parts.induct, blast+)
   217 done
   218 
   219 lemma parts_UN [simp]: "parts(\<Union>x\<in>A. H x) = (\<Union>x\<in>A. parts(H x))"
   220 by (intro equalityI parts_UN_subset1 parts_UN_subset2)
   221 
   222 text{*Added to simplify arguments to parts, analz and synth.
   223   NOTE: the UN versions are no longer used!*}
   224 
   225 
   226 text{*This allows @{text blast} to simplify occurrences of 
   227   @{term "parts(G\<union>H)"} in the assumption.*}
   228 lemmas in_parts_UnE = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE] 
   229 declare in_parts_UnE [elim!]
   230 
   231 lemma parts_insert_subset: "insert X (parts H) \<subseteq> parts(insert X H)"
   232 by (blast intro: parts_mono [THEN [2] rev_subsetD])
   233 
   234 subsubsection{*Idempotence and transitivity *}
   235 
   236 lemma parts_partsD [dest!]: "X\<in> parts (parts H) ==> X\<in> parts H"
   237 by (erule parts.induct, blast+)
   238 
   239 lemma parts_idem [simp]: "parts (parts H) = parts H"
   240 by blast
   241 
   242 ML{*ResAtp.problem_name := "Message__parts_subset_iff"*}
   243 lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)"
   244 apply (rule iffI) 
   245 apply (metis Un_absorb1 Un_subset_iff parts_Un parts_increasing)
   246 apply (metis parts_Un parts_idem parts_increasing parts_mono)
   247 done
   248 
   249 lemma parts_trans: "[| X\<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"
   250 by (blast dest: parts_mono); 
   251 
   252 
   253 ML{*ResAtp.problem_name := "Message__parts_cut"*}
   254 lemma parts_cut: "[|Y\<in> parts(insert X G);  X\<in> parts H|] ==> Y\<in> parts(G \<union> H)"
   255 by (metis Un_subset_iff Un_upper1 Un_upper2 insert_subset parts_Un parts_increasing parts_trans) 
   256 
   257 
   258 
   259 subsubsection{*Rewrite rules for pulling out atomic messages *}
   260 
   261 lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset]
   262 
   263 
   264 lemma parts_insert_Agent [simp]:
   265      "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"
   266 apply (rule parts_insert_eq_I) 
   267 apply (erule parts.induct, auto) 
   268 done
   269 
   270 lemma parts_insert_Nonce [simp]:
   271      "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"
   272 apply (rule parts_insert_eq_I) 
   273 apply (erule parts.induct, auto) 
   274 done
   275 
   276 lemma parts_insert_Number [simp]:
   277      "parts (insert (Number N) H) = insert (Number N) (parts H)"
   278 apply (rule parts_insert_eq_I) 
   279 apply (erule parts.induct, auto) 
   280 done
   281 
   282 lemma parts_insert_Key [simp]:
   283      "parts (insert (Key K) H) = insert (Key K) (parts H)"
   284 apply (rule parts_insert_eq_I) 
   285 apply (erule parts.induct, auto) 
   286 done
   287 
   288 lemma parts_insert_Hash [simp]:
   289      "parts (insert (Hash X) H) = insert (Hash X) (parts H)"
   290 apply (rule parts_insert_eq_I) 
   291 apply (erule parts.induct, auto) 
   292 done
   293 
   294 lemma parts_insert_Crypt [simp]:
   295      "parts (insert (Crypt K X) H) =  
   296           insert (Crypt K X) (parts (insert X H))"
   297 apply (rule equalityI)
   298 apply (rule subsetI)
   299 apply (erule parts.induct, auto)
   300 apply (blast intro: parts.Body)
   301 done
   302 
   303 lemma parts_insert_MPair [simp]:
   304      "parts (insert {|X,Y|} H) =  
   305           insert {|X,Y|} (parts (insert X (insert Y H)))"
   306 apply (rule equalityI)
   307 apply (rule subsetI)
   308 apply (erule parts.induct, auto)
   309 apply (blast intro: parts.Fst parts.Snd)+
   310 done
   311 
   312 lemma parts_image_Key [simp]: "parts (Key`N) = Key`N"
   313 apply auto
   314 apply (erule parts.induct, auto)
   315 done
   316 
   317 
   318 ML{*ResAtp.problem_name := "Message__msg_Nonce_supply"*}
   319 lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n --> Nonce n \<notin> parts {msg}"
   320 apply (induct_tac "msg") 
   321 apply (simp_all add: parts_insert2)
   322 apply (metis Suc_n_not_le_n)
   323 apply (metis le_trans linorder_linear)
   324 done
   325 
   326 subsection{*Inductive relation "analz"*}
   327 
   328 text{*Inductive definition of "analz" -- what can be broken down from a set of
   329     messages, including keys.  A form of downward closure.  Pairs can
   330     be taken apart; messages decrypted with known keys.  *}
   331 
   332 consts  analz   :: "msg set => msg set"
   333 inductive "analz H"
   334   intros 
   335     Inj [intro,simp] :    "X \<in> H ==> X \<in> analz H"
   336     Fst:     "{|X,Y|} \<in> analz H ==> X \<in> analz H"
   337     Snd:     "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
   338     Decrypt [dest]: 
   339              "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
   340 
   341 
   342 text{*Monotonicity; Lemma 1 of Lowe's paper*}
   343 lemma analz_mono: "G\<subseteq>H ==> analz(G) \<subseteq> analz(H)"
   344 apply auto
   345 apply (erule analz.induct) 
   346 apply (auto dest: analz.Fst analz.Snd) 
   347 done
   348 
   349 text{*Making it safe speeds up proofs*}
   350 lemma MPair_analz [elim!]:
   351      "[| {|X,Y|} \<in> analz H;        
   352              [| X \<in> analz H; Y \<in> analz H |] ==> P   
   353           |] ==> P"
   354 by (blast dest: analz.Fst analz.Snd)
   355 
   356 lemma analz_increasing: "H \<subseteq> analz(H)"
   357 by blast
   358 
   359 lemma analz_subset_parts: "analz H \<subseteq> parts H"
   360 apply (rule subsetI)
   361 apply (erule analz.induct, blast+)
   362 done
   363 
   364 lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
   365 
   366 lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
   367 
   368 
   369 ML{*ResAtp.problem_name := "Message__parts_analz"*}
   370 lemma parts_analz [simp]: "parts (analz H) = parts H"
   371 apply (rule equalityI)
   372 apply (metis analz_subset_parts parts_subset_iff)
   373 apply (metis analz_increasing parts_mono)
   374 done
   375 
   376 
   377 lemma analz_parts [simp]: "analz (parts H) = parts H"
   378 apply auto
   379 apply (erule analz.induct, auto)
   380 done
   381 
   382 lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
   383 
   384 subsubsection{*General equational properties *}
   385 
   386 lemma analz_empty [simp]: "analz{} = {}"
   387 apply safe
   388 apply (erule analz.induct, blast+)
   389 done
   390 
   391 text{*Converse fails: we can analz more from the union than from the 
   392   separate parts, as a key in one might decrypt a message in the other*}
   393 lemma analz_Un: "analz(G) \<union> analz(H) \<subseteq> analz(G \<union> H)"
   394 by (intro Un_least analz_mono Un_upper1 Un_upper2)
   395 
   396 lemma analz_insert: "insert X (analz H) \<subseteq> analz(insert X H)"
   397 by (blast intro: analz_mono [THEN [2] rev_subsetD])
   398 
   399 subsubsection{*Rewrite rules for pulling out atomic messages *}
   400 
   401 lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert]
   402 
   403 lemma analz_insert_Agent [simp]:
   404      "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"
   405 apply (rule analz_insert_eq_I) 
   406 apply (erule analz.induct, auto) 
   407 done
   408 
   409 lemma analz_insert_Nonce [simp]:
   410      "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"
   411 apply (rule analz_insert_eq_I) 
   412 apply (erule analz.induct, auto) 
   413 done
   414 
   415 lemma analz_insert_Number [simp]:
   416      "analz (insert (Number N) H) = insert (Number N) (analz H)"
   417 apply (rule analz_insert_eq_I) 
   418 apply (erule analz.induct, auto) 
   419 done
   420 
   421 lemma analz_insert_Hash [simp]:
   422      "analz (insert (Hash X) H) = insert (Hash X) (analz H)"
   423 apply (rule analz_insert_eq_I) 
   424 apply (erule analz.induct, auto) 
   425 done
   426 
   427 text{*Can only pull out Keys if they are not needed to decrypt the rest*}
   428 lemma analz_insert_Key [simp]: 
   429     "K \<notin> keysFor (analz H) ==>   
   430           analz (insert (Key K) H) = insert (Key K) (analz H)"
   431 apply (unfold keysFor_def)
   432 apply (rule analz_insert_eq_I) 
   433 apply (erule analz.induct, auto) 
   434 done
   435 
   436 lemma analz_insert_MPair [simp]:
   437      "analz (insert {|X,Y|} H) =  
   438           insert {|X,Y|} (analz (insert X (insert Y H)))"
   439 apply (rule equalityI)
   440 apply (rule subsetI)
   441 apply (erule analz.induct, auto)
   442 apply (erule analz.induct)
   443 apply (blast intro: analz.Fst analz.Snd)+
   444 done
   445 
   446 text{*Can pull out enCrypted message if the Key is not known*}
   447 lemma analz_insert_Crypt:
   448      "Key (invKey K) \<notin> analz H 
   449       ==> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)"
   450 apply (rule analz_insert_eq_I) 
   451 apply (erule analz.induct, auto) 
   452 
   453 done
   454 
   455 lemma lemma1: "Key (invKey K) \<in> analz H ==>   
   456                analz (insert (Crypt K X) H) \<subseteq>  
   457                insert (Crypt K X) (analz (insert X H))" 
   458 apply (rule subsetI)
   459 apply (erule_tac xa = x in analz.induct, auto)
   460 done
   461 
   462 lemma lemma2: "Key (invKey K) \<in> analz H ==>   
   463                insert (Crypt K X) (analz (insert X H)) \<subseteq>  
   464                analz (insert (Crypt K X) H)"
   465 apply auto
   466 apply (erule_tac xa = x in analz.induct, auto)
   467 apply (blast intro: analz_insertI analz.Decrypt)
   468 done
   469 
   470 lemma analz_insert_Decrypt:
   471      "Key (invKey K) \<in> analz H ==>   
   472                analz (insert (Crypt K X) H) =  
   473                insert (Crypt K X) (analz (insert X H))"
   474 by (intro equalityI lemma1 lemma2)
   475 
   476 text{*Case analysis: either the message is secure, or it is not! Effective,
   477 but can cause subgoals to blow up! Use with @{text "split_if"}; apparently
   478 @{text "split_tac"} does not cope with patterns such as @{term"analz (insert
   479 (Crypt K X) H)"} *} 
   480 lemma analz_Crypt_if [simp]:
   481      "analz (insert (Crypt K X) H) =                 
   482           (if (Key (invKey K) \<in> analz H)                 
   483            then insert (Crypt K X) (analz (insert X H))  
   484            else insert (Crypt K X) (analz H))"
   485 by (simp add: analz_insert_Crypt analz_insert_Decrypt)
   486 
   487 
   488 text{*This rule supposes "for the sake of argument" that we have the key.*}
   489 lemma analz_insert_Crypt_subset:
   490      "analz (insert (Crypt K X) H) \<subseteq>   
   491            insert (Crypt K X) (analz (insert X H))"
   492 apply (rule subsetI)
   493 apply (erule analz.induct, auto)
   494 done
   495 
   496 
   497 lemma analz_image_Key [simp]: "analz (Key`N) = Key`N"
   498 apply auto
   499 apply (erule analz.induct, auto)
   500 done
   501 
   502 
   503 subsubsection{*Idempotence and transitivity *}
   504 
   505 lemma analz_analzD [dest!]: "X\<in> analz (analz H) ==> X\<in> analz H"
   506 by (erule analz.induct, blast+)
   507 
   508 lemma analz_idem [simp]: "analz (analz H) = analz H"
   509 by blast
   510 
   511 lemma analz_subset_iff [simp]: "(analz G \<subseteq> analz H) = (G \<subseteq> analz H)"
   512 apply (rule iffI)
   513 apply (iprover intro: subset_trans analz_increasing)  
   514 apply (frule analz_mono, simp) 
   515 done
   516 
   517 lemma analz_trans: "[| X\<in> analz G;  G \<subseteq> analz H |] ==> X\<in> analz H"
   518 by (drule analz_mono, blast)
   519 
   520 
   521 ML{*ResAtp.problem_name := "Message__analz_cut"*}
   522     declare analz_trans[intro]
   523 lemma analz_cut: "[| Y\<in> analz (insert X H);  X\<in> analz H |] ==> Y\<in> analz H"
   524 (*TOO SLOW
   525 by (metis analz_idem analz_increasing analz_mono insert_absorb insert_mono insert_subset) --{*317s*}
   526 ??*)
   527 by (erule analz_trans, blast)
   528 
   529 
   530 text{*This rewrite rule helps in the simplification of messages that involve
   531   the forwarding of unknown components (X).  Without it, removing occurrences
   532   of X can be very complicated. *}
   533 lemma analz_insert_eq: "X\<in> analz H ==> analz (insert X H) = analz H"
   534 by (blast intro: analz_cut analz_insertI)
   535 
   536 
   537 text{*A congruence rule for "analz" *}
   538 
   539 ML{*ResAtp.problem_name := "Message__analz_subset_cong"*}
   540 lemma analz_subset_cong:
   541      "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H' |] 
   542       ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
   543 apply simp
   544 apply (metis Un_absorb2 Un_commute Un_subset_iff Un_upper1 Un_upper2 analz_mono)
   545 done
   546 
   547 
   548 lemma analz_cong:
   549      "[| analz G = analz G'; analz H = analz H'  
   550                |] ==> analz (G \<union> H) = analz (G' \<union> H')"
   551 by (intro equalityI analz_subset_cong, simp_all) 
   552 
   553 lemma analz_insert_cong:
   554      "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"
   555 by (force simp only: insert_def intro!: analz_cong)
   556 
   557 text{*If there are no pairs or encryptions then analz does nothing*}
   558 lemma analz_trivial:
   559      "[| \<forall>X Y. {|X,Y|} \<notin> H;  \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
   560 apply safe
   561 apply (erule analz.induct, blast+)
   562 done
   563 
   564 text{*These two are obsolete (with a single Spy) but cost little to prove...*}
   565 lemma analz_UN_analz_lemma:
   566      "X\<in> analz (\<Union>i\<in>A. analz (H i)) ==> X\<in> analz (\<Union>i\<in>A. H i)"
   567 apply (erule analz.induct)
   568 apply (blast intro: analz_mono [THEN [2] rev_subsetD])+
   569 done
   570 
   571 lemma analz_UN_analz [simp]: "analz (\<Union>i\<in>A. analz (H i)) = analz (\<Union>i\<in>A. H i)"
   572 by (blast intro: analz_UN_analz_lemma analz_mono [THEN [2] rev_subsetD])
   573 
   574 
   575 subsection{*Inductive relation "synth"*}
   576 
   577 text{*Inductive definition of "synth" -- what can be built up from a set of
   578     messages.  A form of upward closure.  Pairs can be built, messages
   579     encrypted with known keys.  Agent names are public domain.
   580     Numbers can be guessed, but Nonces cannot be.  *}
   581 
   582 consts  synth   :: "msg set => msg set"
   583 inductive "synth H"
   584   intros 
   585     Inj    [intro]:   "X \<in> H ==> X \<in> synth H"
   586     Agent  [intro]:   "Agent agt \<in> synth H"
   587     Number [intro]:   "Number n  \<in> synth H"
   588     Hash   [intro]:   "X \<in> synth H ==> Hash X \<in> synth H"
   589     MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
   590     Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
   591 
   592 text{*Monotonicity*}
   593 lemma synth_mono: "G\<subseteq>H ==> synth(G) \<subseteq> synth(H)"
   594   by (auto, erule synth.induct, auto)  
   595 
   596 text{*NO @{text Agent_synth}, as any Agent name can be synthesized.  
   597   The same holds for @{term Number}*}
   598 inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H"
   599 inductive_cases Key_synth   [elim!]: "Key K \<in> synth H"
   600 inductive_cases Hash_synth  [elim!]: "Hash X \<in> synth H"
   601 inductive_cases MPair_synth [elim!]: "{|X,Y|} \<in> synth H"
   602 inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
   603 
   604 
   605 lemma synth_increasing: "H \<subseteq> synth(H)"
   606 by blast
   607 
   608 subsubsection{*Unions *}
   609 
   610 text{*Converse fails: we can synth more from the union than from the 
   611   separate parts, building a compound message using elements of each.*}
   612 lemma synth_Un: "synth(G) \<union> synth(H) \<subseteq> synth(G \<union> H)"
   613 by (intro Un_least synth_mono Un_upper1 Un_upper2)
   614 
   615 
   616 ML{*ResAtp.problem_name := "Message__synth_insert"*}
   617  
   618 lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)"
   619 by (metis insert_iff insert_subset subset_insertI synth.Inj synth_mono)
   620 
   621 subsubsection{*Idempotence and transitivity *}
   622 
   623 lemma synth_synthD [dest!]: "X\<in> synth (synth H) ==> X\<in> synth H"
   624 by (erule synth.induct, blast+)
   625 
   626 lemma synth_idem: "synth (synth H) = synth H"
   627 by blast
   628 
   629 lemma synth_subset_iff [simp]: "(synth G \<subseteq> synth H) = (G \<subseteq> synth H)"
   630 apply (rule iffI)
   631 apply (iprover intro: subset_trans synth_increasing)  
   632 apply (frule synth_mono, simp add: synth_idem) 
   633 done
   634 
   635 lemma synth_trans: "[| X\<in> synth G;  G \<subseteq> synth H |] ==> X\<in> synth H"
   636 by (drule synth_mono, blast)
   637 
   638 ML{*ResAtp.problem_name := "Message__synth_cut"*}
   639 lemma synth_cut: "[| Y\<in> synth (insert X H);  X\<in> synth H |] ==> Y\<in> synth H"
   640 (*TOO SLOW
   641 by (metis insert_absorb insert_mono insert_subset synth_idem synth_increasing synth_mono)
   642 *)
   643 by (erule synth_trans, blast)
   644 
   645 
   646 lemma Agent_synth [simp]: "Agent A \<in> synth H"
   647 by blast
   648 
   649 lemma Number_synth [simp]: "Number n \<in> synth H"
   650 by blast
   651 
   652 lemma Nonce_synth_eq [simp]: "(Nonce N \<in> synth H) = (Nonce N \<in> H)"
   653 by blast
   654 
   655 lemma Key_synth_eq [simp]: "(Key K \<in> synth H) = (Key K \<in> H)"
   656 by blast
   657 
   658 lemma Crypt_synth_eq [simp]:
   659      "Key K \<notin> H ==> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)"
   660 by blast
   661 
   662 
   663 lemma keysFor_synth [simp]: 
   664     "keysFor (synth H) = keysFor H \<union> invKey`{K. Key K \<in> H}"
   665 by (unfold keysFor_def, blast)
   666 
   667 
   668 subsubsection{*Combinations of parts, analz and synth *}
   669 
   670 ML{*ResAtp.problem_name := "Message__parts_synth"*}
   671 lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"
   672 apply (rule equalityI)
   673 apply (rule subsetI)
   674 apply (erule parts.induct)
   675 apply (metis UnCI)
   676 apply (metis MPair_synth UnCI UnE insert_absorb insert_subset parts.Fst parts_increasing)
   677 apply (metis MPair_synth UnCI UnE insert_absorb insert_subset parts.Snd parts_increasing)
   678 apply (metis Body Crypt_synth UnCI UnE insert_absorb insert_subset parts_increasing)
   679 apply (metis Un_subset_iff parts_increasing parts_mono synth_increasing)
   680 done
   681 
   682 
   683 
   684 
   685 ML{*ResAtp.problem_name := "Message__analz_analz_Un"*}
   686 lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)"
   687 apply (rule equalityI);
   688 apply (metis analz_idem analz_subset_cong order_eq_refl)
   689 apply (metis analz_increasing analz_subset_cong order_eq_refl)
   690 done
   691 
   692 ML{*ResAtp.problem_name := "Message__analz_synth_Un"*}
   693     declare analz_mono [intro] analz.Fst [intro] analz.Snd [intro] Un_least [intro]
   694 lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G"
   695 apply (rule equalityI)
   696 apply (rule subsetI)
   697 apply (erule analz.induct)
   698 apply (metis UnCI UnE Un_commute analz.Inj)
   699 apply (metis MPair_synth UnCI UnE Un_commute Un_upper1 analz.Fst analz_increasing analz_mono insert_absorb insert_subset)
   700 apply (metis MPair_synth UnCI UnE Un_commute Un_upper1 analz.Snd analz_increasing analz_mono insert_absorb insert_subset)
   701 apply (blast intro: analz.Decrypt)
   702 apply (metis Diff_Int Diff_empty Diff_subset_conv Int_empty_right Un_commute Un_subset_iff Un_upper1 analz_increasing analz_mono synth_increasing)
   703 done
   704 
   705 
   706 ML{*ResAtp.problem_name := "Message__analz_synth"*}
   707 lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
   708 proof (neg_clausify)
   709 assume 0: "analz (synth H) \<noteq> analz H \<union> synth H"
   710 have 1: "\<And>X1 X3. sup (analz (sup X3 X1)) (synth X3) = analz (sup (synth X3) X1)"
   711   by (metis analz_synth_Un sup_set_eq sup_set_eq sup_set_eq)
   712 have 2: "sup (analz H) (synth H) \<noteq> analz (synth H)"
   713   by (metis 0 sup_set_eq)
   714 have 3: "\<And>X1 X3. sup (synth X3) (analz (sup X3 X1)) = analz (sup (synth X3) X1)"
   715   by (metis 1 Un_commute sup_set_eq sup_set_eq)
   716 have 4: "\<And>X3. sup (synth X3) (analz X3) = analz (sup (synth X3) {})"
   717   by (metis 3 Un_empty_right sup_set_eq)
   718 have 5: "\<And>X3. sup (synth X3) (analz X3) = analz (synth X3)"
   719   by (metis 4 Un_empty_right sup_set_eq)
   720 have 6: "\<And>X3. sup (analz X3) (synth X3) = analz (synth X3)"
   721   by (metis 5 Un_commute sup_set_eq sup_set_eq)
   722 show "False"
   723   by (metis 2 6)
   724 qed
   725 
   726 
   727 subsubsection{*For reasoning about the Fake rule in traces *}
   728 
   729 ML{*ResAtp.problem_name := "Message__parts_insert_subset_Un"*}
   730 lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
   731 proof (neg_clausify)
   732 assume 0: "X \<in> G"
   733 assume 1: "\<not> parts (insert X H) \<subseteq> parts G \<union> parts H"
   734 have 2: "\<not> parts (insert X H) \<subseteq> parts (G \<union> H)"
   735   by (metis 1 parts_Un)
   736 have 3: "\<not> insert X H \<subseteq> G \<union> H"
   737   by (metis 2 parts_mono)
   738 have 4: "X \<notin> G \<union> H \<or> \<not> H \<subseteq> G \<union> H"
   739   by (metis 3 insert_subset)
   740 have 5: "X \<notin> G \<union> H"
   741   by (metis 4 Un_upper2)
   742 have 6: "X \<notin> G"
   743   by (metis 5 UnCI)
   744 show "False"
   745   by (metis 6 0)
   746 qed
   747 
   748 ML{*ResAtp.problem_name := "Message__Fake_parts_insert"*}
   749 lemma Fake_parts_insert:
   750      "X \<in> synth (analz H) ==>  
   751       parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
   752 proof (neg_clausify)
   753 assume 0: "X \<in> synth (analz H)"
   754 assume 1: "\<not> parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
   755 have 2: "\<And>X3. parts X3 \<union> synth (analz X3) = parts (synth (analz X3))"
   756   by (metis parts_synth parts_analz)
   757 have 3: "\<And>X3. analz X3 \<union> synth (analz X3) = analz (synth (analz X3))"
   758   by (metis analz_synth analz_idem)
   759 have 4: "\<And>X3. analz X3 \<subseteq> analz (synth X3)"
   760   by (metis Un_upper1 analz_synth)
   761 have 5: "\<not> parts (insert X H) \<subseteq> parts H \<union> synth (analz H)"
   762   by (metis 1 Un_commute)
   763 have 6: "\<not> parts (insert X H) \<subseteq> parts (synth (analz H))"
   764   by (metis 5 2)
   765 have 7: "\<not> insert X H \<subseteq> synth (analz H)"
   766   by (metis 6 parts_mono)
   767 have 8: "X \<notin> synth (analz H) \<or> \<not> H \<subseteq> synth (analz H)"
   768   by (metis 7 insert_subset)
   769 have 9: "\<not> H \<subseteq> synth (analz H)"
   770   by (metis 8 0)
   771 have 10: "\<And>X3. X3 \<subseteq> analz (synth X3)"
   772   by (metis analz_subset_iff 4)
   773 have 11: "\<And>X3. X3 \<subseteq> analz (synth (analz X3))"
   774   by (metis analz_subset_iff 10)
   775 have 12: "\<And>X3. analz (synth (analz X3)) = synth (analz X3) \<or>
   776      \<not> analz X3 \<subseteq> synth (analz X3)"
   777   by (metis Un_absorb1 3)
   778 have 13: "\<And>X3. analz (synth (analz X3)) = synth (analz X3)"
   779   by (metis 12 synth_increasing)
   780 have 14: "\<And>X3. X3 \<subseteq> synth (analz X3)"
   781   by (metis 11 13)
   782 show "False"
   783   by (metis 9 14)
   784 qed
   785 
   786 lemma Fake_parts_insert_in_Un:
   787      "[|Z \<in> parts (insert X H);  X: synth (analz H)|] 
   788       ==> Z \<in>  synth (analz H) \<union> parts H";
   789 by (blast dest: Fake_parts_insert  [THEN subsetD, dest])
   790 
   791 ML{*ResAtp.problem_name := "Message__Fake_analz_insert"*}
   792     declare analz_mono [intro] synth_mono [intro] 
   793 lemma Fake_analz_insert:
   794      "X\<in> synth (analz G) ==>  
   795       analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
   796 by (metis Un_commute Un_insert_left Un_insert_right Un_upper1 analz_analz_Un analz_mono analz_synth_Un equalityE insert_absorb order_le_less xt1(12))
   797 
   798 ML{*ResAtp.problem_name := "Message__Fake_analz_insert_simpler"*}
   799 (*simpler problems?  BUT METIS CAN'T PROVE
   800 lemma Fake_analz_insert_simpler:
   801      "X\<in> synth (analz G) ==>  
   802       analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
   803 apply (rule subsetI)
   804 apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> H) ")
   805 apply (metis Un_commute analz_analz_Un analz_synth_Un)
   806 apply (metis Un_commute Un_upper1 Un_upper2 analz_cut analz_increasing analz_mono insert_absorb insert_mono insert_subset)
   807 done
   808 *)
   809 
   810 end