src/HOL/Auth/Message.thy
changeset 14200 d8598e24f8fa
parent 14181 942db403d4bb
child 15032 02aed07e01bf
     1.1 --- a/src/HOL/Auth/Message.thy	Tue Sep 23 15:40:27 2003 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Tue Sep 23 15:41:33 2003 +0200
     1.3 @@ -39,13 +39,13 @@
     1.4    agent = Server | Friend nat | Spy
     1.5  
     1.6  datatype
     1.7 -     msg = Agent  agent	    (*Agent names*)
     1.8 -         | Number nat       (*Ordinary integers, timestamps, ...*)
     1.9 -         | Nonce  nat       (*Unguessable nonces*)
    1.10 -         | Key    key       (*Crypto keys*)
    1.11 -	 | Hash   msg       (*Hashing*)
    1.12 -	 | MPair  msg msg   (*Compound messages*)
    1.13 -	 | Crypt  key msg   (*Encryption, public- or shared-key*)
    1.14 +     msg = Agent  agent	    --{*Agent names*}
    1.15 +         | Number nat       --{*Ordinary integers, timestamps, ...*}
    1.16 +         | Nonce  nat       --{*Unguessable nonces*}
    1.17 +         | Key    key       --{*Crypto keys*}
    1.18 +	 | Hash   msg       --{*Hashing*}
    1.19 +	 | MPair  msg msg   --{*Compound messages*}
    1.20 +	 | Crypt  key msg   --{*Encryption, public- or shared-key*}
    1.21  
    1.22  
    1.23  (*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
    1.24 @@ -69,7 +69,7 @@
    1.25    keysFor :: "msg set => key set"
    1.26    "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"
    1.27  
    1.28 -(** Inductive definition of all "parts" of a message.  **)
    1.29 +subsubsection{*Inductive definition of all "parts" of a message.  *}
    1.30  
    1.31  consts  parts   :: "msg set => msg set"
    1.32  inductive "parts H"
    1.33 @@ -81,7 +81,7 @@
    1.34  
    1.35  
    1.36  (*Monotonicity*)
    1.37 -lemma parts_mono: "G<=H ==> parts(G) <= parts(H)"
    1.38 +lemma parts_mono: "G\<subseteq>H ==> parts(G) \<subseteq> parts(H)"
    1.39  apply auto
    1.40  apply (erule parts.induct) 
    1.41  apply (auto dest: Fst Snd Body) 
    1.42 @@ -99,7 +99,7 @@
    1.43  by auto
    1.44  
    1.45  
    1.46 -(** Inverse of keys **)
    1.47 +subsubsection{*Inverse of keys *}
    1.48  
    1.49  lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
    1.50  apply safe
    1.51 @@ -142,8 +142,7 @@
    1.52  
    1.53  lemma keysFor_insert_Crypt [simp]: 
    1.54      "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"
    1.55 -apply (unfold keysFor_def, auto)
    1.56 -done
    1.57 +by (unfold keysFor_def, auto)
    1.58  
    1.59  lemma keysFor_image_Key [simp]: "keysFor (Key`E) = {}"
    1.60  by (unfold keysFor_def, auto)
    1.61 @@ -183,7 +182,7 @@
    1.62  by (erule parts.induct, blast+)
    1.63  
    1.64  
    1.65 -(** Unions **)
    1.66 +subsubsection{*Unions *}
    1.67  
    1.68  lemma parts_Un_subset1: "parts(G) \<union> parts(H) \<subseteq> parts(G \<union> H)"
    1.69  by (intro Un_least parts_mono Un_upper1 Un_upper2)
    1.70 @@ -203,7 +202,8 @@
    1.71  
    1.72  (*TWO inserts to avoid looping.  This rewrite is better than nothing.
    1.73    Not suitable for Addsimps: its behaviour can be strange.*)
    1.74 -lemma parts_insert2: "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
    1.75 +lemma parts_insert2:
    1.76 +     "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
    1.77  apply (simp add: Un_assoc)
    1.78  apply (simp add: parts_insert [symmetric])
    1.79  done
    1.80 @@ -231,7 +231,7 @@
    1.81  lemma parts_insert_subset: "insert X (parts H) \<subseteq> parts(insert X H)"
    1.82  by (blast intro: parts_mono [THEN [2] rev_subsetD])
    1.83  
    1.84 -(** Idempotence and transitivity **)
    1.85 +subsubsection{*Idempotence and transitivity *}
    1.86  
    1.87  lemma parts_partsD [dest!]: "X\<in> parts (parts H) ==> X\<in> parts H"
    1.88  by (erule parts.induct, blast+)
    1.89 @@ -243,46 +243,51 @@
    1.90  by (drule parts_mono, blast)
    1.91  
    1.92  (*Cut*)
    1.93 -lemma parts_cut: "[| Y\<in> parts (insert X G);  X\<in> parts H |]  
    1.94 -               ==> Y\<in> parts (G \<union> H)"
    1.95 -apply (erule parts_trans, auto)
    1.96 -done
    1.97 +lemma parts_cut:
    1.98 +     "[| Y\<in> parts (insert X G);  X\<in> parts H |] ==> Y\<in> parts (G \<union> H)"
    1.99 +by (erule parts_trans, auto)
   1.100  
   1.101  lemma parts_cut_eq [simp]: "X\<in> parts H ==> parts (insert X H) = parts H"
   1.102  by (force dest!: parts_cut intro: parts_insertI)
   1.103  
   1.104  
   1.105 -(** Rewrite rules for pulling out atomic messages **)
   1.106 +subsubsection{*Rewrite rules for pulling out atomic messages *}
   1.107  
   1.108  lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset]
   1.109  
   1.110  
   1.111 -lemma parts_insert_Agent [simp]: "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"
   1.112 +lemma parts_insert_Agent [simp]:
   1.113 +     "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"
   1.114  apply (rule parts_insert_eq_I) 
   1.115  apply (erule parts.induct, auto) 
   1.116  done
   1.117  
   1.118 -lemma parts_insert_Nonce [simp]: "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"
   1.119 +lemma parts_insert_Nonce [simp]:
   1.120 +     "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"
   1.121  apply (rule parts_insert_eq_I) 
   1.122  apply (erule parts.induct, auto) 
   1.123  done
   1.124  
   1.125 -lemma parts_insert_Number [simp]: "parts (insert (Number N) H) = insert (Number N) (parts H)"
   1.126 +lemma parts_insert_Number [simp]:
   1.127 +     "parts (insert (Number N) H) = insert (Number N) (parts H)"
   1.128  apply (rule parts_insert_eq_I) 
   1.129  apply (erule parts.induct, auto) 
   1.130  done
   1.131  
   1.132 -lemma parts_insert_Key [simp]: "parts (insert (Key K) H) = insert (Key K) (parts H)"
   1.133 +lemma parts_insert_Key [simp]:
   1.134 +     "parts (insert (Key K) H) = insert (Key K) (parts H)"
   1.135  apply (rule parts_insert_eq_I) 
   1.136  apply (erule parts.induct, auto) 
   1.137  done
   1.138  
   1.139 -lemma parts_insert_Hash [simp]: "parts (insert (Hash X) H) = insert (Hash X) (parts H)"
   1.140 +lemma parts_insert_Hash [simp]:
   1.141 +     "parts (insert (Hash X) H) = insert (Hash X) (parts H)"
   1.142  apply (rule parts_insert_eq_I) 
   1.143  apply (erule parts.induct, auto) 
   1.144  done
   1.145  
   1.146 -lemma parts_insert_Crypt [simp]: "parts (insert (Crypt K X) H) =  
   1.147 +lemma parts_insert_Crypt [simp]:
   1.148 +     "parts (insert (Crypt K X) H) =  
   1.149            insert (Crypt K X) (parts (insert X H))"
   1.150  apply (rule equalityI)
   1.151  apply (rule subsetI)
   1.152 @@ -291,7 +296,8 @@
   1.153  apply (blast intro: parts.Body)+
   1.154  done
   1.155  
   1.156 -lemma parts_insert_MPair [simp]: "parts (insert {|X,Y|} H) =  
   1.157 +lemma parts_insert_MPair [simp]:
   1.158 +     "parts (insert {|X,Y|} H) =  
   1.159            insert {|X,Y|} (parts (insert X (insert Y H)))"
   1.160  apply (rule equalityI)
   1.161  apply (rule subsetI)
   1.162 @@ -320,9 +326,9 @@
   1.163  
   1.164  subsection{*Inductive relation "analz"*}
   1.165  
   1.166 -(** Inductive definition of "analz" -- what can be broken down from a set of
   1.167 +text{*Inductive definition of "analz" -- what can be broken down from a set of
   1.168      messages, including keys.  A form of downward closure.  Pairs can
   1.169 -    be taken apart; messages decrypted with known keys.  **)
   1.170 +    be taken apart; messages decrypted with known keys.  *}
   1.171  
   1.172  consts  analz   :: "msg set => msg set"
   1.173  inductive "analz H"
   1.174 @@ -335,7 +341,7 @@
   1.175  
   1.176  
   1.177  (*Monotonicity; Lemma 1 of Lowe's paper*)
   1.178 -lemma analz_mono: "G<=H ==> analz(G) <= analz(H)"
   1.179 +lemma analz_mono: "G\<subseteq>H ==> analz(G) \<subseteq> analz(H)"
   1.180  apply auto
   1.181  apply (erule analz.induct) 
   1.182  apply (auto dest: Fst Snd) 
   1.183 @@ -356,6 +362,8 @@
   1.184  apply (erule analz.induct, blast+)
   1.185  done
   1.186  
   1.187 +lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
   1.188 +
   1.189  lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
   1.190  
   1.191  
   1.192 @@ -372,7 +380,7 @@
   1.193  
   1.194  lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
   1.195  
   1.196 -(** General equational properties **)
   1.197 +subsubsection{*General equational properties *}
   1.198  
   1.199  lemma analz_empty [simp]: "analz{} = {}"
   1.200  apply safe
   1.201 @@ -387,26 +395,30 @@
   1.202  lemma analz_insert: "insert X (analz H) \<subseteq> analz(insert X H)"
   1.203  by (blast intro: analz_mono [THEN [2] rev_subsetD])
   1.204  
   1.205 -(** Rewrite rules for pulling out atomic messages **)
   1.206 +subsubsection{*Rewrite rules for pulling out atomic messages *}
   1.207  
   1.208  lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert]
   1.209  
   1.210 -lemma analz_insert_Agent [simp]: "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"
   1.211 +lemma analz_insert_Agent [simp]:
   1.212 +     "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"
   1.213  apply (rule analz_insert_eq_I) 
   1.214  apply (erule analz.induct, auto) 
   1.215  done
   1.216  
   1.217 -lemma analz_insert_Nonce [simp]: "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"
   1.218 +lemma analz_insert_Nonce [simp]:
   1.219 +     "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"
   1.220  apply (rule analz_insert_eq_I) 
   1.221  apply (erule analz.induct, auto) 
   1.222  done
   1.223  
   1.224 -lemma analz_insert_Number [simp]: "analz (insert (Number N) H) = insert (Number N) (analz H)"
   1.225 +lemma analz_insert_Number [simp]:
   1.226 +     "analz (insert (Number N) H) = insert (Number N) (analz H)"
   1.227  apply (rule analz_insert_eq_I) 
   1.228  apply (erule analz.induct, auto) 
   1.229  done
   1.230  
   1.231 -lemma analz_insert_Hash [simp]: "analz (insert (Hash X) H) = insert (Hash X) (analz H)"
   1.232 +lemma analz_insert_Hash [simp]:
   1.233 +     "analz (insert (Hash X) H) = insert (Hash X) (analz H)"
   1.234  apply (rule analz_insert_eq_I) 
   1.235  apply (erule analz.induct, auto) 
   1.236  done
   1.237 @@ -420,7 +432,8 @@
   1.238  apply (erule analz.induct, auto) 
   1.239  done
   1.240  
   1.241 -lemma analz_insert_MPair [simp]: "analz (insert {|X,Y|} H) =  
   1.242 +lemma analz_insert_MPair [simp]:
   1.243 +     "analz (insert {|X,Y|} H) =  
   1.244            insert {|X,Y|} (analz (insert X (insert Y H)))"
   1.245  apply (rule equalityI)
   1.246  apply (rule subsetI)
   1.247 @@ -453,7 +466,8 @@
   1.248  apply (blast intro: analz_insertI analz.Decrypt)
   1.249  done
   1.250  
   1.251 -lemma analz_insert_Decrypt: "Key (invKey K) \<in> analz H ==>   
   1.252 +lemma analz_insert_Decrypt:
   1.253 +     "Key (invKey K) \<in> analz H ==>   
   1.254                 analz (insert (Crypt K X) H) =  
   1.255                 insert (Crypt K X) (analz (insert X H))"
   1.256  by (intro equalityI lemma1 lemma2)
   1.257 @@ -471,7 +485,8 @@
   1.258  
   1.259  
   1.260  (*This rule supposes "for the sake of argument" that we have the key.*)
   1.261 -lemma analz_insert_Crypt_subset: "analz (insert (Crypt K X) H) \<subseteq>   
   1.262 +lemma analz_insert_Crypt_subset:
   1.263 +     "analz (insert (Crypt K X) H) \<subseteq>   
   1.264             insert (Crypt K X) (analz (insert X H))"
   1.265  apply (rule subsetI)
   1.266  apply (erule analz.induct, auto)
   1.267 @@ -484,7 +499,7 @@
   1.268  done
   1.269  
   1.270  
   1.271 -(** Idempotence and transitivity **)
   1.272 +subsubsection{*Idempotence and transitivity *}
   1.273  
   1.274  lemma analz_analzD [dest!]: "X\<in> analz (analz H) ==> X\<in> analz H"
   1.275  by (erule analz.induct, blast+)
   1.276 @@ -510,32 +525,35 @@
   1.277  by (blast intro: analz_cut analz_insertI)
   1.278  
   1.279  
   1.280 -(** A congruence rule for "analz" **)
   1.281 +text{*A congruence rule for "analz" *}
   1.282  
   1.283 -lemma analz_subset_cong: "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H'  
   1.284 +lemma analz_subset_cong:
   1.285 +     "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H'  
   1.286                 |] ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
   1.287  apply clarify
   1.288  apply (erule analz.induct)
   1.289  apply (best intro: analz_mono [THEN subsetD])+
   1.290  done
   1.291  
   1.292 -lemma analz_cong: "[| analz G = analz G'; analz H = analz H'  
   1.293 +lemma analz_cong:
   1.294 +     "[| analz G = analz G'; analz H = analz H'  
   1.295                 |] ==> analz (G \<union> H) = analz (G' \<union> H')"
   1.296 -apply (intro equalityI analz_subset_cong, simp_all) 
   1.297 -done
   1.298 +by (intro equalityI analz_subset_cong, simp_all) 
   1.299  
   1.300 -
   1.301 -lemma analz_insert_cong: "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"
   1.302 +lemma analz_insert_cong:
   1.303 +     "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"
   1.304  by (force simp only: insert_def intro!: analz_cong)
   1.305  
   1.306  (*If there are no pairs or encryptions then analz does nothing*)
   1.307 -lemma analz_trivial: "[| \<forall>X Y. {|X,Y|} \<notin> H;  \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
   1.308 +lemma analz_trivial:
   1.309 +     "[| \<forall>X Y. {|X,Y|} \<notin> H;  \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
   1.310  apply safe
   1.311  apply (erule analz.induct, blast+)
   1.312  done
   1.313  
   1.314  (*These two are obsolete (with a single Spy) but cost little to prove...*)
   1.315 -lemma analz_UN_analz_lemma: "X\<in> analz (\<Union>i\<in>A. analz (H i)) ==> X\<in> analz (\<Union>i\<in>A. H i)"
   1.316 +lemma analz_UN_analz_lemma:
   1.317 +     "X\<in> analz (\<Union>i\<in>A. analz (H i)) ==> X\<in> analz (\<Union>i\<in>A. H i)"
   1.318  apply (erule analz.induct)
   1.319  apply (blast intro: analz_mono [THEN [2] rev_subsetD])+
   1.320  done
   1.321 @@ -546,10 +564,10 @@
   1.322  
   1.323  subsection{*Inductive relation "synth"*}
   1.324  
   1.325 -(** Inductive definition of "synth" -- what can be built up from a set of
   1.326 +text{*Inductive definition of "synth" -- what can be built up from a set of
   1.327      messages.  A form of upward closure.  Pairs can be built, messages
   1.328      encrypted with known keys.  Agent names are public domain.
   1.329 -    Numbers can be guessed, but Nonces cannot be.  **)
   1.330 +    Numbers can be guessed, but Nonces cannot be.  *}
   1.331  
   1.332  consts  synth   :: "msg set => msg set"
   1.333  inductive "synth H"
   1.334 @@ -562,7 +580,7 @@
   1.335      Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
   1.336  
   1.337  (*Monotonicity*)
   1.338 -lemma synth_mono: "G<=H ==> synth(G) <= synth(H)"
   1.339 +lemma synth_mono: "G\<subseteq>H ==> synth(G) \<subseteq> synth(H)"
   1.340  apply auto
   1.341  apply (erule synth.induct) 
   1.342  apply (auto dest: Fst Snd Body) 
   1.343 @@ -579,7 +597,7 @@
   1.344  lemma synth_increasing: "H \<subseteq> synth(H)"
   1.345  by blast
   1.346  
   1.347 -(** Unions **)
   1.348 +subsubsection{*Unions *}
   1.349  
   1.350  (*Converse fails: we can synth more from the union than from the 
   1.351    separate parts, building a compound message using elements of each.*)
   1.352 @@ -589,7 +607,7 @@
   1.353  lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)"
   1.354  by (blast intro: synth_mono [THEN [2] rev_subsetD])
   1.355  
   1.356 -(** Idempotence and transitivity **)
   1.357 +subsubsection{*Idempotence and transitivity *}
   1.358  
   1.359  lemma synth_synthD [dest!]: "X\<in> synth (synth H) ==> X\<in> synth H"
   1.360  by (erule synth.induct, blast+)
   1.361 @@ -616,17 +634,17 @@
   1.362  lemma Key_synth_eq [simp]: "(Key K \<in> synth H) = (Key K \<in> H)"
   1.363  by blast
   1.364  
   1.365 -lemma Crypt_synth_eq [simp]: "Key K \<notin> H ==> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)"
   1.366 +lemma Crypt_synth_eq [simp]:
   1.367 +     "Key K \<notin> H ==> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)"
   1.368  by blast
   1.369  
   1.370  
   1.371  lemma keysFor_synth [simp]: 
   1.372      "keysFor (synth H) = keysFor H \<union> invKey`{K. Key K \<in> H}"
   1.373 -apply (unfold keysFor_def, blast)
   1.374 -done
   1.375 +by (unfold keysFor_def, blast)
   1.376  
   1.377  
   1.378 -(*** Combinations of parts, analz and synth ***)
   1.379 +subsubsection{*Combinations of parts, analz and synth *}
   1.380  
   1.381  lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"
   1.382  apply (rule equalityI)
   1.383 @@ -655,22 +673,29 @@
   1.384  done
   1.385  
   1.386  
   1.387 -(** For reasoning about the Fake rule in traces **)
   1.388 +subsubsection{*For reasoning about the Fake rule in traces *}
   1.389  
   1.390  lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
   1.391  by (rule subset_trans [OF parts_mono parts_Un_subset2], blast)
   1.392  
   1.393  (*More specifically for Fake.  Very occasionally we could do with a version
   1.394    of the form  parts{X} \<subseteq> synth (analz H) \<union> parts H *)
   1.395 -lemma Fake_parts_insert: "X \<in> synth (analz H) ==>  
   1.396 +lemma Fake_parts_insert:
   1.397 +     "X \<in> synth (analz H) ==>  
   1.398        parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
   1.399  apply (drule parts_insert_subset_Un)
   1.400  apply (simp (no_asm_use))
   1.401  apply blast
   1.402  done
   1.403  
   1.404 +lemma Fake_parts_insert_in_Un:
   1.405 +     "[|Z \<in> parts (insert X H);  X: synth (analz H)|] 
   1.406 +      ==> Z \<in>  synth (analz H) \<union> parts H";
   1.407 +by (blast dest: Fake_parts_insert  [THEN subsetD, dest])
   1.408 +
   1.409  (*H is sometimes (Key ` KK \<union> spies evs), so can't put G=H*)
   1.410 -lemma Fake_analz_insert: "X\<in> synth (analz G) ==>  
   1.411 +lemma Fake_analz_insert:
   1.412 +     "X\<in> synth (analz G) ==>  
   1.413        analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
   1.414  apply (rule subsetI)
   1.415  apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> H) ")
   1.416 @@ -679,10 +704,12 @@
   1.417  apply blast
   1.418  done
   1.419  
   1.420 -lemma analz_conj_parts [simp]: "(X \<in> analz H & X \<in> parts H) = (X \<in> analz H)"
   1.421 +lemma analz_conj_parts [simp]:
   1.422 +     "(X \<in> analz H & X \<in> parts H) = (X \<in> analz H)"
   1.423  by (blast intro: analz_subset_parts [THEN subsetD])
   1.424  
   1.425 -lemma analz_disj_parts [simp]: "(X \<in> analz H | X \<in> parts H) = (X \<in> parts H)"
   1.426 +lemma analz_disj_parts [simp]:
   1.427 +     "(X \<in> analz H | X \<in> parts H) = (X \<in> parts H)"
   1.428  by (blast intro: analz_subset_parts [THEN subsetD])
   1.429  
   1.430  (*Without this equation, other rules for synth and analz would yield
   1.431 @@ -692,19 +719,21 @@
   1.432        (X \<in> synth (analz H) & Y \<in> synth (analz H))"
   1.433  by blast
   1.434  
   1.435 -lemma Crypt_synth_analz: "[| Key K \<in> analz H;  Key (invKey K) \<in> analz H |]  
   1.436 +lemma Crypt_synth_analz:
   1.437 +     "[| Key K \<in> analz H;  Key (invKey K) \<in> analz H |]  
   1.438         ==> (Crypt K X \<in> synth (analz H)) = (X \<in> synth (analz H))"
   1.439  by blast
   1.440  
   1.441  
   1.442 -lemma Hash_synth_analz [simp]: "X \<notin> synth (analz H)  
   1.443 +lemma Hash_synth_analz [simp]:
   1.444 +     "X \<notin> synth (analz H)  
   1.445        ==> (Hash{|X,Y|} \<in> synth (analz H)) = (Hash{|X,Y|} \<in> analz H)"
   1.446  by blast
   1.447  
   1.448  
   1.449  subsection{*HPair: a combination of Hash and MPair*}
   1.450  
   1.451 -(*** Freeness ***)
   1.452 +subsubsection{*Freeness *}
   1.453  
   1.454  lemma Agent_neq_HPair: "Agent A ~= Hash[X] Y"
   1.455  by (unfold HPair_def, simp)
   1.456 @@ -733,14 +762,16 @@
   1.457  lemma HPair_eq [iff]: "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)"
   1.458  by (simp add: HPair_def)
   1.459  
   1.460 -lemma MPair_eq_HPair [iff]: "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)"
   1.461 +lemma MPair_eq_HPair [iff]:
   1.462 +     "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)"
   1.463  by (simp add: HPair_def)
   1.464  
   1.465 -lemma HPair_eq_MPair [iff]: "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)"
   1.466 +lemma HPair_eq_MPair [iff]:
   1.467 +     "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)"
   1.468  by (auto simp add: HPair_def)
   1.469  
   1.470  
   1.471 -(*** Specialized laws, proved in terms of those for Hash and MPair ***)
   1.472 +subsubsection{*Specialized laws, proved in terms of those for Hash and MPair *}
   1.473  
   1.474  lemma keysFor_insert_HPair [simp]: "keysFor (insert (Hash[X] Y) H) = keysFor H"
   1.475  by (simp add: HPair_def)
   1.476 @@ -766,37 +797,10 @@
   1.477  declare parts.Body [rule del]
   1.478  
   1.479  
   1.480 +text{*Rewrites to push in Key and Crypt messages, so that other messages can
   1.481 +    be pulled out using the @{text analz_insert} rules*}
   1.482  ML
   1.483  {*
   1.484 -(*ML bindings for definitions*)
   1.485 -
   1.486 -val invKey = thm "invKey"
   1.487 -val keysFor_def = thm "keysFor_def"
   1.488 -val HPair_def = thm "HPair_def"
   1.489 -val symKeys_def = thm "symKeys_def"
   1.490 -
   1.491 -structure parts =
   1.492 -  struct
   1.493 -  val induct = thm "parts.induct"
   1.494 -  val Inj    = thm "parts.Inj"
   1.495 -  val Fst    = thm "parts.Fst"
   1.496 -  val Snd    = thm "parts.Snd"
   1.497 -  val Body   = thm "parts.Body"
   1.498 -  end
   1.499 -
   1.500 -structure analz =
   1.501 -  struct
   1.502 -  val induct = thm "analz.induct"
   1.503 -  val Inj    = thm "analz.Inj"
   1.504 -  val Fst    = thm "analz.Fst"
   1.505 -  val Snd    = thm "analz.Snd"
   1.506 -  val Decrypt = thm "analz.Decrypt"
   1.507 -  end
   1.508 -
   1.509 -
   1.510 -(** Rewrites to push in Key and Crypt messages, so that other messages can
   1.511 -    be pulled out using the analz_insert rules **)
   1.512 -
   1.513  fun insComm x y = inst "x" x (inst "y" y insert_commute);
   1.514  
   1.515  bind_thms ("pushKeys",
   1.516 @@ -818,79 +822,19 @@
   1.517  subsection{*Tactics useful for many protocol proofs*}
   1.518  ML
   1.519  {*
   1.520 +val invKey = thm "invKey"
   1.521 +val keysFor_def = thm "keysFor_def"
   1.522 +val HPair_def = thm "HPair_def"
   1.523 +val symKeys_def = thm "symKeys_def"
   1.524  val parts_mono = thm "parts_mono";
   1.525  val analz_mono = thm "analz_mono";
   1.526 -val Key_image_eq = thm "Key_image_eq";
   1.527 -val Nonce_Key_image_eq = thm "Nonce_Key_image_eq";
   1.528 -val keysFor_Un = thm "keysFor_Un";
   1.529 -val keysFor_mono = thm "keysFor_mono";
   1.530 -val keysFor_image_Key = thm "keysFor_image_Key";
   1.531 -val Crypt_imp_invKey_keysFor = thm "Crypt_imp_invKey_keysFor";
   1.532 -val MPair_parts = thm "MPair_parts";
   1.533 -val parts_increasing = thm "parts_increasing";
   1.534 -val parts_insertI = thm "parts_insertI";
   1.535 -val parts_empty = thm "parts_empty";
   1.536 -val parts_emptyE = thm "parts_emptyE";
   1.537 -val parts_singleton = thm "parts_singleton";
   1.538 -val parts_Un_subset1 = thm "parts_Un_subset1";
   1.539 -val parts_Un_subset2 = thm "parts_Un_subset2";
   1.540 -val parts_insert = thm "parts_insert";
   1.541 -val parts_insert2 = thm "parts_insert2";
   1.542 -val parts_UN_subset1 = thm "parts_UN_subset1";
   1.543 -val parts_UN_subset2 = thm "parts_UN_subset2";
   1.544 -val parts_UN = thm "parts_UN";
   1.545 -val parts_insert_subset = thm "parts_insert_subset";
   1.546 -val parts_partsD = thm "parts_partsD";
   1.547 -val parts_trans = thm "parts_trans";
   1.548 -val parts_cut = thm "parts_cut";
   1.549 -val parts_cut_eq = thm "parts_cut_eq";
   1.550 -val parts_insert_eq_I = thm "parts_insert_eq_I";
   1.551 -val parts_image_Key = thm "parts_image_Key";
   1.552 -val MPair_analz = thm "MPair_analz";
   1.553 +val synth_mono = thm "synth_mono";
   1.554  val analz_increasing = thm "analz_increasing";
   1.555 +
   1.556 +val analz_insertI = thm "analz_insertI";
   1.557  val analz_subset_parts = thm "analz_subset_parts";
   1.558 -val not_parts_not_analz = thm "not_parts_not_analz";
   1.559 -val parts_analz = thm "parts_analz";
   1.560 -val analz_parts = thm "analz_parts";
   1.561 -val analz_insertI = thm "analz_insertI";
   1.562 -val analz_empty = thm "analz_empty";
   1.563 -val analz_Un = thm "analz_Un";
   1.564 -val analz_insert_Crypt_subset = thm "analz_insert_Crypt_subset";
   1.565 -val analz_image_Key = thm "analz_image_Key";
   1.566 -val analz_analzD = thm "analz_analzD";
   1.567 -val analz_trans = thm "analz_trans";
   1.568 -val analz_cut = thm "analz_cut";
   1.569 -val analz_insert_eq = thm "analz_insert_eq";
   1.570 -val analz_subset_cong = thm "analz_subset_cong";
   1.571 -val analz_cong = thm "analz_cong";
   1.572 -val analz_insert_cong = thm "analz_insert_cong";
   1.573 -val analz_trivial = thm "analz_trivial";
   1.574 -val analz_UN_analz = thm "analz_UN_analz";
   1.575 -val synth_mono = thm "synth_mono";
   1.576 -val synth_increasing = thm "synth_increasing";
   1.577 -val synth_Un = thm "synth_Un";
   1.578 -val synth_insert = thm "synth_insert";
   1.579 -val synth_synthD = thm "synth_synthD";
   1.580 -val synth_trans = thm "synth_trans";
   1.581 -val synth_cut = thm "synth_cut";
   1.582 -val Agent_synth = thm "Agent_synth";
   1.583 -val Number_synth = thm "Number_synth";
   1.584 -val Nonce_synth_eq = thm "Nonce_synth_eq";
   1.585 -val Key_synth_eq = thm "Key_synth_eq";
   1.586 -val Crypt_synth_eq = thm "Crypt_synth_eq";
   1.587 -val keysFor_synth = thm "keysFor_synth";
   1.588 -val parts_synth = thm "parts_synth";
   1.589 -val analz_analz_Un = thm "analz_analz_Un";
   1.590 -val analz_synth_Un = thm "analz_synth_Un";
   1.591 -val analz_synth = thm "analz_synth";
   1.592 -val parts_insert_subset_Un = thm "parts_insert_subset_Un";
   1.593  val Fake_parts_insert = thm "Fake_parts_insert";
   1.594  val Fake_analz_insert = thm "Fake_analz_insert";
   1.595 -val analz_conj_parts = thm "analz_conj_parts";
   1.596 -val analz_disj_parts = thm "analz_disj_parts";
   1.597 -val MPair_synth_analz = thm "MPair_synth_analz";
   1.598 -val Crypt_synth_analz = thm "Crypt_synth_analz";
   1.599 -val Hash_synth_analz = thm "Hash_synth_analz";
   1.600  val pushes = thms "pushes";
   1.601  
   1.602  
   1.603 @@ -952,7 +896,7 @@
   1.604  lemma Hash_notin_image_Key [simp] :"Hash X \<notin> Key ` A"
   1.605  by auto
   1.606  
   1.607 -lemma synth_analz_mono: "G<=H ==> synth (analz(G)) <= synth (analz(H))"
   1.608 +lemma synth_analz_mono: "G\<subseteq>H ==> synth (analz(G)) \<subseteq> synth (analz(H))"
   1.609  by (simp add: synth_mono analz_mono) 
   1.610  
   1.611  lemma Fake_analz_eq [simp]:
   1.612 @@ -964,14 +908,6 @@
   1.613  apply (blast intro: synth_analz_mono [THEN [2] rev_subsetD]) 
   1.614  done
   1.615  
   1.616 -
   1.617 -lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
   1.618 -
   1.619 -lemma Fake_parts_insert_in_Un:
   1.620 -     "[|Z \<in> parts (insert X H);  X: synth (analz H)|] 
   1.621 -      ==> Z \<in>  synth (analz H) \<union> parts H";
   1.622 -by (blast dest: Fake_parts_insert  [THEN subsetD, dest])
   1.623 -
   1.624  text{*Two generalizations of @{text analz_insert_eq}*}
   1.625  lemma gen_analz_insert_eq [rule_format]:
   1.626       "X \<in> analz H ==> ALL G. H \<subseteq> G --> analz (insert X G) = analz G";