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