72 |
71 |
73 primrec |
72 primrec |
74 used_Nil: "used [] = (UN B. parts (initState B))" |
73 used_Nil: "used [] = (UN B. parts (initState B))" |
75 used_Cons: "used (ev # evs) = |
74 used_Cons: "used (ev # evs) = |
76 (case ev of |
75 (case ev of |
77 Says A B X => parts {X} Un (used evs) |
76 Says A B X => parts {X} \<union> (used evs) |
78 | Gets A X => used evs |
77 | Gets A X => used evs |
79 | Notes A X => parts {X} Un (used evs))" |
78 | Notes A X => parts {X} \<union> (used evs))" |
80 |
79 |
81 |
80 |
82 lemma Notes_imp_used [rule_format]: "Notes A X : set evs --> X : used evs" |
81 lemma Notes_imp_used [rule_format]: "Notes A X \<in> set evs --> X \<in> used evs" |
83 apply (induct_tac evs); |
82 apply (induct_tac evs) |
84 apply (auto split: event.split) |
83 apply (auto split: event.split) |
85 done |
84 done |
86 |
85 |
87 lemma Says_imp_used [rule_format]: "Says A B X : set evs --> X : used evs" |
86 lemma Says_imp_used [rule_format]: "Says A B X \<in> set evs --> X \<in> used evs" |
88 apply (induct_tac evs); |
87 apply (induct_tac evs) |
89 apply (auto split: event.split) |
88 apply (auto split: event.split) |
90 done |
89 done |
91 |
90 |
92 lemma MPair_used [rule_format]: |
91 lemma MPair_used [rule_format]: |
93 "MPair X Y : used evs --> X : used evs & Y : used evs" |
92 "MPair X Y \<in> used evs --> X \<in> used evs & Y \<in> used evs" |
94 apply (induct_tac evs); |
93 apply (induct_tac evs) |
95 apply (auto split: event.split) |
94 apply (auto split: event.split) |
96 done |
95 done |
97 |
96 |
98 use "Event_lemmas.ML" |
97 |
|
98 subsection{*Function @{term knows}*} |
|
99 |
|
100 text{*Simplifying @term{"parts (insert X (knows Spy evs)) |
|
101 = parts {X} \<union> parts (knows Spy evs)"}. The general case loops.*) |
|
102 |
|
103 text{*This version won't loop with the simplifier.*} |
|
104 lemmas parts_insert_knows_Spy = parts_insert [of _ "knows Spy evs", standard] |
|
105 |
|
106 lemma knows_Spy_Says [simp]: |
|
107 "knows Spy (Says A B X # evs) = insert X (knows Spy evs)" |
|
108 by simp |
|
109 |
|
110 text{*The point of letting the Spy see "bad" agents' notes is to prevent |
|
111 redundant case-splits on whether A=Spy and whether A:bad*} |
|
112 lemma knows_Spy_Notes [simp]: |
|
113 "knows Spy (Notes A X # evs) = |
|
114 (if A:bad then insert X (knows Spy evs) else knows Spy evs)" |
|
115 by simp |
|
116 |
|
117 lemma knows_Spy_Gets [simp]: "knows Spy (Gets A X # evs) = knows Spy evs" |
|
118 by simp |
|
119 |
|
120 lemma knows_Spy_subset_knows_Spy_Says: |
|
121 "knows Spy evs <= knows Spy (Says A B X # evs)" |
|
122 by (simp add: subset_insertI) |
|
123 |
|
124 lemma knows_Spy_subset_knows_Spy_Notes: |
|
125 "knows Spy evs <= knows Spy (Notes A X # evs)" |
|
126 by force |
|
127 |
|
128 lemma knows_Spy_subset_knows_Spy_Gets: |
|
129 "knows Spy evs <= knows Spy (Gets A X # evs)" |
|
130 by (simp add: subset_insertI) |
|
131 |
|
132 text{*Spy sees what is sent on the traffic*} |
|
133 lemma Says_imp_knows_Spy [rule_format]: |
|
134 "Says A B X \<in> set evs --> X \<in> knows Spy evs" |
|
135 apply (induct_tac "evs") |
|
136 apply (simp_all (no_asm_simp) split add: event.split) |
|
137 done |
|
138 |
|
139 lemma Notes_imp_knows_Spy [rule_format]: |
|
140 "Notes A X \<in> set evs --> A: bad --> X \<in> knows Spy evs" |
|
141 apply (induct_tac "evs") |
|
142 apply (simp_all (no_asm_simp) split add: event.split) |
|
143 done |
|
144 |
|
145 |
|
146 text{*Elimination rules: derive contradictions from old Says events containing |
|
147 items known to be fresh*} |
|
148 lemmas knows_Spy_partsEs = |
|
149 Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard] |
|
150 parts.Body [THEN revcut_rl, standard] |
|
151 |
|
152 text{*Compatibility for the old "spies" function*} |
|
153 lemmas spies_partsEs = knows_Spy_partsEs |
|
154 lemmas Says_imp_spies = Says_imp_knows_Spy |
|
155 lemmas parts_insert_spies = parts_insert_knows_Spy |
|
156 |
|
157 |
|
158 subsection{*Knowledge of Agents*} |
|
159 |
|
160 lemma knows_Says: "knows A (Says A B X # evs) = insert X (knows A evs)" |
|
161 by simp |
|
162 |
|
163 lemma knows_Notes: "knows A (Notes A X # evs) = insert X (knows A evs)" |
|
164 by simp |
|
165 |
|
166 lemma knows_Gets: |
|
167 "A \<noteq> Spy --> knows A (Gets A X # evs) = insert X (knows A evs)" |
|
168 by simp |
|
169 |
|
170 |
|
171 lemma knows_subset_knows_Says: "knows A evs <= knows A (Says A' B X # evs)" |
|
172 apply (simp add: subset_insertI) |
|
173 done |
|
174 |
|
175 lemma knows_subset_knows_Notes: "knows A evs <= knows A (Notes A' X # evs)" |
|
176 apply (simp add: subset_insertI) |
|
177 done |
|
178 |
|
179 lemma knows_subset_knows_Gets: "knows A evs <= knows A (Gets A' X # evs)" |
|
180 apply (simp add: subset_insertI) |
|
181 done |
|
182 |
|
183 text{*Agents know what they say*} |
|
184 lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs --> X \<in> knows A evs" |
|
185 apply (induct_tac "evs") |
|
186 apply (simp_all (no_asm_simp) split add: event.split) |
|
187 apply blast |
|
188 done |
|
189 |
|
190 text{*Agents know what they note*} |
|
191 lemma Notes_imp_knows [rule_format]: "Notes A X \<in> set evs --> X \<in> knows A evs" |
|
192 apply (induct_tac "evs") |
|
193 apply (simp_all (no_asm_simp) split add: event.split) |
|
194 apply blast |
|
195 done |
|
196 |
|
197 text{*Agents know what they receive*} |
|
198 lemma Gets_imp_knows_agents [rule_format]: |
|
199 "A \<noteq> Spy --> Gets A X \<in> set evs --> X \<in> knows A evs" |
|
200 apply (induct_tac "evs") |
|
201 apply (simp_all (no_asm_simp) split add: event.split) |
|
202 done |
|
203 |
|
204 |
|
205 text{*What agents DIFFERENT FROM Spy know |
|
206 was either said, or noted, or got, or known initially*} |
|
207 lemma knows_imp_Says_Gets_Notes_initState [rule_format]: |
|
208 "[| X \<in> knows A evs; A \<noteq> Spy |] ==> EX B. |
|
209 Says A B X \<in> set evs | Gets A X \<in> set evs | Notes A X \<in> set evs | X \<in> initState A" |
|
210 apply (erule rev_mp) |
|
211 apply (induct_tac "evs") |
|
212 apply (simp_all (no_asm_simp) split add: event.split) |
|
213 apply blast |
|
214 done |
|
215 |
|
216 text{*What the Spy knows -- for the time being -- |
|
217 was either said or noted, or known initially*} |
|
218 lemma knows_Spy_imp_Says_Notes_initState [rule_format]: |
|
219 "[| X \<in> knows Spy evs |] ==> EX A B. |
|
220 Says A B X \<in> set evs | Notes A X \<in> set evs | X \<in> initState Spy" |
|
221 apply (erule rev_mp) |
|
222 apply (induct_tac "evs") |
|
223 apply (simp_all (no_asm_simp) split add: event.split) |
|
224 apply blast |
|
225 done |
|
226 |
|
227 |
|
228 |
|
229 |
|
230 text{*NOTE REMOVAL--laws above are cleaner, as they don't involve "case"*} |
|
231 declare knows_Cons [simp del] |
|
232 |
|
233 |
|
234 subsection{*Fresh Nonces*} |
|
235 |
|
236 lemma parts_knows_Spy_subset_used: "parts (knows Spy evs) <= used evs" |
|
237 apply (induct_tac "evs") |
|
238 apply (simp_all (no_asm_simp) add: parts_insert_knows_Spy split add: event.split) |
|
239 apply blast+ |
|
240 done |
|
241 |
|
242 lemmas usedI = parts_knows_Spy_subset_used [THEN subsetD, intro] |
|
243 |
|
244 lemma initState_into_used: "X \<in> parts (initState B) ==> X \<in> used evs" |
|
245 apply (induct_tac "evs") |
|
246 apply (simp_all (no_asm_simp) add: parts_insert_knows_Spy split add: event.split) |
|
247 apply blast |
|
248 done |
|
249 |
|
250 lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} \<union> used evs" |
|
251 by simp |
|
252 |
|
253 lemma used_Notes [simp]: "used (Notes A X # evs) = parts{X} \<union> used evs" |
|
254 by simp |
|
255 |
|
256 lemma used_Gets [simp]: "used (Gets A X # evs) = used evs" |
|
257 by simp |
|
258 |
|
259 lemma used_nil_subset: "used [] <= used evs" |
|
260 apply (simp) |
|
261 apply (blast intro: initState_into_used) |
|
262 done |
|
263 |
|
264 text{*NOTE REMOVAL--laws above are cleaner, as they don't involve "case"*} |
|
265 declare used_Nil [simp del] used_Cons [simp del] |
|
266 |
|
267 |
|
268 text{*For proving theorems of the form @{term "X \<notin> analz (knows Spy evs) --> P"} |
|
269 New events added by induction to "evs" are discarded. Provided |
|
270 this information isn't needed, the proof will be much shorter, since |
|
271 it will omit complicated reasoning about @{term analz}.*} |
|
272 |
|
273 lemmas analz_mono_contra = |
|
274 knows_Spy_subset_knows_Spy_Says [THEN analz_mono, THEN contra_subsetD] |
|
275 knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD] |
|
276 knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD] |
|
277 |
|
278 ML |
|
279 {* |
|
280 val analz_mono_contra_tac = |
|
281 let val analz_impI = inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI |
|
282 in |
|
283 rtac analz_impI THEN' |
|
284 REPEAT1 o |
|
285 (dresolve_tac (thms"analz_mono_contra")) |
|
286 THEN' mp_tac |
|
287 end |
|
288 *} |
|
289 |
99 |
290 |
100 lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)" |
291 lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)" |
101 by (induct e, auto simp: knows_Cons) |
292 by (induct e, auto simp: knows_Cons) |
102 |
293 |
103 lemma initState_subset_knows: "initState A <= knows A evs" |
294 lemma initState_subset_knows: "initState A <= knows A evs" |
104 apply (induct_tac evs) |
295 apply (induct_tac evs, simp) |
105 apply (simp add: ); |
|
106 apply (blast intro: knows_subset_knows_Cons [THEN subsetD]) |
296 apply (blast intro: knows_subset_knows_Cons [THEN subsetD]) |
107 done |
297 done |
108 |
298 |
109 |
299 |
110 (*For proving new_keys_not_used*) |
300 text{*For proving @{text new_keys_not_used}*} |
111 lemma keysFor_parts_insert: |
301 lemma keysFor_parts_insert: |
112 "[| K \<in> keysFor (parts (insert X G)); X \<in> synth (analz H) |] \ |
302 "[| K \<in> keysFor (parts (insert X G)); X \<in> synth (analz H) |] |
113 \ ==> K \<in> keysFor (parts (G Un H)) | Key (invKey K) \<in> parts H"; |
303 ==> K \<in> keysFor (parts (G \<union> H)) | Key (invKey K) \<in> parts H"; |
114 by (force |
304 by (force |
115 dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD] |
305 dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD] |
116 analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD] |
306 analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD] |
117 intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD]) |
307 intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD]) |
118 |
308 |
123 |
313 |
124 subsubsection{*Useful for case analysis on whether a hash is a spoof or not*} |
314 subsubsection{*Useful for case analysis on whether a hash is a spoof or not*} |
125 |
315 |
126 ML |
316 ML |
127 {* |
317 {* |
|
318 val knows_Cons = thm "knows_Cons" |
|
319 val used_Nil = thm "used_Nil" |
|
320 val used_Cons = thm "used_Cons" |
|
321 |
|
322 val Notes_imp_used = thm "Notes_imp_used"; |
|
323 val Says_imp_used = thm "Says_imp_used"; |
|
324 val MPair_used = thm "MPair_used"; |
|
325 val parts_insert_knows_Spy = thm "parts_insert_knows_Spy"; |
|
326 val knows_Spy_Says = thm "knows_Spy_Says"; |
|
327 val knows_Spy_Notes = thm "knows_Spy_Notes"; |
|
328 val knows_Spy_Gets = thm "knows_Spy_Gets"; |
|
329 val knows_Spy_subset_knows_Spy_Says = thm "knows_Spy_subset_knows_Spy_Says"; |
|
330 val knows_Spy_subset_knows_Spy_Notes = thm "knows_Spy_subset_knows_Spy_Notes"; |
|
331 val knows_Spy_subset_knows_Spy_Gets = thm "knows_Spy_subset_knows_Spy_Gets"; |
|
332 val Says_imp_knows_Spy = thm "Says_imp_knows_Spy"; |
|
333 val Notes_imp_knows_Spy = thm "Notes_imp_knows_Spy"; |
|
334 val knows_Spy_partsEs = thms "knows_Spy_partsEs"; |
|
335 val spies_partsEs = thms "spies_partsEs"; |
|
336 val Says_imp_spies = thm "Says_imp_spies"; |
|
337 val parts_insert_spies = thm "parts_insert_spies"; |
|
338 val knows_Says = thm "knows_Says"; |
|
339 val knows_Notes = thm "knows_Notes"; |
|
340 val knows_Gets = thm "knows_Gets"; |
|
341 val knows_subset_knows_Says = thm "knows_subset_knows_Says"; |
|
342 val knows_subset_knows_Notes = thm "knows_subset_knows_Notes"; |
|
343 val knows_subset_knows_Gets = thm "knows_subset_knows_Gets"; |
|
344 val Says_imp_knows = thm "Says_imp_knows"; |
|
345 val Notes_imp_knows = thm "Notes_imp_knows"; |
|
346 val Gets_imp_knows_agents = thm "Gets_imp_knows_agents"; |
|
347 val knows_imp_Says_Gets_Notes_initState = thm "knows_imp_Says_Gets_Notes_initState"; |
|
348 val knows_Spy_imp_Says_Notes_initState = thm "knows_Spy_imp_Says_Notes_initState"; |
|
349 val parts_knows_Spy_subset_used = thm "parts_knows_Spy_subset_used"; |
|
350 val usedI = thm "usedI"; |
|
351 val initState_into_used = thm "initState_into_used"; |
|
352 val used_Says = thm "used_Says"; |
|
353 val used_Notes = thm "used_Notes"; |
|
354 val used_Gets = thm "used_Gets"; |
|
355 val used_nil_subset = thm "used_nil_subset"; |
|
356 val analz_mono_contra = thms "analz_mono_contra"; |
|
357 val knows_subset_knows_Cons = thm "knows_subset_knows_Cons"; |
|
358 val initState_subset_knows = thm "initState_subset_knows"; |
|
359 val keysFor_parts_insert = thm "keysFor_parts_insert"; |
|
360 |
|
361 |
128 val synth_analz_mono = thm "synth_analz_mono"; |
362 val synth_analz_mono = thm "synth_analz_mono"; |
129 |
363 |
130 val synth_analz_mono_contra_tac = |
364 val synth_analz_mono_contra_tac = |
131 let val syan_impI = inst "P" "?Y ~: synth (analz (knows Spy ?evs))" impI |
365 let val syan_impI = inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI |
132 in |
366 in |
133 rtac syan_impI THEN' |
367 rtac syan_impI THEN' |
134 REPEAT1 o |
368 REPEAT1 o |
135 (dresolve_tac |
369 (dresolve_tac |
136 [knows_Spy_subset_knows_Spy_Says RS synth_analz_mono RS contra_subsetD, |
370 [knows_Spy_subset_knows_Spy_Says RS synth_analz_mono RS contra_subsetD, |