tidied
authorpaulson
Wed Jul 13 16:47:23 2005 +0200 (2005-07-13)
changeset 168182b82259cc7b2
parent 16817 63a5782c764e
child 16819 00d8f9300d13
tidied
src/HOL/Auth/Message.thy
     1.1 --- a/src/HOL/Auth/Message.thy	Wed Jul 13 16:32:15 2005 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Wed Jul 13 16:47:23 2005 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4    symKeys :: "key set"
     1.5    "symKeys == {K. invKey K = K}"
     1.6  
     1.7 -datatype  (*We allow any number of friendly agents*)
     1.8 +datatype  --{*We allow any number of friendly agents*}
     1.9    agent = Server | Friend nat | Spy
    1.10  
    1.11  datatype
    1.12 @@ -48,7 +48,7 @@
    1.13  	 | Crypt  key msg   --{*Encryption, public- or shared-key*}
    1.14  
    1.15  
    1.16 -(*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
    1.17 +text{*Concrete syntax: messages appear as {|A,B,NA|}, etc...*}
    1.18  syntax
    1.19    "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
    1.20  
    1.21 @@ -61,15 +61,16 @@
    1.22  
    1.23  
    1.24  constdefs
    1.25 -  (*Message Y, paired with a MAC computed with the help of X*)
    1.26    HPair :: "[msg,msg] => msg"                       ("(4Hash[_] /_)" [0, 1000])
    1.27 +    --{*Message Y paired with a MAC computed with the help of X*}
    1.28      "Hash[X] Y == {| Hash{|X,Y|}, Y|}"
    1.29  
    1.30 -  (*Keys useful to decrypt elements of a message set*)
    1.31    keysFor :: "msg set => key set"
    1.32 +    --{*Keys useful to decrypt elements of a message set*}
    1.33    "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"
    1.34  
    1.35 -subsubsection{*Inductive definition of all "parts" of a message.  *}
    1.36 +
    1.37 +subsubsection{*Inductive Definition of All Parts" of a Message*}
    1.38  
    1.39  consts  parts   :: "msg set => msg set"
    1.40  inductive "parts H"
    1.41 @@ -80,15 +81,15 @@
    1.42      Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
    1.43  
    1.44  
    1.45 -(*Monotonicity*)
    1.46 -lemma parts_mono: "G\<subseteq>H ==> parts(G) \<subseteq> parts(H)"
    1.47 +text{*Monotonicity*}
    1.48 +lemma parts_mono: "G \<subseteq> H ==> parts(G) \<subseteq> parts(H)"
    1.49  apply auto
    1.50  apply (erule parts.induct) 
    1.51 -apply (blast dest: Fst Snd Body)+
    1.52 +apply (blast dest: parts.Fst parts.Snd parts.Body)+
    1.53  done
    1.54  
    1.55  
    1.56 -text{*Equations hold because constructors are injective; cannot prove for all f*}
    1.57 +text{*Equations hold because constructors are injective.*}
    1.58  lemma Friend_image_eq [simp]: "(Friend x \<in> Friend`A) = (x:A)"
    1.59  by auto
    1.60  
    1.61 @@ -118,8 +119,8 @@
    1.62  lemma keysFor_UN [simp]: "keysFor (\<Union>i\<in>A. H i) = (\<Union>i\<in>A. keysFor (H i))"
    1.63  by (unfold keysFor_def, blast)
    1.64  
    1.65 -(*Monotonicity*)
    1.66 -lemma keysFor_mono: "G\<subseteq>H ==> keysFor(G) \<subseteq> keysFor(H)"
    1.67 +text{*Monotonicity*}
    1.68 +lemma keysFor_mono: "G \<subseteq> H ==> keysFor(G) \<subseteq> keysFor(H)"
    1.69  by (unfold keysFor_def, blast)
    1.70  
    1.71  lemma keysFor_insert_Agent [simp]: "keysFor (insert (Agent A) H) = keysFor H"
    1.72 @@ -177,7 +178,7 @@
    1.73  lemma parts_emptyE [elim!]: "X\<in> parts{} ==> P"
    1.74  by simp
    1.75  
    1.76 -(*WARNING: loops if H = {Y}, therefore must not be repeated!*)
    1.77 +text{*WARNING: loops if H = {Y}, therefore must not be repeated!*}
    1.78  lemma parts_singleton: "X\<in> parts H ==> \<exists>Y\<in>H. X\<in> parts {Y}"
    1.79  by (erule parts.induct, blast+)
    1.80  
    1.81 @@ -200,8 +201,8 @@
    1.82  apply (simp only: parts_Un)
    1.83  done
    1.84  
    1.85 -(*TWO inserts to avoid looping.  This rewrite is better than nothing.
    1.86 -  Not suitable for Addsimps: its behaviour can be strange.*)
    1.87 +text{*TWO inserts to avoid looping.  This rewrite is better than nothing.
    1.88 +  Not suitable for Addsimps: its behaviour can be strange.*}
    1.89  lemma parts_insert2:
    1.90       "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
    1.91  apply (simp add: Un_assoc)
    1.92 @@ -219,8 +220,8 @@
    1.93  lemma parts_UN [simp]: "parts(\<Union>x\<in>A. H x) = (\<Union>x\<in>A. parts(H x))"
    1.94  by (intro equalityI parts_UN_subset1 parts_UN_subset2)
    1.95  
    1.96 -(*Added to simplify arguments to parts, analz and synth.
    1.97 -  NOTE: the UN versions are no longer used!*)
    1.98 +text{*Added to simplify arguments to parts, analz and synth.
    1.99 +  NOTE: the UN versions are no longer used!*}
   1.100  
   1.101  
   1.102  text{*This allows @{text blast} to simplify occurrences of 
   1.103 @@ -242,7 +243,7 @@
   1.104  lemma parts_trans: "[| X\<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"
   1.105  by (drule parts_mono, blast)
   1.106  
   1.107 -(*Cut*)
   1.108 +text{*Cut*}
   1.109  lemma parts_cut:
   1.110       "[| Y\<in> parts (insert X G);  X\<in> parts H |] ==> Y\<in> parts (G \<union> H)"
   1.111  by (erule parts_trans, auto)
   1.112 @@ -312,15 +313,14 @@
   1.113  done
   1.114  
   1.115  
   1.116 -(*In any message, there is an upper bound N on its greatest nonce.*)
   1.117 +text{*In any message, there is an upper bound N on its greatest nonce.*}
   1.118  lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n --> Nonce n \<notin> parts {msg}"
   1.119  apply (induct_tac "msg")
   1.120  apply (simp_all (no_asm_simp) add: exI parts_insert2)
   1.121 -(*MPair case: blast_tac works out the necessary sum itself!*)
   1.122 -prefer 2 apply (blast elim!: add_leE)
   1.123 -(*Nonce case*)
   1.124 -apply (rule_tac x = "N + Suc nat" in exI)
   1.125 -apply (auto elim!: add_leE)
   1.126 + txt{*MPair case: blast works out the necessary sum itself!*}
   1.127 + prefer 2 apply (blast elim!: add_leE)
   1.128 +txt{*Nonce case*}
   1.129 +apply (rule_tac x = "N + Suc nat" in exI, auto) 
   1.130  done
   1.131  
   1.132  
   1.133 @@ -340,11 +340,11 @@
   1.134               "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
   1.135  
   1.136  
   1.137 -(*Monotonicity; Lemma 1 of Lowe's paper*)
   1.138 +text{*Monotonicity; Lemma 1 of Lowe's paper*}
   1.139  lemma analz_mono: "G\<subseteq>H ==> analz(G) \<subseteq> analz(H)"
   1.140  apply auto
   1.141  apply (erule analz.induct) 
   1.142 -apply (auto dest: Fst Snd) 
   1.143 +apply (auto dest: analz.Fst analz.Snd) 
   1.144  done
   1.145  
   1.146  text{*Making it safe speeds up proofs*}
   1.147 @@ -387,8 +387,8 @@
   1.148  apply (erule analz.induct, blast+)
   1.149  done
   1.150  
   1.151 -(*Converse fails: we can analz more from the union than from the 
   1.152 -  separate parts, as a key in one might decrypt a message in the other*)
   1.153 +text{*Converse fails: we can analz more from the union than from the 
   1.154 +  separate parts, as a key in one might decrypt a message in the other*}
   1.155  lemma analz_Un: "analz(G) \<union> analz(H) \<subseteq> analz(G \<union> H)"
   1.156  by (intro Un_least analz_mono Un_upper1 Un_upper2)
   1.157  
   1.158 @@ -423,7 +423,7 @@
   1.159  apply (erule analz.induct, auto) 
   1.160  done
   1.161  
   1.162 -(*Can only pull out Keys if they are not needed to decrypt the rest*)
   1.163 +text{*Can only pull out Keys if they are not needed to decrypt the rest*}
   1.164  lemma analz_insert_Key [simp]: 
   1.165      "K \<notin> keysFor (analz H) ==>   
   1.166            analz (insert (Key K) H) = insert (Key K) (analz H)"
   1.167 @@ -442,7 +442,7 @@
   1.168  apply (blast intro: analz.Fst analz.Snd)+
   1.169  done
   1.170  
   1.171 -(*Can pull out enCrypted message if the Key is not known*)
   1.172 +text{*Can pull out enCrypted message if the Key is not known*}
   1.173  lemma analz_insert_Crypt:
   1.174       "Key (invKey K) \<notin> analz H 
   1.175        ==> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)"
   1.176 @@ -472,10 +472,10 @@
   1.177                 insert (Crypt K X) (analz (insert X H))"
   1.178  by (intro equalityI lemma1 lemma2)
   1.179  
   1.180 -(*Case analysis: either the message is secure, or it is not!
   1.181 -  Effective, but can cause subgoals to blow up!
   1.182 -  Use with split_if;  apparently split_tac does not cope with patterns
   1.183 -  such as "analz (insert (Crypt K X) H)" *)
   1.184 +text{*Case analysis: either the message is secure, or it is not! Effective,
   1.185 +but can cause subgoals to blow up! Use with @{text "split_if"}; apparently
   1.186 +@{text "split_tac"} does not cope with patterns such as @{term"analz (insert
   1.187 +(Crypt K X) H)"} *} 
   1.188  lemma analz_Crypt_if [simp]:
   1.189       "analz (insert (Crypt K X) H) =                 
   1.190            (if (Key (invKey K) \<in> analz H)                 
   1.191 @@ -484,7 +484,7 @@
   1.192  by (simp add: analz_insert_Crypt analz_insert_Decrypt)
   1.193  
   1.194  
   1.195 -(*This rule supposes "for the sake of argument" that we have the key.*)
   1.196 +text{*This rule supposes "for the sake of argument" that we have the key.*}
   1.197  lemma analz_insert_Crypt_subset:
   1.198       "analz (insert (Crypt K X) H) \<subseteq>   
   1.199             insert (Crypt K X) (analz (insert X H))"
   1.200 @@ -510,7 +510,7 @@
   1.201  lemma analz_trans: "[| X\<in> analz G;  G \<subseteq> analz H |] ==> X\<in> analz H"
   1.202  by (drule analz_mono, blast)
   1.203  
   1.204 -(*Cut; Lemma 2 of Lowe*)
   1.205 +text{*Cut; Lemma 2 of Lowe*}
   1.206  lemma analz_cut: "[| Y\<in> analz (insert X H);  X\<in> analz H |] ==> Y\<in> analz H"
   1.207  by (erule analz_trans, blast)
   1.208  
   1.209 @@ -518,9 +518,9 @@
   1.210     "Y: analz (insert X H) ==> X: analz H --> Y: analz H"
   1.211  *)
   1.212  
   1.213 -(*This rewrite rule helps in the simplification of messages that involve
   1.214 +text{*This rewrite rule helps in the simplification of messages that involve
   1.215    the forwarding of unknown components (X).  Without it, removing occurrences
   1.216 -  of X can be very complicated. *)
   1.217 +  of X can be very complicated. *}
   1.218  lemma analz_insert_eq: "X\<in> analz H ==> analz (insert X H) = analz H"
   1.219  by (blast intro: analz_cut analz_insertI)
   1.220  
   1.221 @@ -544,14 +544,14 @@
   1.222       "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"
   1.223  by (force simp only: insert_def intro!: analz_cong)
   1.224  
   1.225 -(*If there are no pairs or encryptions then analz does nothing*)
   1.226 +text{*If there are no pairs or encryptions then analz does nothing*}
   1.227  lemma analz_trivial:
   1.228       "[| \<forall>X Y. {|X,Y|} \<notin> H;  \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
   1.229  apply safe
   1.230  apply (erule analz.induct, blast+)
   1.231  done
   1.232  
   1.233 -(*These two are obsolete (with a single Spy) but cost little to prove...*)
   1.234 +text{*These two are obsolete (with a single Spy) but cost little to prove...*}
   1.235  lemma analz_UN_analz_lemma:
   1.236       "X\<in> analz (\<Union>i\<in>A. analz (H i)) ==> X\<in> analz (\<Union>i\<in>A. H i)"
   1.237  apply (erule analz.induct)
   1.238 @@ -579,14 +579,12 @@
   1.239      MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
   1.240      Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
   1.241  
   1.242 -(*Monotonicity*)
   1.243 +text{*Monotonicity*}
   1.244  lemma synth_mono: "G\<subseteq>H ==> synth(G) \<subseteq> synth(H)"
   1.245 -apply auto
   1.246 -apply (erule synth.induct) 
   1.247 -apply (auto dest: Fst Snd Body) 
   1.248 -done
   1.249 +  by (auto, erule synth.induct, auto)  
   1.250  
   1.251 -(*NO Agent_synth, as any Agent name can be synthesized.  Ditto for Number*)
   1.252 +text{*NO @{text Agent_synth}, as any Agent name can be synthesized.  
   1.253 +  The same holds for @{term Number}*}
   1.254  inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H"
   1.255  inductive_cases Key_synth   [elim!]: "Key K \<in> synth H"
   1.256  inductive_cases Hash_synth  [elim!]: "Hash X \<in> synth H"
   1.257 @@ -599,8 +597,8 @@
   1.258  
   1.259  subsubsection{*Unions *}
   1.260  
   1.261 -(*Converse fails: we can synth more from the union than from the 
   1.262 -  separate parts, building a compound message using elements of each.*)
   1.263 +text{*Converse fails: we can synth more from the union than from the 
   1.264 +  separate parts, building a compound message using elements of each.*}
   1.265  lemma synth_Un: "synth(G) \<union> synth(H) \<subseteq> synth(G \<union> H)"
   1.266  by (intro Un_least synth_mono Un_upper1 Un_upper2)
   1.267  
   1.268 @@ -618,7 +616,7 @@
   1.269  lemma synth_trans: "[| X\<in> synth G;  G \<subseteq> synth H |] ==> X\<in> synth H"
   1.270  by (drule synth_mono, blast)
   1.271  
   1.272 -(*Cut; Lemma 2 of Lowe*)
   1.273 +text{*Cut; Lemma 2 of Lowe*}
   1.274  lemma synth_cut: "[| Y\<in> synth (insert X H);  X\<in> synth H |] ==> Y\<in> synth H"
   1.275  by (erule synth_trans, blast)
   1.276  
   1.277 @@ -678,8 +676,8 @@
   1.278  lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
   1.279  by (rule subset_trans [OF parts_mono parts_Un_subset2], blast)
   1.280  
   1.281 -(*More specifically for Fake.  Very occasionally we could do with a version
   1.282 -  of the form  parts{X} \<subseteq> synth (analz H) \<union> parts H *)
   1.283 +text{*More specifically for Fake.  Very occasionally we could do with a version
   1.284 +  of the form  @{term"parts{X} \<subseteq> synth (analz H) \<union> parts H"} *}
   1.285  lemma Fake_parts_insert:
   1.286       "X \<in> synth (analz H) ==>  
   1.287        parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
   1.288 @@ -693,7 +691,8 @@
   1.289        ==> Z \<in>  synth (analz H) \<union> parts H";
   1.290  by (blast dest: Fake_parts_insert  [THEN subsetD, dest])
   1.291  
   1.292 -(*H is sometimes (Key ` KK \<union> spies evs), so can't put G=H*)
   1.293 +text{*@{term H} is sometimes @{term"Key ` KK \<union> spies evs"}, so can't put 
   1.294 +  @{term "G=H"}.*}
   1.295  lemma Fake_analz_insert:
   1.296       "X\<in> synth (analz G) ==>  
   1.297        analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
   1.298 @@ -712,8 +711,8 @@
   1.299       "(X \<in> analz H | X \<in> parts H) = (X \<in> parts H)"
   1.300  by (blast intro: analz_subset_parts [THEN subsetD])
   1.301  
   1.302 -(*Without this equation, other rules for synth and analz would yield
   1.303 -  redundant cases*)
   1.304 +text{*Without this equation, other rules for synth and analz would yield
   1.305 +  redundant cases*}
   1.306  lemma MPair_synth_analz [iff]:
   1.307       "({|X,Y|} \<in> synth (analz H)) =  
   1.308        (X \<in> synth (analz H) & Y \<in> synth (analz H))"
   1.309 @@ -793,7 +792,7 @@
   1.310  by (simp add: HPair_def)
   1.311  
   1.312  
   1.313 -(*We do NOT want Crypt... messages broken up in protocols!!*)
   1.314 +text{*We do NOT want Crypt... messages broken up in protocols!!*}
   1.315  declare parts.Body [rule del]
   1.316  
   1.317  
   1.318 @@ -884,9 +883,9 @@
   1.319  fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i
   1.320  *}
   1.321  
   1.322 -(*By default only o_apply is built-in.  But in the presence of eta-expansion
   1.323 -  this means that some terms displayed as (f o g) will be rewritten, and others
   1.324 -  will not!*)
   1.325 +text{*By default only @{text o_apply} is built-in.  But in the presence of
   1.326 +eta-expansion this means that some terms displayed as @{term "f o g"} will be
   1.327 +rewritten, and others will not!*}
   1.328  declare o_def [simp]
   1.329  
   1.330