src/HOL/Metis_Examples/Message.thy
author wenzelm
Thu Feb 11 21:33:25 2010 +0100 (2010-02-11)
changeset 35109 0015a0a99ae9
parent 35095 6cdf9bbd0342
child 35416 d8d7d1b785af
permissions -rw-r--r--
modernized syntax/translations;
     1 (*  Title:      HOL/MetisTest/Message.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3 
     4 Testing the metis method.
     5 *)
     6 
     7 theory Message imports Main begin
     8 
     9 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
    10 lemma strange_Un_eq [simp]: "A \<union> (B \<union> A) = B \<union> A"
    11 by blast
    12 
    13 types 
    14   key = nat
    15 
    16 consts
    17   all_symmetric :: bool        --{*true if all keys are symmetric*}
    18   invKey        :: "key=>key"  --{*inverse of a symmetric key*}
    19 
    20 specification (invKey)
    21   invKey [simp]: "invKey (invKey K) = K"
    22   invKey_symmetric: "all_symmetric --> invKey = id"
    23     by (rule exI [of _ id], auto)
    24 
    25 
    26 text{*The inverse of a symmetric key is itself; that of a public key
    27       is the private key and vice versa*}
    28 
    29 constdefs
    30   symKeys :: "key set"
    31   "symKeys == {K. invKey K = K}"
    32 
    33 datatype  --{*We allow any number of friendly agents*}
    34   agent = Server | Friend nat | Spy
    35 
    36 datatype
    37      msg = Agent  agent     --{*Agent names*}
    38          | Number nat       --{*Ordinary integers, timestamps, ...*}
    39          | Nonce  nat       --{*Unguessable nonces*}
    40          | Key    key       --{*Crypto keys*}
    41          | Hash   msg       --{*Hashing*}
    42          | MPair  msg msg   --{*Compound messages*}
    43          | Crypt  key msg   --{*Encryption, public- or shared-key*}
    44 
    45 
    46 text{*Concrete syntax: messages appear as {|A,B,NA|}, etc...*}
    47 syntax
    48   "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
    49 
    50 syntax (xsymbols)
    51   "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
    52 
    53 translations
    54   "{|x, y, z|}"   == "{|x, {|y, z|}|}"
    55   "{|x, y|}"      == "CONST MPair x y"
    56 
    57 
    58 constdefs
    59   HPair :: "[msg,msg] => msg"                       ("(4Hash[_] /_)" [0, 1000])
    60     --{*Message Y paired with a MAC computed with the help of X*}
    61     "Hash[X] Y == {| Hash{|X,Y|}, Y|}"
    62 
    63   keysFor :: "msg set => key set"
    64     --{*Keys useful to decrypt elements of a message set*}
    65   "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"
    66 
    67 
    68 subsubsection{*Inductive Definition of All Parts" of a Message*}
    69 
    70 inductive_set
    71   parts :: "msg set => msg set"
    72   for H :: "msg set"
    73   where
    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 declare [[ atp_problem_prefix = "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 declare [[ atp_problem_prefix = "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 fast+
   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 declare [[ atp_problem_prefix = "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 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 declare [[ atp_problem_prefix = "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_idem 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 declare [[ atp_problem_prefix = "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_insert_left Un_insert_right insert_absorb mem_def parts_Un parts_idem sup1CI)
   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 declare [[ atp_problem_prefix = "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 inductive_set
   333   analz :: "msg set => msg set"
   334   for H :: "msg set"
   335   where
   336     Inj [intro,simp] :    "X \<in> H ==> X \<in> analz H"
   337   | Fst:     "{|X,Y|} \<in> analz H ==> X \<in> analz H"
   338   | Snd:     "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
   339   | Decrypt [dest]: 
   340              "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
   341 
   342 
   343 text{*Monotonicity; Lemma 1 of Lowe's paper*}
   344 lemma analz_mono: "G\<subseteq>H ==> analz(G) \<subseteq> analz(H)"
   345 apply auto
   346 apply (erule analz.induct) 
   347 apply (auto dest: analz.Fst analz.Snd) 
   348 done
   349 
   350 text{*Making it safe speeds up proofs*}
   351 lemma MPair_analz [elim!]:
   352      "[| {|X,Y|} \<in> analz H;        
   353              [| X \<in> analz H; Y \<in> analz H |] ==> P   
   354           |] ==> P"
   355 by (blast dest: analz.Fst analz.Snd)
   356 
   357 lemma analz_increasing: "H \<subseteq> analz(H)"
   358 by blast
   359 
   360 lemma analz_subset_parts: "analz H \<subseteq> parts H"
   361 apply (rule subsetI)
   362 apply (erule analz.induct, blast+)
   363 done
   364 
   365 lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
   366 
   367 lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
   368 
   369 
   370 declare [[ atp_problem_prefix = "Message__parts_analz" ]]
   371 lemma parts_analz [simp]: "parts (analz H) = parts H"
   372 apply (rule equalityI)
   373 apply (metis analz_subset_parts parts_subset_iff)
   374 apply (metis analz_increasing parts_mono)
   375 done
   376 
   377 
   378 lemma analz_parts [simp]: "analz (parts H) = parts H"
   379 apply auto
   380 apply (erule analz.induct, auto)
   381 done
   382 
   383 lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
   384 
   385 subsubsection{*General equational properties *}
   386 
   387 lemma analz_empty [simp]: "analz{} = {}"
   388 apply safe
   389 apply (erule analz.induct, blast+)
   390 done
   391 
   392 text{*Converse fails: we can analz more from the union than from the 
   393   separate parts, as a key in one might decrypt a message in the other*}
   394 lemma analz_Un: "analz(G) \<union> analz(H) \<subseteq> analz(G \<union> H)"
   395 by (intro Un_least analz_mono Un_upper1 Un_upper2)
   396 
   397 lemma analz_insert: "insert X (analz H) \<subseteq> analz(insert X H)"
   398 by (blast intro: analz_mono [THEN [2] rev_subsetD])
   399 
   400 subsubsection{*Rewrite rules for pulling out atomic messages *}
   401 
   402 lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert]
   403 
   404 lemma analz_insert_Agent [simp]:
   405      "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"
   406 apply (rule analz_insert_eq_I) 
   407 apply (erule analz.induct, auto) 
   408 done
   409 
   410 lemma analz_insert_Nonce [simp]:
   411      "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"
   412 apply (rule analz_insert_eq_I) 
   413 apply (erule analz.induct, auto) 
   414 done
   415 
   416 lemma analz_insert_Number [simp]:
   417      "analz (insert (Number N) H) = insert (Number N) (analz H)"
   418 apply (rule analz_insert_eq_I) 
   419 apply (erule analz.induct, auto) 
   420 done
   421 
   422 lemma analz_insert_Hash [simp]:
   423      "analz (insert (Hash X) H) = insert (Hash X) (analz H)"
   424 apply (rule analz_insert_eq_I) 
   425 apply (erule analz.induct, auto) 
   426 done
   427 
   428 text{*Can only pull out Keys if they are not needed to decrypt the rest*}
   429 lemma analz_insert_Key [simp]: 
   430     "K \<notin> keysFor (analz H) ==>   
   431           analz (insert (Key K) H) = insert (Key K) (analz H)"
   432 apply (unfold keysFor_def)
   433 apply (rule analz_insert_eq_I) 
   434 apply (erule analz.induct, auto) 
   435 done
   436 
   437 lemma analz_insert_MPair [simp]:
   438      "analz (insert {|X,Y|} H) =  
   439           insert {|X,Y|} (analz (insert X (insert Y H)))"
   440 apply (rule equalityI)
   441 apply (rule subsetI)
   442 apply (erule analz.induct, auto)
   443 apply (erule analz.induct)
   444 apply (blast intro: analz.Fst analz.Snd)+
   445 done
   446 
   447 text{*Can pull out enCrypted message if the Key is not known*}
   448 lemma analz_insert_Crypt:
   449      "Key (invKey K) \<notin> analz H 
   450       ==> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)"
   451 apply (rule analz_insert_eq_I) 
   452 apply (erule analz.induct, auto) 
   453 
   454 done
   455 
   456 lemma lemma1: "Key (invKey K) \<in> analz H ==>   
   457                analz (insert (Crypt K X) H) \<subseteq>  
   458                insert (Crypt K X) (analz (insert X H))" 
   459 apply (rule subsetI)
   460 apply (erule_tac x = x in analz.induct, auto)
   461 done
   462 
   463 lemma lemma2: "Key (invKey K) \<in> analz H ==>   
   464                insert (Crypt K X) (analz (insert X H)) \<subseteq>  
   465                analz (insert (Crypt K X) H)"
   466 apply auto
   467 apply (erule_tac x = x in analz.induct, auto)
   468 apply (blast intro: analz_insertI analz.Decrypt)
   469 done
   470 
   471 lemma analz_insert_Decrypt:
   472      "Key (invKey K) \<in> analz H ==>   
   473                analz (insert (Crypt K X) H) =  
   474                insert (Crypt K X) (analz (insert X H))"
   475 by (intro equalityI lemma1 lemma2)
   476 
   477 text{*Case analysis: either the message is secure, or it is not! Effective,
   478 but can cause subgoals to blow up! Use with @{text "split_if"}; apparently
   479 @{text "split_tac"} does not cope with patterns such as @{term"analz (insert
   480 (Crypt K X) H)"} *} 
   481 lemma analz_Crypt_if [simp]:
   482      "analz (insert (Crypt K X) H) =                 
   483           (if (Key (invKey K) \<in> analz H)                 
   484            then insert (Crypt K X) (analz (insert X H))  
   485            else insert (Crypt K X) (analz H))"
   486 by (simp add: analz_insert_Crypt analz_insert_Decrypt)
   487 
   488 
   489 text{*This rule supposes "for the sake of argument" that we have the key.*}
   490 lemma analz_insert_Crypt_subset:
   491      "analz (insert (Crypt K X) H) \<subseteq>   
   492            insert (Crypt K X) (analz (insert X H))"
   493 apply (rule subsetI)
   494 apply (erule analz.induct, auto)
   495 done
   496 
   497 
   498 lemma analz_image_Key [simp]: "analz (Key`N) = Key`N"
   499 apply auto
   500 apply (erule analz.induct, auto)
   501 done
   502 
   503 
   504 subsubsection{*Idempotence and transitivity *}
   505 
   506 lemma analz_analzD [dest!]: "X\<in> analz (analz H) ==> X\<in> analz H"
   507 by (erule analz.induct, blast+)
   508 
   509 lemma analz_idem [simp]: "analz (analz H) = analz H"
   510 by blast
   511 
   512 lemma analz_subset_iff [simp]: "(analz G \<subseteq> analz H) = (G \<subseteq> analz H)"
   513 apply (rule iffI)
   514 apply (iprover intro: subset_trans analz_increasing)  
   515 apply (frule analz_mono, simp) 
   516 done
   517 
   518 lemma analz_trans: "[| X\<in> analz G;  G \<subseteq> analz H |] ==> X\<in> analz H"
   519 by (drule analz_mono, blast)
   520 
   521 
   522 declare [[ atp_problem_prefix = "Message__analz_cut" ]]
   523     declare analz_trans[intro]
   524 lemma analz_cut: "[| Y\<in> analz (insert X H);  X\<in> analz H |] ==> Y\<in> analz H"
   525 (*TOO SLOW
   526 by (metis analz_idem analz_increasing analz_mono insert_absorb insert_mono insert_subset) --{*317s*}
   527 ??*)
   528 by (erule analz_trans, blast)
   529 
   530 
   531 text{*This rewrite rule helps in the simplification of messages that involve
   532   the forwarding of unknown components (X).  Without it, removing occurrences
   533   of X can be very complicated. *}
   534 lemma analz_insert_eq: "X\<in> analz H ==> analz (insert X H) = analz H"
   535 by (blast intro: analz_cut analz_insertI)
   536 
   537 
   538 text{*A congruence rule for "analz" *}
   539 
   540 declare [[ atp_problem_prefix = "Message__analz_subset_cong" ]]
   541 lemma analz_subset_cong:
   542      "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H' |] 
   543       ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
   544 apply simp
   545 apply (metis Un_absorb2 Un_commute Un_subset_iff Un_upper1 Un_upper2 analz_mono)
   546 done
   547 
   548 
   549 lemma analz_cong:
   550      "[| analz G = analz G'; analz H = analz H'  
   551                |] ==> analz (G \<union> H) = analz (G' \<union> H')"
   552 by (intro equalityI analz_subset_cong, simp_all) 
   553 
   554 lemma analz_insert_cong:
   555      "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"
   556 by (force simp only: insert_def intro!: analz_cong)
   557 
   558 text{*If there are no pairs or encryptions then analz does nothing*}
   559 lemma analz_trivial:
   560      "[| \<forall>X Y. {|X,Y|} \<notin> H;  \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
   561 apply safe
   562 apply (erule analz.induct, blast+)
   563 done
   564 
   565 text{*These two are obsolete (with a single Spy) but cost little to prove...*}
   566 lemma analz_UN_analz_lemma:
   567      "X\<in> analz (\<Union>i\<in>A. analz (H i)) ==> X\<in> analz (\<Union>i\<in>A. H i)"
   568 apply (erule analz.induct)
   569 apply (blast intro: analz_mono [THEN [2] rev_subsetD])+
   570 done
   571 
   572 lemma analz_UN_analz [simp]: "analz (\<Union>i\<in>A. analz (H i)) = analz (\<Union>i\<in>A. H i)"
   573 by (blast intro: analz_UN_analz_lemma analz_mono [THEN [2] rev_subsetD])
   574 
   575 
   576 subsection{*Inductive relation "synth"*}
   577 
   578 text{*Inductive definition of "synth" -- what can be built up from a set of
   579     messages.  A form of upward closure.  Pairs can be built, messages
   580     encrypted with known keys.  Agent names are public domain.
   581     Numbers can be guessed, but Nonces cannot be.  *}
   582 
   583 inductive_set
   584   synth :: "msg set => msg set"
   585   for H :: "msg set"
   586   where
   587     Inj    [intro]:   "X \<in> H ==> X \<in> synth H"
   588   | Agent  [intro]:   "Agent agt \<in> synth H"
   589   | Number [intro]:   "Number n  \<in> synth H"
   590   | Hash   [intro]:   "X \<in> synth H ==> Hash X \<in> synth H"
   591   | MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
   592   | Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
   593 
   594 text{*Monotonicity*}
   595 lemma synth_mono: "G\<subseteq>H ==> synth(G) \<subseteq> synth(H)"
   596   by (auto, erule synth.induct, auto)  
   597 
   598 text{*NO @{text Agent_synth}, as any Agent name can be synthesized.  
   599   The same holds for @{term Number}*}
   600 inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H"
   601 inductive_cases Key_synth   [elim!]: "Key K \<in> synth H"
   602 inductive_cases Hash_synth  [elim!]: "Hash X \<in> synth H"
   603 inductive_cases MPair_synth [elim!]: "{|X,Y|} \<in> synth H"
   604 inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
   605 
   606 
   607 lemma synth_increasing: "H \<subseteq> synth(H)"
   608 by blast
   609 
   610 subsubsection{*Unions *}
   611 
   612 text{*Converse fails: we can synth more from the union than from the 
   613   separate parts, building a compound message using elements of each.*}
   614 lemma synth_Un: "synth(G) \<union> synth(H) \<subseteq> synth(G \<union> H)"
   615 by (intro Un_least synth_mono Un_upper1 Un_upper2)
   616 
   617 
   618 declare [[ atp_problem_prefix = "Message__synth_insert" ]]
   619  
   620 lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)"
   621 by (metis insert_iff insert_subset subset_insertI synth.Inj synth_mono)
   622 
   623 subsubsection{*Idempotence and transitivity *}
   624 
   625 lemma synth_synthD [dest!]: "X\<in> synth (synth H) ==> X\<in> synth H"
   626 by (erule synth.induct, blast+)
   627 
   628 lemma synth_idem: "synth (synth H) = synth H"
   629 by blast
   630 
   631 lemma synth_subset_iff [simp]: "(synth G \<subseteq> synth H) = (G \<subseteq> synth H)"
   632 apply (rule iffI)
   633 apply (iprover intro: subset_trans synth_increasing)  
   634 apply (frule synth_mono, simp add: synth_idem) 
   635 done
   636 
   637 lemma synth_trans: "[| X\<in> synth G;  G \<subseteq> synth H |] ==> X\<in> synth H"
   638 by (drule synth_mono, blast)
   639 
   640 declare [[ atp_problem_prefix = "Message__synth_cut" ]]
   641 lemma synth_cut: "[| Y\<in> synth (insert X H);  X\<in> synth H |] ==> Y\<in> synth H"
   642 (*TOO SLOW
   643 by (metis insert_absorb insert_mono insert_subset synth_idem synth_increasing synth_mono)
   644 *)
   645 by (erule synth_trans, blast)
   646 
   647 
   648 lemma Agent_synth [simp]: "Agent A \<in> synth H"
   649 by blast
   650 
   651 lemma Number_synth [simp]: "Number n \<in> synth H"
   652 by blast
   653 
   654 lemma Nonce_synth_eq [simp]: "(Nonce N \<in> synth H) = (Nonce N \<in> H)"
   655 by blast
   656 
   657 lemma Key_synth_eq [simp]: "(Key K \<in> synth H) = (Key K \<in> H)"
   658 by blast
   659 
   660 lemma Crypt_synth_eq [simp]:
   661      "Key K \<notin> H ==> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)"
   662 by blast
   663 
   664 
   665 lemma keysFor_synth [simp]: 
   666     "keysFor (synth H) = keysFor H \<union> invKey`{K. Key K \<in> H}"
   667 by (unfold keysFor_def, blast)
   668 
   669 
   670 subsubsection{*Combinations of parts, analz and synth *}
   671 
   672 declare [[ atp_problem_prefix = "Message__parts_synth" ]]
   673 lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"
   674 apply (rule equalityI)
   675 apply (rule subsetI)
   676 apply (erule parts.induct)
   677 apply (metis UnCI)
   678 apply (metis MPair_synth UnCI UnE insert_absorb insert_subset parts.Fst parts_increasing)
   679 apply (metis MPair_synth UnCI UnE insert_absorb insert_subset parts.Snd parts_increasing)
   680 apply (metis Body Crypt_synth UnCI UnE insert_absorb insert_subset parts_increasing)
   681 apply (metis Un_subset_iff parts_increasing parts_mono synth_increasing)
   682 done
   683 
   684 
   685 
   686 
   687 declare [[ atp_problem_prefix = "Message__analz_analz_Un" ]]
   688 lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)"
   689 apply (rule equalityI);
   690 apply (metis analz_idem analz_subset_cong order_eq_refl)
   691 apply (metis analz_increasing analz_subset_cong order_eq_refl)
   692 done
   693 
   694 declare [[ atp_problem_prefix = "Message__analz_synth_Un" ]]
   695     declare analz_mono [intro] analz.Fst [intro] analz.Snd [intro] Un_least [intro]
   696 lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G"
   697 apply (rule equalityI)
   698 apply (rule subsetI)
   699 apply (erule analz.induct)
   700 apply (metis UnCI UnE Un_commute analz.Inj)
   701 apply (metis MPair_synth UnCI UnE Un_commute analz.Fst analz.Inj mem_def)
   702 apply (metis MPair_synth UnCI UnE Un_commute analz.Inj analz.Snd mem_def)
   703 apply (blast intro: analz.Decrypt)
   704 apply blast
   705 done
   706 
   707 declare [[ atp_problem_prefix = "Message__analz_synth" ]]
   708 lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
   709 proof (neg_clausify)
   710 assume 0: "analz (synth H) \<noteq> analz H \<union> synth H"
   711 have 1: "\<And>X1 X3. sup (analz (sup X3 X1)) (synth X3) = analz (sup (synth X3) X1)"
   712   by (metis analz_synth_Un)
   713 have 2: "sup (analz H) (synth H) \<noteq> analz (synth H)"
   714   by (metis 0)
   715 have 3: "\<And>X1 X3. sup (synth X3) (analz (sup X3 X1)) = analz (sup (synth X3) X1)"
   716   by (metis 1 Un_commute)
   717 have 4: "\<And>X3. sup (synth X3) (analz X3) = analz (sup (synth X3) {})"
   718   by (metis 3 Un_empty_right)
   719 have 5: "\<And>X3. sup (synth X3) (analz X3) = analz (synth X3)"
   720   by (metis 4 Un_empty_right)
   721 have 6: "\<And>X3. sup (analz X3) (synth X3) = analz (synth X3)"
   722   by (metis 5 Un_commute)
   723 show "False"
   724   by (metis 2 6)
   725 qed
   726 
   727 
   728 subsubsection{*For reasoning about the Fake rule in traces *}
   729 
   730 declare [[ atp_problem_prefix = "Message__parts_insert_subset_Un" ]]
   731 lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
   732 proof (neg_clausify)
   733 assume 0: "X \<in> G"
   734 assume 1: "\<not> parts (insert X H) \<subseteq> parts G \<union> parts H"
   735 have 2: "\<not> parts (insert X H) \<subseteq> parts (G \<union> H)"
   736   by (metis 1 parts_Un)
   737 have 3: "\<not> insert X H \<subseteq> G \<union> H"
   738   by (metis 2 parts_mono)
   739 have 4: "X \<notin> G \<union> H \<or> \<not> H \<subseteq> G \<union> H"
   740   by (metis 3 insert_subset)
   741 have 5: "X \<notin> G \<union> H"
   742   by (metis 4 Un_upper2)
   743 have 6: "X \<notin> G"
   744   by (metis 5 UnCI)
   745 show "False"
   746   by (metis 6 0)
   747 qed
   748 
   749 declare [[ atp_problem_prefix = "Message__Fake_parts_insert" ]]
   750 lemma Fake_parts_insert:
   751      "X \<in> synth (analz H) ==>  
   752       parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
   753 proof (neg_clausify)
   754 assume 0: "X \<in> synth (analz H)"
   755 assume 1: "\<not> parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
   756 have 2: "\<And>X3. parts X3 \<union> synth (analz X3) = parts (synth (analz X3))"
   757   by (metis parts_synth parts_analz)
   758 have 3: "\<And>X3. analz X3 \<union> synth (analz X3) = analz (synth (analz X3))"
   759   by (metis analz_synth analz_idem)
   760 have 4: "\<And>X3. analz X3 \<subseteq> analz (synth X3)"
   761   by (metis Un_upper1 analz_synth)
   762 have 5: "\<not> parts (insert X H) \<subseteq> parts H \<union> synth (analz H)"
   763   by (metis 1 Un_commute)
   764 have 6: "\<not> parts (insert X H) \<subseteq> parts (synth (analz H))"
   765   by (metis 5 2)
   766 have 7: "\<not> insert X H \<subseteq> synth (analz H)"
   767   by (metis 6 parts_mono)
   768 have 8: "X \<notin> synth (analz H) \<or> \<not> H \<subseteq> synth (analz H)"
   769   by (metis 7 insert_subset)
   770 have 9: "\<not> H \<subseteq> synth (analz H)"
   771   by (metis 8 0)
   772 have 10: "\<And>X3. X3 \<subseteq> analz (synth X3)"
   773   by (metis analz_subset_iff 4)
   774 have 11: "\<And>X3. X3 \<subseteq> analz (synth (analz X3))"
   775   by (metis analz_subset_iff 10)
   776 have 12: "\<And>X3. analz (synth (analz X3)) = synth (analz X3) \<or>
   777      \<not> analz X3 \<subseteq> synth (analz X3)"
   778   by (metis Un_absorb1 3)
   779 have 13: "\<And>X3. analz (synth (analz X3)) = synth (analz X3)"
   780   by (metis 12 synth_increasing)
   781 have 14: "\<And>X3. X3 \<subseteq> synth (analz X3)"
   782   by (metis 11 13)
   783 show "False"
   784   by (metis 9 14)
   785 qed
   786 
   787 lemma Fake_parts_insert_in_Un:
   788      "[|Z \<in> parts (insert X H);  X: synth (analz H)|] 
   789       ==> Z \<in>  synth (analz H) \<union> parts H";
   790 by (blast dest: Fake_parts_insert  [THEN subsetD, dest])
   791 
   792 declare [[ atp_problem_prefix = "Message__Fake_analz_insert" ]]
   793     declare analz_mono [intro] synth_mono [intro] 
   794 lemma Fake_analz_insert:
   795      "X\<in> synth (analz G) ==>  
   796       analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
   797 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))
   798 
   799 declare [[ atp_problem_prefix = "Message__Fake_analz_insert_simpler" ]]
   800 (*simpler problems?  BUT METIS CAN'T PROVE
   801 lemma Fake_analz_insert_simpler:
   802      "X\<in> synth (analz G) ==>  
   803       analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
   804 apply (rule subsetI)
   805 apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> H) ")
   806 apply (metis Un_commute analz_analz_Un analz_synth_Un)
   807 apply (metis Un_commute Un_upper1 Un_upper2 analz_cut analz_increasing analz_mono insert_absorb insert_mono insert_subset)
   808 done
   809 *)
   810 
   811 end