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