src/HOL/Metis_Examples/Message.thy
changeset 33027 9cf389429f6d
parent 32960 69916a850301
child 35054 a5db9779b026
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Metis_Examples/Message.thy	Tue Oct 20 19:52:04 2009 +0200
     1.3 @@ -0,0 +1,812 @@
     1.4 +(*  Title:      HOL/MetisTest/Message.thy
     1.5 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.6 +
     1.7 +Testing the metis method.
     1.8 +*)
     1.9 +
    1.10 +theory Message imports Main begin
    1.11 +
    1.12 +(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
    1.13 +lemma strange_Un_eq [simp]: "A \<union> (B \<union> A) = B \<union> A"
    1.14 +by blast
    1.15 +
    1.16 +types 
    1.17 +  key = nat
    1.18 +
    1.19 +consts
    1.20 +  all_symmetric :: bool        --{*true if all keys are symmetric*}
    1.21 +  invKey        :: "key=>key"  --{*inverse of a symmetric key*}
    1.22 +
    1.23 +specification (invKey)
    1.24 +  invKey [simp]: "invKey (invKey K) = K"
    1.25 +  invKey_symmetric: "all_symmetric --> invKey = id"
    1.26 +    by (rule exI [of _ id], auto)
    1.27 +
    1.28 +
    1.29 +text{*The inverse of a symmetric key is itself; that of a public key
    1.30 +      is the private key and vice versa*}
    1.31 +
    1.32 +constdefs
    1.33 +  symKeys :: "key set"
    1.34 +  "symKeys == {K. invKey K = K}"
    1.35 +
    1.36 +datatype  --{*We allow any number of friendly agents*}
    1.37 +  agent = Server | Friend nat | Spy
    1.38 +
    1.39 +datatype
    1.40 +     msg = Agent  agent     --{*Agent names*}
    1.41 +         | Number nat       --{*Ordinary integers, timestamps, ...*}
    1.42 +         | Nonce  nat       --{*Unguessable nonces*}
    1.43 +         | Key    key       --{*Crypto keys*}
    1.44 +         | Hash   msg       --{*Hashing*}
    1.45 +         | MPair  msg msg   --{*Compound messages*}
    1.46 +         | Crypt  key msg   --{*Encryption, public- or shared-key*}
    1.47 +
    1.48 +
    1.49 +text{*Concrete syntax: messages appear as {|A,B,NA|}, etc...*}
    1.50 +syntax
    1.51 +  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
    1.52 +
    1.53 +syntax (xsymbols)
    1.54 +  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
    1.55 +
    1.56 +translations
    1.57 +  "{|x, y, z|}"   == "{|x, {|y, z|}|}"
    1.58 +  "{|x, y|}"      == "MPair x y"
    1.59 +
    1.60 +
    1.61 +constdefs
    1.62 +  HPair :: "[msg,msg] => msg"                       ("(4Hash[_] /_)" [0, 1000])
    1.63 +    --{*Message Y paired with a MAC computed with the help of X*}
    1.64 +    "Hash[X] Y == {| Hash{|X,Y|}, Y|}"
    1.65 +
    1.66 +  keysFor :: "msg set => key set"
    1.67 +    --{*Keys useful to decrypt elements of a message set*}
    1.68 +  "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"
    1.69 +
    1.70 +
    1.71 +subsubsection{*Inductive Definition of All Parts" of a Message*}
    1.72 +
    1.73 +inductive_set
    1.74 +  parts :: "msg set => msg set"
    1.75 +  for H :: "msg set"
    1.76 +  where
    1.77 +    Inj [intro]:               "X \<in> H ==> X \<in> parts H"
    1.78 +  | Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
    1.79 +  | Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
    1.80 +  | Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
    1.81 +
    1.82 +
    1.83 +declare [[ atp_problem_prefix = "Message__parts_mono" ]]
    1.84 +lemma parts_mono: "G \<subseteq> H ==> parts(G) \<subseteq> parts(H)"
    1.85 +apply auto
    1.86 +apply (erule parts.induct) 
    1.87 +apply (metis Inj set_mp)
    1.88 +apply (metis Fst)
    1.89 +apply (metis Snd)
    1.90 +apply (metis Body)
    1.91 +done
    1.92 +
    1.93 +
    1.94 +text{*Equations hold because constructors are injective.*}
    1.95 +lemma Friend_image_eq [simp]: "(Friend x \<in> Friend`A) = (x:A)"
    1.96 +by auto
    1.97 +
    1.98 +lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x\<in>A)"
    1.99 +by auto
   1.100 +
   1.101 +lemma Nonce_Key_image_eq [simp]: "(Nonce x \<notin> Key`A)"
   1.102 +by auto
   1.103 +
   1.104 +
   1.105 +subsubsection{*Inverse of keys *}
   1.106 +
   1.107 +declare [[ atp_problem_prefix = "Message__invKey_eq" ]]
   1.108 +lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
   1.109 +by (metis invKey)
   1.110 +
   1.111 +
   1.112 +subsection{*keysFor operator*}
   1.113 +
   1.114 +lemma keysFor_empty [simp]: "keysFor {} = {}"
   1.115 +by (unfold keysFor_def, blast)
   1.116 +
   1.117 +lemma keysFor_Un [simp]: "keysFor (H \<union> H') = keysFor H \<union> keysFor H'"
   1.118 +by (unfold keysFor_def, blast)
   1.119 +
   1.120 +lemma keysFor_UN [simp]: "keysFor (\<Union>i\<in>A. H i) = (\<Union>i\<in>A. keysFor (H i))"
   1.121 +by (unfold keysFor_def, blast)
   1.122 +
   1.123 +text{*Monotonicity*}
   1.124 +lemma keysFor_mono: "G \<subseteq> H ==> keysFor(G) \<subseteq> keysFor(H)"
   1.125 +by (unfold keysFor_def, blast)
   1.126 +
   1.127 +lemma keysFor_insert_Agent [simp]: "keysFor (insert (Agent A) H) = keysFor H"
   1.128 +by (unfold keysFor_def, auto)
   1.129 +
   1.130 +lemma keysFor_insert_Nonce [simp]: "keysFor (insert (Nonce N) H) = keysFor H"
   1.131 +by (unfold keysFor_def, auto)
   1.132 +
   1.133 +lemma keysFor_insert_Number [simp]: "keysFor (insert (Number N) H) = keysFor H"
   1.134 +by (unfold keysFor_def, auto)
   1.135 +
   1.136 +lemma keysFor_insert_Key [simp]: "keysFor (insert (Key K) H) = keysFor H"
   1.137 +by (unfold keysFor_def, auto)
   1.138 +
   1.139 +lemma keysFor_insert_Hash [simp]: "keysFor (insert (Hash X) H) = keysFor H"
   1.140 +by (unfold keysFor_def, auto)
   1.141 +
   1.142 +lemma keysFor_insert_MPair [simp]: "keysFor (insert {|X,Y|} H) = keysFor H"
   1.143 +by (unfold keysFor_def, auto)
   1.144 +
   1.145 +lemma keysFor_insert_Crypt [simp]: 
   1.146 +    "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"
   1.147 +by (unfold keysFor_def, auto)
   1.148 +
   1.149 +lemma keysFor_image_Key [simp]: "keysFor (Key`E) = {}"
   1.150 +by (unfold keysFor_def, auto)
   1.151 +
   1.152 +lemma Crypt_imp_invKey_keysFor: "Crypt K X \<in> H ==> invKey K \<in> keysFor H"
   1.153 +by (unfold keysFor_def, blast)
   1.154 +
   1.155 +
   1.156 +subsection{*Inductive relation "parts"*}
   1.157 +
   1.158 +lemma MPair_parts:
   1.159 +     "[| {|X,Y|} \<in> parts H;        
   1.160 +         [| X \<in> parts H; Y \<in> parts H |] ==> P |] ==> P"
   1.161 +by (blast dest: parts.Fst parts.Snd) 
   1.162 +
   1.163 +    declare MPair_parts [elim!]  parts.Body [dest!]
   1.164 +text{*NB These two rules are UNSAFE in the formal sense, as they discard the
   1.165 +     compound message.  They work well on THIS FILE.  
   1.166 +  @{text MPair_parts} is left as SAFE because it speeds up proofs.
   1.167 +  The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*}
   1.168 +
   1.169 +lemma parts_increasing: "H \<subseteq> parts(H)"
   1.170 +by blast
   1.171 +
   1.172 +lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD, standard]
   1.173 +
   1.174 +lemma parts_empty [simp]: "parts{} = {}"
   1.175 +apply safe
   1.176 +apply (erule parts.induct)
   1.177 +apply blast+
   1.178 +done
   1.179 +
   1.180 +lemma parts_emptyE [elim!]: "X\<in> parts{} ==> P"
   1.181 +by simp
   1.182 +
   1.183 +text{*WARNING: loops if H = {Y}, therefore must not be repeated!*}
   1.184 +lemma parts_singleton: "X\<in> parts H ==> \<exists>Y\<in>H. X\<in> parts {Y}"
   1.185 +apply (erule parts.induct)
   1.186 +apply fast+
   1.187 +done
   1.188 +
   1.189 +
   1.190 +subsubsection{*Unions *}
   1.191 +
   1.192 +lemma parts_Un_subset1: "parts(G) \<union> parts(H) \<subseteq> parts(G \<union> H)"
   1.193 +by (intro Un_least parts_mono Un_upper1 Un_upper2)
   1.194 +
   1.195 +lemma parts_Un_subset2: "parts(G \<union> H) \<subseteq> parts(G) \<union> parts(H)"
   1.196 +apply (rule subsetI)
   1.197 +apply (erule parts.induct, blast+)
   1.198 +done
   1.199 +
   1.200 +lemma parts_Un [simp]: "parts(G \<union> H) = parts(G) \<union> parts(H)"
   1.201 +by (intro equalityI parts_Un_subset1 parts_Un_subset2)
   1.202 +
   1.203 +lemma parts_insert: "parts (insert X H) = parts {X} \<union> parts H"
   1.204 +apply (subst insert_is_Un [of _ H])
   1.205 +apply (simp only: parts_Un)
   1.206 +done
   1.207 +
   1.208 +declare [[ atp_problem_prefix = "Message__parts_insert_two" ]]
   1.209 +lemma parts_insert2:
   1.210 +     "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
   1.211 +by (metis Un_commute Un_empty_left Un_empty_right Un_insert_left Un_insert_right parts_Un)
   1.212 +
   1.213 +
   1.214 +lemma parts_UN_subset1: "(\<Union>x\<in>A. parts(H x)) \<subseteq> parts(\<Union>x\<in>A. H x)"
   1.215 +by (intro UN_least parts_mono UN_upper)
   1.216 +
   1.217 +lemma parts_UN_subset2: "parts(\<Union>x\<in>A. H x) \<subseteq> (\<Union>x\<in>A. parts(H x))"
   1.218 +apply (rule subsetI)
   1.219 +apply (erule parts.induct, blast+)
   1.220 +done
   1.221 +
   1.222 +lemma parts_UN [simp]: "parts(\<Union>x\<in>A. H x) = (\<Union>x\<in>A. parts(H x))"
   1.223 +by (intro equalityI parts_UN_subset1 parts_UN_subset2)
   1.224 +
   1.225 +text{*Added to simplify arguments to parts, analz and synth.
   1.226 +  NOTE: the UN versions are no longer used!*}
   1.227 +
   1.228 +
   1.229 +text{*This allows @{text blast} to simplify occurrences of 
   1.230 +  @{term "parts(G\<union>H)"} in the assumption.*}
   1.231 +lemmas in_parts_UnE = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE] 
   1.232 +declare in_parts_UnE [elim!]
   1.233 +
   1.234 +lemma parts_insert_subset: "insert X (parts H) \<subseteq> parts(insert X H)"
   1.235 +by (blast intro: parts_mono [THEN [2] rev_subsetD])
   1.236 +
   1.237 +subsubsection{*Idempotence and transitivity *}
   1.238 +
   1.239 +lemma parts_partsD [dest!]: "X\<in> parts (parts H) ==> X\<in> parts H"
   1.240 +by (erule parts.induct, blast+)
   1.241 +
   1.242 +lemma parts_idem [simp]: "parts (parts H) = parts H"
   1.243 +by blast
   1.244 +
   1.245 +declare [[ atp_problem_prefix = "Message__parts_subset_iff" ]]
   1.246 +lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)"
   1.247 +apply (rule iffI) 
   1.248 +apply (metis Un_absorb1 Un_subset_iff parts_Un parts_increasing)
   1.249 +apply (metis parts_idem parts_mono)
   1.250 +done
   1.251 +
   1.252 +lemma parts_trans: "[| X\<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"
   1.253 +by (blast dest: parts_mono); 
   1.254 +
   1.255 +
   1.256 +declare [[ atp_problem_prefix = "Message__parts_cut" ]]
   1.257 +lemma parts_cut: "[|Y\<in> parts(insert X G);  X\<in> parts H|] ==> Y\<in> parts(G \<union> H)"
   1.258 +by (metis Un_subset_iff insert_subset parts_increasing parts_trans) 
   1.259 +
   1.260 +
   1.261 +
   1.262 +subsubsection{*Rewrite rules for pulling out atomic messages *}
   1.263 +
   1.264 +lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset]
   1.265 +
   1.266 +
   1.267 +lemma parts_insert_Agent [simp]:
   1.268 +     "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"
   1.269 +apply (rule parts_insert_eq_I) 
   1.270 +apply (erule parts.induct, auto) 
   1.271 +done
   1.272 +
   1.273 +lemma parts_insert_Nonce [simp]:
   1.274 +     "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"
   1.275 +apply (rule parts_insert_eq_I) 
   1.276 +apply (erule parts.induct, auto) 
   1.277 +done
   1.278 +
   1.279 +lemma parts_insert_Number [simp]:
   1.280 +     "parts (insert (Number N) H) = insert (Number N) (parts H)"
   1.281 +apply (rule parts_insert_eq_I) 
   1.282 +apply (erule parts.induct, auto) 
   1.283 +done
   1.284 +
   1.285 +lemma parts_insert_Key [simp]:
   1.286 +     "parts (insert (Key K) H) = insert (Key K) (parts H)"
   1.287 +apply (rule parts_insert_eq_I) 
   1.288 +apply (erule parts.induct, auto) 
   1.289 +done
   1.290 +
   1.291 +lemma parts_insert_Hash [simp]:
   1.292 +     "parts (insert (Hash X) H) = insert (Hash X) (parts H)"
   1.293 +apply (rule parts_insert_eq_I) 
   1.294 +apply (erule parts.induct, auto) 
   1.295 +done
   1.296 +
   1.297 +lemma parts_insert_Crypt [simp]:
   1.298 +     "parts (insert (Crypt K X) H) =  
   1.299 +          insert (Crypt K X) (parts (insert X H))"
   1.300 +apply (rule equalityI)
   1.301 +apply (rule subsetI)
   1.302 +apply (erule parts.induct, auto)
   1.303 +apply (blast intro: parts.Body)
   1.304 +done
   1.305 +
   1.306 +lemma parts_insert_MPair [simp]:
   1.307 +     "parts (insert {|X,Y|} H) =  
   1.308 +          insert {|X,Y|} (parts (insert X (insert Y H)))"
   1.309 +apply (rule equalityI)
   1.310 +apply (rule subsetI)
   1.311 +apply (erule parts.induct, auto)
   1.312 +apply (blast intro: parts.Fst parts.Snd)+
   1.313 +done
   1.314 +
   1.315 +lemma parts_image_Key [simp]: "parts (Key`N) = Key`N"
   1.316 +apply auto
   1.317 +apply (erule parts.induct, auto)
   1.318 +done
   1.319 +
   1.320 +
   1.321 +declare [[ atp_problem_prefix = "Message__msg_Nonce_supply" ]]
   1.322 +lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n --> Nonce n \<notin> parts {msg}"
   1.323 +apply (induct_tac "msg") 
   1.324 +apply (simp_all add: parts_insert2)
   1.325 +apply (metis Suc_n_not_le_n)
   1.326 +apply (metis le_trans linorder_linear)
   1.327 +done
   1.328 +
   1.329 +subsection{*Inductive relation "analz"*}
   1.330 +
   1.331 +text{*Inductive definition of "analz" -- what can be broken down from a set of
   1.332 +    messages, including keys.  A form of downward closure.  Pairs can
   1.333 +    be taken apart; messages decrypted with known keys.  *}
   1.334 +
   1.335 +inductive_set
   1.336 +  analz :: "msg set => msg set"
   1.337 +  for H :: "msg set"
   1.338 +  where
   1.339 +    Inj [intro,simp] :    "X \<in> H ==> X \<in> analz H"
   1.340 +  | Fst:     "{|X,Y|} \<in> analz H ==> X \<in> analz H"
   1.341 +  | Snd:     "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
   1.342 +  | Decrypt [dest]: 
   1.343 +             "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
   1.344 +
   1.345 +
   1.346 +text{*Monotonicity; Lemma 1 of Lowe's paper*}
   1.347 +lemma analz_mono: "G\<subseteq>H ==> analz(G) \<subseteq> analz(H)"
   1.348 +apply auto
   1.349 +apply (erule analz.induct) 
   1.350 +apply (auto dest: analz.Fst analz.Snd) 
   1.351 +done
   1.352 +
   1.353 +text{*Making it safe speeds up proofs*}
   1.354 +lemma MPair_analz [elim!]:
   1.355 +     "[| {|X,Y|} \<in> analz H;        
   1.356 +             [| X \<in> analz H; Y \<in> analz H |] ==> P   
   1.357 +          |] ==> P"
   1.358 +by (blast dest: analz.Fst analz.Snd)
   1.359 +
   1.360 +lemma analz_increasing: "H \<subseteq> analz(H)"
   1.361 +by blast
   1.362 +
   1.363 +lemma analz_subset_parts: "analz H \<subseteq> parts H"
   1.364 +apply (rule subsetI)
   1.365 +apply (erule analz.induct, blast+)
   1.366 +done
   1.367 +
   1.368 +lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
   1.369 +
   1.370 +lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
   1.371 +
   1.372 +
   1.373 +declare [[ atp_problem_prefix = "Message__parts_analz" ]]
   1.374 +lemma parts_analz [simp]: "parts (analz H) = parts H"
   1.375 +apply (rule equalityI)
   1.376 +apply (metis analz_subset_parts parts_subset_iff)
   1.377 +apply (metis analz_increasing parts_mono)
   1.378 +done
   1.379 +
   1.380 +
   1.381 +lemma analz_parts [simp]: "analz (parts H) = parts H"
   1.382 +apply auto
   1.383 +apply (erule analz.induct, auto)
   1.384 +done
   1.385 +
   1.386 +lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
   1.387 +
   1.388 +subsubsection{*General equational properties *}
   1.389 +
   1.390 +lemma analz_empty [simp]: "analz{} = {}"
   1.391 +apply safe
   1.392 +apply (erule analz.induct, blast+)
   1.393 +done
   1.394 +
   1.395 +text{*Converse fails: we can analz more from the union than from the 
   1.396 +  separate parts, as a key in one might decrypt a message in the other*}
   1.397 +lemma analz_Un: "analz(G) \<union> analz(H) \<subseteq> analz(G \<union> H)"
   1.398 +by (intro Un_least analz_mono Un_upper1 Un_upper2)
   1.399 +
   1.400 +lemma analz_insert: "insert X (analz H) \<subseteq> analz(insert X H)"
   1.401 +by (blast intro: analz_mono [THEN [2] rev_subsetD])
   1.402 +
   1.403 +subsubsection{*Rewrite rules for pulling out atomic messages *}
   1.404 +
   1.405 +lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert]
   1.406 +
   1.407 +lemma analz_insert_Agent [simp]:
   1.408 +     "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"
   1.409 +apply (rule analz_insert_eq_I) 
   1.410 +apply (erule analz.induct, auto) 
   1.411 +done
   1.412 +
   1.413 +lemma analz_insert_Nonce [simp]:
   1.414 +     "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"
   1.415 +apply (rule analz_insert_eq_I) 
   1.416 +apply (erule analz.induct, auto) 
   1.417 +done
   1.418 +
   1.419 +lemma analz_insert_Number [simp]:
   1.420 +     "analz (insert (Number N) H) = insert (Number N) (analz H)"
   1.421 +apply (rule analz_insert_eq_I) 
   1.422 +apply (erule analz.induct, auto) 
   1.423 +done
   1.424 +
   1.425 +lemma analz_insert_Hash [simp]:
   1.426 +     "analz (insert (Hash X) H) = insert (Hash X) (analz H)"
   1.427 +apply (rule analz_insert_eq_I) 
   1.428 +apply (erule analz.induct, auto) 
   1.429 +done
   1.430 +
   1.431 +text{*Can only pull out Keys if they are not needed to decrypt the rest*}
   1.432 +lemma analz_insert_Key [simp]: 
   1.433 +    "K \<notin> keysFor (analz H) ==>   
   1.434 +          analz (insert (Key K) H) = insert (Key K) (analz H)"
   1.435 +apply (unfold keysFor_def)
   1.436 +apply (rule analz_insert_eq_I) 
   1.437 +apply (erule analz.induct, auto) 
   1.438 +done
   1.439 +
   1.440 +lemma analz_insert_MPair [simp]:
   1.441 +     "analz (insert {|X,Y|} H) =  
   1.442 +          insert {|X,Y|} (analz (insert X (insert Y H)))"
   1.443 +apply (rule equalityI)
   1.444 +apply (rule subsetI)
   1.445 +apply (erule analz.induct, auto)
   1.446 +apply (erule analz.induct)
   1.447 +apply (blast intro: analz.Fst analz.Snd)+
   1.448 +done
   1.449 +
   1.450 +text{*Can pull out enCrypted message if the Key is not known*}
   1.451 +lemma analz_insert_Crypt:
   1.452 +     "Key (invKey K) \<notin> analz H 
   1.453 +      ==> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)"
   1.454 +apply (rule analz_insert_eq_I) 
   1.455 +apply (erule analz.induct, auto) 
   1.456 +
   1.457 +done
   1.458 +
   1.459 +lemma lemma1: "Key (invKey K) \<in> analz H ==>   
   1.460 +               analz (insert (Crypt K X) H) \<subseteq>  
   1.461 +               insert (Crypt K X) (analz (insert X H))" 
   1.462 +apply (rule subsetI)
   1.463 +apply (erule_tac x = x in analz.induct, auto)
   1.464 +done
   1.465 +
   1.466 +lemma lemma2: "Key (invKey K) \<in> analz H ==>   
   1.467 +               insert (Crypt K X) (analz (insert X H)) \<subseteq>  
   1.468 +               analz (insert (Crypt K X) H)"
   1.469 +apply auto
   1.470 +apply (erule_tac x = x in analz.induct, auto)
   1.471 +apply (blast intro: analz_insertI analz.Decrypt)
   1.472 +done
   1.473 +
   1.474 +lemma analz_insert_Decrypt:
   1.475 +     "Key (invKey K) \<in> analz H ==>   
   1.476 +               analz (insert (Crypt K X) H) =  
   1.477 +               insert (Crypt K X) (analz (insert X H))"
   1.478 +by (intro equalityI lemma1 lemma2)
   1.479 +
   1.480 +text{*Case analysis: either the message is secure, or it is not! Effective,
   1.481 +but can cause subgoals to blow up! Use with @{text "split_if"}; apparently
   1.482 +@{text "split_tac"} does not cope with patterns such as @{term"analz (insert
   1.483 +(Crypt K X) H)"} *} 
   1.484 +lemma analz_Crypt_if [simp]:
   1.485 +     "analz (insert (Crypt K X) H) =                 
   1.486 +          (if (Key (invKey K) \<in> analz H)                 
   1.487 +           then insert (Crypt K X) (analz (insert X H))  
   1.488 +           else insert (Crypt K X) (analz H))"
   1.489 +by (simp add: analz_insert_Crypt analz_insert_Decrypt)
   1.490 +
   1.491 +
   1.492 +text{*This rule supposes "for the sake of argument" that we have the key.*}
   1.493 +lemma analz_insert_Crypt_subset:
   1.494 +     "analz (insert (Crypt K X) H) \<subseteq>   
   1.495 +           insert (Crypt K X) (analz (insert X H))"
   1.496 +apply (rule subsetI)
   1.497 +apply (erule analz.induct, auto)
   1.498 +done
   1.499 +
   1.500 +
   1.501 +lemma analz_image_Key [simp]: "analz (Key`N) = Key`N"
   1.502 +apply auto
   1.503 +apply (erule analz.induct, auto)
   1.504 +done
   1.505 +
   1.506 +
   1.507 +subsubsection{*Idempotence and transitivity *}
   1.508 +
   1.509 +lemma analz_analzD [dest!]: "X\<in> analz (analz H) ==> X\<in> analz H"
   1.510 +by (erule analz.induct, blast+)
   1.511 +
   1.512 +lemma analz_idem [simp]: "analz (analz H) = analz H"
   1.513 +by blast
   1.514 +
   1.515 +lemma analz_subset_iff [simp]: "(analz G \<subseteq> analz H) = (G \<subseteq> analz H)"
   1.516 +apply (rule iffI)
   1.517 +apply (iprover intro: subset_trans analz_increasing)  
   1.518 +apply (frule analz_mono, simp) 
   1.519 +done
   1.520 +
   1.521 +lemma analz_trans: "[| X\<in> analz G;  G \<subseteq> analz H |] ==> X\<in> analz H"
   1.522 +by (drule analz_mono, blast)
   1.523 +
   1.524 +
   1.525 +declare [[ atp_problem_prefix = "Message__analz_cut" ]]
   1.526 +    declare analz_trans[intro]
   1.527 +lemma analz_cut: "[| Y\<in> analz (insert X H);  X\<in> analz H |] ==> Y\<in> analz H"
   1.528 +(*TOO SLOW
   1.529 +by (metis analz_idem analz_increasing analz_mono insert_absorb insert_mono insert_subset) --{*317s*}
   1.530 +??*)
   1.531 +by (erule analz_trans, blast)
   1.532 +
   1.533 +
   1.534 +text{*This rewrite rule helps in the simplification of messages that involve
   1.535 +  the forwarding of unknown components (X).  Without it, removing occurrences
   1.536 +  of X can be very complicated. *}
   1.537 +lemma analz_insert_eq: "X\<in> analz H ==> analz (insert X H) = analz H"
   1.538 +by (blast intro: analz_cut analz_insertI)
   1.539 +
   1.540 +
   1.541 +text{*A congruence rule for "analz" *}
   1.542 +
   1.543 +declare [[ atp_problem_prefix = "Message__analz_subset_cong" ]]
   1.544 +lemma analz_subset_cong:
   1.545 +     "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H' |] 
   1.546 +      ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
   1.547 +apply simp
   1.548 +apply (metis Un_absorb2 Un_commute Un_subset_iff Un_upper1 Un_upper2 analz_mono)
   1.549 +done
   1.550 +
   1.551 +
   1.552 +lemma analz_cong:
   1.553 +     "[| analz G = analz G'; analz H = analz H'  
   1.554 +               |] ==> analz (G \<union> H) = analz (G' \<union> H')"
   1.555 +by (intro equalityI analz_subset_cong, simp_all) 
   1.556 +
   1.557 +lemma analz_insert_cong:
   1.558 +     "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"
   1.559 +by (force simp only: insert_def intro!: analz_cong)
   1.560 +
   1.561 +text{*If there are no pairs or encryptions then analz does nothing*}
   1.562 +lemma analz_trivial:
   1.563 +     "[| \<forall>X Y. {|X,Y|} \<notin> H;  \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
   1.564 +apply safe
   1.565 +apply (erule analz.induct, blast+)
   1.566 +done
   1.567 +
   1.568 +text{*These two are obsolete (with a single Spy) but cost little to prove...*}
   1.569 +lemma analz_UN_analz_lemma:
   1.570 +     "X\<in> analz (\<Union>i\<in>A. analz (H i)) ==> X\<in> analz (\<Union>i\<in>A. H i)"
   1.571 +apply (erule analz.induct)
   1.572 +apply (blast intro: analz_mono [THEN [2] rev_subsetD])+
   1.573 +done
   1.574 +
   1.575 +lemma analz_UN_analz [simp]: "analz (\<Union>i\<in>A. analz (H i)) = analz (\<Union>i\<in>A. H i)"
   1.576 +by (blast intro: analz_UN_analz_lemma analz_mono [THEN [2] rev_subsetD])
   1.577 +
   1.578 +
   1.579 +subsection{*Inductive relation "synth"*}
   1.580 +
   1.581 +text{*Inductive definition of "synth" -- what can be built up from a set of
   1.582 +    messages.  A form of upward closure.  Pairs can be built, messages
   1.583 +    encrypted with known keys.  Agent names are public domain.
   1.584 +    Numbers can be guessed, but Nonces cannot be.  *}
   1.585 +
   1.586 +inductive_set
   1.587 +  synth :: "msg set => msg set"
   1.588 +  for H :: "msg set"
   1.589 +  where
   1.590 +    Inj    [intro]:   "X \<in> H ==> X \<in> synth H"
   1.591 +  | Agent  [intro]:   "Agent agt \<in> synth H"
   1.592 +  | Number [intro]:   "Number n  \<in> synth H"
   1.593 +  | Hash   [intro]:   "X \<in> synth H ==> Hash X \<in> synth H"
   1.594 +  | MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
   1.595 +  | Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
   1.596 +
   1.597 +text{*Monotonicity*}
   1.598 +lemma synth_mono: "G\<subseteq>H ==> synth(G) \<subseteq> synth(H)"
   1.599 +  by (auto, erule synth.induct, auto)  
   1.600 +
   1.601 +text{*NO @{text Agent_synth}, as any Agent name can be synthesized.  
   1.602 +  The same holds for @{term Number}*}
   1.603 +inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H"
   1.604 +inductive_cases Key_synth   [elim!]: "Key K \<in> synth H"
   1.605 +inductive_cases Hash_synth  [elim!]: "Hash X \<in> synth H"
   1.606 +inductive_cases MPair_synth [elim!]: "{|X,Y|} \<in> synth H"
   1.607 +inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
   1.608 +
   1.609 +
   1.610 +lemma synth_increasing: "H \<subseteq> synth(H)"
   1.611 +by blast
   1.612 +
   1.613 +subsubsection{*Unions *}
   1.614 +
   1.615 +text{*Converse fails: we can synth more from the union than from the 
   1.616 +  separate parts, building a compound message using elements of each.*}
   1.617 +lemma synth_Un: "synth(G) \<union> synth(H) \<subseteq> synth(G \<union> H)"
   1.618 +by (intro Un_least synth_mono Un_upper1 Un_upper2)
   1.619 +
   1.620 +
   1.621 +declare [[ atp_problem_prefix = "Message__synth_insert" ]]
   1.622 + 
   1.623 +lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)"
   1.624 +by (metis insert_iff insert_subset subset_insertI synth.Inj synth_mono)
   1.625 +
   1.626 +subsubsection{*Idempotence and transitivity *}
   1.627 +
   1.628 +lemma synth_synthD [dest!]: "X\<in> synth (synth H) ==> X\<in> synth H"
   1.629 +by (erule synth.induct, blast+)
   1.630 +
   1.631 +lemma synth_idem: "synth (synth H) = synth H"
   1.632 +by blast
   1.633 +
   1.634 +lemma synth_subset_iff [simp]: "(synth G \<subseteq> synth H) = (G \<subseteq> synth H)"
   1.635 +apply (rule iffI)
   1.636 +apply (iprover intro: subset_trans synth_increasing)  
   1.637 +apply (frule synth_mono, simp add: synth_idem) 
   1.638 +done
   1.639 +
   1.640 +lemma synth_trans: "[| X\<in> synth G;  G \<subseteq> synth H |] ==> X\<in> synth H"
   1.641 +by (drule synth_mono, blast)
   1.642 +
   1.643 +declare [[ atp_problem_prefix = "Message__synth_cut" ]]
   1.644 +lemma synth_cut: "[| Y\<in> synth (insert X H);  X\<in> synth H |] ==> Y\<in> synth H"
   1.645 +(*TOO SLOW
   1.646 +by (metis insert_absorb insert_mono insert_subset synth_idem synth_increasing synth_mono)
   1.647 +*)
   1.648 +by (erule synth_trans, blast)
   1.649 +
   1.650 +
   1.651 +lemma Agent_synth [simp]: "Agent A \<in> synth H"
   1.652 +by blast
   1.653 +
   1.654 +lemma Number_synth [simp]: "Number n \<in> synth H"
   1.655 +by blast
   1.656 +
   1.657 +lemma Nonce_synth_eq [simp]: "(Nonce N \<in> synth H) = (Nonce N \<in> H)"
   1.658 +by blast
   1.659 +
   1.660 +lemma Key_synth_eq [simp]: "(Key K \<in> synth H) = (Key K \<in> H)"
   1.661 +by blast
   1.662 +
   1.663 +lemma Crypt_synth_eq [simp]:
   1.664 +     "Key K \<notin> H ==> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)"
   1.665 +by blast
   1.666 +
   1.667 +
   1.668 +lemma keysFor_synth [simp]: 
   1.669 +    "keysFor (synth H) = keysFor H \<union> invKey`{K. Key K \<in> H}"
   1.670 +by (unfold keysFor_def, blast)
   1.671 +
   1.672 +
   1.673 +subsubsection{*Combinations of parts, analz and synth *}
   1.674 +
   1.675 +declare [[ atp_problem_prefix = "Message__parts_synth" ]]
   1.676 +lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"
   1.677 +apply (rule equalityI)
   1.678 +apply (rule subsetI)
   1.679 +apply (erule parts.induct)
   1.680 +apply (metis UnCI)
   1.681 +apply (metis MPair_synth UnCI UnE insert_absorb insert_subset parts.Fst parts_increasing)
   1.682 +apply (metis MPair_synth UnCI UnE insert_absorb insert_subset parts.Snd parts_increasing)
   1.683 +apply (metis Body Crypt_synth UnCI UnE insert_absorb insert_subset parts_increasing)
   1.684 +apply (metis Un_subset_iff parts_increasing parts_mono synth_increasing)
   1.685 +done
   1.686 +
   1.687 +
   1.688 +
   1.689 +
   1.690 +declare [[ atp_problem_prefix = "Message__analz_analz_Un" ]]
   1.691 +lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)"
   1.692 +apply (rule equalityI);
   1.693 +apply (metis analz_idem analz_subset_cong order_eq_refl)
   1.694 +apply (metis analz_increasing analz_subset_cong order_eq_refl)
   1.695 +done
   1.696 +
   1.697 +declare [[ atp_problem_prefix = "Message__analz_synth_Un" ]]
   1.698 +    declare analz_mono [intro] analz.Fst [intro] analz.Snd [intro] Un_least [intro]
   1.699 +lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G"
   1.700 +apply (rule equalityI)
   1.701 +apply (rule subsetI)
   1.702 +apply (erule analz.induct)
   1.703 +apply (metis UnCI UnE Un_commute analz.Inj)
   1.704 +apply (metis MPair_synth UnCI UnE Un_commute Un_upper1 analz.Fst analz_increasing analz_mono insert_absorb insert_subset)
   1.705 +apply (metis MPair_synth UnCI UnE Un_commute Un_upper1 analz.Snd analz_increasing analz_mono insert_absorb insert_subset)
   1.706 +apply (blast intro: analz.Decrypt)
   1.707 +apply blast
   1.708 +done
   1.709 +
   1.710 +
   1.711 +declare [[ atp_problem_prefix = "Message__analz_synth" ]]
   1.712 +lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
   1.713 +proof (neg_clausify)
   1.714 +assume 0: "analz (synth H) \<noteq> analz H \<union> synth H"
   1.715 +have 1: "\<And>X1 X3. sup (analz (sup X3 X1)) (synth X3) = analz (sup (synth X3) X1)"
   1.716 +  by (metis analz_synth_Un)
   1.717 +have 2: "sup (analz H) (synth H) \<noteq> analz (synth H)"
   1.718 +  by (metis 0)
   1.719 +have 3: "\<And>X1 X3. sup (synth X3) (analz (sup X3 X1)) = analz (sup (synth X3) X1)"
   1.720 +  by (metis 1 Un_commute)
   1.721 +have 4: "\<And>X3. sup (synth X3) (analz X3) = analz (sup (synth X3) {})"
   1.722 +  by (metis 3 Un_empty_right)
   1.723 +have 5: "\<And>X3. sup (synth X3) (analz X3) = analz (synth X3)"
   1.724 +  by (metis 4 Un_empty_right)
   1.725 +have 6: "\<And>X3. sup (analz X3) (synth X3) = analz (synth X3)"
   1.726 +  by (metis 5 Un_commute)
   1.727 +show "False"
   1.728 +  by (metis 2 6)
   1.729 +qed
   1.730 +
   1.731 +
   1.732 +subsubsection{*For reasoning about the Fake rule in traces *}
   1.733 +
   1.734 +declare [[ atp_problem_prefix = "Message__parts_insert_subset_Un" ]]
   1.735 +lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
   1.736 +proof (neg_clausify)
   1.737 +assume 0: "X \<in> G"
   1.738 +assume 1: "\<not> parts (insert X H) \<subseteq> parts G \<union> parts H"
   1.739 +have 2: "\<not> parts (insert X H) \<subseteq> parts (G \<union> H)"
   1.740 +  by (metis 1 parts_Un)
   1.741 +have 3: "\<not> insert X H \<subseteq> G \<union> H"
   1.742 +  by (metis 2 parts_mono)
   1.743 +have 4: "X \<notin> G \<union> H \<or> \<not> H \<subseteq> G \<union> H"
   1.744 +  by (metis 3 insert_subset)
   1.745 +have 5: "X \<notin> G \<union> H"
   1.746 +  by (metis 4 Un_upper2)
   1.747 +have 6: "X \<notin> G"
   1.748 +  by (metis 5 UnCI)
   1.749 +show "False"
   1.750 +  by (metis 6 0)
   1.751 +qed
   1.752 +
   1.753 +declare [[ atp_problem_prefix = "Message__Fake_parts_insert" ]]
   1.754 +lemma Fake_parts_insert:
   1.755 +     "X \<in> synth (analz H) ==>  
   1.756 +      parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
   1.757 +proof (neg_clausify)
   1.758 +assume 0: "X \<in> synth (analz H)"
   1.759 +assume 1: "\<not> parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
   1.760 +have 2: "\<And>X3. parts X3 \<union> synth (analz X3) = parts (synth (analz X3))"
   1.761 +  by (metis parts_synth parts_analz)
   1.762 +have 3: "\<And>X3. analz X3 \<union> synth (analz X3) = analz (synth (analz X3))"
   1.763 +  by (metis analz_synth analz_idem)
   1.764 +have 4: "\<And>X3. analz X3 \<subseteq> analz (synth X3)"
   1.765 +  by (metis Un_upper1 analz_synth)
   1.766 +have 5: "\<not> parts (insert X H) \<subseteq> parts H \<union> synth (analz H)"
   1.767 +  by (metis 1 Un_commute)
   1.768 +have 6: "\<not> parts (insert X H) \<subseteq> parts (synth (analz H))"
   1.769 +  by (metis 5 2)
   1.770 +have 7: "\<not> insert X H \<subseteq> synth (analz H)"
   1.771 +  by (metis 6 parts_mono)
   1.772 +have 8: "X \<notin> synth (analz H) \<or> \<not> H \<subseteq> synth (analz H)"
   1.773 +  by (metis 7 insert_subset)
   1.774 +have 9: "\<not> H \<subseteq> synth (analz H)"
   1.775 +  by (metis 8 0)
   1.776 +have 10: "\<And>X3. X3 \<subseteq> analz (synth X3)"
   1.777 +  by (metis analz_subset_iff 4)
   1.778 +have 11: "\<And>X3. X3 \<subseteq> analz (synth (analz X3))"
   1.779 +  by (metis analz_subset_iff 10)
   1.780 +have 12: "\<And>X3. analz (synth (analz X3)) = synth (analz X3) \<or>
   1.781 +     \<not> analz X3 \<subseteq> synth (analz X3)"
   1.782 +  by (metis Un_absorb1 3)
   1.783 +have 13: "\<And>X3. analz (synth (analz X3)) = synth (analz X3)"
   1.784 +  by (metis 12 synth_increasing)
   1.785 +have 14: "\<And>X3. X3 \<subseteq> synth (analz X3)"
   1.786 +  by (metis 11 13)
   1.787 +show "False"
   1.788 +  by (metis 9 14)
   1.789 +qed
   1.790 +
   1.791 +lemma Fake_parts_insert_in_Un:
   1.792 +     "[|Z \<in> parts (insert X H);  X: synth (analz H)|] 
   1.793 +      ==> Z \<in>  synth (analz H) \<union> parts H";
   1.794 +by (blast dest: Fake_parts_insert  [THEN subsetD, dest])
   1.795 +
   1.796 +declare [[ atp_problem_prefix = "Message__Fake_analz_insert" ]]
   1.797 +    declare analz_mono [intro] synth_mono [intro] 
   1.798 +lemma Fake_analz_insert:
   1.799 +     "X\<in> synth (analz G) ==>  
   1.800 +      analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
   1.801 +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))
   1.802 +
   1.803 +declare [[ atp_problem_prefix = "Message__Fake_analz_insert_simpler" ]]
   1.804 +(*simpler problems?  BUT METIS CAN'T PROVE
   1.805 +lemma Fake_analz_insert_simpler:
   1.806 +     "X\<in> synth (analz G) ==>  
   1.807 +      analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
   1.808 +apply (rule subsetI)
   1.809 +apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> H) ")
   1.810 +apply (metis Un_commute analz_analz_Un analz_synth_Un)
   1.811 +apply (metis Un_commute Un_upper1 Un_upper2 analz_cut analz_increasing analz_mono insert_absorb insert_mono insert_subset)
   1.812 +done
   1.813 +*)
   1.814 +
   1.815 +end