author | paulson |
Fri, 27 Apr 2001 17:16:21 +0200 | |
changeset 11270 | a315a3862bb4 |
parent 11264 | a47a9288f3f6 |
permissions | -rw-r--r-- |
11189 | 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"; |
|
11230
756c5034f08b
misc tidying; changing the predicate isSymKey to the set symKeys
paulson
parents:
11217
diff
changeset
|
17 |
val symKeys_def = thm "symKeys_def"; |
11189 | 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*) |
|
11217 | 49 |
Goal "(Friend x \\<in> Friend`A) = (x:A)"; |
11189 | 50 |
by Auto_tac; |
51 |
qed "Friend_image_eq"; |
|
52 |
||
11251 | 53 |
Goal "(Key x \\<in> Key`A) = (x\\<in>A)"; |
11189 | 54 |
by Auto_tac; |
55 |
qed "Key_image_eq"; |
|
56 |
||
11217 | 57 |
Goal "(Nonce x \\<notin> Key`A)"; |
11189 | 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 |
||
11251 | 85 |
Goalw [keysFor_def] "keysFor (\\<Union>i\\<in>A. H i) = (\\<Union>i\\<in>A. keysFor (H i))"; |
11189 | 86 |
by (Blast_tac 1); |
87 |
qed "keysFor_UN"; |
|
88 |
||
89 |
(*Monotonicity*) |
|
11251 | 90 |
Goalw [keysFor_def] "G\\<subseteq>H ==> keysFor(G) \\<subseteq> keysFor(H)"; |
11189 | 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 |
||
11217 | 135 |
Goalw [keysFor_def] "Crypt K X \\<in> H ==> invKey K \\<in> keysFor H"; |
11189 | 136 |
by (Blast_tac 1); |
137 |
qed "Crypt_imp_invKey_keysFor"; |
|
138 |
||
139 |
||
140 |
(**** Inductive relation "parts" ****) |
|
141 |
||
142 |
val major::prems = |
|
11217 | 143 |
Goal "[| {|X,Y|} \\<in> parts H; \ |
144 |
\ [| X \\<in> parts H; Y \\<in> parts H |] ==> P \ |
|
11189 | 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 |
||
11251 | 157 |
Goal "H \\<subseteq> parts(H)"; |
11189 | 158 |
by (Blast_tac 1); |
159 |
qed "parts_increasing"; |
|
160 |
||
11264 | 161 |
bind_thm ("parts_insertI", impOfSubs (subset_insertI RS parts_mono)); |
11189 | 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 |
||
11251 | 170 |
Goal "X\\<in> parts{} ==> P"; |
11189 | 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!*) |
|
11251 | 176 |
Goal "X\\<in> parts H ==> \\<exists>Y\\<in>H. X\\<in> parts {Y}"; |
11189 | 177 |
by (etac parts.induct 1); |
178 |
by (ALLGOALS Blast_tac); |
|
179 |
qed "parts_singleton"; |
|
180 |
||
181 |
||
182 |
(** Unions **) |
|
183 |
||
11251 | 184 |
Goal "parts(G) Un parts(H) \\<subseteq> parts(G Un H)"; |
11189 | 185 |
by (REPEAT (ares_tac [Un_least, parts_mono, Un_upper1, Un_upper2] 1)); |
186 |
val parts_Un_subset1 = result(); |
|
187 |
||
11251 | 188 |
Goal "parts(G Un H) \\<subseteq> parts(G) Un parts(H)"; |
11189 | 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 |
||
11251 | 210 |
Goal "(\\<Union>x\\<in>A. parts(H x)) \\<subseteq> parts(\\<Union>x\\<in>A. H x)"; |
11189 | 211 |
by (REPEAT (ares_tac [UN_least, parts_mono, UN_upper] 1)); |
212 |
val parts_UN_subset1 = result(); |
|
213 |
||
11251 | 214 |
Goal "parts(\\<Union>x\\<in>A. H x) \\<subseteq> (\\<Union>x\\<in>A. parts(H x))"; |
11189 | 215 |
by (rtac subsetI 1); |
216 |
by (etac parts.induct 1); |
|
217 |
by (ALLGOALS Blast_tac); |
|
218 |
val parts_UN_subset2 = result(); |
|
219 |
||
11251 | 220 |
Goal "parts(\\<Union>x\\<in>A. H x) = (\\<Union>x\\<in>A. parts(H x))"; |
11189 | 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 |
||
11251 | 230 |
Goal "insert X (parts H) \\<subseteq> parts(insert X H)"; |
11189 | 231 |
by (blast_tac (claset() addIs [impOfSubs parts_mono]) 1); |
232 |
qed "parts_insert_subset"; |
|
233 |
||
234 |
(** Idempotence and transitivity **) |
|
235 |
||
11251 | 236 |
Goal "X\\<in> parts (parts H) ==> X\\<in> parts H"; |
11189 | 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 |
||
11251 | 247 |
Goal "[| X\\<in> parts G; G \\<subseteq> parts H |] ==> X\\<in> parts H"; |
11189 | 248 |
by (dtac parts_mono 1); |
249 |
by (Blast_tac 1); |
|
250 |
qed "parts_trans"; |
|
251 |
||
252 |
(*Cut*) |
|
11251 | 253 |
Goal "[| Y\\<in> parts (insert X G); X\\<in> parts H |] \ |
254 |
\ ==> Y\\<in> parts (G Un H)"; |
|
11189 | 255 |
by (etac parts_trans 1); |
256 |
by Auto_tac; |
|
257 |
qed "parts_cut"; |
|
258 |
||
11251 | 259 |
Goal "X\\<in> parts H ==> parts (insert X H) = parts H"; |
11189 | 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.*) |
|
11251 | 329 |
Goal "\\<exists>N. \\<forall>n. N\\<le>n --> Nonce n \\<notin> parts {msg}"; |
11189 | 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 = |
|
11217 | 343 |
Goal "[| {|X,Y|} \\<in> analz H; \ |
344 |
\ [| X \\<in> analz H; Y \\<in> analz H |] ==> P \ |
|
11189 | 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 |
||
11251 | 353 |
Goal "H \\<subseteq> analz(H)"; |
11189 | 354 |
by (Blast_tac 1); |
355 |
qed "analz_increasing"; |
|
356 |
||
11251 | 357 |
Goal "analz H \\<subseteq> parts H"; |
11189 | 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*) |
|
11251 | 394 |
Goal "analz(G) Un analz(H) \\<subseteq> analz(G Un H)"; |
11189 | 395 |
by (REPEAT (ares_tac [Un_least, analz_mono, Un_upper1, Un_upper2] 1)); |
396 |
qed "analz_Un"; |
|
397 |
||
11251 | 398 |
Goal "insert X (analz H) \\<subseteq> analz(insert X H)"; |
11189 | 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] |
|
11217 | 427 |
"K \\<notin> keysFor (analz H) ==> \ |
11189 | 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*) |
|
11217 | 443 |
Goal "Key (invKey K) \\<notin> analz H ==> \ |
11189 | 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 |
||
11217 | 449 |
Goal "Key (invKey K) \\<in> analz H ==> \ |
11251 | 450 |
\ analz (insert (Crypt K X) H) \\<subseteq> \ |
11189 | 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 |
||
11217 | 457 |
Goal "Key (invKey K) \\<in> analz H ==> \ |
11251 | 458 |
\ insert (Crypt K X) (analz (insert X H)) \\<subseteq> \ |
11189 | 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 |
||
11217 | 466 |
Goal "Key (invKey K) \\<in> analz H ==> \ |
11189 | 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) = \ |
|
11217 | 477 |
\ (if (Key (invKey K) \\<in> analz H) \ |
11189 | 478 |
\ then insert (Crypt K X) (analz (insert X H)) \ |
479 |
\ else insert (Crypt K X) (analz H))"; |
|
11217 | 480 |
by (case_tac "Key (invKey K) \\<in> analz H " 1); |
11189 | 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.*) |
|
11251 | 490 |
Goal "analz (insert (Crypt K X) H) \\<subseteq> \ |
11189 | 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 |
||
11251 | 509 |
Goal "X\\<in> analz (analz H) ==> X\\<in> analz H"; |
11189 | 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 |
||
11251 | 520 |
Goal "[| X\\<in> analz G; G \\<subseteq> analz H |] ==> X\\<in> analz H"; |
11189 | 521 |
by (dtac analz_mono 1); |
522 |
by (Blast_tac 1); |
|
523 |
qed "analz_trans"; |
|
524 |
||
525 |
(*Cut; Lemma 2 of Lowe*) |
|
11251 | 526 |
Goal "[| Y\\<in> analz (insert X H); X\\<in> analz H |] ==> Y\\<in> analz H"; |
11189 | 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. *) |
|
11251 | 538 |
Goal "X\\<in> analz H ==> analz (insert X H) = analz H"; |
11189 | 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 |
||
11251 | 545 |
Goal "[| analz G \\<subseteq> analz G'; analz H \\<subseteq> analz H' \ |
546 |
\ |] ==> analz (G Un H) \\<subseteq> analz (G' Un H')"; |
|
11189 | 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*) |
|
11251 | 565 |
Goal "[| \\<forall>X Y. {|X,Y|} \\<notin> H; \\<forall>X K. Crypt K X \\<notin> H |] ==> analz H = H"; |
11189 | 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...*) |
|
11251 | 572 |
Goal "X\\<in> analz (\\<Union>i\\<in>A. analz (H i)) ==> X\\<in> analz (\\<Union>i\\<in>A. H i)"; |
11189 | 573 |
by (etac analz.induct 1); |
574 |
by (ALLGOALS (blast_tac (claset() addIs [impOfSubs analz_mono]))); |
|
575 |
val lemma = result(); |
|
576 |
||
11251 | 577 |
Goal "analz (\\<Union>i\\<in>A. analz (H i)) = analz (\\<Union>i\\<in>A. H i)"; |
11189 | 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 |
||
11251 | 585 |
Goal "H \\<subseteq> synth(H)"; |
11189 | 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.*) |
|
11251 | 593 |
Goal "synth(G) Un synth(H) \\<subseteq> synth(G Un H)"; |
11189 | 594 |
by (REPEAT (ares_tac [Un_least, synth_mono, Un_upper1, Un_upper2] 1)); |
595 |
qed "synth_Un"; |
|
596 |
||
11251 | 597 |
Goal "insert X (synth H) \\<subseteq> synth(insert X H)"; |
11189 | 598 |
by (blast_tac (claset() addIs [impOfSubs synth_mono]) 1); |
599 |
qed "synth_insert"; |
|
600 |
||
601 |
(** Idempotence and transitivity **) |
|
602 |
||
11251 | 603 |
Goal "X\\<in> synth (synth H) ==> X\\<in> synth H"; |
11189 | 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 |
||
11251 | 613 |
Goal "[| X\\<in> synth G; G \\<subseteq> synth H |] ==> X\\<in> synth H"; |
11189 | 614 |
by (dtac synth_mono 1); |
615 |
by (Blast_tac 1); |
|
616 |
qed "synth_trans"; |
|
617 |
||
618 |
(*Cut; Lemma 2 of Lowe*) |
|
11251 | 619 |
Goal "[| Y\\<in> synth (insert X H); X\\<in> synth H |] ==> Y\\<in> synth H"; |
11189 | 620 |
by (etac synth_trans 1); |
621 |
by (Blast_tac 1); |
|
622 |
qed "synth_cut"; |
|
623 |
||
11217 | 624 |
Goal "Agent A \\<in> synth H"; |
11189 | 625 |
by (Blast_tac 1); |
626 |
qed "Agent_synth"; |
|
627 |
||
11217 | 628 |
Goal "Number n \\<in> synth H"; |
11189 | 629 |
by (Blast_tac 1); |
630 |
qed "Number_synth"; |
|
631 |
||
11217 | 632 |
Goal "(Nonce N \\<in> synth H) = (Nonce N \\<in> H)"; |
11189 | 633 |
by (Blast_tac 1); |
634 |
qed "Nonce_synth_eq"; |
|
635 |
||
11217 | 636 |
Goal "(Key K \\<in> synth H) = (Key K \\<in> H)"; |
11189 | 637 |
by (Blast_tac 1); |
638 |
qed "Key_synth_eq"; |
|
639 |
||
11217 | 640 |
Goal "Key K \\<notin> H ==> (Crypt K X \\<in> synth H) = (Crypt K X \\<in> H)"; |
11189 | 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] |
|
11217 | 649 |
"keysFor (synth H) = keysFor H Un invKey`{K. Key K \\<in> H}"; |
11189 | 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 |
||
11251 | 690 |
Goal "X\\<in> G ==> parts(insert X H) \\<subseteq> parts G Un parts H"; |
11189 | 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 |
|
11251 | 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"; |
|
11189 | 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*) |
|
11251 | 705 |
Goal "X\\<in> synth (analz G) ==> \ |
706 |
\ analz (insert X H) \\<subseteq> synth (analz G) Un analz (G Un H)"; |
|
11189 | 707 |
by (rtac subsetI 1); |
11217 | 708 |
by (subgoal_tac "x \\<in> analz (synth (analz G) Un H)" 1); |
11189 | 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 |
||
11251 | 715 |
Goal "(X\\<in> analz H & X\\<in> parts H) = (X\\<in> analz H)"; |
11189 | 716 |
by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1); |
717 |
val analz_conj_parts = result(); |
|
718 |
||
11251 | 719 |
Goal "(X\\<in> analz H | X\\<in> parts H) = (X\\<in> parts H)"; |
11189 | 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*) |
|
11217 | 727 |
Goal "({|X,Y|} \\<in> synth (analz H)) = \ |
728 |
\ (X \\<in> synth (analz H) & Y \\<in> synth (analz H))"; |
|
11189 | 729 |
by (Blast_tac 1); |
730 |
qed "MPair_synth_analz"; |
|
731 |
||
732 |
AddIffs [MPair_synth_analz]; |
|
733 |
||
11217 | 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))"; |
|
11189 | 736 |
by (Blast_tac 1); |
737 |
qed "Crypt_synth_analz"; |
|
738 |
||
739 |
||
11217 | 740 |
Goal "X \\<notin> synth (analz H) \ |
741 |
\ ==> (Hash{|X,Y|} \\<in> synth (analz H)) = (Hash{|X,Y|} \\<in> analz H)"; |
|
11189 | 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 |
||
11217 | 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))"; |
|
11189 | 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 |
|
11217 | 849 |
concerns Crypt K X \\<notin> Key`shrK`bad and cannot be proved by rewriting |
11189 | 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 |
|
11217 | 861 |
Y \\<in> parts(insert X H) and Y \\<in> analz(insert X H) |
11189 | 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 |
||
11270
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11264
diff
changeset
|
868 |
fun Fake_insert_simp_tac ss i = |
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11264
diff
changeset
|
869 |
REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i; |
11189 | 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 |
||
11270
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11264
diff
changeset
|
877 |
fun atomic_spy_analz_tac (cs,ss) = SELECT_GOAL |
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11264
diff
changeset
|
878 |
(Fake_insert_simp_tac ss 1 |
11189 | 879 |
THEN |
880 |
IF_UNSOLVED (Blast.depth_tac |
|
11270
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11264
diff
changeset
|
881 |
(cs addIs [analz_insertI, |
11189 | 882 |
impOfSubs analz_subset_parts]) 4 1)); |
883 |
||
11270
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11264
diff
changeset
|
884 |
(*The explicit claset and simpset arguments help it work with Isar*) |
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11264
diff
changeset
|
885 |
fun gen_spy_analz_tac (cs,ss) i = |
11189 | 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*) |
|
11270
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11264
diff
changeset
|
893 |
simp_tac ss 1, |
11189 | 894 |
REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])), |
11270
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11264
diff
changeset
|
895 |
DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i); |
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11264
diff
changeset
|
896 |
|
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11264
diff
changeset
|
897 |
fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i; |
11189 | 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]; |