author | paulson |
Fri, 13 Dec 1996 10:17:35 +0100 | |
changeset 2373 | 490ffa16952e |
parent 2327 | 00ac25b2791d |
child 2415 | 46de4b035f00 |
permissions | -rw-r--r-- |
1839 | 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; |
|
1913 | 7 |
Inductive relations "parts", "analz" and "synth" |
1839 | 8 |
*) |
9 |
||
2327 | 10 |
val prems = goal HOL.thy "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)"; |
11 |
by (case_tac "P" 1); |
|
12 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps prems))); |
|
13 |
val expand_case = result(); |
|
14 |
||
15 |
fun expand_case_tac P i = |
|
16 |
res_inst_tac [("P",P)] expand_case i THEN |
|
17 |
Simp_tac (i+1) THEN |
|
18 |
Simp_tac i; |
|
19 |
||
20 |
||
21 |
||
22 |
(*GOALS.ML??*) |
|
23 |
fun prlim n = (goals_limit:=n; pr()); |
|
24 |
||
25 |
(*FUN.ML?? WE NEED A NOTION OF INVERSE IMAGE, OR GRAPH!!*) |
|
26 |
goal Set.thy "!!f. B <= range f = (B = f`` {x. f x: B})"; |
|
27 |
by (fast_tac (!claset addEs [equalityE]) 1); |
|
28 |
val subset_range_iff = result(); |
|
29 |
||
30 |
||
1839 | 31 |
open Message; |
32 |
||
2373 | 33 |
AddIffs (msg.inject); |
1839 | 34 |
|
35 |
(** Inverse of keys **) |
|
36 |
||
37 |
goal thy "!!K K'. (invKey K = invKey K') = (K=K')"; |
|
38 |
by (Step_tac 1); |
|
2032 | 39 |
by (rtac box_equals 1); |
1839 | 40 |
by (REPEAT (rtac invKey 2)); |
41 |
by (Asm_simp_tac 1); |
|
42 |
qed "invKey_eq"; |
|
43 |
||
44 |
Addsimps [invKey, invKey_eq]; |
|
45 |
||
46 |
||
47 |
(**** keysFor operator ****) |
|
48 |
||
49 |
goalw thy [keysFor_def] "keysFor {} = {}"; |
|
50 |
by (Fast_tac 1); |
|
51 |
qed "keysFor_empty"; |
|
52 |
||
53 |
goalw thy [keysFor_def] "keysFor (H Un H') = keysFor H Un keysFor H'"; |
|
54 |
by (Fast_tac 1); |
|
55 |
qed "keysFor_Un"; |
|
56 |
||
57 |
goalw thy [keysFor_def] "keysFor (UN i. H i) = (UN i. keysFor (H i))"; |
|
58 |
by (Fast_tac 1); |
|
59 |
qed "keysFor_UN"; |
|
60 |
||
61 |
(*Monotonicity*) |
|
62 |
goalw thy [keysFor_def] "!!G H. G<=H ==> keysFor(G) <= keysFor(H)"; |
|
63 |
by (Fast_tac 1); |
|
64 |
qed "keysFor_mono"; |
|
65 |
||
66 |
goalw thy [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H"; |
|
67 |
by (fast_tac (!claset addss (!simpset)) 1); |
|
68 |
qed "keysFor_insert_Agent"; |
|
69 |
||
70 |
goalw thy [keysFor_def] "keysFor (insert (Nonce N) H) = keysFor H"; |
|
71 |
by (fast_tac (!claset addss (!simpset)) 1); |
|
72 |
qed "keysFor_insert_Nonce"; |
|
73 |
||
74 |
goalw thy [keysFor_def] "keysFor (insert (Key K) H) = keysFor H"; |
|
75 |
by (fast_tac (!claset addss (!simpset)) 1); |
|
76 |
qed "keysFor_insert_Key"; |
|
77 |
||
2373 | 78 |
goalw thy [keysFor_def] "keysFor (insert (Hash X) H) = keysFor H"; |
79 |
by (fast_tac (!claset addss (!simpset)) 1); |
|
80 |
qed "keysFor_insert_Hash"; |
|
81 |
||
1839 | 82 |
goalw thy [keysFor_def] "keysFor (insert {|X,Y|} H) = keysFor H"; |
83 |
by (fast_tac (!claset addss (!simpset)) 1); |
|
84 |
qed "keysFor_insert_MPair"; |
|
85 |
||
86 |
goalw thy [keysFor_def] |
|
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset
|
87 |
"keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"; |
1839 | 88 |
by (Auto_tac()); |
89 |
qed "keysFor_insert_Crypt"; |
|
90 |
||
91 |
Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, |
|
2373 | 92 |
keysFor_insert_Agent, keysFor_insert_Nonce, keysFor_insert_Key, |
93 |
keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt]; |
|
1839 | 94 |
|
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset
|
95 |
goalw thy [keysFor_def] "!!H. Crypt K X : H ==> invKey K : keysFor H"; |
2068 | 96 |
by (Fast_tac 1); |
97 |
qed "Crypt_imp_invKey_keysFor"; |
|
98 |
||
1839 | 99 |
|
100 |
(**** Inductive relation "parts" ****) |
|
101 |
||
102 |
val major::prems = |
|
103 |
goal thy "[| {|X,Y|} : parts H; \ |
|
104 |
\ [| X : parts H; Y : parts H |] ==> P \ |
|
105 |
\ |] ==> P"; |
|
106 |
by (cut_facts_tac [major] 1); |
|
2032 | 107 |
by (resolve_tac prems 1); |
1839 | 108 |
by (REPEAT (eresolve_tac [asm_rl, parts.Fst, parts.Snd] 1)); |
109 |
qed "MPair_parts"; |
|
110 |
||
111 |
AddIs [parts.Inj]; |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
112 |
|
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
113 |
val partsEs = [MPair_parts, make_elim parts.Body]; |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
114 |
|
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
115 |
AddSEs partsEs; |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
116 |
(*NB These two rules are UNSAFE in the formal sense, as they discard the |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
117 |
compound message. They work well on THIS FILE, perhaps because its |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
118 |
proofs concern only atomic messages.*) |
1839 | 119 |
|
120 |
goal thy "H <= parts(H)"; |
|
121 |
by (Fast_tac 1); |
|
122 |
qed "parts_increasing"; |
|
123 |
||
124 |
(*Monotonicity*) |
|
125 |
goalw thy parts.defs "!!G H. G<=H ==> parts(G) <= parts(H)"; |
|
126 |
by (rtac lfp_mono 1); |
|
127 |
by (REPEAT (ares_tac basic_monos 1)); |
|
128 |
qed "parts_mono"; |
|
129 |
||
2373 | 130 |
val parts_insertI = impOfSubs (subset_insertI RS parts_mono); |
131 |
||
1839 | 132 |
goal thy "parts{} = {}"; |
133 |
by (Step_tac 1); |
|
2032 | 134 |
by (etac parts.induct 1); |
1839 | 135 |
by (ALLGOALS Fast_tac); |
136 |
qed "parts_empty"; |
|
137 |
Addsimps [parts_empty]; |
|
138 |
||
139 |
goal thy "!!X. X: parts{} ==> P"; |
|
140 |
by (Asm_full_simp_tac 1); |
|
141 |
qed "parts_emptyE"; |
|
142 |
AddSEs [parts_emptyE]; |
|
143 |
||
1893 | 144 |
(*WARNING: loops if H = {Y}, therefore must not be repeated!*) |
145 |
goal thy "!!H. X: parts H ==> EX Y:H. X: parts {Y}"; |
|
2032 | 146 |
by (etac parts.induct 1); |
1893 | 147 |
by (ALLGOALS Fast_tac); |
148 |
qed "parts_singleton"; |
|
149 |
||
1839 | 150 |
|
151 |
(** Unions **) |
|
152 |
||
153 |
goal thy "parts(G) Un parts(H) <= parts(G Un H)"; |
|
154 |
by (REPEAT (ares_tac [Un_least, parts_mono, Un_upper1, Un_upper2] 1)); |
|
155 |
val parts_Un_subset1 = result(); |
|
156 |
||
157 |
goal thy "parts(G Un H) <= parts(G) Un parts(H)"; |
|
2032 | 158 |
by (rtac subsetI 1); |
159 |
by (etac parts.induct 1); |
|
1839 | 160 |
by (ALLGOALS Fast_tac); |
161 |
val parts_Un_subset2 = result(); |
|
162 |
||
163 |
goal thy "parts(G Un H) = parts(G) Un parts(H)"; |
|
164 |
by (REPEAT (ares_tac [equalityI, parts_Un_subset1, parts_Un_subset2] 1)); |
|
165 |
qed "parts_Un"; |
|
166 |
||
2011 | 167 |
goal thy "parts (insert X H) = parts {X} Un parts H"; |
1852 | 168 |
by (stac (read_instantiate [("A","H")] insert_is_Un) 1); |
2011 | 169 |
by (simp_tac (HOL_ss addsimps [parts_Un]) 1); |
170 |
qed "parts_insert"; |
|
171 |
||
172 |
(*TWO inserts to avoid looping. This rewrite is better than nothing. |
|
173 |
Not suitable for Addsimps: its behaviour can be strange.*) |
|
174 |
goal thy "parts (insert X (insert Y H)) = parts {X} Un parts {Y} Un parts H"; |
|
175 |
by (simp_tac (!simpset addsimps [Un_assoc]) 1); |
|
176 |
by (simp_tac (!simpset addsimps [parts_insert RS sym]) 1); |
|
1852 | 177 |
qed "parts_insert2"; |
178 |
||
1839 | 179 |
goal thy "(UN x:A. parts(H x)) <= parts(UN x:A. H x)"; |
180 |
by (REPEAT (ares_tac [UN_least, parts_mono, UN_upper] 1)); |
|
181 |
val parts_UN_subset1 = result(); |
|
182 |
||
183 |
goal thy "parts(UN x:A. H x) <= (UN x:A. parts(H x))"; |
|
2032 | 184 |
by (rtac subsetI 1); |
185 |
by (etac parts.induct 1); |
|
1839 | 186 |
by (ALLGOALS Fast_tac); |
187 |
val parts_UN_subset2 = result(); |
|
188 |
||
189 |
goal thy "parts(UN x:A. H x) = (UN x:A. parts(H x))"; |
|
190 |
by (REPEAT (ares_tac [equalityI, parts_UN_subset1, parts_UN_subset2] 1)); |
|
191 |
qed "parts_UN"; |
|
192 |
||
193 |
goal thy "parts(UN x. H x) = (UN x. parts(H x))"; |
|
194 |
by (simp_tac (!simpset addsimps [UNION1_def, parts_UN]) 1); |
|
195 |
qed "parts_UN1"; |
|
196 |
||
1913 | 197 |
(*Added to simplify arguments to parts, analz and synth*) |
1839 | 198 |
Addsimps [parts_Un, parts_UN, parts_UN1]; |
199 |
||
200 |
goal thy "insert X (parts H) <= parts(insert X H)"; |
|
1852 | 201 |
by (fast_tac (!claset addEs [impOfSubs parts_mono]) 1); |
1839 | 202 |
qed "parts_insert_subset"; |
203 |
||
204 |
(** Idempotence and transitivity **) |
|
205 |
||
206 |
goal thy "!!H. X: parts (parts H) ==> X: parts H"; |
|
2032 | 207 |
by (etac parts.induct 1); |
1839 | 208 |
by (ALLGOALS Fast_tac); |
209 |
qed "parts_partsE"; |
|
210 |
AddSEs [parts_partsE]; |
|
211 |
||
212 |
goal thy "parts (parts H) = parts H"; |
|
213 |
by (Fast_tac 1); |
|
214 |
qed "parts_idem"; |
|
215 |
Addsimps [parts_idem]; |
|
216 |
||
217 |
goal thy "!!H. [| X: parts G; G <= parts H |] ==> X: parts H"; |
|
218 |
by (dtac parts_mono 1); |
|
219 |
by (Fast_tac 1); |
|
220 |
qed "parts_trans"; |
|
221 |
||
222 |
(*Cut*) |
|
2373 | 223 |
goal thy "!!H. [| Y: parts (insert X G); X: parts H |] \ |
224 |
\ ==> Y: parts (G Un H)"; |
|
2032 | 225 |
by (etac parts_trans 1); |
2373 | 226 |
by (Auto_tac()); |
1839 | 227 |
qed "parts_cut"; |
228 |
||
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
229 |
goal thy "!!H. X: parts H ==> parts (insert X H) = parts H"; |
2373 | 230 |
by (fast_tac (!claset addSDs [parts_cut] |
231 |
addIs [parts_insertI] |
|
232 |
addss (!simpset)) 1); |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
233 |
qed "parts_cut_eq"; |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
234 |
|
2028
738bb98d65ec
Last working version prior to addition of "lost" component
paulson
parents:
2026
diff
changeset
|
235 |
Addsimps [parts_cut_eq]; |
738bb98d65ec
Last working version prior to addition of "lost" component
paulson
parents:
2026
diff
changeset
|
236 |
|
1839 | 237 |
|
238 |
(** Rewrite rules for pulling out atomic messages **) |
|
239 |
||
2373 | 240 |
fun parts_tac i = |
241 |
EVERY [rtac ([subsetI, parts_insert_subset] MRS equalityI) i, |
|
242 |
etac parts.induct i, |
|
243 |
REPEAT (fast_tac (!claset addss (!simpset)) i)]; |
|
244 |
||
1839 | 245 |
goal thy "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"; |
2373 | 246 |
by (parts_tac 1); |
1839 | 247 |
qed "parts_insert_Agent"; |
248 |
||
249 |
goal thy "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"; |
|
2373 | 250 |
by (parts_tac 1); |
1839 | 251 |
qed "parts_insert_Nonce"; |
252 |
||
253 |
goal thy "parts (insert (Key K) H) = insert (Key K) (parts H)"; |
|
2373 | 254 |
by (parts_tac 1); |
1839 | 255 |
qed "parts_insert_Key"; |
256 |
||
2373 | 257 |
goal thy "parts (insert (Hash X) H) = insert (Hash X) (parts H)"; |
258 |
by (parts_tac 1); |
|
259 |
qed "parts_insert_Hash"; |
|
260 |
||
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset
|
261 |
goal thy "parts (insert (Crypt K X) H) = \ |
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset
|
262 |
\ insert (Crypt K X) (parts (insert X H))"; |
2032 | 263 |
by (rtac equalityI 1); |
264 |
by (rtac subsetI 1); |
|
265 |
by (etac parts.induct 1); |
|
1839 | 266 |
by (Auto_tac()); |
2032 | 267 |
by (etac parts.induct 1); |
1839 | 268 |
by (ALLGOALS (best_tac (!claset addIs [parts.Body]))); |
269 |
qed "parts_insert_Crypt"; |
|
270 |
||
271 |
goal thy "parts (insert {|X,Y|} H) = \ |
|
272 |
\ insert {|X,Y|} (parts (insert X (insert Y H)))"; |
|
2032 | 273 |
by (rtac equalityI 1); |
274 |
by (rtac subsetI 1); |
|
275 |
by (etac parts.induct 1); |
|
1839 | 276 |
by (Auto_tac()); |
2032 | 277 |
by (etac parts.induct 1); |
1839 | 278 |
by (ALLGOALS (best_tac (!claset addIs [parts.Fst, parts.Snd]))); |
279 |
qed "parts_insert_MPair"; |
|
280 |
||
2373 | 281 |
Addsimps [parts_insert_Agent, parts_insert_Nonce, parts_insert_Key, |
282 |
parts_insert_Hash, parts_insert_Crypt, parts_insert_MPair]; |
|
1839 | 283 |
|
284 |
||
2026
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset
|
285 |
goal thy "parts (Key``N) = Key``N"; |
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset
|
286 |
by (Auto_tac()); |
2032 | 287 |
by (etac parts.induct 1); |
2026
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset
|
288 |
by (Auto_tac()); |
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset
|
289 |
qed "parts_image_Key"; |
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset
|
290 |
|
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset
|
291 |
Addsimps [parts_image_Key]; |
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset
|
292 |
|
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset
|
293 |
|
1913 | 294 |
(**** Inductive relation "analz" ****) |
1839 | 295 |
|
296 |
val major::prems = |
|
1913 | 297 |
goal thy "[| {|X,Y|} : analz H; \ |
298 |
\ [| X : analz H; Y : analz H |] ==> P \ |
|
1839 | 299 |
\ |] ==> P"; |
300 |
by (cut_facts_tac [major] 1); |
|
2032 | 301 |
by (resolve_tac prems 1); |
1913 | 302 |
by (REPEAT (eresolve_tac [asm_rl, analz.Fst, analz.Snd] 1)); |
303 |
qed "MPair_analz"; |
|
1839 | 304 |
|
1913 | 305 |
AddIs [analz.Inj]; |
2011 | 306 |
AddSEs [MPair_analz]; (*Perhaps it should NOT be deemed safe!*) |
1913 | 307 |
AddDs [analz.Decrypt]; |
1839 | 308 |
|
1913 | 309 |
Addsimps [analz.Inj]; |
1885 | 310 |
|
1913 | 311 |
goal thy "H <= analz(H)"; |
1839 | 312 |
by (Fast_tac 1); |
1913 | 313 |
qed "analz_increasing"; |
1839 | 314 |
|
1913 | 315 |
goal thy "analz H <= parts H"; |
1839 | 316 |
by (rtac subsetI 1); |
2032 | 317 |
by (etac analz.induct 1); |
1839 | 318 |
by (ALLGOALS Fast_tac); |
1913 | 319 |
qed "analz_subset_parts"; |
1839 | 320 |
|
1913 | 321 |
bind_thm ("not_parts_not_analz", analz_subset_parts RS contra_subsetD); |
1839 | 322 |
|
323 |
||
1913 | 324 |
goal thy "parts (analz H) = parts H"; |
2032 | 325 |
by (rtac equalityI 1); |
326 |
by (rtac (analz_subset_parts RS parts_mono RS subset_trans) 1); |
|
1839 | 327 |
by (Simp_tac 1); |
1913 | 328 |
by (fast_tac (!claset addDs [analz_increasing RS parts_mono RS subsetD]) 1); |
329 |
qed "parts_analz"; |
|
330 |
Addsimps [parts_analz]; |
|
1839 | 331 |
|
1913 | 332 |
goal thy "analz (parts H) = parts H"; |
1885 | 333 |
by (Auto_tac()); |
2032 | 334 |
by (etac analz.induct 1); |
1885 | 335 |
by (Auto_tac()); |
1913 | 336 |
qed "analz_parts"; |
337 |
Addsimps [analz_parts]; |
|
1885 | 338 |
|
1839 | 339 |
(*Monotonicity; Lemma 1 of Lowe*) |
1913 | 340 |
goalw thy analz.defs "!!G H. G<=H ==> analz(G) <= analz(H)"; |
1839 | 341 |
by (rtac lfp_mono 1); |
342 |
by (REPEAT (ares_tac basic_monos 1)); |
|
1913 | 343 |
qed "analz_mono"; |
1839 | 344 |
|
2373 | 345 |
val analz_insertI = impOfSubs (subset_insertI RS analz_mono); |
346 |
||
1839 | 347 |
(** General equational properties **) |
348 |
||
1913 | 349 |
goal thy "analz{} = {}"; |
1839 | 350 |
by (Step_tac 1); |
2032 | 351 |
by (etac analz.induct 1); |
1839 | 352 |
by (ALLGOALS Fast_tac); |
1913 | 353 |
qed "analz_empty"; |
354 |
Addsimps [analz_empty]; |
|
1839 | 355 |
|
1913 | 356 |
(*Converse fails: we can analz more from the union than from the |
1839 | 357 |
separate parts, as a key in one might decrypt a message in the other*) |
1913 | 358 |
goal thy "analz(G) Un analz(H) <= analz(G Un H)"; |
359 |
by (REPEAT (ares_tac [Un_least, analz_mono, Un_upper1, Un_upper2] 1)); |
|
360 |
qed "analz_Un"; |
|
1839 | 361 |
|
1913 | 362 |
goal thy "insert X (analz H) <= analz(insert X H)"; |
363 |
by (fast_tac (!claset addEs [impOfSubs analz_mono]) 1); |
|
364 |
qed "analz_insert"; |
|
1839 | 365 |
|
366 |
(** Rewrite rules for pulling out atomic messages **) |
|
367 |
||
2373 | 368 |
fun analz_tac i = |
369 |
EVERY [rtac ([subsetI, analz_insert] MRS equalityI) i, |
|
370 |
etac analz.induct i, |
|
371 |
REPEAT (fast_tac (!claset addss (!simpset)) i)]; |
|
372 |
||
1913 | 373 |
goal thy "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"; |
2373 | 374 |
by (analz_tac 1); |
1913 | 375 |
qed "analz_insert_Agent"; |
1839 | 376 |
|
1913 | 377 |
goal thy "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"; |
2373 | 378 |
by (analz_tac 1); |
1913 | 379 |
qed "analz_insert_Nonce"; |
1839 | 380 |
|
2373 | 381 |
goal thy "analz (insert (Hash X) H) = insert (Hash X) (analz H)"; |
382 |
by (analz_tac 1); |
|
383 |
qed "analz_insert_Hash"; |
|
384 |
||
1839 | 385 |
(*Can only pull out Keys if they are not needed to decrypt the rest*) |
386 |
goalw thy [keysFor_def] |
|
1913 | 387 |
"!!K. K ~: keysFor (analz H) ==> \ |
388 |
\ analz (insert (Key K) H) = insert (Key K) (analz H)"; |
|
2373 | 389 |
by (analz_tac 1); |
1913 | 390 |
qed "analz_insert_Key"; |
1839 | 391 |
|
1913 | 392 |
goal thy "analz (insert {|X,Y|} H) = \ |
393 |
\ insert {|X,Y|} (analz (insert X (insert Y H)))"; |
|
2032 | 394 |
by (rtac equalityI 1); |
395 |
by (rtac subsetI 1); |
|
396 |
by (etac analz.induct 1); |
|
1885 | 397 |
by (Auto_tac()); |
2032 | 398 |
by (etac analz.induct 1); |
2102 | 399 |
by (ALLGOALS |
400 |
(deepen_tac (!claset addIs [analz.Fst, analz.Snd, analz.Decrypt]) 0)); |
|
1913 | 401 |
qed "analz_insert_MPair"; |
1885 | 402 |
|
403 |
(*Can pull out enCrypted message if the Key is not known*) |
|
1913 | 404 |
goal thy "!!H. Key (invKey K) ~: analz H ==> \ |
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset
|
405 |
\ analz (insert (Crypt K X) H) = \ |
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset
|
406 |
\ insert (Crypt K X) (analz H)"; |
2373 | 407 |
by (analz_tac 1); |
1913 | 408 |
qed "analz_insert_Crypt"; |
1839 | 409 |
|
1913 | 410 |
goal thy "!!H. Key (invKey K) : analz H ==> \ |
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset
|
411 |
\ analz (insert (Crypt K X) H) <= \ |
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset
|
412 |
\ insert (Crypt K X) (analz (insert X H))"; |
2032 | 413 |
by (rtac subsetI 1); |
1913 | 414 |
by (eres_inst_tac [("za","x")] analz.induct 1); |
1839 | 415 |
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); |
416 |
val lemma1 = result(); |
|
417 |
||
1913 | 418 |
goal thy "!!H. Key (invKey K) : analz H ==> \ |
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset
|
419 |
\ insert (Crypt K X) (analz (insert X H)) <= \ |
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset
|
420 |
\ analz (insert (Crypt K X) H)"; |
1839 | 421 |
by (Auto_tac()); |
1913 | 422 |
by (eres_inst_tac [("za","x")] analz.induct 1); |
1839 | 423 |
by (Auto_tac()); |
1913 | 424 |
by (best_tac (!claset addIs [subset_insertI RS analz_mono RS subsetD, |
2032 | 425 |
analz.Decrypt]) 1); |
1839 | 426 |
val lemma2 = result(); |
427 |
||
1913 | 428 |
goal thy "!!H. Key (invKey K) : analz H ==> \ |
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset
|
429 |
\ analz (insert (Crypt K X) H) = \ |
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset
|
430 |
\ insert (Crypt K X) (analz (insert X H))"; |
1839 | 431 |
by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1)); |
1913 | 432 |
qed "analz_insert_Decrypt"; |
1839 | 433 |
|
1885 | 434 |
(*Case analysis: either the message is secure, or it is not! |
1946 | 435 |
Effective, but can cause subgoals to blow up! |
1885 | 436 |
Use with expand_if; apparently split_tac does not cope with patterns |
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset
|
437 |
such as "analz (insert (Crypt K X) H)" *) |
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset
|
438 |
goal thy "analz (insert (Crypt K X) H) = \ |
2154 | 439 |
\ (if (Key (invKey K) : analz H) \ |
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset
|
440 |
\ then insert (Crypt K X) (analz (insert X H)) \ |
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset
|
441 |
\ else insert (Crypt K X) (analz H))"; |
2102 | 442 |
by (case_tac "Key (invKey K) : analz H " 1); |
1913 | 443 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps [analz_insert_Crypt, |
2032 | 444 |
analz_insert_Decrypt]))); |
1913 | 445 |
qed "analz_Crypt_if"; |
1885 | 446 |
|
2373 | 447 |
Addsimps [analz_insert_Agent, analz_insert_Nonce, analz_insert_Key, |
448 |
analz_insert_Hash, analz_insert_MPair, analz_Crypt_if]; |
|
1839 | 449 |
|
450 |
(*This rule supposes "for the sake of argument" that we have the key.*) |
|
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset
|
451 |
goal thy "analz (insert (Crypt K X) H) <= \ |
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset
|
452 |
\ insert (Crypt K X) (analz (insert X H))"; |
2032 | 453 |
by (rtac subsetI 1); |
454 |
by (etac analz.induct 1); |
|
1839 | 455 |
by (Auto_tac()); |
1913 | 456 |
qed "analz_insert_Crypt_subset"; |
1839 | 457 |
|
458 |
||
2026
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset
|
459 |
goal thy "analz (Key``N) = Key``N"; |
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset
|
460 |
by (Auto_tac()); |
2032 | 461 |
by (etac analz.induct 1); |
2026
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset
|
462 |
by (Auto_tac()); |
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset
|
463 |
qed "analz_image_Key"; |
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset
|
464 |
|
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset
|
465 |
Addsimps [analz_image_Key]; |
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset
|
466 |
|
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset
|
467 |
|
1839 | 468 |
(** Idempotence and transitivity **) |
469 |
||
1913 | 470 |
goal thy "!!H. X: analz (analz H) ==> X: analz H"; |
2032 | 471 |
by (etac analz.induct 1); |
1839 | 472 |
by (ALLGOALS Fast_tac); |
1913 | 473 |
qed "analz_analzE"; |
474 |
AddSEs [analz_analzE]; |
|
1839 | 475 |
|
1913 | 476 |
goal thy "analz (analz H) = analz H"; |
1839 | 477 |
by (Fast_tac 1); |
1913 | 478 |
qed "analz_idem"; |
479 |
Addsimps [analz_idem]; |
|
1839 | 480 |
|
1913 | 481 |
goal thy "!!H. [| X: analz G; G <= analz H |] ==> X: analz H"; |
482 |
by (dtac analz_mono 1); |
|
1839 | 483 |
by (Fast_tac 1); |
1913 | 484 |
qed "analz_trans"; |
1839 | 485 |
|
486 |
(*Cut; Lemma 2 of Lowe*) |
|
1998
f8230821f1e8
Reordering of premises for cut theorems, and new law MPair_synth_analz
paulson
parents:
1994
diff
changeset
|
487 |
goal thy "!!H. [| Y: analz (insert X H); X: analz H |] ==> Y: analz H"; |
2032 | 488 |
by (etac analz_trans 1); |
1839 | 489 |
by (Fast_tac 1); |
1913 | 490 |
qed "analz_cut"; |
1839 | 491 |
|
492 |
(*Cut can be proved easily by induction on |
|
1913 | 493 |
"!!H. Y: analz (insert X H) ==> X: analz H --> Y: analz H" |
1839 | 494 |
*) |
495 |
||
1885 | 496 |
|
1913 | 497 |
(** A congruence rule for "analz" **) |
1885 | 498 |
|
1913 | 499 |
goal thy "!!H. [| analz G <= analz G'; analz H <= analz H' \ |
500 |
\ |] ==> analz (G Un H) <= analz (G' Un H')"; |
|
1885 | 501 |
by (Step_tac 1); |
2032 | 502 |
by (etac analz.induct 1); |
1913 | 503 |
by (ALLGOALS (best_tac (!claset addIs [analz_mono RS subsetD]))); |
504 |
qed "analz_subset_cong"; |
|
1885 | 505 |
|
1913 | 506 |
goal thy "!!H. [| analz G = analz G'; analz H = analz H' \ |
507 |
\ |] ==> analz (G Un H) = analz (G' Un H')"; |
|
508 |
by (REPEAT_FIRST (ares_tac [equalityI, analz_subset_cong] |
|
2032 | 509 |
ORELSE' etac equalityE)); |
1913 | 510 |
qed "analz_cong"; |
1885 | 511 |
|
512 |
||
1913 | 513 |
goal thy "!!H. analz H = analz H' ==> analz(insert X H) = analz(insert X H')"; |
1885 | 514 |
by (asm_simp_tac (!simpset addsimps [insert_def] |
2032 | 515 |
setloop (rtac analz_cong)) 1); |
1913 | 516 |
qed "analz_insert_cong"; |
1885 | 517 |
|
1913 | 518 |
(*If there are no pairs or encryptions then analz does nothing*) |
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset
|
519 |
goal thy "!!H. [| ALL X Y. {|X,Y|} ~: H; ALL X K. Crypt K X ~: H |] ==> \ |
1913 | 520 |
\ analz H = H"; |
1839 | 521 |
by (Step_tac 1); |
2032 | 522 |
by (etac analz.induct 1); |
1839 | 523 |
by (ALLGOALS Fast_tac); |
1913 | 524 |
qed "analz_trivial"; |
1839 | 525 |
|
526 |
(*Helps to prove Fake cases*) |
|
1913 | 527 |
goal thy "!!X. X: analz (UN i. analz (H i)) ==> X: analz (UN i. H i)"; |
2032 | 528 |
by (etac analz.induct 1); |
1913 | 529 |
by (ALLGOALS (fast_tac (!claset addEs [impOfSubs analz_mono]))); |
1839 | 530 |
val lemma = result(); |
531 |
||
1913 | 532 |
goal thy "analz (UN i. analz (H i)) = analz (UN i. H i)"; |
1839 | 533 |
by (fast_tac (!claset addIs [lemma] |
2032 | 534 |
addEs [impOfSubs analz_mono]) 1); |
1913 | 535 |
qed "analz_UN_analz"; |
536 |
Addsimps [analz_UN_analz]; |
|
1839 | 537 |
|
538 |
||
1913 | 539 |
(**** Inductive relation "synth" ****) |
1839 | 540 |
|
1913 | 541 |
AddIs synth.intrs; |
1839 | 542 |
|
2011 | 543 |
(*Can only produce a nonce or key if it is already known, |
544 |
but can synth a pair or encryption from its components...*) |
|
545 |
val mk_cases = synth.mk_cases msg.simps; |
|
546 |
||
547 |
(*NO Agent_synth, as any Agent name can be synthd*) |
|
548 |
val Nonce_synth = mk_cases "Nonce n : synth H"; |
|
549 |
val Key_synth = mk_cases "Key K : synth H"; |
|
2373 | 550 |
val Hash_synth = mk_cases "Hash X : synth H"; |
2011 | 551 |
val MPair_synth = mk_cases "{|X,Y|} : synth H"; |
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset
|
552 |
val Crypt_synth = mk_cases "Crypt K X : synth H"; |
2011 | 553 |
|
2373 | 554 |
AddSEs [Nonce_synth, Key_synth, Hash_synth, MPair_synth, Crypt_synth]; |
2011 | 555 |
|
1913 | 556 |
goal thy "H <= synth(H)"; |
1839 | 557 |
by (Fast_tac 1); |
1913 | 558 |
qed "synth_increasing"; |
1839 | 559 |
|
560 |
(*Monotonicity*) |
|
1913 | 561 |
goalw thy synth.defs "!!G H. G<=H ==> synth(G) <= synth(H)"; |
1839 | 562 |
by (rtac lfp_mono 1); |
563 |
by (REPEAT (ares_tac basic_monos 1)); |
|
1913 | 564 |
qed "synth_mono"; |
1839 | 565 |
|
566 |
(** Unions **) |
|
567 |
||
1913 | 568 |
(*Converse fails: we can synth more from the union than from the |
1839 | 569 |
separate parts, building a compound message using elements of each.*) |
1913 | 570 |
goal thy "synth(G) Un synth(H) <= synth(G Un H)"; |
571 |
by (REPEAT (ares_tac [Un_least, synth_mono, Un_upper1, Un_upper2] 1)); |
|
572 |
qed "synth_Un"; |
|
1839 | 573 |
|
1913 | 574 |
goal thy "insert X (synth H) <= synth(insert X H)"; |
575 |
by (fast_tac (!claset addEs [impOfSubs synth_mono]) 1); |
|
576 |
qed "synth_insert"; |
|
1885 | 577 |
|
1839 | 578 |
(** Idempotence and transitivity **) |
579 |
||
1913 | 580 |
goal thy "!!H. X: synth (synth H) ==> X: synth H"; |
2032 | 581 |
by (etac synth.induct 1); |
1839 | 582 |
by (ALLGOALS Fast_tac); |
1913 | 583 |
qed "synth_synthE"; |
584 |
AddSEs [synth_synthE]; |
|
1839 | 585 |
|
1913 | 586 |
goal thy "synth (synth H) = synth H"; |
1839 | 587 |
by (Fast_tac 1); |
1913 | 588 |
qed "synth_idem"; |
1839 | 589 |
|
1913 | 590 |
goal thy "!!H. [| X: synth G; G <= synth H |] ==> X: synth H"; |
591 |
by (dtac synth_mono 1); |
|
1839 | 592 |
by (Fast_tac 1); |
1913 | 593 |
qed "synth_trans"; |
1839 | 594 |
|
595 |
(*Cut; Lemma 2 of Lowe*) |
|
1998
f8230821f1e8
Reordering of premises for cut theorems, and new law MPair_synth_analz
paulson
parents:
1994
diff
changeset
|
596 |
goal thy "!!H. [| Y: synth (insert X H); X: synth H |] ==> Y: synth H"; |
2032 | 597 |
by (etac synth_trans 1); |
1839 | 598 |
by (Fast_tac 1); |
1913 | 599 |
qed "synth_cut"; |
1839 | 600 |
|
1946 | 601 |
goal thy "Agent A : synth H"; |
602 |
by (Fast_tac 1); |
|
603 |
qed "Agent_synth"; |
|
604 |
||
1913 | 605 |
goal thy "(Nonce N : synth H) = (Nonce N : H)"; |
1839 | 606 |
by (Fast_tac 1); |
1913 | 607 |
qed "Nonce_synth_eq"; |
1839 | 608 |
|
1913 | 609 |
goal thy "(Key K : synth H) = (Key K : H)"; |
1839 | 610 |
by (Fast_tac 1); |
1913 | 611 |
qed "Key_synth_eq"; |
1839 | 612 |
|
2373 | 613 |
goal thy "!!K. Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X : H)"; |
2011 | 614 |
by (Fast_tac 1); |
615 |
qed "Crypt_synth_eq"; |
|
616 |
||
617 |
Addsimps [Agent_synth, Nonce_synth_eq, Key_synth_eq, Crypt_synth_eq]; |
|
1839 | 618 |
|
619 |
||
620 |
goalw thy [keysFor_def] |
|
1913 | 621 |
"keysFor (synth H) = keysFor H Un invKey``{K. Key K : H}"; |
1839 | 622 |
by (Fast_tac 1); |
1913 | 623 |
qed "keysFor_synth"; |
624 |
Addsimps [keysFor_synth]; |
|
1839 | 625 |
|
626 |
||
1913 | 627 |
(*** Combinations of parts, analz and synth ***) |
1839 | 628 |
|
1913 | 629 |
goal thy "parts (synth H) = parts H Un synth H"; |
2032 | 630 |
by (rtac equalityI 1); |
631 |
by (rtac subsetI 1); |
|
632 |
by (etac parts.induct 1); |
|
1839 | 633 |
by (ALLGOALS |
1913 | 634 |
(best_tac (!claset addIs ((synth_increasing RS parts_mono RS subsetD) |
2032 | 635 |
::parts.intrs)))); |
1913 | 636 |
qed "parts_synth"; |
637 |
Addsimps [parts_synth]; |
|
1839 | 638 |
|
2373 | 639 |
goal thy "analz (analz G Un H) = analz (G Un H)"; |
640 |
by (REPEAT_FIRST (resolve_tac [equalityI, analz_subset_cong])); |
|
641 |
by (ALLGOALS Simp_tac); |
|
642 |
qed "analz_analz_Un"; |
|
643 |
||
644 |
goal thy "analz (synth G Un H) = analz (G Un H) Un synth G"; |
|
2032 | 645 |
by (rtac equalityI 1); |
646 |
by (rtac subsetI 1); |
|
647 |
by (etac analz.induct 1); |
|
2373 | 648 |
by (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 5); |
1839 | 649 |
(*Strange that best_tac just can't hack this one...*) |
1913 | 650 |
by (ALLGOALS (deepen_tac (!claset addIs analz.intrs) 0)); |
2373 | 651 |
qed "analz_synth_Un"; |
652 |
||
653 |
goal thy "analz (synth H) = analz H Un synth H"; |
|
654 |
by (cut_inst_tac [("H","{}")] analz_synth_Un 1); |
|
655 |
by (Full_simp_tac 1); |
|
1913 | 656 |
qed "analz_synth"; |
2373 | 657 |
Addsimps [analz_analz_Un, analz_synth_Un, analz_synth]; |
1839 | 658 |
|
2032 | 659 |
(*Hard to prove; still needed now that there's only one Spy?*) |
1913 | 660 |
goal thy "analz (UN i. synth (H i)) = \ |
661 |
\ analz (UN i. H i) Un (UN i. synth (H i))"; |
|
2032 | 662 |
by (rtac equalityI 1); |
663 |
by (rtac subsetI 1); |
|
664 |
by (etac analz.induct 1); |
|
1839 | 665 |
by (best_tac |
1913 | 666 |
(!claset addEs [impOfSubs synth_increasing, |
2032 | 667 |
impOfSubs analz_mono]) 5); |
1839 | 668 |
by (Best_tac 1); |
1913 | 669 |
by (deepen_tac (!claset addIs [analz.Fst]) 0 1); |
670 |
by (deepen_tac (!claset addIs [analz.Snd]) 0 1); |
|
671 |
by (deepen_tac (!claset addSEs [analz.Decrypt] |
|
2032 | 672 |
addIs [analz.Decrypt]) 0 1); |
1913 | 673 |
qed "analz_UN1_synth"; |
674 |
Addsimps [analz_UN1_synth]; |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
675 |
|
1946 | 676 |
|
677 |
(** For reasoning about the Fake rule in traces **) |
|
678 |
||
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
679 |
goal thy "!!Y. X: G ==> parts(insert X H) <= parts G Un parts H"; |
2032 | 680 |
by (rtac ([parts_mono, parts_Un_subset2] MRS subset_trans) 1); |
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
681 |
by (Fast_tac 1); |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
682 |
qed "parts_insert_subset_Un"; |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
683 |
|
1946 | 684 |
(*More specifically for Fake*) |
685 |
goal thy "!!H. X: synth (analz G) ==> \ |
|
686 |
\ parts (insert X H) <= synth (analz G) Un parts G Un parts H"; |
|
2032 | 687 |
by (dtac parts_insert_subset_Un 1); |
1946 | 688 |
by (Full_simp_tac 1); |
689 |
by (Deepen_tac 0 1); |
|
690 |
qed "Fake_parts_insert"; |
|
691 |
||
2061 | 692 |
goal thy |
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset
|
693 |
"!!H. [| Crypt K Y : parts (insert X H); X: synth (analz G); \ |
2061 | 694 |
\ Key K ~: analz G |] \ |
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset
|
695 |
\ ==> Crypt K Y : parts G Un parts H"; |
2061 | 696 |
by (dtac (impOfSubs Fake_parts_insert) 1); |
2170 | 697 |
by (assume_tac 1); |
2061 | 698 |
by (fast_tac (!claset addDs [impOfSubs analz_subset_parts] |
699 |
addss (!simpset)) 1); |
|
700 |
qed "Crypt_Fake_parts_insert"; |
|
701 |
||
2373 | 702 |
goal thy "!!H. X: synth (analz G) ==> \ |
703 |
\ analz (insert X H) <= synth (analz G) Un analz (G Un H)"; |
|
704 |
by (rtac subsetI 1); |
|
705 |
by (subgoal_tac "x : analz (synth (analz G) Un H)" 1); |
|
706 |
by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)] |
|
707 |
addSEs [impOfSubs analz_mono]) 2); |
|
708 |
by (Full_simp_tac 1); |
|
709 |
by (Fast_tac 1); |
|
710 |
qed "Fake_analz_insert"; |
|
711 |
||
712 |
(*Needed????????????????*) |
|
1946 | 713 |
goal thy "!!H. [| X: synth (analz G); G <= H |] ==> \ |
714 |
\ analz (insert X H) <= synth (analz H) Un analz H"; |
|
2032 | 715 |
by (rtac subsetI 1); |
1946 | 716 |
by (subgoal_tac "x : analz (synth (analz H))" 1); |
717 |
by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)] |
|
718 |
addSEs [impOfSubs analz_mono]) 2); |
|
719 |
by (Full_simp_tac 1); |
|
720 |
by (Fast_tac 1); |
|
2373 | 721 |
qed "Fake_analz_insert_old"; |
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
722 |
|
2011 | 723 |
goal thy "(X: analz H & X: parts H) = (X: analz H)"; |
724 |
by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]) 1); |
|
725 |
val analz_conj_parts = result(); |
|
726 |
||
727 |
goal thy "(X: analz H | X: parts H) = (X: parts H)"; |
|
728 |
by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]) 1); |
|
729 |
val analz_disj_parts = result(); |
|
730 |
||
731 |
AddIffs [analz_conj_parts, analz_disj_parts]; |
|
732 |
||
1998
f8230821f1e8
Reordering of premises for cut theorems, and new law MPair_synth_analz
paulson
parents:
1994
diff
changeset
|
733 |
(*Without this equation, other rules for synth and analz would yield |
f8230821f1e8
Reordering of premises for cut theorems, and new law MPair_synth_analz
paulson
parents:
1994
diff
changeset
|
734 |
redundant cases*) |
f8230821f1e8
Reordering of premises for cut theorems, and new law MPair_synth_analz
paulson
parents:
1994
diff
changeset
|
735 |
goal thy "({|X,Y|} : synth (analz H)) = \ |
f8230821f1e8
Reordering of premises for cut theorems, and new law MPair_synth_analz
paulson
parents:
1994
diff
changeset
|
736 |
\ (X : synth (analz H) & Y : synth (analz H))"; |
f8230821f1e8
Reordering of premises for cut theorems, and new law MPair_synth_analz
paulson
parents:
1994
diff
changeset
|
737 |
by (Fast_tac 1); |
f8230821f1e8
Reordering of premises for cut theorems, and new law MPair_synth_analz
paulson
parents:
1994
diff
changeset
|
738 |
qed "MPair_synth_analz"; |
f8230821f1e8
Reordering of premises for cut theorems, and new law MPair_synth_analz
paulson
parents:
1994
diff
changeset
|
739 |
|
f8230821f1e8
Reordering of premises for cut theorems, and new law MPair_synth_analz
paulson
parents:
1994
diff
changeset
|
740 |
AddIffs [MPair_synth_analz]; |
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
741 |
|
2154 | 742 |
goal thy "!!K. [| Key K : analz H; Key (invKey K) : analz H |] \ |
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset
|
743 |
\ ==> (Crypt K X : synth (analz H)) = (X : synth (analz H))"; |
2154 | 744 |
by (Fast_tac 1); |
745 |
qed "Crypt_synth_analz"; |
|
746 |
||
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
747 |
|
2373 | 748 |
goal thy "!!K. Key K ~: analz H \ |
749 |
\ ==> (Hash{|Key K,X|} : synth (analz H)) = (Hash{|Key K,X|} : analz H)"; |
|
750 |
by (Fast_tac 1); |
|
751 |
qed "Hash_synth_analz"; |
|
752 |
Addsimps [Hash_synth_analz]; |
|
753 |
||
754 |
||
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
755 |
(*We do NOT want Crypt... messages broken up in protocols!!*) |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
756 |
Delrules partsEs; |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
757 |
|
2327 | 758 |
|
759 |
(** Rewrites to push in Key and Crypt messages, so that other messages can |
|
760 |
be pulled out using the analz_insert rules **) |
|
761 |
||
762 |
fun insComm thy x y = read_instantiate_sg (sign_of thy) [("x",x), ("y",y)] |
|
763 |
insert_commute; |
|
764 |
||
765 |
val pushKeys = map (insComm thy "Key ?K") |
|
2373 | 766 |
["Agent ?C", "Nonce ?N", "Hash ?X", |
767 |
"MPair ?X ?Y", "Crypt ?X ?K'"]; |
|
2327 | 768 |
|
769 |
val pushCrypts = map (insComm thy "Crypt ?X ?K") |
|
2373 | 770 |
["Agent ?C", "Nonce ?N", "Hash ?X'", "MPair ?X' ?Y"]; |
2327 | 771 |
|
772 |
(*Cannot be added with Addsimps -- we don't always want to re-order messages*) |
|
773 |
val pushes = pushKeys@pushCrypts; |
|
774 |
||
775 |
||
776 |
(*No premature instantiation of variables. For proving weak liveness.*) |
|
777 |
fun safe_solver prems = |
|
778 |
match_tac (TrueI::refl::prems) ORELSE' eq_assume_tac |
|
779 |
ORELSE' etac FalseE; |
|
780 |
||
2373 | 781 |
val Fake_insert_tac = |
782 |
dresolve_tac [impOfSubs Fake_analz_insert, |
|
783 |
impOfSubs Fake_parts_insert] THEN' |
|
784 |
eresolve_tac [asm_rl, synth.Inj]; |
|
785 |
||
786 |
(*Analysis of Fake cases and of messages that forward unknown parts. |
|
2327 | 787 |
Abstraction over i is ESSENTIAL: it delays the dereferencing of claset |
788 |
DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *) |
|
789 |
fun spy_analz_tac i = |
|
2373 | 790 |
DETERM |
791 |
(SELECT_GOAL |
|
792 |
(EVERY |
|
793 |
[ (*push in occurrences of X...*) |
|
794 |
(REPEAT o CHANGED) |
|
795 |
(res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1), |
|
796 |
(*...allowing further simplifications*) |
|
797 |
simp_tac (!simpset setloop split_tac [expand_if]) 1, |
|
798 |
REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI])), |
|
799 |
DEPTH_SOLVE |
|
800 |
(REPEAT (Fake_insert_tac 1) THEN Asm_full_simp_tac 1 |
|
801 |
THEN |
|
802 |
IF_UNSOLVED (depth_tac (!claset addIs [impOfSubs analz_mono, |
|
803 |
impOfSubs analz_subset_parts]) 2 1)) |
|
804 |
]) i); |
|
2327 | 805 |
|
806 |
(*Useful in many uniqueness proofs*) |
|
807 |
fun ex_strip_tac i = REPEAT (swap_res_tac [exI, conjI] i) THEN |
|
808 |
assume_tac (i+1); |
|
809 |
||
2373 | 810 |
|
811 |
(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*) |
|
812 |
goal Set.thy "A Un (B Un A) = B Un A"; |
|
813 |
by (Fast_tac 1); |
|
814 |
val Un_absorb3 = result(); |
|
815 |
Addsimps [Un_absorb3]; |