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";
|
|
17 |
val isSymKey_def = thm "isSymKey_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 : Friend`A) = (x:A)";
|
|
50 |
by Auto_tac;
|
|
51 |
qed "Friend_image_eq";
|
|
52 |
|
|
53 |
Goal "(Key x : Key`A) = (x:A)";
|
|
54 |
by Auto_tac;
|
|
55 |
qed "Key_image_eq";
|
|
56 |
|
|
57 |
Goal "(Nonce x ~: 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 (UN i:A. H i) = (UN i:A. keysFor (H i))";
|
|
86 |
by (Blast_tac 1);
|
|
87 |
qed "keysFor_UN";
|
|
88 |
|
|
89 |
(*Monotonicity*)
|
|
90 |
Goalw [keysFor_def] "G<=H ==> keysFor(G) <= 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 : H ==> invKey K : 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|} : parts H; \
|
|
144 |
\ [| X : parts H; Y : 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 <= parts(H)";
|
|
158 |
by (Blast_tac 1);
|
|
159 |
qed "parts_increasing";
|
|
160 |
|
|
161 |
val 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: 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: parts H ==> EX Y:H. X: 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) <= 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) <= 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 "(UN x:A. parts(H x)) <= parts(UN x: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(UN x:A. H x) <= (UN x: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(UN x:A. H x) = (UN x: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) <= 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: parts (parts H) ==> X: 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: parts G; G <= parts H |] ==> X: parts H";
|
|
248 |
by (dtac parts_mono 1);
|
|
249 |
by (Blast_tac 1);
|
|
250 |
qed "parts_trans";
|
|
251 |
|
|
252 |
(*Cut*)
|
|
253 |
Goal "[| Y: parts (insert X G); X: parts H |] \
|
|
254 |
\ ==> Y: parts (G Un H)";
|
|
255 |
by (etac parts_trans 1);
|
|
256 |
by Auto_tac;
|
|
257 |
qed "parts_cut";
|
|
258 |
|
|
259 |
Goal "X: 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 "EX N. ALL n. N<=n --> Nonce n ~: 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|} : analz H; \
|
|
344 |
\ [| X : analz H; Y : 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 <= analz(H)";
|
|
354 |
by (Blast_tac 1);
|
|
355 |
qed "analz_increasing";
|
|
356 |
|
|
357 |
Goal "analz H <= 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) <= 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) <= 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 ~: 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) ~: 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) : analz H ==> \
|
|
450 |
\ analz (insert (Crypt K X) H) <= \
|
|
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) : analz H ==> \
|
|
458 |
\ insert (Crypt K X) (analz (insert X H)) <= \
|
|
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) : 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) : 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) : 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) <= \
|
|
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: analz (analz H) ==> X: 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: analz G; G <= analz H |] ==> X: 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: analz (insert X H); X: analz H |] ==> Y: 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: 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 <= analz G'; analz H <= analz H' \
|
|
546 |
\ |] ==> analz (G Un H) <= 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 "[| ALL X Y. {|X,Y|} ~: H; ALL X K. Crypt K X ~: H |] ==> \
|
|
566 |
\ analz H = H";
|
|
567 |
by Safe_tac;
|
|
568 |
by (etac analz.induct 1);
|
|
569 |
by (ALLGOALS Blast_tac);
|
|
570 |
qed "analz_trivial";
|
|
571 |
|
|
572 |
(*These two are obsolete (with a single Spy) but cost little to prove...*)
|
|
573 |
Goal "X: analz (UN i:A. analz (H i)) ==> X: analz (UN i:A. H i)";
|
|
574 |
by (etac analz.induct 1);
|
|
575 |
by (ALLGOALS (blast_tac (claset() addIs [impOfSubs analz_mono])));
|
|
576 |
val lemma = result();
|
|
577 |
|
|
578 |
Goal "analz (UN i:A. analz (H i)) = analz (UN i:A. H i)";
|
|
579 |
by (blast_tac (claset() addIs [lemma, impOfSubs analz_mono]) 1);
|
|
580 |
qed "analz_UN_analz";
|
|
581 |
Addsimps [analz_UN_analz];
|
|
582 |
|
|
583 |
|
|
584 |
(**** Inductive relation "synth" ****)
|
|
585 |
|
|
586 |
Goal "H <= synth(H)";
|
|
587 |
by (Blast_tac 1);
|
|
588 |
qed "synth_increasing";
|
|
589 |
|
|
590 |
(** Unions **)
|
|
591 |
|
|
592 |
(*Converse fails: we can synth more from the union than from the
|
|
593 |
separate parts, building a compound message using elements of each.*)
|
|
594 |
Goal "synth(G) Un synth(H) <= synth(G Un H)";
|
|
595 |
by (REPEAT (ares_tac [Un_least, synth_mono, Un_upper1, Un_upper2] 1));
|
|
596 |
qed "synth_Un";
|
|
597 |
|
|
598 |
Goal "insert X (synth H) <= synth(insert X H)";
|
|
599 |
by (blast_tac (claset() addIs [impOfSubs synth_mono]) 1);
|
|
600 |
qed "synth_insert";
|
|
601 |
|
|
602 |
(** Idempotence and transitivity **)
|
|
603 |
|
|
604 |
Goal "X: synth (synth H) ==> X: synth H";
|
|
605 |
by (etac synth.induct 1);
|
|
606 |
by (ALLGOALS Blast_tac);
|
|
607 |
qed "synth_synthD";
|
|
608 |
AddSDs [synth_synthD];
|
|
609 |
|
|
610 |
Goal "synth (synth H) = synth H";
|
|
611 |
by (Blast_tac 1);
|
|
612 |
qed "synth_idem";
|
|
613 |
|
|
614 |
Goal "[| X: synth G; G <= synth H |] ==> X: synth H";
|
|
615 |
by (dtac synth_mono 1);
|
|
616 |
by (Blast_tac 1);
|
|
617 |
qed "synth_trans";
|
|
618 |
|
|
619 |
(*Cut; Lemma 2 of Lowe*)
|
|
620 |
Goal "[| Y: synth (insert X H); X: synth H |] ==> Y: synth H";
|
|
621 |
by (etac synth_trans 1);
|
|
622 |
by (Blast_tac 1);
|
|
623 |
qed "synth_cut";
|
|
624 |
|
|
625 |
Goal "Agent A : synth H";
|
|
626 |
by (Blast_tac 1);
|
|
627 |
qed "Agent_synth";
|
|
628 |
|
|
629 |
Goal "Number n : synth H";
|
|
630 |
by (Blast_tac 1);
|
|
631 |
qed "Number_synth";
|
|
632 |
|
|
633 |
Goal "(Nonce N : synth H) = (Nonce N : H)";
|
|
634 |
by (Blast_tac 1);
|
|
635 |
qed "Nonce_synth_eq";
|
|
636 |
|
|
637 |
Goal "(Key K : synth H) = (Key K : H)";
|
|
638 |
by (Blast_tac 1);
|
|
639 |
qed "Key_synth_eq";
|
|
640 |
|
|
641 |
Goal "Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X : H)";
|
|
642 |
by (Blast_tac 1);
|
|
643 |
qed "Crypt_synth_eq";
|
|
644 |
|
|
645 |
Addsimps [Agent_synth, Number_synth,
|
|
646 |
Nonce_synth_eq, Key_synth_eq, Crypt_synth_eq];
|
|
647 |
|
|
648 |
|
|
649 |
Goalw [keysFor_def]
|
|
650 |
"keysFor (synth H) = keysFor H Un invKey`{K. Key K : H}";
|
|
651 |
by (Blast_tac 1);
|
|
652 |
qed "keysFor_synth";
|
|
653 |
Addsimps [keysFor_synth];
|
|
654 |
|
|
655 |
|
|
656 |
(*** Combinations of parts, analz and synth ***)
|
|
657 |
|
|
658 |
Goal "parts (synth H) = parts H Un synth H";
|
|
659 |
by (rtac equalityI 1);
|
|
660 |
by (rtac subsetI 1);
|
|
661 |
by (etac parts.induct 1);
|
|
662 |
by (ALLGOALS
|
|
663 |
(blast_tac (claset() addIs [synth_increasing RS parts_mono RS subsetD,
|
|
664 |
parts.Fst, parts.Snd, parts.Body])));
|
|
665 |
qed "parts_synth";
|
|
666 |
Addsimps [parts_synth];
|
|
667 |
|
|
668 |
Goal "analz (analz G Un H) = analz (G Un H)";
|
|
669 |
by (REPEAT_FIRST (resolve_tac [equalityI, analz_subset_cong]));
|
|
670 |
by (ALLGOALS Simp_tac);
|
|
671 |
qed "analz_analz_Un";
|
|
672 |
|
|
673 |
Goal "analz (synth G Un H) = analz (G Un H) Un synth G";
|
|
674 |
by (rtac equalityI 1);
|
|
675 |
by (rtac subsetI 1);
|
|
676 |
by (etac analz.induct 1);
|
|
677 |
by (blast_tac (claset() addIs [impOfSubs analz_mono]) 5);
|
|
678 |
by (ALLGOALS
|
|
679 |
(blast_tac (claset() addIs [analz.Fst, analz.Snd, analz.Decrypt])));
|
|
680 |
qed "analz_synth_Un";
|
|
681 |
|
|
682 |
Goal "analz (synth H) = analz H Un synth H";
|
|
683 |
by (cut_inst_tac [("H","{}")] analz_synth_Un 1);
|
|
684 |
by (Full_simp_tac 1);
|
|
685 |
qed "analz_synth";
|
|
686 |
Addsimps [analz_analz_Un, analz_synth_Un, analz_synth];
|
|
687 |
|
|
688 |
|
|
689 |
(** For reasoning about the Fake rule in traces **)
|
|
690 |
|
|
691 |
Goal "X: G ==> parts(insert X H) <= parts G Un parts H";
|
|
692 |
by (rtac ([parts_mono, parts_Un_subset2] MRS subset_trans) 1);
|
|
693 |
by (Blast_tac 1);
|
|
694 |
qed "parts_insert_subset_Un";
|
|
695 |
|
|
696 |
(*More specifically for Fake. Very occasionally we could do with a version
|
|
697 |
of the form parts{X} <= synth (analz H) Un parts H *)
|
|
698 |
Goal "X: synth (analz H) ==> \
|
|
699 |
\ parts (insert X H) <= synth (analz H) Un parts H";
|
|
700 |
by (dtac parts_insert_subset_Un 1);
|
|
701 |
by (Full_simp_tac 1);
|
|
702 |
by (Blast_tac 1);
|
|
703 |
qed "Fake_parts_insert";
|
|
704 |
|
|
705 |
(*H is sometimes (Key ` KK Un spies evs), so can't put G=H*)
|
|
706 |
Goal "X: synth (analz G) ==> \
|
|
707 |
\ analz (insert X H) <= synth (analz G) Un analz (G Un H)";
|
|
708 |
by (rtac subsetI 1);
|
|
709 |
by (subgoal_tac "x : analz (synth (analz G) Un H)" 1);
|
|
710 |
by (blast_tac (claset() addIs [impOfSubs analz_mono,
|
|
711 |
impOfSubs (analz_mono RS synth_mono)]) 2);
|
|
712 |
by (Full_simp_tac 1);
|
|
713 |
by (Blast_tac 1);
|
|
714 |
qed "Fake_analz_insert";
|
|
715 |
|
|
716 |
Goal "(X: analz H & X: parts H) = (X: analz H)";
|
|
717 |
by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1);
|
|
718 |
val analz_conj_parts = result();
|
|
719 |
|
|
720 |
Goal "(X: analz H | X: parts H) = (X: parts H)";
|
|
721 |
by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1);
|
|
722 |
val analz_disj_parts = result();
|
|
723 |
|
|
724 |
AddIffs [analz_conj_parts, analz_disj_parts];
|
|
725 |
|
|
726 |
(*Without this equation, other rules for synth and analz would yield
|
|
727 |
redundant cases*)
|
|
728 |
Goal "({|X,Y|} : synth (analz H)) = \
|
|
729 |
\ (X : synth (analz H) & Y : synth (analz H))";
|
|
730 |
by (Blast_tac 1);
|
|
731 |
qed "MPair_synth_analz";
|
|
732 |
|
|
733 |
AddIffs [MPair_synth_analz];
|
|
734 |
|
|
735 |
Goal "[| Key K : analz H; Key (invKey K) : analz H |] \
|
|
736 |
\ ==> (Crypt K X : synth (analz H)) = (X : synth (analz H))";
|
|
737 |
by (Blast_tac 1);
|
|
738 |
qed "Crypt_synth_analz";
|
|
739 |
|
|
740 |
|
|
741 |
Goal "X ~: synth (analz H) \
|
|
742 |
\ ==> (Hash{|X,Y|} : synth (analz H)) = (Hash{|X,Y|} : analz H)";
|
|
743 |
by (Blast_tac 1);
|
|
744 |
qed "Hash_synth_analz";
|
|
745 |
Addsimps [Hash_synth_analz];
|
|
746 |
|
|
747 |
|
|
748 |
(**** HPair: a combination of Hash and MPair ****)
|
|
749 |
|
|
750 |
(*** Freeness ***)
|
|
751 |
|
|
752 |
Goalw [HPair_def] "Agent A ~= Hash[X] Y";
|
|
753 |
by (Simp_tac 1);
|
|
754 |
qed "Agent_neq_HPair";
|
|
755 |
|
|
756 |
Goalw [HPair_def] "Nonce N ~= Hash[X] Y";
|
|
757 |
by (Simp_tac 1);
|
|
758 |
qed "Nonce_neq_HPair";
|
|
759 |
|
|
760 |
Goalw [HPair_def] "Number N ~= Hash[X] Y";
|
|
761 |
by (Simp_tac 1);
|
|
762 |
qed "Number_neq_HPair";
|
|
763 |
|
|
764 |
Goalw [HPair_def] "Key K ~= Hash[X] Y";
|
|
765 |
by (Simp_tac 1);
|
|
766 |
qed "Key_neq_HPair";
|
|
767 |
|
|
768 |
Goalw [HPair_def] "Hash Z ~= Hash[X] Y";
|
|
769 |
by (Simp_tac 1);
|
|
770 |
qed "Hash_neq_HPair";
|
|
771 |
|
|
772 |
Goalw [HPair_def] "Crypt K X' ~= Hash[X] Y";
|
|
773 |
by (Simp_tac 1);
|
|
774 |
qed "Crypt_neq_HPair";
|
|
775 |
|
|
776 |
val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair, Number_neq_HPair,
|
|
777 |
Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair];
|
|
778 |
|
|
779 |
AddIffs HPair_neqs;
|
|
780 |
AddIffs (HPair_neqs RL [not_sym]);
|
|
781 |
|
|
782 |
Goalw [HPair_def] "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)";
|
|
783 |
by (Simp_tac 1);
|
|
784 |
qed "HPair_eq";
|
|
785 |
|
|
786 |
Goalw [HPair_def] "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)";
|
|
787 |
by (Simp_tac 1);
|
|
788 |
qed "MPair_eq_HPair";
|
|
789 |
|
|
790 |
Goalw [HPair_def] "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)";
|
|
791 |
by Auto_tac;
|
|
792 |
qed "HPair_eq_MPair";
|
|
793 |
|
|
794 |
AddIffs [HPair_eq, MPair_eq_HPair, HPair_eq_MPair];
|
|
795 |
|
|
796 |
|
|
797 |
(*** Specialized laws, proved in terms of those for Hash and MPair ***)
|
|
798 |
|
|
799 |
Goalw [HPair_def] "keysFor (insert (Hash[X] Y) H) = keysFor H";
|
|
800 |
by (Simp_tac 1);
|
|
801 |
qed "keysFor_insert_HPair";
|
|
802 |
|
|
803 |
Goalw [HPair_def]
|
|
804 |
"parts (insert (Hash[X] Y) H) = \
|
|
805 |
\ insert (Hash[X] Y) (insert (Hash{|X,Y|}) (parts (insert Y H)))";
|
|
806 |
by (Simp_tac 1);
|
|
807 |
qed "parts_insert_HPair";
|
|
808 |
|
|
809 |
Goalw [HPair_def]
|
|
810 |
"analz (insert (Hash[X] Y) H) = \
|
|
811 |
\ insert (Hash[X] Y) (insert (Hash{|X,Y|}) (analz (insert Y H)))";
|
|
812 |
by (Simp_tac 1);
|
|
813 |
qed "analz_insert_HPair";
|
|
814 |
|
|
815 |
Goalw [HPair_def] "X ~: synth (analz H) \
|
|
816 |
\ ==> (Hash[X] Y : synth (analz H)) = \
|
|
817 |
\ (Hash {|X, Y|} : analz H & Y : synth (analz H))";
|
|
818 |
by (Simp_tac 1);
|
|
819 |
by (Blast_tac 1);
|
|
820 |
qed "HPair_synth_analz";
|
|
821 |
|
|
822 |
Addsimps [keysFor_insert_HPair, parts_insert_HPair, analz_insert_HPair,
|
|
823 |
HPair_synth_analz, HPair_synth_analz];
|
|
824 |
|
|
825 |
|
|
826 |
(*We do NOT want Crypt... messages broken up in protocols!!*)
|
|
827 |
Delrules [make_elim parts.Body];
|
|
828 |
|
|
829 |
|
|
830 |
(** Rewrites to push in Key and Crypt messages, so that other messages can
|
|
831 |
be pulled out using the analz_insert rules **)
|
|
832 |
|
|
833 |
fun insComm x y = inst "x" x (inst "y" y insert_commute);
|
|
834 |
|
|
835 |
val pushKeys = map (insComm "Key ?K")
|
|
836 |
["Agent ?C", "Nonce ?N", "Number ?N",
|
|
837 |
"Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"];
|
|
838 |
|
|
839 |
val pushCrypts = map (insComm "Crypt ?X ?K")
|
|
840 |
["Agent ?C", "Nonce ?N", "Number ?N",
|
|
841 |
"Hash ?X'", "MPair ?X' ?Y"];
|
|
842 |
|
|
843 |
(*Cannot be added with Addsimps -- we don't always want to re-order messages*)
|
|
844 |
bind_thms ("pushes", pushKeys@pushCrypts);
|
|
845 |
|
|
846 |
|
|
847 |
(*** Tactics useful for many protocol proofs ***)
|
|
848 |
|
|
849 |
(*Prove base case (subgoal i) and simplify others. A typical base case
|
|
850 |
concerns Crypt K X ~: Key`shrK`bad and cannot be proved by rewriting
|
|
851 |
alone.*)
|
|
852 |
fun prove_simple_subgoals_tac i =
|
|
853 |
force_tac (claset(), simpset() addsimps [image_eq_UN]) i THEN
|
|
854 |
ALLGOALS Asm_simp_tac;
|
|
855 |
|
|
856 |
fun Fake_parts_insert_tac i =
|
|
857 |
blast_tac (claset() addIs [parts_insertI]
|
|
858 |
addDs [impOfSubs analz_subset_parts,
|
|
859 |
impOfSubs Fake_parts_insert]) i;
|
|
860 |
|
|
861 |
(*Apply rules to break down assumptions of the form
|
|
862 |
Y : parts(insert X H) and Y : analz(insert X H)
|
|
863 |
*)
|
|
864 |
val Fake_insert_tac =
|
|
865 |
dresolve_tac [impOfSubs Fake_analz_insert,
|
|
866 |
impOfSubs Fake_parts_insert] THEN'
|
|
867 |
eresolve_tac [asm_rl, synth.Inj];
|
|
868 |
|
|
869 |
fun Fake_insert_simp_tac i =
|
|
870 |
REPEAT (Fake_insert_tac i) THEN Asm_full_simp_tac i;
|
|
871 |
|
|
872 |
|
|
873 |
(*Analysis of Fake cases. Also works for messages that forward unknown parts,
|
|
874 |
but this application is no longer necessary if analz_insert_eq is used.
|
|
875 |
Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
|
|
876 |
DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
|
|
877 |
|
|
878 |
val atomic_spy_analz_tac = SELECT_GOAL
|
|
879 |
(Fake_insert_simp_tac 1
|
|
880 |
THEN
|
|
881 |
IF_UNSOLVED (Blast.depth_tac
|
|
882 |
(claset() addIs [analz_insertI,
|
|
883 |
impOfSubs analz_subset_parts]) 4 1));
|
|
884 |
|
|
885 |
fun spy_analz_tac 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 1,
|
|
894 |
REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
|
|
895 |
DEPTH_SOLVE (atomic_spy_analz_tac 1)]) i);
|
|
896 |
|
|
897 |
(*By default only o_apply is built-in. But in the presence of eta-expansion
|
|
898 |
this means that some terms displayed as (f o g) will be rewritten, and others
|
|
899 |
will not!*)
|
|
900 |
Addsimps [o_def];
|