1 (* Title: HOL/Auth/Message |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1996 University of Cambridge |
|
5 |
|
6 Datatypes of agents and messages; |
|
7 Inductive relations "parts", "analz" and "synth" |
|
8 *) |
|
9 |
|
10 (*ML bindings for definitions and axioms*) |
|
11 val invKey = thm "invKey"; |
|
12 val keysFor_def = thm "keysFor_def"; |
|
13 val parts_mono = thm "parts_mono"; |
|
14 val analz_mono = thm "analz_mono"; |
|
15 val synth_mono = thm "synth_mono"; |
|
16 val HPair_def = thm "HPair_def"; |
|
17 val symKeys_def = thm "symKeys_def"; |
|
18 |
|
19 structure parts = |
|
20 struct |
|
21 val induct = thm "parts.induct"; |
|
22 val Inj = thm "parts.Inj"; |
|
23 val Fst = thm "parts.Fst"; |
|
24 val Snd = thm "parts.Snd"; |
|
25 val Body = thm "parts.Body"; |
|
26 end; |
|
27 |
|
28 structure analz = |
|
29 struct |
|
30 val induct = thm "analz.induct"; |
|
31 val Inj = thm "analz.Inj"; |
|
32 val Fst = thm "analz.Fst"; |
|
33 val Snd = thm "analz.Snd"; |
|
34 val Decrypt = thm "analz.Decrypt"; |
|
35 end; |
|
36 |
|
37 structure synth = |
|
38 struct |
|
39 val induct = thm "synth.induct"; |
|
40 val Inj = thm "synth.Inj"; |
|
41 val Agent = thm "synth.Agent"; |
|
42 val Number = thm "synth.Number"; |
|
43 val Hash = thm "synth.Hash"; |
|
44 val Crypt = thm "synth.Crypt"; |
|
45 end; |
|
46 |
|
47 |
|
48 (*Equations hold because constructors are injective; cannot prove for all f*) |
|
49 Goal "(Friend x \\<in> Friend`A) = (x:A)"; |
|
50 by Auto_tac; |
|
51 qed "Friend_image_eq"; |
|
52 |
|
53 Goal "(Key x \\<in> Key`A) = (x\\<in>A)"; |
|
54 by Auto_tac; |
|
55 qed "Key_image_eq"; |
|
56 |
|
57 Goal "(Nonce x \\<notin> Key`A)"; |
|
58 by Auto_tac; |
|
59 qed "Nonce_Key_image_eq"; |
|
60 Addsimps [Friend_image_eq, Key_image_eq, Nonce_Key_image_eq]; |
|
61 |
|
62 |
|
63 (** Inverse of keys **) |
|
64 |
|
65 Goal "(invKey K = invKey K') = (K=K')"; |
|
66 by Safe_tac; |
|
67 by (rtac box_equals 1); |
|
68 by (REPEAT (rtac invKey 2)); |
|
69 by (Asm_simp_tac 1); |
|
70 qed "invKey_eq"; |
|
71 |
|
72 Addsimps [invKey_eq]; |
|
73 |
|
74 |
|
75 (**** keysFor operator ****) |
|
76 |
|
77 Goalw [keysFor_def] "keysFor {} = {}"; |
|
78 by (Blast_tac 1); |
|
79 qed "keysFor_empty"; |
|
80 |
|
81 Goalw [keysFor_def] "keysFor (H Un H') = keysFor H Un keysFor H'"; |
|
82 by (Blast_tac 1); |
|
83 qed "keysFor_Un"; |
|
84 |
|
85 Goalw [keysFor_def] "keysFor (\\<Union>i\\<in>A. H i) = (\\<Union>i\\<in>A. keysFor (H i))"; |
|
86 by (Blast_tac 1); |
|
87 qed "keysFor_UN"; |
|
88 |
|
89 (*Monotonicity*) |
|
90 Goalw [keysFor_def] "G\\<subseteq>H ==> keysFor(G) \\<subseteq> keysFor(H)"; |
|
91 by (Blast_tac 1); |
|
92 qed "keysFor_mono"; |
|
93 |
|
94 Goalw [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H"; |
|
95 by Auto_tac; |
|
96 qed "keysFor_insert_Agent"; |
|
97 |
|
98 Goalw [keysFor_def] "keysFor (insert (Nonce N) H) = keysFor H"; |
|
99 by Auto_tac; |
|
100 qed "keysFor_insert_Nonce"; |
|
101 |
|
102 Goalw [keysFor_def] "keysFor (insert (Number N) H) = keysFor H"; |
|
103 by Auto_tac; |
|
104 qed "keysFor_insert_Number"; |
|
105 |
|
106 Goalw [keysFor_def] "keysFor (insert (Key K) H) = keysFor H"; |
|
107 by Auto_tac; |
|
108 qed "keysFor_insert_Key"; |
|
109 |
|
110 Goalw [keysFor_def] "keysFor (insert (Hash X) H) = keysFor H"; |
|
111 by Auto_tac; |
|
112 qed "keysFor_insert_Hash"; |
|
113 |
|
114 Goalw [keysFor_def] "keysFor (insert {|X,Y|} H) = keysFor H"; |
|
115 by Auto_tac; |
|
116 qed "keysFor_insert_MPair"; |
|
117 |
|
118 Goalw [keysFor_def] |
|
119 "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"; |
|
120 by Auto_tac; |
|
121 qed "keysFor_insert_Crypt"; |
|
122 |
|
123 Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, |
|
124 keysFor_insert_Agent, keysFor_insert_Nonce, |
|
125 keysFor_insert_Number, keysFor_insert_Key, |
|
126 keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt]; |
|
127 AddSEs [keysFor_Un RS equalityD1 RS subsetD RS UnE, |
|
128 keysFor_UN RS equalityD1 RS subsetD RS UN_E]; |
|
129 |
|
130 Goalw [keysFor_def] "keysFor (Key`E) = {}"; |
|
131 by Auto_tac; |
|
132 qed "keysFor_image_Key"; |
|
133 Addsimps [keysFor_image_Key]; |
|
134 |
|
135 Goalw [keysFor_def] "Crypt K X \\<in> H ==> invKey K \\<in> keysFor H"; |
|
136 by (Blast_tac 1); |
|
137 qed "Crypt_imp_invKey_keysFor"; |
|
138 |
|
139 |
|
140 (**** Inductive relation "parts" ****) |
|
141 |
|
142 val major::prems = |
|
143 Goal "[| {|X,Y|} \\<in> parts H; \ |
|
144 \ [| X \\<in> parts H; Y \\<in> parts H |] ==> P \ |
|
145 \ |] ==> P"; |
|
146 by (cut_facts_tac [major] 1); |
|
147 by (resolve_tac prems 1); |
|
148 by (REPEAT (eresolve_tac [asm_rl, parts.Fst, parts.Snd] 1)); |
|
149 qed "MPair_parts"; |
|
150 |
|
151 AddSEs [MPair_parts, make_elim parts.Body]; |
|
152 (*NB These two rules are UNSAFE in the formal sense, as they discard the |
|
153 compound message. They work well on THIS FILE. |
|
154 MPair_parts is left as SAFE because it speeds up proofs. |
|
155 The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*) |
|
156 |
|
157 Goal "H \\<subseteq> parts(H)"; |
|
158 by (Blast_tac 1); |
|
159 qed "parts_increasing"; |
|
160 |
|
161 bind_thm ("parts_insertI", impOfSubs (subset_insertI RS parts_mono)); |
|
162 |
|
163 Goal "parts{} = {}"; |
|
164 by Safe_tac; |
|
165 by (etac parts.induct 1); |
|
166 by (ALLGOALS Blast_tac); |
|
167 qed "parts_empty"; |
|
168 Addsimps [parts_empty]; |
|
169 |
|
170 Goal "X\\<in> parts{} ==> P"; |
|
171 by (Asm_full_simp_tac 1); |
|
172 qed "parts_emptyE"; |
|
173 AddSEs [parts_emptyE]; |
|
174 |
|
175 (*WARNING: loops if H = {Y}, therefore must not be repeated!*) |
|
176 Goal "X\\<in> parts H ==> \\<exists>Y\\<in>H. X\\<in> parts {Y}"; |
|
177 by (etac parts.induct 1); |
|
178 by (ALLGOALS Blast_tac); |
|
179 qed "parts_singleton"; |
|
180 |
|
181 |
|
182 (** Unions **) |
|
183 |
|
184 Goal "parts(G) Un parts(H) \\<subseteq> parts(G Un H)"; |
|
185 by (REPEAT (ares_tac [Un_least, parts_mono, Un_upper1, Un_upper2] 1)); |
|
186 val parts_Un_subset1 = result(); |
|
187 |
|
188 Goal "parts(G Un H) \\<subseteq> parts(G) Un parts(H)"; |
|
189 by (rtac subsetI 1); |
|
190 by (etac parts.induct 1); |
|
191 by (ALLGOALS Blast_tac); |
|
192 val parts_Un_subset2 = result(); |
|
193 |
|
194 Goal "parts(G Un H) = parts(G) Un parts(H)"; |
|
195 by (REPEAT (ares_tac [equalityI, parts_Un_subset1, parts_Un_subset2] 1)); |
|
196 qed "parts_Un"; |
|
197 |
|
198 Goal "parts (insert X H) = parts {X} Un parts H"; |
|
199 by (stac (read_instantiate [("A","H")] insert_is_Un) 1); |
|
200 by (simp_tac (HOL_ss addsimps [parts_Un]) 1); |
|
201 qed "parts_insert"; |
|
202 |
|
203 (*TWO inserts to avoid looping. This rewrite is better than nothing. |
|
204 Not suitable for Addsimps: its behaviour can be strange.*) |
|
205 Goal "parts (insert X (insert Y H)) = parts {X} Un parts {Y} Un parts H"; |
|
206 by (simp_tac (simpset() addsimps [Un_assoc]) 1); |
|
207 by (simp_tac (simpset() addsimps [parts_insert RS sym]) 1); |
|
208 qed "parts_insert2"; |
|
209 |
|
210 Goal "(\\<Union>x\\<in>A. parts(H x)) \\<subseteq> parts(\\<Union>x\\<in>A. H x)"; |
|
211 by (REPEAT (ares_tac [UN_least, parts_mono, UN_upper] 1)); |
|
212 val parts_UN_subset1 = result(); |
|
213 |
|
214 Goal "parts(\\<Union>x\\<in>A. H x) \\<subseteq> (\\<Union>x\\<in>A. parts(H x))"; |
|
215 by (rtac subsetI 1); |
|
216 by (etac parts.induct 1); |
|
217 by (ALLGOALS Blast_tac); |
|
218 val parts_UN_subset2 = result(); |
|
219 |
|
220 Goal "parts(\\<Union>x\\<in>A. H x) = (\\<Union>x\\<in>A. parts(H x))"; |
|
221 by (REPEAT (ares_tac [equalityI, parts_UN_subset1, parts_UN_subset2] 1)); |
|
222 qed "parts_UN"; |
|
223 |
|
224 (*Added to simplify arguments to parts, analz and synth. |
|
225 NOTE: the UN versions are no longer used!*) |
|
226 Addsimps [parts_Un, parts_UN]; |
|
227 AddSEs [parts_Un RS equalityD1 RS subsetD RS UnE, |
|
228 parts_UN RS equalityD1 RS subsetD RS UN_E]; |
|
229 |
|
230 Goal "insert X (parts H) \\<subseteq> parts(insert X H)"; |
|
231 by (blast_tac (claset() addIs [impOfSubs parts_mono]) 1); |
|
232 qed "parts_insert_subset"; |
|
233 |
|
234 (** Idempotence and transitivity **) |
|
235 |
|
236 Goal "X\\<in> parts (parts H) ==> X\\<in> parts H"; |
|
237 by (etac parts.induct 1); |
|
238 by (ALLGOALS Blast_tac); |
|
239 qed "parts_partsD"; |
|
240 AddSDs [parts_partsD]; |
|
241 |
|
242 Goal "parts (parts H) = parts H"; |
|
243 by (Blast_tac 1); |
|
244 qed "parts_idem"; |
|
245 Addsimps [parts_idem]; |
|
246 |
|
247 Goal "[| X\\<in> parts G; G \\<subseteq> parts H |] ==> X\\<in> parts H"; |
|
248 by (dtac parts_mono 1); |
|
249 by (Blast_tac 1); |
|
250 qed "parts_trans"; |
|
251 |
|
252 (*Cut*) |
|
253 Goal "[| Y\\<in> parts (insert X G); X\\<in> parts H |] \ |
|
254 \ ==> Y\\<in> parts (G Un H)"; |
|
255 by (etac parts_trans 1); |
|
256 by Auto_tac; |
|
257 qed "parts_cut"; |
|
258 |
|
259 Goal "X\\<in> parts H ==> parts (insert X H) = parts H"; |
|
260 by (fast_tac (claset() addSDs [parts_cut] |
|
261 addIs [parts_insertI] |
|
262 addss (simpset())) 1); |
|
263 qed "parts_cut_eq"; |
|
264 |
|
265 Addsimps [parts_cut_eq]; |
|
266 |
|
267 |
|
268 (** Rewrite rules for pulling out atomic messages **) |
|
269 |
|
270 fun parts_tac i = |
|
271 EVERY [rtac ([subsetI, parts_insert_subset] MRS equalityI) i, |
|
272 etac parts.induct i, |
|
273 Auto_tac]; |
|
274 |
|
275 Goal "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"; |
|
276 by (parts_tac 1); |
|
277 qed "parts_insert_Agent"; |
|
278 |
|
279 Goal "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"; |
|
280 by (parts_tac 1); |
|
281 qed "parts_insert_Nonce"; |
|
282 |
|
283 Goal "parts (insert (Number N) H) = insert (Number N) (parts H)"; |
|
284 by (parts_tac 1); |
|
285 qed "parts_insert_Number"; |
|
286 |
|
287 Goal "parts (insert (Key K) H) = insert (Key K) (parts H)"; |
|
288 by (parts_tac 1); |
|
289 qed "parts_insert_Key"; |
|
290 |
|
291 Goal "parts (insert (Hash X) H) = insert (Hash X) (parts H)"; |
|
292 by (parts_tac 1); |
|
293 qed "parts_insert_Hash"; |
|
294 |
|
295 Goal "parts (insert (Crypt K X) H) = \ |
|
296 \ insert (Crypt K X) (parts (insert X H))"; |
|
297 by (rtac equalityI 1); |
|
298 by (rtac subsetI 1); |
|
299 by (etac parts.induct 1); |
|
300 by Auto_tac; |
|
301 by (etac parts.induct 1); |
|
302 by (ALLGOALS (blast_tac (claset() addIs [parts.Body]))); |
|
303 qed "parts_insert_Crypt"; |
|
304 |
|
305 Goal "parts (insert {|X,Y|} H) = \ |
|
306 \ insert {|X,Y|} (parts (insert X (insert Y H)))"; |
|
307 by (rtac equalityI 1); |
|
308 by (rtac subsetI 1); |
|
309 by (etac parts.induct 1); |
|
310 by Auto_tac; |
|
311 by (etac parts.induct 1); |
|
312 by (ALLGOALS (blast_tac (claset() addIs [parts.Fst, parts.Snd]))); |
|
313 qed "parts_insert_MPair"; |
|
314 |
|
315 Addsimps [parts_insert_Agent, parts_insert_Nonce, |
|
316 parts_insert_Number, parts_insert_Key, |
|
317 parts_insert_Hash, parts_insert_Crypt, parts_insert_MPair]; |
|
318 |
|
319 |
|
320 Goal "parts (Key`N) = Key`N"; |
|
321 by Auto_tac; |
|
322 by (etac parts.induct 1); |
|
323 by Auto_tac; |
|
324 qed "parts_image_Key"; |
|
325 Addsimps [parts_image_Key]; |
|
326 |
|
327 |
|
328 (*In any message, there is an upper bound N on its greatest nonce.*) |
|
329 Goal "\\<exists>N. \\<forall>n. N\\<le>n --> Nonce n \\<notin> parts {msg}"; |
|
330 by (induct_tac "msg" 1); |
|
331 by (ALLGOALS (asm_simp_tac (simpset() addsimps [exI, parts_insert2]))); |
|
332 (*MPair case: blast_tac works out the necessary sum itself!*) |
|
333 by (blast_tac (claset() addSEs [add_leE]) 2); |
|
334 (*Nonce case*) |
|
335 by (res_inst_tac [("x","N + Suc nat")] exI 1); |
|
336 by (auto_tac (claset() addSEs [add_leE], simpset())); |
|
337 qed "msg_Nonce_supply"; |
|
338 |
|
339 |
|
340 (**** Inductive relation "analz" ****) |
|
341 |
|
342 val major::prems = |
|
343 Goal "[| {|X,Y|} \\<in> analz H; \ |
|
344 \ [| X \\<in> analz H; Y \\<in> analz H |] ==> P \ |
|
345 \ |] ==> P"; |
|
346 by (cut_facts_tac [major] 1); |
|
347 by (resolve_tac prems 1); |
|
348 by (REPEAT (eresolve_tac [asm_rl, analz.Fst, analz.Snd] 1)); |
|
349 qed "MPair_analz"; |
|
350 |
|
351 AddSEs [MPair_analz]; (*Making it safe speeds up proofs*) |
|
352 |
|
353 Goal "H \\<subseteq> analz(H)"; |
|
354 by (Blast_tac 1); |
|
355 qed "analz_increasing"; |
|
356 |
|
357 Goal "analz H \\<subseteq> parts H"; |
|
358 by (rtac subsetI 1); |
|
359 by (etac analz.induct 1); |
|
360 by (ALLGOALS Blast_tac); |
|
361 qed "analz_subset_parts"; |
|
362 |
|
363 bind_thm ("not_parts_not_analz", analz_subset_parts RS contra_subsetD); |
|
364 |
|
365 |
|
366 Goal "parts (analz H) = parts H"; |
|
367 by (rtac equalityI 1); |
|
368 by (rtac (analz_subset_parts RS parts_mono RS subset_trans) 1); |
|
369 by (Simp_tac 1); |
|
370 by (blast_tac (claset() addIs [analz_increasing RS parts_mono RS subsetD]) 1); |
|
371 qed "parts_analz"; |
|
372 Addsimps [parts_analz]; |
|
373 |
|
374 Goal "analz (parts H) = parts H"; |
|
375 by Auto_tac; |
|
376 by (etac analz.induct 1); |
|
377 by Auto_tac; |
|
378 qed "analz_parts"; |
|
379 Addsimps [analz_parts]; |
|
380 |
|
381 bind_thm ("analz_insertI", impOfSubs (subset_insertI RS analz_mono)); |
|
382 |
|
383 (** General equational properties **) |
|
384 |
|
385 Goal "analz{} = {}"; |
|
386 by Safe_tac; |
|
387 by (etac analz.induct 1); |
|
388 by (ALLGOALS Blast_tac); |
|
389 qed "analz_empty"; |
|
390 Addsimps [analz_empty]; |
|
391 |
|
392 (*Converse fails: we can analz more from the union than from the |
|
393 separate parts, as a key in one might decrypt a message in the other*) |
|
394 Goal "analz(G) Un analz(H) \\<subseteq> analz(G Un H)"; |
|
395 by (REPEAT (ares_tac [Un_least, analz_mono, Un_upper1, Un_upper2] 1)); |
|
396 qed "analz_Un"; |
|
397 |
|
398 Goal "insert X (analz H) \\<subseteq> analz(insert X H)"; |
|
399 by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1); |
|
400 qed "analz_insert"; |
|
401 |
|
402 (** Rewrite rules for pulling out atomic messages **) |
|
403 |
|
404 fun analz_tac i = |
|
405 EVERY [rtac ([subsetI, analz_insert] MRS equalityI) i, |
|
406 etac analz.induct i, |
|
407 Auto_tac]; |
|
408 |
|
409 Goal "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"; |
|
410 by (analz_tac 1); |
|
411 qed "analz_insert_Agent"; |
|
412 |
|
413 Goal "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"; |
|
414 by (analz_tac 1); |
|
415 qed "analz_insert_Nonce"; |
|
416 |
|
417 Goal "analz (insert (Number N) H) = insert (Number N) (analz H)"; |
|
418 by (analz_tac 1); |
|
419 qed "analz_insert_Number"; |
|
420 |
|
421 Goal "analz (insert (Hash X) H) = insert (Hash X) (analz H)"; |
|
422 by (analz_tac 1); |
|
423 qed "analz_insert_Hash"; |
|
424 |
|
425 (*Can only pull out Keys if they are not needed to decrypt the rest*) |
|
426 Goalw [keysFor_def] |
|
427 "K \\<notin> keysFor (analz H) ==> \ |
|
428 \ analz (insert (Key K) H) = insert (Key K) (analz H)"; |
|
429 by (analz_tac 1); |
|
430 qed "analz_insert_Key"; |
|
431 |
|
432 Goal "analz (insert {|X,Y|} H) = \ |
|
433 \ insert {|X,Y|} (analz (insert X (insert Y H)))"; |
|
434 by (rtac equalityI 1); |
|
435 by (rtac subsetI 1); |
|
436 by (etac analz.induct 1); |
|
437 by Auto_tac; |
|
438 by (etac analz.induct 1); |
|
439 by (ALLGOALS (blast_tac (claset() addIs [analz.Fst, analz.Snd]))); |
|
440 qed "analz_insert_MPair"; |
|
441 |
|
442 (*Can pull out enCrypted message if the Key is not known*) |
|
443 Goal "Key (invKey K) \\<notin> analz H ==> \ |
|
444 \ analz (insert (Crypt K X) H) = \ |
|
445 \ insert (Crypt K X) (analz H)"; |
|
446 by (analz_tac 1); |
|
447 qed "analz_insert_Crypt"; |
|
448 |
|
449 Goal "Key (invKey K) \\<in> analz H ==> \ |
|
450 \ analz (insert (Crypt K X) H) \\<subseteq> \ |
|
451 \ insert (Crypt K X) (analz (insert X H))"; |
|
452 by (rtac subsetI 1); |
|
453 by (eres_inst_tac [("xa","x")] analz.induct 1); |
|
454 by Auto_tac; |
|
455 val lemma1 = result(); |
|
456 |
|
457 Goal "Key (invKey K) \\<in> analz H ==> \ |
|
458 \ insert (Crypt K X) (analz (insert X H)) \\<subseteq> \ |
|
459 \ analz (insert (Crypt K X) H)"; |
|
460 by Auto_tac; |
|
461 by (eres_inst_tac [("xa","x")] analz.induct 1); |
|
462 by Auto_tac; |
|
463 by (blast_tac (claset() addIs [analz_insertI, analz.Decrypt]) 1); |
|
464 val lemma2 = result(); |
|
465 |
|
466 Goal "Key (invKey K) \\<in> analz H ==> \ |
|
467 \ analz (insert (Crypt K X) H) = \ |
|
468 \ insert (Crypt K X) (analz (insert X H))"; |
|
469 by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1)); |
|
470 qed "analz_insert_Decrypt"; |
|
471 |
|
472 (*Case analysis: either the message is secure, or it is not! |
|
473 Effective, but can cause subgoals to blow up! |
|
474 Use with split_if; apparently split_tac does not cope with patterns |
|
475 such as "analz (insert (Crypt K X) H)" *) |
|
476 Goal "analz (insert (Crypt K X) H) = \ |
|
477 \ (if (Key (invKey K) \\<in> analz H) \ |
|
478 \ then insert (Crypt K X) (analz (insert X H)) \ |
|
479 \ else insert (Crypt K X) (analz H))"; |
|
480 by (case_tac "Key (invKey K) \\<in> analz H " 1); |
|
481 by (ALLGOALS (asm_simp_tac (simpset() addsimps [analz_insert_Crypt, |
|
482 analz_insert_Decrypt]))); |
|
483 qed "analz_Crypt_if"; |
|
484 |
|
485 Addsimps [analz_insert_Agent, analz_insert_Nonce, |
|
486 analz_insert_Number, analz_insert_Key, |
|
487 analz_insert_Hash, analz_insert_MPair, analz_Crypt_if]; |
|
488 |
|
489 (*This rule supposes "for the sake of argument" that we have the key.*) |
|
490 Goal "analz (insert (Crypt K X) H) \\<subseteq> \ |
|
491 \ insert (Crypt K X) (analz (insert X H))"; |
|
492 by (rtac subsetI 1); |
|
493 by (etac analz.induct 1); |
|
494 by Auto_tac; |
|
495 qed "analz_insert_Crypt_subset"; |
|
496 |
|
497 |
|
498 Goal "analz (Key`N) = Key`N"; |
|
499 by Auto_tac; |
|
500 by (etac analz.induct 1); |
|
501 by Auto_tac; |
|
502 qed "analz_image_Key"; |
|
503 |
|
504 Addsimps [analz_image_Key]; |
|
505 |
|
506 |
|
507 (** Idempotence and transitivity **) |
|
508 |
|
509 Goal "X\\<in> analz (analz H) ==> X\\<in> analz H"; |
|
510 by (etac analz.induct 1); |
|
511 by (ALLGOALS Blast_tac); |
|
512 qed "analz_analzD"; |
|
513 AddSDs [analz_analzD]; |
|
514 |
|
515 Goal "analz (analz H) = analz H"; |
|
516 by (Blast_tac 1); |
|
517 qed "analz_idem"; |
|
518 Addsimps [analz_idem]; |
|
519 |
|
520 Goal "[| X\\<in> analz G; G \\<subseteq> analz H |] ==> X\\<in> analz H"; |
|
521 by (dtac analz_mono 1); |
|
522 by (Blast_tac 1); |
|
523 qed "analz_trans"; |
|
524 |
|
525 (*Cut; Lemma 2 of Lowe*) |
|
526 Goal "[| Y\\<in> analz (insert X H); X\\<in> analz H |] ==> Y\\<in> analz H"; |
|
527 by (etac analz_trans 1); |
|
528 by (Blast_tac 1); |
|
529 qed "analz_cut"; |
|
530 |
|
531 (*Cut can be proved easily by induction on |
|
532 "Y: analz (insert X H) ==> X: analz H --> Y: analz H" |
|
533 *) |
|
534 |
|
535 (*This rewrite rule helps in the simplification of messages that involve |
|
536 the forwarding of unknown components (X). Without it, removing occurrences |
|
537 of X can be very complicated. *) |
|
538 Goal "X\\<in> analz H ==> analz (insert X H) = analz H"; |
|
539 by (blast_tac (claset() addIs [analz_cut, analz_insertI]) 1); |
|
540 qed "analz_insert_eq"; |
|
541 |
|
542 |
|
543 (** A congruence rule for "analz" **) |
|
544 |
|
545 Goal "[| analz G \\<subseteq> analz G'; analz H \\<subseteq> analz H' \ |
|
546 \ |] ==> analz (G Un H) \\<subseteq> analz (G' Un H')"; |
|
547 by (Clarify_tac 1); |
|
548 by (etac analz.induct 1); |
|
549 by (ALLGOALS (best_tac (claset() addIs [analz_mono RS subsetD]))); |
|
550 qed "analz_subset_cong"; |
|
551 |
|
552 Goal "[| analz G = analz G'; analz H = analz H' \ |
|
553 \ |] ==> analz (G Un H) = analz (G' Un H')"; |
|
554 by (REPEAT_FIRST (ares_tac [equalityI, analz_subset_cong] |
|
555 ORELSE' etac equalityE)); |
|
556 qed "analz_cong"; |
|
557 |
|
558 |
|
559 Goal "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"; |
|
560 by (asm_simp_tac (simpset() addsimps [insert_def] delsimps [singleton_conv] |
|
561 setloop (rtac analz_cong)) 1); |
|
562 qed "analz_insert_cong"; |
|
563 |
|
564 (*If there are no pairs or encryptions then analz does nothing*) |
|
565 Goal "[| \\<forall>X Y. {|X,Y|} \\<notin> H; \\<forall>X K. Crypt K X \\<notin> H |] ==> analz H = H"; |
|
566 by Safe_tac; |
|
567 by (etac analz.induct 1); |
|
568 by (ALLGOALS Blast_tac); |
|
569 qed "analz_trivial"; |
|
570 |
|
571 (*These two are obsolete (with a single Spy) but cost little to prove...*) |
|
572 Goal "X\\<in> analz (\\<Union>i\\<in>A. analz (H i)) ==> X\\<in> analz (\\<Union>i\\<in>A. H i)"; |
|
573 by (etac analz.induct 1); |
|
574 by (ALLGOALS (blast_tac (claset() addIs [impOfSubs analz_mono]))); |
|
575 val lemma = result(); |
|
576 |
|
577 Goal "analz (\\<Union>i\\<in>A. analz (H i)) = analz (\\<Union>i\\<in>A. H i)"; |
|
578 by (blast_tac (claset() addIs [lemma, impOfSubs analz_mono]) 1); |
|
579 qed "analz_UN_analz"; |
|
580 Addsimps [analz_UN_analz]; |
|
581 |
|
582 |
|
583 (**** Inductive relation "synth" ****) |
|
584 |
|
585 Goal "H \\<subseteq> synth(H)"; |
|
586 by (Blast_tac 1); |
|
587 qed "synth_increasing"; |
|
588 |
|
589 (** Unions **) |
|
590 |
|
591 (*Converse fails: we can synth more from the union than from the |
|
592 separate parts, building a compound message using elements of each.*) |
|
593 Goal "synth(G) Un synth(H) \\<subseteq> synth(G Un H)"; |
|
594 by (REPEAT (ares_tac [Un_least, synth_mono, Un_upper1, Un_upper2] 1)); |
|
595 qed "synth_Un"; |
|
596 |
|
597 Goal "insert X (synth H) \\<subseteq> synth(insert X H)"; |
|
598 by (blast_tac (claset() addIs [impOfSubs synth_mono]) 1); |
|
599 qed "synth_insert"; |
|
600 |
|
601 (** Idempotence and transitivity **) |
|
602 |
|
603 Goal "X\\<in> synth (synth H) ==> X\\<in> synth H"; |
|
604 by (etac synth.induct 1); |
|
605 by (ALLGOALS Blast_tac); |
|
606 qed "synth_synthD"; |
|
607 AddSDs [synth_synthD]; |
|
608 |
|
609 Goal "synth (synth H) = synth H"; |
|
610 by (Blast_tac 1); |
|
611 qed "synth_idem"; |
|
612 |
|
613 Goal "[| X\\<in> synth G; G \\<subseteq> synth H |] ==> X\\<in> synth H"; |
|
614 by (dtac synth_mono 1); |
|
615 by (Blast_tac 1); |
|
616 qed "synth_trans"; |
|
617 |
|
618 (*Cut; Lemma 2 of Lowe*) |
|
619 Goal "[| Y\\<in> synth (insert X H); X\\<in> synth H |] ==> Y\\<in> synth H"; |
|
620 by (etac synth_trans 1); |
|
621 by (Blast_tac 1); |
|
622 qed "synth_cut"; |
|
623 |
|
624 Goal "Agent A \\<in> synth H"; |
|
625 by (Blast_tac 1); |
|
626 qed "Agent_synth"; |
|
627 |
|
628 Goal "Number n \\<in> synth H"; |
|
629 by (Blast_tac 1); |
|
630 qed "Number_synth"; |
|
631 |
|
632 Goal "(Nonce N \\<in> synth H) = (Nonce N \\<in> H)"; |
|
633 by (Blast_tac 1); |
|
634 qed "Nonce_synth_eq"; |
|
635 |
|
636 Goal "(Key K \\<in> synth H) = (Key K \\<in> H)"; |
|
637 by (Blast_tac 1); |
|
638 qed "Key_synth_eq"; |
|
639 |
|
640 Goal "Key K \\<notin> H ==> (Crypt K X \\<in> synth H) = (Crypt K X \\<in> H)"; |
|
641 by (Blast_tac 1); |
|
642 qed "Crypt_synth_eq"; |
|
643 |
|
644 Addsimps [Agent_synth, Number_synth, |
|
645 Nonce_synth_eq, Key_synth_eq, Crypt_synth_eq]; |
|
646 |
|
647 |
|
648 Goalw [keysFor_def] |
|
649 "keysFor (synth H) = keysFor H Un invKey`{K. Key K \\<in> H}"; |
|
650 by (Blast_tac 1); |
|
651 qed "keysFor_synth"; |
|
652 Addsimps [keysFor_synth]; |
|
653 |
|
654 |
|
655 (*** Combinations of parts, analz and synth ***) |
|
656 |
|
657 Goal "parts (synth H) = parts H Un synth H"; |
|
658 by (rtac equalityI 1); |
|
659 by (rtac subsetI 1); |
|
660 by (etac parts.induct 1); |
|
661 by (ALLGOALS |
|
662 (blast_tac (claset() addIs [synth_increasing RS parts_mono RS subsetD, |
|
663 parts.Fst, parts.Snd, parts.Body]))); |
|
664 qed "parts_synth"; |
|
665 Addsimps [parts_synth]; |
|
666 |
|
667 Goal "analz (analz G Un H) = analz (G Un H)"; |
|
668 by (REPEAT_FIRST (resolve_tac [equalityI, analz_subset_cong])); |
|
669 by (ALLGOALS Simp_tac); |
|
670 qed "analz_analz_Un"; |
|
671 |
|
672 Goal "analz (synth G Un H) = analz (G Un H) Un synth G"; |
|
673 by (rtac equalityI 1); |
|
674 by (rtac subsetI 1); |
|
675 by (etac analz.induct 1); |
|
676 by (blast_tac (claset() addIs [impOfSubs analz_mono]) 5); |
|
677 by (ALLGOALS |
|
678 (blast_tac (claset() addIs [analz.Fst, analz.Snd, analz.Decrypt]))); |
|
679 qed "analz_synth_Un"; |
|
680 |
|
681 Goal "analz (synth H) = analz H Un synth H"; |
|
682 by (cut_inst_tac [("H","{}")] analz_synth_Un 1); |
|
683 by (Full_simp_tac 1); |
|
684 qed "analz_synth"; |
|
685 Addsimps [analz_analz_Un, analz_synth_Un, analz_synth]; |
|
686 |
|
687 |
|
688 (** For reasoning about the Fake rule in traces **) |
|
689 |
|
690 Goal "X\\<in> G ==> parts(insert X H) \\<subseteq> parts G Un parts H"; |
|
691 by (rtac ([parts_mono, parts_Un_subset2] MRS subset_trans) 1); |
|
692 by (Blast_tac 1); |
|
693 qed "parts_insert_subset_Un"; |
|
694 |
|
695 (*More specifically for Fake. Very occasionally we could do with a version |
|
696 of the form parts{X} \\<subseteq> synth (analz H) Un parts H *) |
|
697 Goal "X\\<in> synth (analz H) ==> \ |
|
698 \ parts (insert X H) \\<subseteq> synth (analz H) Un parts H"; |
|
699 by (dtac parts_insert_subset_Un 1); |
|
700 by (Full_simp_tac 1); |
|
701 by (Blast_tac 1); |
|
702 qed "Fake_parts_insert"; |
|
703 |
|
704 (*H is sometimes (Key ` KK Un spies evs), so can't put G=H*) |
|
705 Goal "X\\<in> synth (analz G) ==> \ |
|
706 \ analz (insert X H) \\<subseteq> synth (analz G) Un analz (G Un H)"; |
|
707 by (rtac subsetI 1); |
|
708 by (subgoal_tac "x \\<in> analz (synth (analz G) Un H)" 1); |
|
709 by (blast_tac (claset() addIs [impOfSubs analz_mono, |
|
710 impOfSubs (analz_mono RS synth_mono)]) 2); |
|
711 by (Full_simp_tac 1); |
|
712 by (Blast_tac 1); |
|
713 qed "Fake_analz_insert"; |
|
714 |
|
715 Goal "(X\\<in> analz H & X\\<in> parts H) = (X\\<in> analz H)"; |
|
716 by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1); |
|
717 val analz_conj_parts = result(); |
|
718 |
|
719 Goal "(X\\<in> analz H | X\\<in> parts H) = (X\\<in> parts H)"; |
|
720 by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1); |
|
721 val analz_disj_parts = result(); |
|
722 |
|
723 AddIffs [analz_conj_parts, analz_disj_parts]; |
|
724 |
|
725 (*Without this equation, other rules for synth and analz would yield |
|
726 redundant cases*) |
|
727 Goal "({|X,Y|} \\<in> synth (analz H)) = \ |
|
728 \ (X \\<in> synth (analz H) & Y \\<in> synth (analz H))"; |
|
729 by (Blast_tac 1); |
|
730 qed "MPair_synth_analz"; |
|
731 |
|
732 AddIffs [MPair_synth_analz]; |
|
733 |
|
734 Goal "[| Key K \\<in> analz H; Key (invKey K) \\<in> analz H |] \ |
|
735 \ ==> (Crypt K X \\<in> synth (analz H)) = (X \\<in> synth (analz H))"; |
|
736 by (Blast_tac 1); |
|
737 qed "Crypt_synth_analz"; |
|
738 |
|
739 |
|
740 Goal "X \\<notin> synth (analz H) \ |
|
741 \ ==> (Hash{|X,Y|} \\<in> synth (analz H)) = (Hash{|X,Y|} \\<in> analz H)"; |
|
742 by (Blast_tac 1); |
|
743 qed "Hash_synth_analz"; |
|
744 Addsimps [Hash_synth_analz]; |
|
745 |
|
746 |
|
747 (**** HPair: a combination of Hash and MPair ****) |
|
748 |
|
749 (*** Freeness ***) |
|
750 |
|
751 Goalw [HPair_def] "Agent A ~= Hash[X] Y"; |
|
752 by (Simp_tac 1); |
|
753 qed "Agent_neq_HPair"; |
|
754 |
|
755 Goalw [HPair_def] "Nonce N ~= Hash[X] Y"; |
|
756 by (Simp_tac 1); |
|
757 qed "Nonce_neq_HPair"; |
|
758 |
|
759 Goalw [HPair_def] "Number N ~= Hash[X] Y"; |
|
760 by (Simp_tac 1); |
|
761 qed "Number_neq_HPair"; |
|
762 |
|
763 Goalw [HPair_def] "Key K ~= Hash[X] Y"; |
|
764 by (Simp_tac 1); |
|
765 qed "Key_neq_HPair"; |
|
766 |
|
767 Goalw [HPair_def] "Hash Z ~= Hash[X] Y"; |
|
768 by (Simp_tac 1); |
|
769 qed "Hash_neq_HPair"; |
|
770 |
|
771 Goalw [HPair_def] "Crypt K X' ~= Hash[X] Y"; |
|
772 by (Simp_tac 1); |
|
773 qed "Crypt_neq_HPair"; |
|
774 |
|
775 val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair, Number_neq_HPair, |
|
776 Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair]; |
|
777 |
|
778 AddIffs HPair_neqs; |
|
779 AddIffs (HPair_neqs RL [not_sym]); |
|
780 |
|
781 Goalw [HPair_def] "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)"; |
|
782 by (Simp_tac 1); |
|
783 qed "HPair_eq"; |
|
784 |
|
785 Goalw [HPair_def] "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)"; |
|
786 by (Simp_tac 1); |
|
787 qed "MPair_eq_HPair"; |
|
788 |
|
789 Goalw [HPair_def] "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)"; |
|
790 by Auto_tac; |
|
791 qed "HPair_eq_MPair"; |
|
792 |
|
793 AddIffs [HPair_eq, MPair_eq_HPair, HPair_eq_MPair]; |
|
794 |
|
795 |
|
796 (*** Specialized laws, proved in terms of those for Hash and MPair ***) |
|
797 |
|
798 Goalw [HPair_def] "keysFor (insert (Hash[X] Y) H) = keysFor H"; |
|
799 by (Simp_tac 1); |
|
800 qed "keysFor_insert_HPair"; |
|
801 |
|
802 Goalw [HPair_def] |
|
803 "parts (insert (Hash[X] Y) H) = \ |
|
804 \ insert (Hash[X] Y) (insert (Hash{|X,Y|}) (parts (insert Y H)))"; |
|
805 by (Simp_tac 1); |
|
806 qed "parts_insert_HPair"; |
|
807 |
|
808 Goalw [HPair_def] |
|
809 "analz (insert (Hash[X] Y) H) = \ |
|
810 \ insert (Hash[X] Y) (insert (Hash{|X,Y|}) (analz (insert Y H)))"; |
|
811 by (Simp_tac 1); |
|
812 qed "analz_insert_HPair"; |
|
813 |
|
814 Goalw [HPair_def] "X \\<notin> synth (analz H) \ |
|
815 \ ==> (Hash[X] Y \\<in> synth (analz H)) = \ |
|
816 \ (Hash {|X, Y|} \\<in> analz H & Y \\<in> synth (analz H))"; |
|
817 by (Simp_tac 1); |
|
818 by (Blast_tac 1); |
|
819 qed "HPair_synth_analz"; |
|
820 |
|
821 Addsimps [keysFor_insert_HPair, parts_insert_HPair, analz_insert_HPair, |
|
822 HPair_synth_analz, HPair_synth_analz]; |
|
823 |
|
824 |
|
825 (*We do NOT want Crypt... messages broken up in protocols!!*) |
|
826 Delrules [make_elim parts.Body]; |
|
827 |
|
828 |
|
829 (** Rewrites to push in Key and Crypt messages, so that other messages can |
|
830 be pulled out using the analz_insert rules **) |
|
831 |
|
832 fun insComm x y = inst "x" x (inst "y" y insert_commute); |
|
833 |
|
834 val pushKeys = map (insComm "Key ?K") |
|
835 ["Agent ?C", "Nonce ?N", "Number ?N", |
|
836 "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"]; |
|
837 |
|
838 val pushCrypts = map (insComm "Crypt ?X ?K") |
|
839 ["Agent ?C", "Nonce ?N", "Number ?N", |
|
840 "Hash ?X'", "MPair ?X' ?Y"]; |
|
841 |
|
842 (*Cannot be added with Addsimps -- we don't always want to re-order messages*) |
|
843 bind_thms ("pushes", pushKeys@pushCrypts); |
|
844 |
|
845 |
|
846 (*** Tactics useful for many protocol proofs ***) |
|
847 |
|
848 (*Prove base case (subgoal i) and simplify others. A typical base case |
|
849 concerns Crypt K X \\<notin> Key`shrK`bad and cannot be proved by rewriting |
|
850 alone.*) |
|
851 fun prove_simple_subgoals_tac i = |
|
852 force_tac (claset(), simpset() addsimps [image_eq_UN]) i THEN |
|
853 ALLGOALS Asm_simp_tac; |
|
854 |
|
855 fun Fake_parts_insert_tac i = |
|
856 blast_tac (claset() addIs [parts_insertI] |
|
857 addDs [impOfSubs analz_subset_parts, |
|
858 impOfSubs Fake_parts_insert]) i; |
|
859 |
|
860 (*Apply rules to break down assumptions of the form |
|
861 Y \\<in> parts(insert X H) and Y \\<in> analz(insert X H) |
|
862 *) |
|
863 val Fake_insert_tac = |
|
864 dresolve_tac [impOfSubs Fake_analz_insert, |
|
865 impOfSubs Fake_parts_insert] THEN' |
|
866 eresolve_tac [asm_rl, synth.Inj]; |
|
867 |
|
868 fun Fake_insert_simp_tac ss i = |
|
869 REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i; |
|
870 |
|
871 |
|
872 (*Analysis of Fake cases. Also works for messages that forward unknown parts, |
|
873 but this application is no longer necessary if analz_insert_eq is used. |
|
874 Abstraction over i is ESSENTIAL: it delays the dereferencing of claset |
|
875 DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *) |
|
876 |
|
877 fun atomic_spy_analz_tac (cs,ss) = SELECT_GOAL |
|
878 (Fake_insert_simp_tac ss 1 |
|
879 THEN |
|
880 IF_UNSOLVED (Blast.depth_tac |
|
881 (cs addIs [analz_insertI, |
|
882 impOfSubs analz_subset_parts]) 4 1)); |
|
883 |
|
884 (*The explicit claset and simpset arguments help it work with Isar*) |
|
885 fun gen_spy_analz_tac (cs,ss) i = |
|
886 DETERM |
|
887 (SELECT_GOAL |
|
888 (EVERY |
|
889 [ (*push in occurrences of X...*) |
|
890 (REPEAT o CHANGED) |
|
891 (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1), |
|
892 (*...allowing further simplifications*) |
|
893 simp_tac ss 1, |
|
894 REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])), |
|
895 DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i); |
|
896 |
|
897 fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i; |
|
898 |
|
899 (*By default only o_apply is built-in. But in the presence of eta-expansion |
|
900 this means that some terms displayed as (f o g) will be rewritten, and others |
|
901 will not!*) |
|
902 Addsimps [o_def]; |
|