src/HOL/Auth/Event.thy
changeset 13926 6e62e5357a10
parent 13922 75ae4244a596
child 13935 4822d9597d1e
     1.1 --- a/src/HOL/Auth/Event.thy	Sat Apr 26 12:38:17 2003 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Sat Apr 26 12:38:42 2003 +0200
     1.3 @@ -11,8 +11,7 @@
     1.4      stores are visible to him
     1.5  *)
     1.6  
     1.7 -theory Event = Message
     1.8 -files ("Event_lemmas.ML"):
     1.9 +theory Event = Message:
    1.10  
    1.11  consts  (*Initial states of agents -- parameter of the construction*)
    1.12    initState :: "agent => msg set"
    1.13 @@ -74,43 +73,234 @@
    1.14    used_Nil:   "used []         = (UN B. parts (initState B))"
    1.15    used_Cons:  "used (ev # evs) =
    1.16  		     (case ev of
    1.17 -			Says A B X => parts {X} Un (used evs)
    1.18 +			Says A B X => parts {X} \<union> (used evs)
    1.19  		      | Gets A X   => used evs
    1.20 -		      | Notes A X  => parts {X} Un (used evs))"
    1.21 +		      | Notes A X  => parts {X} \<union> (used evs))"
    1.22  
    1.23  
    1.24 -lemma Notes_imp_used [rule_format]: "Notes A X : set evs --> X : used evs"
    1.25 -apply (induct_tac evs);
    1.26 +lemma Notes_imp_used [rule_format]: "Notes A X \<in> set evs --> X \<in> used evs"
    1.27 +apply (induct_tac evs)
    1.28  apply (auto split: event.split) 
    1.29  done
    1.30  
    1.31 -lemma Says_imp_used [rule_format]: "Says A B X : set evs --> X : used evs"
    1.32 -apply (induct_tac evs);
    1.33 +lemma Says_imp_used [rule_format]: "Says A B X \<in> set evs --> X \<in> used evs"
    1.34 +apply (induct_tac evs)
    1.35  apply (auto split: event.split) 
    1.36  done
    1.37  
    1.38  lemma MPair_used [rule_format]:
    1.39 -     "MPair X Y : used evs --> X : used evs & Y : used evs"
    1.40 -apply (induct_tac evs);
    1.41 +     "MPair X Y \<in> used evs --> X \<in> used evs & Y \<in> used evs"
    1.42 +apply (induct_tac evs)
    1.43  apply (auto split: event.split) 
    1.44  done
    1.45  
    1.46 -use "Event_lemmas.ML"
    1.47 +
    1.48 +subsection{*Function @{term knows}*}
    1.49 +
    1.50 +text{*Simplifying   @term{"parts (insert X (knows Spy evs))
    1.51 +      = parts {X} \<union> parts (knows Spy evs)"}.  The general case loops.*)
    1.52 +
    1.53 +text{*This version won't loop with the simplifier.*}
    1.54 +lemmas parts_insert_knows_Spy = parts_insert [of _ "knows Spy evs", standard]
    1.55 +
    1.56 +lemma knows_Spy_Says [simp]:
    1.57 +     "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
    1.58 +by simp
    1.59 +
    1.60 +text{*The point of letting the Spy see "bad" agents' notes is to prevent
    1.61 +  redundant case-splits on whether A=Spy and whether A:bad*}
    1.62 +lemma knows_Spy_Notes [simp]:
    1.63 +     "knows Spy (Notes A X # evs) =  
    1.64 +          (if A:bad then insert X (knows Spy evs) else knows Spy evs)"
    1.65 +by simp
    1.66 +
    1.67 +lemma knows_Spy_Gets [simp]: "knows Spy (Gets A X # evs) = knows Spy evs"
    1.68 +by simp
    1.69 +
    1.70 +lemma knows_Spy_subset_knows_Spy_Says:
    1.71 +     "knows Spy evs <= knows Spy (Says A B X # evs)"
    1.72 +by (simp add: subset_insertI)
    1.73 +
    1.74 +lemma knows_Spy_subset_knows_Spy_Notes:
    1.75 +     "knows Spy evs <= knows Spy (Notes A X # evs)"
    1.76 +by force
    1.77 +
    1.78 +lemma knows_Spy_subset_knows_Spy_Gets:
    1.79 +     "knows Spy evs <= knows Spy (Gets A X # evs)"
    1.80 +by (simp add: subset_insertI)
    1.81 +
    1.82 +text{*Spy sees what is sent on the traffic*}
    1.83 +lemma Says_imp_knows_Spy [rule_format]:
    1.84 +     "Says A B X \<in> set evs --> X \<in> knows Spy evs"
    1.85 +apply (induct_tac "evs")
    1.86 +apply (simp_all (no_asm_simp) split add: event.split)
    1.87 +done
    1.88 +
    1.89 +lemma Notes_imp_knows_Spy [rule_format]:
    1.90 +     "Notes A X \<in> set evs --> A: bad --> X \<in> knows Spy evs"
    1.91 +apply (induct_tac "evs")
    1.92 +apply (simp_all (no_asm_simp) split add: event.split)
    1.93 +done
    1.94 +
    1.95 +
    1.96 +text{*Elimination rules: derive contradictions from old Says events containing
    1.97 +  items known to be fresh*}
    1.98 +lemmas knows_Spy_partsEs =
    1.99 +     Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard] 
   1.100 +     parts.Body [THEN revcut_rl, standard]
   1.101 +
   1.102 +text{*Compatibility for the old "spies" function*}
   1.103 +lemmas spies_partsEs = knows_Spy_partsEs
   1.104 +lemmas Says_imp_spies = Says_imp_knows_Spy
   1.105 +lemmas parts_insert_spies = parts_insert_knows_Spy
   1.106 +
   1.107 +
   1.108 +subsection{*Knowledge of Agents*}
   1.109 +
   1.110 +lemma knows_Says: "knows A (Says A B X # evs) = insert X (knows A evs)"
   1.111 +by simp
   1.112 +
   1.113 +lemma knows_Notes: "knows A (Notes A X # evs) = insert X (knows A evs)"
   1.114 +by simp
   1.115 +
   1.116 +lemma knows_Gets:
   1.117 +     "A \<noteq> Spy --> knows A (Gets A X # evs) = insert X (knows A evs)"
   1.118 +by simp
   1.119 +
   1.120 +
   1.121 +lemma knows_subset_knows_Says: "knows A evs <= knows A (Says A' B X # evs)"
   1.122 +apply (simp add: subset_insertI)
   1.123 +done
   1.124 +
   1.125 +lemma knows_subset_knows_Notes: "knows A evs <= knows A (Notes A' X # evs)"
   1.126 +apply (simp add: subset_insertI)
   1.127 +done
   1.128 +
   1.129 +lemma knows_subset_knows_Gets: "knows A evs <= knows A (Gets A' X # evs)"
   1.130 +apply (simp add: subset_insertI)
   1.131 +done
   1.132 +
   1.133 +text{*Agents know what they say*}
   1.134 +lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs --> X \<in> knows A evs"
   1.135 +apply (induct_tac "evs")
   1.136 +apply (simp_all (no_asm_simp) split add: event.split)
   1.137 +apply blast
   1.138 +done
   1.139 +
   1.140 +text{*Agents know what they note*}
   1.141 +lemma Notes_imp_knows [rule_format]: "Notes A X \<in> set evs --> X \<in> knows A evs"
   1.142 +apply (induct_tac "evs")
   1.143 +apply (simp_all (no_asm_simp) split add: event.split)
   1.144 +apply blast
   1.145 +done
   1.146 +
   1.147 +text{*Agents know what they receive*}
   1.148 +lemma Gets_imp_knows_agents [rule_format]:
   1.149 +     "A \<noteq> Spy --> Gets A X \<in> set evs --> X \<in> knows A evs"
   1.150 +apply (induct_tac "evs")
   1.151 +apply (simp_all (no_asm_simp) split add: event.split)
   1.152 +done
   1.153 +
   1.154 +
   1.155 +text{*What agents DIFFERENT FROM Spy know 
   1.156 +  was either said, or noted, or got, or known initially*}
   1.157 +lemma knows_imp_Says_Gets_Notes_initState [rule_format]:
   1.158 +     "[| X \<in> knows A evs; A \<noteq> Spy |] ==> EX B.  
   1.159 +  Says A B X \<in> set evs | Gets A X \<in> set evs | Notes A X \<in> set evs | X \<in> initState A"
   1.160 +apply (erule rev_mp)
   1.161 +apply (induct_tac "evs")
   1.162 +apply (simp_all (no_asm_simp) split add: event.split)
   1.163 +apply blast
   1.164 +done
   1.165 +
   1.166 +text{*What the Spy knows -- for the time being --
   1.167 +  was either said or noted, or known initially*}
   1.168 +lemma knows_Spy_imp_Says_Notes_initState [rule_format]:
   1.169 +     "[| X \<in> knows Spy evs |] ==> EX A B.  
   1.170 +  Says A B X \<in> set evs | Notes A X \<in> set evs | X \<in> initState Spy"
   1.171 +apply (erule rev_mp)
   1.172 +apply (induct_tac "evs")
   1.173 +apply (simp_all (no_asm_simp) split add: event.split)
   1.174 +apply blast
   1.175 +done
   1.176 +
   1.177 +
   1.178 +
   1.179 +
   1.180 +text{*NOTE REMOVAL--laws above are cleaner, as they don't involve "case"*}
   1.181 +declare knows_Cons [simp del]
   1.182 +
   1.183 +
   1.184 +subsection{*Fresh Nonces*}
   1.185 +
   1.186 +lemma parts_knows_Spy_subset_used: "parts (knows Spy evs) <= used evs"
   1.187 +apply (induct_tac "evs")
   1.188 +apply (simp_all (no_asm_simp) add: parts_insert_knows_Spy split add: event.split)
   1.189 +apply blast+
   1.190 +done
   1.191 +
   1.192 +lemmas usedI = parts_knows_Spy_subset_used [THEN subsetD, intro]
   1.193 +
   1.194 +lemma initState_into_used: "X \<in> parts (initState B) ==> X \<in> used evs"
   1.195 +apply (induct_tac "evs")
   1.196 +apply (simp_all (no_asm_simp) add: parts_insert_knows_Spy split add: event.split)
   1.197 +apply blast
   1.198 +done
   1.199 +
   1.200 +lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} \<union> used evs"
   1.201 +by simp
   1.202 +
   1.203 +lemma used_Notes [simp]: "used (Notes A X # evs) = parts{X} \<union> used evs"
   1.204 +by simp
   1.205 +
   1.206 +lemma used_Gets [simp]: "used (Gets A X # evs) = used evs"
   1.207 +by simp
   1.208 +
   1.209 +lemma used_nil_subset: "used [] <= used evs"
   1.210 +apply (simp)
   1.211 +apply (blast intro: initState_into_used)
   1.212 +done
   1.213 +
   1.214 +text{*NOTE REMOVAL--laws above are cleaner, as they don't involve "case"*}
   1.215 +declare used_Nil [simp del] used_Cons [simp del]
   1.216 +
   1.217 +
   1.218 +text{*For proving theorems of the form @{term "X \<notin> analz (knows Spy evs) --> P"}
   1.219 +  New events added by induction to "evs" are discarded.  Provided 
   1.220 +  this information isn't needed, the proof will be much shorter, since
   1.221 +  it will omit complicated reasoning about @{term analz}.*}
   1.222 +
   1.223 +lemmas analz_mono_contra =
   1.224 +       knows_Spy_subset_knows_Spy_Says [THEN analz_mono, THEN contra_subsetD]
   1.225 +       knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD]
   1.226 +       knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD]
   1.227 +
   1.228 +ML
   1.229 +{*
   1.230 +val analz_mono_contra_tac = 
   1.231 +  let val analz_impI = inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
   1.232 +  in
   1.233 +    rtac analz_impI THEN' 
   1.234 +    REPEAT1 o 
   1.235 +      (dresolve_tac (thms"analz_mono_contra"))
   1.236 +    THEN' mp_tac
   1.237 +  end
   1.238 +*}
   1.239 +
   1.240  
   1.241  lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
   1.242  by (induct e, auto simp: knows_Cons)
   1.243  
   1.244  lemma initState_subset_knows: "initState A <= knows A evs"
   1.245 -apply (induct_tac evs)
   1.246 -apply (simp add: ); 
   1.247 +apply (induct_tac evs, simp) 
   1.248  apply (blast intro: knows_subset_knows_Cons [THEN subsetD])
   1.249  done
   1.250  
   1.251  
   1.252 -(*For proving new_keys_not_used*)
   1.253 +text{*For proving @{text new_keys_not_used}*}
   1.254  lemma keysFor_parts_insert:
   1.255 -     "[| K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) |] \
   1.256 -\     ==> K \<in> keysFor (parts (G Un H)) | Key (invKey K) \<in> parts H"; 
   1.257 +     "[| K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) |] 
   1.258 +      ==> K \<in> keysFor (parts (G \<union> H)) | Key (invKey K) \<in> parts H"; 
   1.259  by (force 
   1.260      dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
   1.261             analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD]
   1.262 @@ -125,10 +315,54 @@
   1.263  
   1.264  ML
   1.265  {*
   1.266 +val knows_Cons     = thm "knows_Cons"
   1.267 +val used_Nil       = thm "used_Nil"
   1.268 +val used_Cons      = thm "used_Cons"
   1.269 +
   1.270 +val Notes_imp_used = thm "Notes_imp_used";
   1.271 +val Says_imp_used = thm "Says_imp_used";
   1.272 +val MPair_used = thm "MPair_used";
   1.273 +val parts_insert_knows_Spy = thm "parts_insert_knows_Spy";
   1.274 +val knows_Spy_Says = thm "knows_Spy_Says";
   1.275 +val knows_Spy_Notes = thm "knows_Spy_Notes";
   1.276 +val knows_Spy_Gets = thm "knows_Spy_Gets";
   1.277 +val knows_Spy_subset_knows_Spy_Says = thm "knows_Spy_subset_knows_Spy_Says";
   1.278 +val knows_Spy_subset_knows_Spy_Notes = thm "knows_Spy_subset_knows_Spy_Notes";
   1.279 +val knows_Spy_subset_knows_Spy_Gets = thm "knows_Spy_subset_knows_Spy_Gets";
   1.280 +val Says_imp_knows_Spy = thm "Says_imp_knows_Spy";
   1.281 +val Notes_imp_knows_Spy = thm "Notes_imp_knows_Spy";
   1.282 +val knows_Spy_partsEs = thms "knows_Spy_partsEs";
   1.283 +val spies_partsEs = thms "spies_partsEs";
   1.284 +val Says_imp_spies = thm "Says_imp_spies";
   1.285 +val parts_insert_spies = thm "parts_insert_spies";
   1.286 +val knows_Says = thm "knows_Says";
   1.287 +val knows_Notes = thm "knows_Notes";
   1.288 +val knows_Gets = thm "knows_Gets";
   1.289 +val knows_subset_knows_Says = thm "knows_subset_knows_Says";
   1.290 +val knows_subset_knows_Notes = thm "knows_subset_knows_Notes";
   1.291 +val knows_subset_knows_Gets = thm "knows_subset_knows_Gets";
   1.292 +val Says_imp_knows = thm "Says_imp_knows";
   1.293 +val Notes_imp_knows = thm "Notes_imp_knows";
   1.294 +val Gets_imp_knows_agents = thm "Gets_imp_knows_agents";
   1.295 +val knows_imp_Says_Gets_Notes_initState = thm "knows_imp_Says_Gets_Notes_initState";
   1.296 +val knows_Spy_imp_Says_Notes_initState = thm "knows_Spy_imp_Says_Notes_initState";
   1.297 +val parts_knows_Spy_subset_used = thm "parts_knows_Spy_subset_used";
   1.298 +val usedI = thm "usedI";
   1.299 +val initState_into_used = thm "initState_into_used";
   1.300 +val used_Says = thm "used_Says";
   1.301 +val used_Notes = thm "used_Notes";
   1.302 +val used_Gets = thm "used_Gets";
   1.303 +val used_nil_subset = thm "used_nil_subset";
   1.304 +val analz_mono_contra = thms "analz_mono_contra";
   1.305 +val knows_subset_knows_Cons = thm "knows_subset_knows_Cons";
   1.306 +val initState_subset_knows = thm "initState_subset_knows";
   1.307 +val keysFor_parts_insert = thm "keysFor_parts_insert";
   1.308 +
   1.309 +
   1.310  val synth_analz_mono = thm "synth_analz_mono";
   1.311  
   1.312  val synth_analz_mono_contra_tac = 
   1.313 -  let val syan_impI = inst "P" "?Y ~: synth (analz (knows Spy ?evs))" impI
   1.314 +  let val syan_impI = inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI
   1.315    in
   1.316      rtac syan_impI THEN' 
   1.317      REPEAT1 o