author | paulson |
Tue, 20 Aug 1996 17:46:24 +0200 | |
changeset 1929 | f0839bab4b00 |
parent 1913 | 2809adb15eb0 |
child 1946 | b59a3d686436 |
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 |
||
10 |
open Message; |
|
11 |
||
12 |
||
13 |
(** Inverse of keys **) |
|
14 |
||
15 |
goal thy "!!K K'. (invKey K = invKey K') = (K=K')"; |
|
16 |
by (Step_tac 1); |
|
17 |
br box_equals 1; |
|
18 |
by (REPEAT (rtac invKey 2)); |
|
19 |
by (Asm_simp_tac 1); |
|
20 |
qed "invKey_eq"; |
|
21 |
||
22 |
Addsimps [invKey, invKey_eq]; |
|
23 |
||
24 |
||
25 |
(**** keysFor operator ****) |
|
26 |
||
27 |
goalw thy [keysFor_def] "keysFor {} = {}"; |
|
28 |
by (Fast_tac 1); |
|
29 |
qed "keysFor_empty"; |
|
30 |
||
31 |
goalw thy [keysFor_def] "keysFor (H Un H') = keysFor H Un keysFor H'"; |
|
32 |
by (Fast_tac 1); |
|
33 |
qed "keysFor_Un"; |
|
34 |
||
35 |
goalw thy [keysFor_def] "keysFor (UN i. H i) = (UN i. keysFor (H i))"; |
|
36 |
by (Fast_tac 1); |
|
37 |
qed "keysFor_UN"; |
|
38 |
||
39 |
(*Monotonicity*) |
|
40 |
goalw thy [keysFor_def] "!!G H. G<=H ==> keysFor(G) <= keysFor(H)"; |
|
41 |
by (Fast_tac 1); |
|
42 |
qed "keysFor_mono"; |
|
43 |
||
44 |
goalw thy [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H"; |
|
45 |
by (fast_tac (!claset addss (!simpset)) 1); |
|
46 |
qed "keysFor_insert_Agent"; |
|
47 |
||
48 |
goalw thy [keysFor_def] "keysFor (insert (Nonce N) H) = keysFor H"; |
|
49 |
by (fast_tac (!claset addss (!simpset)) 1); |
|
50 |
qed "keysFor_insert_Nonce"; |
|
51 |
||
52 |
goalw thy [keysFor_def] "keysFor (insert (Key K) H) = keysFor H"; |
|
53 |
by (fast_tac (!claset addss (!simpset)) 1); |
|
54 |
qed "keysFor_insert_Key"; |
|
55 |
||
56 |
goalw thy [keysFor_def] "keysFor (insert {|X,Y|} H) = keysFor H"; |
|
57 |
by (fast_tac (!claset addss (!simpset)) 1); |
|
58 |
qed "keysFor_insert_MPair"; |
|
59 |
||
60 |
goalw thy [keysFor_def] |
|
61 |
"keysFor (insert (Crypt X K) H) = insert (invKey K) (keysFor H)"; |
|
62 |
by (Auto_tac()); |
|
63 |
by (fast_tac (!claset addIs [image_eqI]) 1); |
|
64 |
qed "keysFor_insert_Crypt"; |
|
65 |
||
66 |
Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, |
|
67 |
keysFor_insert_Agent, keysFor_insert_Nonce, |
|
68 |
keysFor_insert_Key, keysFor_insert_MPair, |
|
69 |
keysFor_insert_Crypt]; |
|
70 |
||
71 |
||
72 |
(**** Inductive relation "parts" ****) |
|
73 |
||
74 |
val major::prems = |
|
75 |
goal thy "[| {|X,Y|} : parts H; \ |
|
76 |
\ [| X : parts H; Y : parts H |] ==> P \ |
|
77 |
\ |] ==> P"; |
|
78 |
by (cut_facts_tac [major] 1); |
|
79 |
brs prems 1; |
|
80 |
by (REPEAT (eresolve_tac [asm_rl, parts.Fst, parts.Snd] 1)); |
|
81 |
qed "MPair_parts"; |
|
82 |
||
83 |
AddIs [parts.Inj]; |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
84 |
|
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
85 |
val partsEs = [MPair_parts, make_elim parts.Body]; |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
86 |
|
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
87 |
AddSEs partsEs; |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
88 |
(*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
|
89 |
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
|
90 |
proofs concern only atomic messages.*) |
1839 | 91 |
|
92 |
goal thy "H <= parts(H)"; |
|
93 |
by (Fast_tac 1); |
|
94 |
qed "parts_increasing"; |
|
95 |
||
96 |
(*Monotonicity*) |
|
97 |
goalw thy parts.defs "!!G H. G<=H ==> parts(G) <= parts(H)"; |
|
98 |
by (rtac lfp_mono 1); |
|
99 |
by (REPEAT (ares_tac basic_monos 1)); |
|
100 |
qed "parts_mono"; |
|
101 |
||
102 |
goal thy "parts{} = {}"; |
|
103 |
by (Step_tac 1); |
|
104 |
be parts.induct 1; |
|
105 |
by (ALLGOALS Fast_tac); |
|
106 |
qed "parts_empty"; |
|
107 |
Addsimps [parts_empty]; |
|
108 |
||
109 |
goal thy "!!X. X: parts{} ==> P"; |
|
110 |
by (Asm_full_simp_tac 1); |
|
111 |
qed "parts_emptyE"; |
|
112 |
AddSEs [parts_emptyE]; |
|
113 |
||
1893 | 114 |
(*WARNING: loops if H = {Y}, therefore must not be repeated!*) |
115 |
goal thy "!!H. X: parts H ==> EX Y:H. X: parts {Y}"; |
|
116 |
be parts.induct 1; |
|
117 |
by (ALLGOALS Fast_tac); |
|
118 |
qed "parts_singleton"; |
|
119 |
||
1839 | 120 |
|
121 |
(** Unions **) |
|
122 |
||
123 |
goal thy "parts(G) Un parts(H) <= parts(G Un H)"; |
|
124 |
by (REPEAT (ares_tac [Un_least, parts_mono, Un_upper1, Un_upper2] 1)); |
|
125 |
val parts_Un_subset1 = result(); |
|
126 |
||
127 |
goal thy "parts(G Un H) <= parts(G) Un parts(H)"; |
|
128 |
br subsetI 1; |
|
129 |
be parts.induct 1; |
|
130 |
by (ALLGOALS Fast_tac); |
|
131 |
val parts_Un_subset2 = result(); |
|
132 |
||
133 |
goal thy "parts(G Un H) = parts(G) Un parts(H)"; |
|
134 |
by (REPEAT (ares_tac [equalityI, parts_Un_subset1, parts_Un_subset2] 1)); |
|
135 |
qed "parts_Un"; |
|
136 |
||
1852 | 137 |
(*TWO inserts to avoid looping. This rewrite is better than nothing...*) |
138 |
goal thy "parts (insert X (insert Y H)) = parts {X} Un parts {Y} Un parts H"; |
|
139 |
by (stac (read_instantiate [("A","H")] insert_is_Un) 1); |
|
140 |
by (stac (read_instantiate [("A","{Y} Un H")] insert_is_Un) 1); |
|
141 |
by (simp_tac (HOL_ss addsimps [parts_Un, Un_assoc]) 1); |
|
142 |
qed "parts_insert2"; |
|
143 |
||
1839 | 144 |
goal thy "(UN x:A. parts(H x)) <= parts(UN x:A. H x)"; |
145 |
by (REPEAT (ares_tac [UN_least, parts_mono, UN_upper] 1)); |
|
146 |
val parts_UN_subset1 = result(); |
|
147 |
||
148 |
goal thy "parts(UN x:A. H x) <= (UN x:A. parts(H x))"; |
|
149 |
br subsetI 1; |
|
150 |
be parts.induct 1; |
|
151 |
by (ALLGOALS Fast_tac); |
|
152 |
val parts_UN_subset2 = result(); |
|
153 |
||
154 |
goal thy "parts(UN x:A. H x) = (UN x:A. parts(H x))"; |
|
155 |
by (REPEAT (ares_tac [equalityI, parts_UN_subset1, parts_UN_subset2] 1)); |
|
156 |
qed "parts_UN"; |
|
157 |
||
158 |
goal thy "parts(UN x. H x) = (UN x. parts(H x))"; |
|
159 |
by (simp_tac (!simpset addsimps [UNION1_def, parts_UN]) 1); |
|
160 |
qed "parts_UN1"; |
|
161 |
||
1913 | 162 |
(*Added to simplify arguments to parts, analz and synth*) |
1839 | 163 |
Addsimps [parts_Un, parts_UN, parts_UN1]; |
164 |
||
165 |
goal thy "insert X (parts H) <= parts(insert X H)"; |
|
1852 | 166 |
by (fast_tac (!claset addEs [impOfSubs parts_mono]) 1); |
1839 | 167 |
qed "parts_insert_subset"; |
168 |
||
169 |
(** Idempotence and transitivity **) |
|
170 |
||
171 |
goal thy "!!H. X: parts (parts H) ==> X: parts H"; |
|
172 |
be parts.induct 1; |
|
173 |
by (ALLGOALS Fast_tac); |
|
174 |
qed "parts_partsE"; |
|
175 |
AddSEs [parts_partsE]; |
|
176 |
||
177 |
goal thy "parts (parts H) = parts H"; |
|
178 |
by (Fast_tac 1); |
|
179 |
qed "parts_idem"; |
|
180 |
Addsimps [parts_idem]; |
|
181 |
||
182 |
goal thy "!!H. [| X: parts G; G <= parts H |] ==> X: parts H"; |
|
183 |
by (dtac parts_mono 1); |
|
184 |
by (Fast_tac 1); |
|
185 |
qed "parts_trans"; |
|
186 |
||
187 |
(*Cut*) |
|
188 |
goal thy "!!H. [| X: parts H; Y: parts (insert X H) |] ==> Y: parts H"; |
|
189 |
be parts_trans 1; |
|
190 |
by (Fast_tac 1); |
|
191 |
qed "parts_cut"; |
|
192 |
||
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
193 |
goal thy "!!H. X: parts H ==> parts (insert X H) = parts H"; |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
194 |
by (fast_tac (!claset addSEs [parts_cut] |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
195 |
addIs [impOfSubs (subset_insertI RS parts_mono)]) 1); |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
196 |
qed "parts_cut_eq"; |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
197 |
|
1839 | 198 |
|
199 |
(** Rewrite rules for pulling out atomic messages **) |
|
200 |
||
201 |
goal thy "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"; |
|
202 |
by (rtac (parts_insert_subset RSN (2, equalityI)) 1); |
|
203 |
br subsetI 1; |
|
204 |
be parts.induct 1; |
|
205 |
(*Simplification breaks up equalities between messages; |
|
206 |
how to make it work for fast_tac??*) |
|
207 |
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); |
|
208 |
qed "parts_insert_Agent"; |
|
209 |
||
210 |
goal thy "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"; |
|
211 |
by (rtac (parts_insert_subset RSN (2, equalityI)) 1); |
|
212 |
br subsetI 1; |
|
213 |
be parts.induct 1; |
|
214 |
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); |
|
215 |
qed "parts_insert_Nonce"; |
|
216 |
||
217 |
goal thy "parts (insert (Key K) H) = insert (Key K) (parts H)"; |
|
218 |
by (rtac (parts_insert_subset RSN (2, equalityI)) 1); |
|
219 |
br subsetI 1; |
|
220 |
be parts.induct 1; |
|
221 |
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); |
|
222 |
qed "parts_insert_Key"; |
|
223 |
||
224 |
goal thy "parts (insert (Crypt X K) H) = \ |
|
225 |
\ insert (Crypt X K) (parts (insert X H))"; |
|
226 |
br equalityI 1; |
|
227 |
br subsetI 1; |
|
228 |
be parts.induct 1; |
|
229 |
by (Auto_tac()); |
|
230 |
be parts.induct 1; |
|
231 |
by (ALLGOALS (best_tac (!claset addIs [parts.Body]))); |
|
232 |
qed "parts_insert_Crypt"; |
|
233 |
||
234 |
goal thy "parts (insert {|X,Y|} H) = \ |
|
235 |
\ insert {|X,Y|} (parts (insert X (insert Y H)))"; |
|
236 |
br equalityI 1; |
|
237 |
br subsetI 1; |
|
238 |
be parts.induct 1; |
|
239 |
by (Auto_tac()); |
|
240 |
be parts.induct 1; |
|
241 |
by (ALLGOALS (best_tac (!claset addIs [parts.Fst, parts.Snd]))); |
|
242 |
qed "parts_insert_MPair"; |
|
243 |
||
244 |
Addsimps [parts_insert_Agent, parts_insert_Nonce, |
|
245 |
parts_insert_Key, parts_insert_Crypt, parts_insert_MPair]; |
|
246 |
||
247 |
||
1913 | 248 |
(**** Inductive relation "analz" ****) |
1839 | 249 |
|
250 |
val major::prems = |
|
1913 | 251 |
goal thy "[| {|X,Y|} : analz H; \ |
252 |
\ [| X : analz H; Y : analz H |] ==> P \ |
|
1839 | 253 |
\ |] ==> P"; |
254 |
by (cut_facts_tac [major] 1); |
|
255 |
brs prems 1; |
|
1913 | 256 |
by (REPEAT (eresolve_tac [asm_rl, analz.Fst, analz.Snd] 1)); |
257 |
qed "MPair_analz"; |
|
1839 | 258 |
|
1913 | 259 |
AddIs [analz.Inj]; |
260 |
AddSEs [MPair_analz]; |
|
261 |
AddDs [analz.Decrypt]; |
|
1839 | 262 |
|
1913 | 263 |
Addsimps [analz.Inj]; |
1885 | 264 |
|
1913 | 265 |
goal thy "H <= analz(H)"; |
1839 | 266 |
by (Fast_tac 1); |
1913 | 267 |
qed "analz_increasing"; |
1839 | 268 |
|
1913 | 269 |
goal thy "analz H <= parts H"; |
1839 | 270 |
by (rtac subsetI 1); |
1913 | 271 |
be analz.induct 1; |
1839 | 272 |
by (ALLGOALS Fast_tac); |
1913 | 273 |
qed "analz_subset_parts"; |
1839 | 274 |
|
1913 | 275 |
bind_thm ("not_parts_not_analz", analz_subset_parts RS contra_subsetD); |
1839 | 276 |
|
277 |
||
1913 | 278 |
goal thy "parts (analz H) = parts H"; |
1839 | 279 |
br equalityI 1; |
1913 | 280 |
br (analz_subset_parts RS parts_mono RS subset_trans) 1; |
1839 | 281 |
by (Simp_tac 1); |
1913 | 282 |
by (fast_tac (!claset addDs [analz_increasing RS parts_mono RS subsetD]) 1); |
283 |
qed "parts_analz"; |
|
284 |
Addsimps [parts_analz]; |
|
1839 | 285 |
|
1913 | 286 |
goal thy "analz (parts H) = parts H"; |
1885 | 287 |
by (Auto_tac()); |
1913 | 288 |
be analz.induct 1; |
1885 | 289 |
by (Auto_tac()); |
1913 | 290 |
qed "analz_parts"; |
291 |
Addsimps [analz_parts]; |
|
1885 | 292 |
|
1839 | 293 |
(*Monotonicity; Lemma 1 of Lowe*) |
1913 | 294 |
goalw thy analz.defs "!!G H. G<=H ==> analz(G) <= analz(H)"; |
1839 | 295 |
by (rtac lfp_mono 1); |
296 |
by (REPEAT (ares_tac basic_monos 1)); |
|
1913 | 297 |
qed "analz_mono"; |
1839 | 298 |
|
299 |
(** General equational properties **) |
|
300 |
||
1913 | 301 |
goal thy "analz{} = {}"; |
1839 | 302 |
by (Step_tac 1); |
1913 | 303 |
be analz.induct 1; |
1839 | 304 |
by (ALLGOALS Fast_tac); |
1913 | 305 |
qed "analz_empty"; |
306 |
Addsimps [analz_empty]; |
|
1839 | 307 |
|
1913 | 308 |
(*Converse fails: we can analz more from the union than from the |
1839 | 309 |
separate parts, as a key in one might decrypt a message in the other*) |
1913 | 310 |
goal thy "analz(G) Un analz(H) <= analz(G Un H)"; |
311 |
by (REPEAT (ares_tac [Un_least, analz_mono, Un_upper1, Un_upper2] 1)); |
|
312 |
qed "analz_Un"; |
|
1839 | 313 |
|
1913 | 314 |
goal thy "insert X (analz H) <= analz(insert X H)"; |
315 |
by (fast_tac (!claset addEs [impOfSubs analz_mono]) 1); |
|
316 |
qed "analz_insert"; |
|
1839 | 317 |
|
318 |
(** Rewrite rules for pulling out atomic messages **) |
|
319 |
||
1913 | 320 |
goal thy "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"; |
321 |
by (rtac (analz_insert RSN (2, equalityI)) 1); |
|
1839 | 322 |
br subsetI 1; |
1913 | 323 |
be analz.induct 1; |
1839 | 324 |
(*Simplification breaks up equalities between messages; |
325 |
how to make it work for fast_tac??*) |
|
326 |
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); |
|
1913 | 327 |
qed "analz_insert_Agent"; |
1839 | 328 |
|
1913 | 329 |
goal thy "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"; |
330 |
by (rtac (analz_insert RSN (2, equalityI)) 1); |
|
1839 | 331 |
br subsetI 1; |
1913 | 332 |
be analz.induct 1; |
1839 | 333 |
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); |
1913 | 334 |
qed "analz_insert_Nonce"; |
1839 | 335 |
|
336 |
(*Can only pull out Keys if they are not needed to decrypt the rest*) |
|
337 |
goalw thy [keysFor_def] |
|
1913 | 338 |
"!!K. K ~: keysFor (analz H) ==> \ |
339 |
\ analz (insert (Key K) H) = insert (Key K) (analz H)"; |
|
340 |
by (rtac (analz_insert RSN (2, equalityI)) 1); |
|
1839 | 341 |
br subsetI 1; |
1913 | 342 |
be analz.induct 1; |
1839 | 343 |
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); |
1913 | 344 |
qed "analz_insert_Key"; |
1839 | 345 |
|
1913 | 346 |
goal thy "analz (insert {|X,Y|} H) = \ |
347 |
\ insert {|X,Y|} (analz (insert X (insert Y H)))"; |
|
1885 | 348 |
br equalityI 1; |
349 |
br subsetI 1; |
|
1913 | 350 |
be analz.induct 1; |
1885 | 351 |
by (Auto_tac()); |
1913 | 352 |
be analz.induct 1; |
353 |
by (ALLGOALS (deepen_tac (!claset addIs [analz.Fst, analz.Snd, analz.Decrypt]) 0)); |
|
354 |
qed "analz_insert_MPair"; |
|
1885 | 355 |
|
356 |
(*Can pull out enCrypted message if the Key is not known*) |
|
1913 | 357 |
goal thy "!!H. Key (invKey K) ~: analz H ==> \ |
358 |
\ analz (insert (Crypt X K) H) = \ |
|
359 |
\ insert (Crypt X K) (analz H)"; |
|
360 |
by (rtac (analz_insert RSN (2, equalityI)) 1); |
|
1839 | 361 |
br subsetI 1; |
1913 | 362 |
be analz.induct 1; |
1839 | 363 |
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); |
1913 | 364 |
qed "analz_insert_Crypt"; |
1839 | 365 |
|
1913 | 366 |
goal thy "!!H. Key (invKey K) : analz H ==> \ |
367 |
\ analz (insert (Crypt X K) H) <= \ |
|
368 |
\ insert (Crypt X K) (analz (insert X H))"; |
|
1839 | 369 |
br subsetI 1; |
1913 | 370 |
by (eres_inst_tac [("za","x")] analz.induct 1); |
1839 | 371 |
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); |
372 |
val lemma1 = result(); |
|
373 |
||
1913 | 374 |
goal thy "!!H. Key (invKey K) : analz H ==> \ |
375 |
\ insert (Crypt X K) (analz (insert X H)) <= \ |
|
376 |
\ analz (insert (Crypt X K) H)"; |
|
1839 | 377 |
by (Auto_tac()); |
1913 | 378 |
by (eres_inst_tac [("za","x")] analz.induct 1); |
1839 | 379 |
by (Auto_tac()); |
1913 | 380 |
by (best_tac (!claset addIs [subset_insertI RS analz_mono RS subsetD, |
381 |
analz.Decrypt]) 1); |
|
1839 | 382 |
val lemma2 = result(); |
383 |
||
1913 | 384 |
goal thy "!!H. Key (invKey K) : analz H ==> \ |
385 |
\ analz (insert (Crypt X K) H) = \ |
|
386 |
\ insert (Crypt X K) (analz (insert X H))"; |
|
1839 | 387 |
by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1)); |
1913 | 388 |
qed "analz_insert_Decrypt"; |
1839 | 389 |
|
1885 | 390 |
(*Case analysis: either the message is secure, or it is not! |
391 |
Use with expand_if; apparently split_tac does not cope with patterns |
|
1913 | 392 |
such as "analz (insert (Crypt X' K) H)" *) |
393 |
goal thy "analz (insert (Crypt X' K) H) = \ |
|
394 |
\ (if (Key (invKey K) : analz H) then \ |
|
395 |
\ insert (Crypt X' K) (analz (insert X' H)) \ |
|
396 |
\ else insert (Crypt X' K) (analz H))"; |
|
397 |
by (excluded_middle_tac "Key (invKey K) : analz H " 1); |
|
398 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps [analz_insert_Crypt, |
|
399 |
analz_insert_Decrypt]))); |
|
400 |
qed "analz_Crypt_if"; |
|
1885 | 401 |
|
1913 | 402 |
Addsimps [analz_insert_Agent, analz_insert_Nonce, |
403 |
analz_insert_Key, analz_insert_MPair, |
|
404 |
analz_Crypt_if]; |
|
1839 | 405 |
|
406 |
(*This rule supposes "for the sake of argument" that we have the key.*) |
|
1913 | 407 |
goal thy "analz (insert (Crypt X K) H) <= \ |
408 |
\ insert (Crypt X K) (analz (insert X H))"; |
|
1839 | 409 |
br subsetI 1; |
1913 | 410 |
be analz.induct 1; |
1839 | 411 |
by (Auto_tac()); |
1913 | 412 |
qed "analz_insert_Crypt_subset"; |
1839 | 413 |
|
414 |
||
415 |
(** Idempotence and transitivity **) |
|
416 |
||
1913 | 417 |
goal thy "!!H. X: analz (analz H) ==> X: analz H"; |
418 |
be analz.induct 1; |
|
1839 | 419 |
by (ALLGOALS Fast_tac); |
1913 | 420 |
qed "analz_analzE"; |
421 |
AddSEs [analz_analzE]; |
|
1839 | 422 |
|
1913 | 423 |
goal thy "analz (analz H) = analz H"; |
1839 | 424 |
by (Fast_tac 1); |
1913 | 425 |
qed "analz_idem"; |
426 |
Addsimps [analz_idem]; |
|
1839 | 427 |
|
1913 | 428 |
goal thy "!!H. [| X: analz G; G <= analz H |] ==> X: analz H"; |
429 |
by (dtac analz_mono 1); |
|
1839 | 430 |
by (Fast_tac 1); |
1913 | 431 |
qed "analz_trans"; |
1839 | 432 |
|
433 |
(*Cut; Lemma 2 of Lowe*) |
|
1913 | 434 |
goal thy "!!H. [| X: analz H; Y: analz (insert X H) |] ==> Y: analz H"; |
435 |
be analz_trans 1; |
|
1839 | 436 |
by (Fast_tac 1); |
1913 | 437 |
qed "analz_cut"; |
1839 | 438 |
|
439 |
(*Cut can be proved easily by induction on |
|
1913 | 440 |
"!!H. Y: analz (insert X H) ==> X: analz H --> Y: analz H" |
1839 | 441 |
*) |
442 |
||
1885 | 443 |
|
1913 | 444 |
(** A congruence rule for "analz" **) |
1885 | 445 |
|
1913 | 446 |
goal thy "!!H. [| analz G <= analz G'; analz H <= analz H' \ |
447 |
\ |] ==> analz (G Un H) <= analz (G' Un H')"; |
|
1885 | 448 |
by (Step_tac 1); |
1913 | 449 |
be analz.induct 1; |
450 |
by (ALLGOALS (best_tac (!claset addIs [analz_mono RS subsetD]))); |
|
451 |
qed "analz_subset_cong"; |
|
1885 | 452 |
|
1913 | 453 |
goal thy "!!H. [| analz G = analz G'; analz H = analz H' \ |
454 |
\ |] ==> analz (G Un H) = analz (G' Un H')"; |
|
455 |
by (REPEAT_FIRST (ares_tac [equalityI, analz_subset_cong] |
|
1885 | 456 |
ORELSE' etac equalityE)); |
1913 | 457 |
qed "analz_cong"; |
1885 | 458 |
|
459 |
||
1913 | 460 |
goal thy "!!H. analz H = analz H' ==> analz(insert X H) = analz(insert X H')"; |
1885 | 461 |
by (asm_simp_tac (!simpset addsimps [insert_def] |
1913 | 462 |
setloop (rtac analz_cong)) 1); |
463 |
qed "analz_insert_cong"; |
|
1885 | 464 |
|
1913 | 465 |
(*If there are no pairs or encryptions then analz does nothing*) |
1839 | 466 |
goal thy "!!H. [| ALL X Y. {|X,Y|} ~: H; ALL X K. Crypt X K ~: H |] ==> \ |
1913 | 467 |
\ analz H = H"; |
1839 | 468 |
by (Step_tac 1); |
1913 | 469 |
be analz.induct 1; |
1839 | 470 |
by (ALLGOALS Fast_tac); |
1913 | 471 |
qed "analz_trivial"; |
1839 | 472 |
|
473 |
(*Helps to prove Fake cases*) |
|
1913 | 474 |
goal thy "!!X. X: analz (UN i. analz (H i)) ==> X: analz (UN i. H i)"; |
475 |
be analz.induct 1; |
|
476 |
by (ALLGOALS (fast_tac (!claset addEs [impOfSubs analz_mono]))); |
|
1839 | 477 |
val lemma = result(); |
478 |
||
1913 | 479 |
goal thy "analz (UN i. analz (H i)) = analz (UN i. H i)"; |
1839 | 480 |
by (fast_tac (!claset addIs [lemma] |
1913 | 481 |
addEs [impOfSubs analz_mono]) 1); |
482 |
qed "analz_UN_analz"; |
|
483 |
Addsimps [analz_UN_analz]; |
|
1839 | 484 |
|
485 |
||
1913 | 486 |
(**** Inductive relation "synth" ****) |
1839 | 487 |
|
1913 | 488 |
AddIs synth.intrs; |
1839 | 489 |
|
1913 | 490 |
goal thy "H <= synth(H)"; |
1839 | 491 |
by (Fast_tac 1); |
1913 | 492 |
qed "synth_increasing"; |
1839 | 493 |
|
494 |
(*Monotonicity*) |
|
1913 | 495 |
goalw thy synth.defs "!!G H. G<=H ==> synth(G) <= synth(H)"; |
1839 | 496 |
by (rtac lfp_mono 1); |
497 |
by (REPEAT (ares_tac basic_monos 1)); |
|
1913 | 498 |
qed "synth_mono"; |
1839 | 499 |
|
500 |
(** Unions **) |
|
501 |
||
1913 | 502 |
(*Converse fails: we can synth more from the union than from the |
1839 | 503 |
separate parts, building a compound message using elements of each.*) |
1913 | 504 |
goal thy "synth(G) Un synth(H) <= synth(G Un H)"; |
505 |
by (REPEAT (ares_tac [Un_least, synth_mono, Un_upper1, Un_upper2] 1)); |
|
506 |
qed "synth_Un"; |
|
1839 | 507 |
|
1913 | 508 |
goal thy "insert X (synth H) <= synth(insert X H)"; |
509 |
by (fast_tac (!claset addEs [impOfSubs synth_mono]) 1); |
|
510 |
qed "synth_insert"; |
|
1885 | 511 |
|
1839 | 512 |
(** Idempotence and transitivity **) |
513 |
||
1913 | 514 |
goal thy "!!H. X: synth (synth H) ==> X: synth H"; |
515 |
be synth.induct 1; |
|
1839 | 516 |
by (ALLGOALS Fast_tac); |
1913 | 517 |
qed "synth_synthE"; |
518 |
AddSEs [synth_synthE]; |
|
1839 | 519 |
|
1913 | 520 |
goal thy "synth (synth H) = synth H"; |
1839 | 521 |
by (Fast_tac 1); |
1913 | 522 |
qed "synth_idem"; |
1839 | 523 |
|
1913 | 524 |
goal thy "!!H. [| X: synth G; G <= synth H |] ==> X: synth H"; |
525 |
by (dtac synth_mono 1); |
|
1839 | 526 |
by (Fast_tac 1); |
1913 | 527 |
qed "synth_trans"; |
1839 | 528 |
|
529 |
(*Cut; Lemma 2 of Lowe*) |
|
1913 | 530 |
goal thy "!!H. [| X: synth H; Y: synth (insert X H) |] ==> Y: synth H"; |
531 |
be synth_trans 1; |
|
1839 | 532 |
by (Fast_tac 1); |
1913 | 533 |
qed "synth_cut"; |
1839 | 534 |
|
535 |
||
536 |
(*Can only produce a nonce or key if it is already known, |
|
1913 | 537 |
but can synth a pair or encryption from its components...*) |
538 |
val mk_cases = synth.mk_cases msg.simps; |
|
1839 | 539 |
|
1913 | 540 |
(*NO Agent_synth, as any Agent name can be synthd*) |
541 |
val Nonce_synth = mk_cases "Nonce n : synth H"; |
|
542 |
val Key_synth = mk_cases "Key K : synth H"; |
|
543 |
val MPair_synth = mk_cases "{|X,Y|} : synth H"; |
|
544 |
val Crypt_synth = mk_cases "Crypt X K : synth H"; |
|
1839 | 545 |
|
1913 | 546 |
AddSEs [Nonce_synth, Key_synth, MPair_synth, Crypt_synth]; |
1839 | 547 |
|
1913 | 548 |
goal thy "(Nonce N : synth H) = (Nonce N : H)"; |
1839 | 549 |
by (Fast_tac 1); |
1913 | 550 |
qed "Nonce_synth_eq"; |
1839 | 551 |
|
1913 | 552 |
goal thy "(Key K : synth H) = (Key K : H)"; |
1839 | 553 |
by (Fast_tac 1); |
1913 | 554 |
qed "Key_synth_eq"; |
1839 | 555 |
|
1913 | 556 |
Addsimps [Nonce_synth_eq, Key_synth_eq]; |
1839 | 557 |
|
558 |
||
559 |
goalw thy [keysFor_def] |
|
1913 | 560 |
"keysFor (synth H) = keysFor H Un invKey``{K. Key K : H}"; |
1839 | 561 |
by (Fast_tac 1); |
1913 | 562 |
qed "keysFor_synth"; |
563 |
Addsimps [keysFor_synth]; |
|
1839 | 564 |
|
565 |
||
1913 | 566 |
(*** Combinations of parts, analz and synth ***) |
1839 | 567 |
|
1913 | 568 |
goal thy "parts (synth H) = parts H Un synth H"; |
1839 | 569 |
br equalityI 1; |
570 |
br subsetI 1; |
|
571 |
be parts.induct 1; |
|
572 |
by (ALLGOALS |
|
1913 | 573 |
(best_tac (!claset addIs ((synth_increasing RS parts_mono RS subsetD) |
1839 | 574 |
::parts.intrs)))); |
1913 | 575 |
qed "parts_synth"; |
576 |
Addsimps [parts_synth]; |
|
1839 | 577 |
|
1913 | 578 |
goal thy "analz (synth H) = analz H Un synth H"; |
1839 | 579 |
br equalityI 1; |
580 |
br subsetI 1; |
|
1913 | 581 |
be analz.induct 1; |
1839 | 582 |
by (best_tac |
1913 | 583 |
(!claset addIs [synth_increasing RS analz_mono RS subsetD]) 5); |
1839 | 584 |
(*Strange that best_tac just can't hack this one...*) |
1913 | 585 |
by (ALLGOALS (deepen_tac (!claset addIs analz.intrs) 0)); |
586 |
qed "analz_synth"; |
|
587 |
Addsimps [analz_synth]; |
|
1839 | 588 |
|
589 |
(*Hard to prove; still needed now that there's only one Enemy?*) |
|
1913 | 590 |
goal thy "analz (UN i. synth (H i)) = \ |
591 |
\ analz (UN i. H i) Un (UN i. synth (H i))"; |
|
1839 | 592 |
br equalityI 1; |
593 |
br subsetI 1; |
|
1913 | 594 |
be analz.induct 1; |
1839 | 595 |
by (best_tac |
1913 | 596 |
(!claset addEs [impOfSubs synth_increasing, |
597 |
impOfSubs analz_mono]) 5); |
|
1839 | 598 |
by (Best_tac 1); |
1913 | 599 |
by (deepen_tac (!claset addIs [analz.Fst]) 0 1); |
600 |
by (deepen_tac (!claset addIs [analz.Snd]) 0 1); |
|
601 |
by (deepen_tac (!claset addSEs [analz.Decrypt] |
|
602 |
addIs [analz.Decrypt]) 0 1); |
|
603 |
qed "analz_UN1_synth"; |
|
604 |
Addsimps [analz_UN1_synth]; |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
605 |
|
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
606 |
(*Especially for reasoning about the Fake rule in traces*) |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
607 |
goal thy "!!Y. X: G ==> parts(insert X H) <= parts G Un parts H"; |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
608 |
br ([parts_mono, parts_Un_subset2] MRS subset_trans) 1; |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
609 |
by (Fast_tac 1); |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
610 |
qed "parts_insert_subset_Un"; |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
611 |
|
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
612 |
(*Also for the Fake rule, but more specific*) |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
613 |
goal thy "!!H. X: synth (analz H) ==> \ |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
614 |
\ parts (insert X H) <= synth (analz H) Un parts H"; |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
615 |
bd parts_insert_subset_Un 1; |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
616 |
by (Full_simp_tac 1); |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
617 |
by (Fast_tac 1); |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
618 |
qed "synth_analz_parts_insert_subset_Un"; |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
619 |
|
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
620 |
|
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
621 |
|
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
622 |
(*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
|
623 |
Delrules partsEs; |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
624 |