author | paulson |
Thu, 26 Sep 1996 12:50:48 +0200 | |
changeset 2032 | 1bbf1bdcaf56 |
parent 1942 | 6c9c1a42a869 |
child 2134 | 04a71407089d |
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 |
Datatype of events; |
|
7 |
inductive relation "traces" for Needham-Schroeder (shared keys) |
|
1852 | 8 |
|
2032 | 9 |
Rewrites should not refer to initState (Friend i) -- not in normal form |
1839 | 10 |
*) |
11 |
||
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
12 |
Addsimps [parts_cut_eq]; |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
13 |
|
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
14 |
|
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
15 |
(*INSTALLED ON NAT.ML*) |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
16 |
goalw Nat.thy [le_def] "(m <= n) = (m < Suc n)"; |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
17 |
by (rtac not_less_eq 1); |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
18 |
qed "le_eq_less_Suc"; |
1839 | 19 |
|
1885 | 20 |
proof_timing:=true; |
21 |
||
22 |
(*FOR LIST.ML??*) |
|
1913 | 23 |
goal List.thy "x : set_of_list (x#xs)"; |
1885 | 24 |
by (Simp_tac 1); |
1913 | 25 |
qed "set_of_list_I1"; |
1885 | 26 |
|
1913 | 27 |
goal List.thy "!!x. xs = x#xs' ==> x : set_of_list xs"; |
1885 | 28 |
by (Asm_simp_tac 1); |
1913 | 29 |
qed "set_of_list_eqI1"; |
1885 | 30 |
|
1913 | 31 |
(*FUN.ML?? WE NEED A NOTION OF INVERSE IMAGE, OR GRAPH!!*) |
1885 | 32 |
goal Set.thy "!!f. B <= range f = (B = f`` {x. f x: B})"; |
33 |
by (fast_tac (!claset addEs [equalityE]) 1); |
|
34 |
val subset_range_iff = result(); |
|
35 |
||
36 |
||
1839 | 37 |
open Event; |
38 |
||
1885 | 39 |
Addsimps [Un_insert_left, Un_insert_right]; |
40 |
||
41 |
(*By default only o_apply is built-in. But in the presence of eta-expansion |
|
42 |
this means that some terms displayed as (f o g) will be rewritten, and others |
|
43 |
will not!*) |
|
44 |
Addsimps [o_def]; |
|
1852 | 45 |
|
1942 | 46 |
(*** Basic properties of shrK and newK ***) |
1852 | 47 |
|
1942 | 48 |
(* invKey (shrK A) = shrK A *) |
49 |
bind_thm ("invKey_shrK", rewrite_rule [isSymKey_def] isSym_shrK); |
|
1839 | 50 |
|
1852 | 51 |
(* invKey (newK evs) = newK evs *) |
1839 | 52 |
bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK); |
1942 | 53 |
Addsimps [invKey_shrK, invKey_newK]; |
1839 | 54 |
|
55 |
||
56 |
(*New keys and nonces are fresh*) |
|
1942 | 57 |
val shrK_inject = inj_shrK RS injD; |
1852 | 58 |
val newN_inject = inj_newN RS injD |
59 |
and newK_inject = inj_newK RS injD; |
|
1942 | 60 |
AddSEs [shrK_inject, newN_inject, newK_inject, |
2032 | 61 |
fresh_newK RS notE, fresh_newN RS notE]; |
1942 | 62 |
Addsimps [inj_shrK RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq]; |
1839 | 63 |
Addsimps [fresh_newN, fresh_newK]; |
64 |
||
1942 | 65 |
goal thy "newK evs ~= shrK B"; |
66 |
by (subgoal_tac "newK evs = shrK B --> \ |
|
1852 | 67 |
\ Key (newK evs) : parts (initState B)" 1); |
1839 | 68 |
by (Fast_tac 1); |
69 |
by (agent.induct_tac "B" 1); |
|
70 |
by (auto_tac (!claset addIs [range_eqI], !simpset)); |
|
1942 | 71 |
qed "newK_neq_shrK"; |
1839 | 72 |
|
1942 | 73 |
Addsimps [newK_neq_shrK, newK_neq_shrK RS not_sym]; |
1839 | 74 |
|
75 |
(*Good for talking about Server's initial state*) |
|
1885 | 76 |
goal thy "!!H. H <= Key``E ==> parts H = H"; |
77 |
by (Auto_tac ()); |
|
2032 | 78 |
by (etac parts.induct 1); |
1839 | 79 |
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); |
1885 | 80 |
qed "parts_image_subset"; |
1839 | 81 |
|
1885 | 82 |
bind_thm ("parts_image_Key", subset_refl RS parts_image_subset); |
83 |
||
1913 | 84 |
goal thy "!!H. H <= Key``E ==> analz H = H"; |
1885 | 85 |
by (Auto_tac ()); |
2032 | 86 |
by (etac analz.induct 1); |
1839 | 87 |
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); |
1913 | 88 |
qed "analz_image_subset"; |
1839 | 89 |
|
1913 | 90 |
bind_thm ("analz_image_Key", subset_refl RS analz_image_subset); |
1885 | 91 |
|
1913 | 92 |
Addsimps [parts_image_Key, analz_image_Key]; |
1839 | 93 |
|
94 |
goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}"; |
|
95 |
by (agent.induct_tac "C" 1); |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
96 |
by (auto_tac (!claset addIs [range_eqI] delrules partsEs, !simpset)); |
1839 | 97 |
qed "keysFor_parts_initState"; |
98 |
Addsimps [keysFor_parts_initState]; |
|
99 |
||
1885 | 100 |
goalw thy [keysFor_def] "keysFor (Key``E) = {}"; |
101 |
by (Auto_tac ()); |
|
102 |
qed "keysFor_image_Key"; |
|
103 |
Addsimps [keysFor_image_Key]; |
|
104 |
||
1942 | 105 |
goal thy "shrK A ~: newK``E"; |
1885 | 106 |
by (agent.induct_tac "A" 1); |
107 |
by (Auto_tac ()); |
|
1942 | 108 |
qed "shrK_notin_image_newK"; |
109 |
Addsimps [shrK_notin_image_newK]; |
|
1885 | 110 |
|
111 |
||
1942 | 112 |
(*Agents see their own shrKs!*) |
113 |
goal thy "Key (shrK A) : analz (sees A evs)"; |
|
1885 | 114 |
by (list.induct_tac "evs" 1); |
1913 | 115 |
by (asm_simp_tac (!simpset addsimps [impOfSubs(Un_upper2 RS analz_mono)]) 2); |
1885 | 116 |
by (agent.induct_tac "A" 1); |
117 |
by (auto_tac (!claset addIs [range_eqI], !simpset)); |
|
1942 | 118 |
qed "analz_own_shrK"; |
1885 | 119 |
|
1942 | 120 |
bind_thm ("parts_own_shrK", |
2032 | 121 |
[analz_subset_parts, analz_own_shrK] MRS subsetD); |
1885 | 122 |
|
1942 | 123 |
Addsimps [analz_own_shrK, parts_own_shrK]; |
1885 | 124 |
|
125 |
||
1839 | 126 |
|
127 |
(**** Inductive relation "traces" -- basic properties ****) |
|
128 |
||
129 |
val mk_cases = traces.mk_cases (list.simps @ agent.simps @ event.simps); |
|
130 |
||
131 |
val Says_tracesE = mk_cases "Says A B X # evs: traces"; |
|
132 |
val Says_Server_tracesE = mk_cases "Says Server B X # evs: traces"; |
|
2032 | 133 |
val Says_Spy_tracesE = mk_cases "Says Spy B X # evs: traces"; |
1839 | 134 |
val Says_to_Server_tracesE = mk_cases "Says A Server X # evs: traces"; |
135 |
val Notes_tracesE = mk_cases "Notes A X # evs: traces"; |
|
136 |
||
137 |
(*The tail of a trace is a trace*) |
|
138 |
goal thy "!!ev evs. ev#evs : traces ==> evs : traces"; |
|
139 |
by (fast_tac (!claset addEs [mk_cases "ev#evs:traces"]) 1); |
|
140 |
qed "traces_ConsE"; |
|
141 |
||
1885 | 142 |
goal thy "!!ev evs. [| evs = ev#evs'; evs : traces |] ==> evs' : traces"; |
143 |
by (fast_tac (!claset addEs [mk_cases "ev#evs:traces"]) 1); |
|
144 |
qed "traces_eq_ConsE"; |
|
145 |
||
146 |
||
1839 | 147 |
(** Specialized rewrite rules for (sees A (Says...#evs)) **) |
148 |
||
149 |
goal thy "sees A (Says A B X # evs) = insert X (sees A evs)"; |
|
150 |
by (Simp_tac 1); |
|
151 |
qed "sees_own"; |
|
152 |
||
153 |
goal thy "!!A. Server ~= A ==> \ |
|
154 |
\ sees Server (Says A B X # evs) = sees Server evs"; |
|
155 |
by (Asm_simp_tac 1); |
|
156 |
qed "sees_Server"; |
|
157 |
||
158 |
goal thy "!!A. Friend i ~= A ==> \ |
|
159 |
\ sees (Friend i) (Says A B X # evs) = sees (Friend i) evs"; |
|
160 |
by (Asm_simp_tac 1); |
|
161 |
qed "sees_Friend"; |
|
162 |
||
2032 | 163 |
goal thy "sees Spy (Says A B X # evs) = insert X (sees Spy evs)"; |
1839 | 164 |
by (Simp_tac 1); |
2032 | 165 |
qed "sees_Spy"; |
1839 | 166 |
|
167 |
goal thy "sees A (Says A' B X # evs) <= insert X (sees A evs)"; |
|
168 |
by (simp_tac (!simpset setloop split_tac [expand_if]) 1); |
|
169 |
by (Fast_tac 1); |
|
1852 | 170 |
qed "sees_Says_subset_insert"; |
171 |
||
172 |
goal thy "sees A evs <= sees A (Says A' B X # evs)"; |
|
173 |
by (simp_tac (!simpset setloop split_tac [expand_if]) 1); |
|
174 |
by (Fast_tac 1); |
|
175 |
qed "sees_subset_sees_Says"; |
|
1839 | 176 |
|
177 |
(*Pushing Unions into parts; one of the A's equals B, and thus sees Y*) |
|
178 |
goal thy "(UN A. parts (sees A (Says B C Y # evs))) = \ |
|
179 |
\ parts {Y} Un (UN A. parts (sees A evs))"; |
|
180 |
by (Step_tac 1); |
|
2032 | 181 |
by (etac rev_mp 1); (*for some reason, split_tac does not work on assumptions*) |
1839 | 182 |
val ss = (!simpset addsimps [parts_Un, sees_Cons] |
2032 | 183 |
setloop split_tac [expand_if]); |
1839 | 184 |
by (ALLGOALS (fast_tac (!claset addss ss))); |
185 |
qed "UN_parts_sees_Says"; |
|
186 |
||
2032 | 187 |
goal thy "Says A B X : set_of_list evs --> X : sees Spy evs"; |
1885 | 188 |
by (list.induct_tac "evs" 1); |
189 |
by (Auto_tac ()); |
|
2032 | 190 |
qed_spec_mp "Says_imp_sees_Spy"; |
1885 | 191 |
|
2032 | 192 |
Addsimps [Says_imp_sees_Spy]; |
193 |
AddIs [Says_imp_sees_Spy]; |
|
1839 | 194 |
|
1942 | 195 |
goal thy "initState C <= Key `` range shrK"; |
1893 | 196 |
by (agent.induct_tac "C" 1); |
197 |
by (Auto_tac ()); |
|
198 |
qed "initState_subset"; |
|
199 |
||
200 |
goal thy "X : sees C evs --> \ |
|
1913 | 201 |
\ (EX A B. Says A B X : set_of_list evs) | \ |
202 |
\ (EX A. Notes A X : set_of_list evs) | \ |
|
1942 | 203 |
\ (EX A. X = Key (shrK A))"; |
1893 | 204 |
by (list.induct_tac "evs" 1); |
205 |
by (ALLGOALS Asm_simp_tac); |
|
206 |
by (fast_tac (!claset addDs [impOfSubs initState_subset]) 1); |
|
2032 | 207 |
by (rtac conjI 1); |
1893 | 208 |
by (Fast_tac 2); |
209 |
by (event.induct_tac "a" 1); |
|
210 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps [mem_if]))); |
|
211 |
by (ALLGOALS Fast_tac); |
|
212 |
qed_spec_mp "seesD"; |
|
213 |
||
214 |
||
2032 | 215 |
Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Spy]; |
216 |
Delsimps [sees_Cons]; (**** NOTE REMOVAL -- laws above are cleaner ****) |
|
1839 | 217 |
|
218 |
||
219 |
(**** Inductive proofs about traces ****) |
|
220 |
||
2032 | 221 |
(*The Spy can see more than anybody else, except for their initial state*) |
1839 | 222 |
goal thy |
223 |
"!!evs. evs : traces ==> \ |
|
2032 | 224 |
\ sees A evs <= initState A Un sees Spy evs"; |
225 |
by (etac traces.induct 1); |
|
1852 | 226 |
by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] |
2032 | 227 |
addss (!simpset)))); |
228 |
qed "sees_agent_subset_sees_Spy"; |
|
1839 | 229 |
|
230 |
||
1885 | 231 |
(*Nobody sends themselves messages*) |
1913 | 232 |
goal thy "!!evs. evs : traces ==> ALL A X. Says A A X ~: set_of_list evs"; |
2032 | 233 |
by (etac traces.induct 1); |
1852 | 234 |
by (Auto_tac()); |
235 |
qed_spec_mp "not_Says_to_self"; |
|
236 |
Addsimps [not_Says_to_self]; |
|
237 |
AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
|
238 |
||
1913 | 239 |
goal thy "!!evs. evs : traces ==> Notes A X ~: set_of_list evs"; |
2032 | 240 |
by (etac traces.induct 1); |
1893 | 241 |
by (Auto_tac()); |
242 |
qed "not_Notes"; |
|
243 |
Addsimps [not_Notes]; |
|
244 |
AddSEs [not_Notes RSN (2, rev_notE)]; |
|
245 |
||
1852 | 246 |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
247 |
goal thy "!!evs. (Says S A (Crypt {|N, B, K, X|} KA)) : set_of_list evs ==> \ |
2032 | 248 |
\ X : parts (sees Spy evs)"; |
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
249 |
by (fast_tac (!claset addSEs partsEs |
2032 | 250 |
addSDs [Says_imp_sees_Spy RS parts.Inj]) 1); |
251 |
qed "NS3_msg_in_parts_sees_Spy"; |
|
252 |
||
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
253 |
|
1839 | 254 |
(*** Server keys are not betrayed ***) |
255 |
||
2032 | 256 |
(*Spy never sees another agent's server key!*) |
1839 | 257 |
goal thy |
2032 | 258 |
"!!evs. [| evs : traces; A ~= Spy |] ==> \ |
259 |
\ Key (shrK A) ~: parts (sees Spy evs)"; |
|
260 |
by (etac traces.induct 1); |
|
261 |
by (dtac NS3_msg_in_parts_sees_Spy 5); |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
262 |
by (Auto_tac()); |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
263 |
(*Deals with Fake message*) |
1913 | 264 |
by (best_tac (!claset addDs [impOfSubs analz_subset_parts, |
2032 | 265 |
impOfSubs synth_analz_parts_insert_subset_Un]) 1); |
266 |
qed "Spy_not_see_shrK"; |
|
1839 | 267 |
|
2032 | 268 |
bind_thm ("Spy_not_analz_shrK", |
269 |
[analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD); |
|
1852 | 270 |
|
2032 | 271 |
Addsimps [Spy_not_see_shrK, |
272 |
not_sym RSN (2, Spy_not_see_shrK), |
|
273 |
Spy_not_analz_shrK, |
|
274 |
not_sym RSN (2, Spy_not_analz_shrK)]; |
|
1852 | 275 |
|
1893 | 276 |
(*We go to some trouble to preserve R in the 3rd subgoal*) |
277 |
val major::prems = |
|
2032 | 278 |
goal thy "[| Key (shrK A) : parts (sees Spy evs); \ |
1893 | 279 |
\ evs : traces; \ |
2032 | 280 |
\ A=Spy ==> R \ |
1893 | 281 |
\ |] ==> R"; |
2032 | 282 |
by (rtac ccontr 1); |
283 |
by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1); |
|
1893 | 284 |
by (swap_res_tac prems 2); |
285 |
by (ALLGOALS (fast_tac (!claset addIs prems))); |
|
2032 | 286 |
qed "Spy_see_shrK_E"; |
1893 | 287 |
|
2032 | 288 |
bind_thm ("Spy_analz_shrK_E", |
289 |
analz_subset_parts RS subsetD RS Spy_see_shrK_E); |
|
1893 | 290 |
|
291 |
(*Classical reasoner doesn't need the not_sym versions (with swapped ~=) *) |
|
2032 | 292 |
AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E]; |
1893 | 293 |
|
1839 | 294 |
|
1852 | 295 |
(*No Friend will ever see another agent's server key |
2032 | 296 |
(excluding the Spy, who might transmit his). |
1885 | 297 |
The Server, of course, knows all server keys.*) |
1839 | 298 |
goal thy |
2032 | 299 |
"!!evs. [| evs : traces; A ~= Spy; A ~= Friend j |] ==> \ |
1942 | 300 |
\ Key (shrK A) ~: parts (sees (Friend j) evs)"; |
2032 | 301 |
by (rtac (sees_agent_subset_sees_Spy RS parts_mono RS contra_subsetD) 1); |
1852 | 302 |
by (ALLGOALS Asm_simp_tac); |
1942 | 303 |
qed "Friend_not_see_shrK"; |
1839 | 304 |
|
305 |
||
1885 | 306 |
(*Not for Addsimps -- it can cause goals to blow up!*) |
307 |
goal thy |
|
308 |
"!!evs. evs : traces ==> \ |
|
1942 | 309 |
\ (Key (shrK A) \ |
2032 | 310 |
\ : analz (insert (Key (shrK B)) (sees Spy evs))) = \ |
311 |
\ (A=B | A=Spy)"; |
|
1913 | 312 |
by (best_tac (!claset addDs [impOfSubs analz_subset_parts] |
2032 | 313 |
addIs [impOfSubs (subset_insertI RS analz_mono)] |
314 |
addss (!simpset)) 1); |
|
1942 | 315 |
qed "shrK_mem_analz"; |
1885 | 316 |
|
317 |
||
318 |
||
319 |
||
1839 | 320 |
(*** Future keys can't be seen or used! ***) |
321 |
||
322 |
(*Nobody can have SEEN keys that will be generated in the future. |
|
323 |
This has to be proved anew for each protocol description, |
|
324 |
but should go by similar reasoning every time. Hardest case is the |
|
325 |
standard Fake rule. |
|
326 |
The length comparison, and Union over C, are essential for the |
|
327 |
induction! *) |
|
328 |
goal thy "!!evs. evs : traces ==> \ |
|
329 |
\ length evs <= length evs' --> \ |
|
1852 | 330 |
\ Key (newK evs') ~: (UN C. parts (sees C evs))"; |
2032 | 331 |
by (etac traces.induct 1); |
332 |
by (dtac NS3_msg_in_parts_sees_Spy 5); |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
333 |
(*auto_tac does not work here, as it performs safe_tac first*) |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
334 |
by (ALLGOALS Asm_simp_tac); |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
335 |
by (ALLGOALS (best_tac (!claset addDs [impOfSubs analz_subset_parts, |
2032 | 336 |
impOfSubs parts_insert_subset_Un, |
337 |
Suc_leD] |
|
338 |
addss (!simpset)))); |
|
1839 | 339 |
val lemma = result(); |
340 |
||
341 |
(*Variant needed for the main theorem below*) |
|
342 |
goal thy |
|
343 |
"!!evs. [| evs : traces; length evs <= length evs' |] ==> \ |
|
1852 | 344 |
\ Key (newK evs') ~: parts (sees C evs)"; |
1839 | 345 |
by (fast_tac (!claset addDs [lemma]) 1); |
346 |
qed "new_keys_not_seen"; |
|
1893 | 347 |
Addsimps [new_keys_not_seen]; |
1839 | 348 |
|
1893 | 349 |
(*Another variant: old messages must contain old keys!*) |
350 |
goal thy |
|
1913 | 351 |
"!!evs. [| Says A B X : set_of_list evs; \ |
1893 | 352 |
\ Key (newK evt) : parts {X}; \ |
353 |
\ evs : traces \ |
|
354 |
\ |] ==> length evt < length evs"; |
|
2032 | 355 |
by (rtac ccontr 1); |
356 |
by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy] |
|
357 |
addIs [impOfSubs parts_mono, leI]) 1); |
|
1893 | 358 |
qed "Says_imp_old_keys"; |
359 |
||
1885 | 360 |
|
1852 | 361 |
goal thy "!!K. newK evs = invKey K ==> newK evs = K"; |
2032 | 362 |
by (rtac (invKey_eq RS iffD1) 1); |
1839 | 363 |
by (Simp_tac 1); |
364 |
val newK_invKey = result(); |
|
365 |
||
1852 | 366 |
|
367 |
val keysFor_parts_mono = parts_mono RS keysFor_mono; |
|
368 |
||
1839 | 369 |
(*Nobody can have USED keys that will be generated in the future. |
370 |
...very like new_keys_not_seen*) |
|
371 |
goal thy "!!evs. evs : traces ==> \ |
|
372 |
\ length evs <= length evs' --> \ |
|
1852 | 373 |
\ newK evs' ~: keysFor (UN C. parts (sees C evs))"; |
2032 | 374 |
by (etac traces.induct 1); |
375 |
by (dtac NS3_msg_in_parts_sees_Spy 5); |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
376 |
by (ALLGOALS Asm_simp_tac); |
1930 | 377 |
(*NS1 and NS2*) |
378 |
map (by o fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [3,2]; |
|
379 |
(*Fake and NS3*) |
|
380 |
map (by o best_tac |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
381 |
(!claset addSDs [newK_invKey] |
2032 | 382 |
addDs [impOfSubs (analz_subset_parts RS keysFor_mono), |
383 |
impOfSubs (parts_insert_subset_Un RS keysFor_mono), |
|
384 |
Suc_leD] |
|
385 |
addEs [new_keys_not_seen RS not_parts_not_analz RSN (2,rev_notE)] |
|
386 |
addss (!simpset))) |
|
1930 | 387 |
[2,1]; |
1933 | 388 |
(*NS4 and NS5: nonce exchange*) |
389 |
by (ALLGOALS (deepen_tac (!claset addSDs [newK_invKey, Says_imp_old_keys] |
|
2032 | 390 |
addIs [less_SucI, impOfSubs keysFor_mono] |
391 |
addss (!simpset addsimps [le_def])) 0)); |
|
1839 | 392 |
val lemma = result(); |
393 |
||
394 |
goal thy |
|
395 |
"!!evs. [| evs : traces; length evs <= length evs' |] ==> \ |
|
1852 | 396 |
\ newK evs' ~: keysFor (parts (sees C evs))"; |
1839 | 397 |
by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1); |
398 |
qed "new_keys_not_used"; |
|
399 |
||
1913 | 400 |
bind_thm ("new_keys_not_analzd", |
2032 | 401 |
[analz_subset_parts RS keysFor_mono, |
402 |
new_keys_not_used] MRS contra_subsetD); |
|
1839 | 403 |
|
1913 | 404 |
Addsimps [new_keys_not_used, new_keys_not_analzd]; |
1852 | 405 |
|
406 |
||
1885 | 407 |
(** Rewrites to push in Key and Crypt messages, so that other messages can |
1913 | 408 |
be pulled out using the analz_insert rules **) |
1885 | 409 |
|
410 |
fun insComm x y = read_instantiate_sg (sign_of thy) [("x",x), ("y",y)] |
|
411 |
insert_commute; |
|
1839 | 412 |
|
1885 | 413 |
val pushKeys = map (insComm "Key ?K") |
414 |
["Agent ?C", "Nonce ?N", "MPair ?X ?Y", "Crypt ?X ?K'"]; |
|
415 |
||
416 |
val pushCrypts = map (insComm "Crypt ?X ?K") |
|
417 |
["Agent ?C", "Nonce ?N", "MPair ?X' ?Y"]; |
|
418 |
||
419 |
(*Cannot be added with Addsimps -- we don't always want to re-order messages*) |
|
420 |
val pushes = pushKeys@pushCrypts; |
|
421 |
||
1942 | 422 |
val pushKey_newK = insComm "Key (newK ?evs)" "Key (shrK ?C)"; |
1839 | 423 |
|
1852 | 424 |
|
1839 | 425 |
(** Lemmas concerning the form of items passed in messages **) |
426 |
||
1885 | 427 |
(*Describes the form *and age* of K, and the form of X, |
428 |
when the following message is sent*) |
|
1839 | 429 |
goal thy |
1913 | 430 |
"!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') : set_of_list evs; \ |
1885 | 431 |
\ evs : traces \ |
1893 | 432 |
\ |] ==> (EX evt:traces. \ |
433 |
\ K = Key(newK evt) & \ |
|
1942 | 434 |
\ X = (Crypt {|K, Agent A|} (shrK B)) & \ |
435 |
\ K' = shrK A & \ |
|
1893 | 436 |
\ length evt < length evs)"; |
2032 | 437 |
by (etac rev_mp 1); |
438 |
by (etac traces.induct 1); |
|
1839 | 439 |
by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset)))); |
1885 | 440 |
qed "Says_Server_message_form"; |
1839 | 441 |
|
1913 | 442 |
(* c ~: keysFor (parts H) ==> c ~: keysFor (analz H) *) |
443 |
bind_thm ("not_parts_not_keysFor_analz", |
|
2032 | 444 |
analz_subset_parts RS keysFor_mono RS contra_subsetD); |
1852 | 445 |
|
446 |
||
1885 | 447 |
|
448 |
(*USELESS for NS3, case 1, as the ind hyp says the same thing! |
|
449 |
goal thy |
|
450 |
"!!evs. [| evs = Says Server (Friend i) \ |
|
451 |
\ (Crypt {|N, Agent(Friend j), K, X|} K') # evs'; \ |
|
452 |
\ evs : traces; i~=k \ |
|
453 |
\ |] ==> \ |
|
2032 | 454 |
\ K ~: analz (insert (Key (shrK (Friend k))) (sees Spy evs))"; |
455 |
by (etac rev_mp 1); |
|
456 |
by (etac traces.induct 1); |
|
1885 | 457 |
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes))); |
458 |
by (Step_tac 1); |
|
1913 | 459 |
by (asm_full_simp_tac (!simpset addsimps[analz_subset_parts RS contra_subsetD]) 1); |
2032 | 460 |
val Spy_not_see_encrypted_key_lemma = result(); |
1885 | 461 |
*) |
462 |
||
463 |
||
464 |
(*Describes the form of X when the following message is sent*) |
|
465 |
goal thy |
|
466 |
"!!evs. evs : traces ==> \ |
|
467 |
\ ALL A NA B K X. \ |
|
1942 | 468 |
\ (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \ |
2032 | 469 |
\ : parts (sees Spy evs) & A ~= Spy --> \ |
1885 | 470 |
\ (EX evt:traces. K = newK evt & \ |
1942 | 471 |
\ X = (Crypt {|Key K, Agent A|} (shrK B)))"; |
2032 | 472 |
by (etac traces.induct 1); |
473 |
by (dtac NS3_msg_in_parts_sees_Spy 5); |
|
1885 | 474 |
by (Step_tac 1); |
475 |
by (ALLGOALS Asm_full_simp_tac); |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
476 |
(*Remaining cases are Fake and NS2*) |
1885 | 477 |
by (fast_tac (!claset addSDs [spec]) 2); |
478 |
(*Now for the Fake case*) |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
479 |
by (best_tac (!claset addDs [impOfSubs analz_subset_parts, |
2032 | 480 |
impOfSubs synth_analz_parts_insert_subset_Un] |
481 |
addss (!simpset)) 1); |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
482 |
qed_spec_mp "encrypted_form"; |
1885 | 483 |
|
484 |
||
2032 | 485 |
(*For eliminating the A ~= Spy condition from the previous result*) |
1885 | 486 |
goal thy |
487 |
"!!evs. evs : traces ==> \ |
|
488 |
\ ALL S A NA B K X. \ |
|
1942 | 489 |
\ Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \ |
1913 | 490 |
\ : set_of_list evs --> \ |
2032 | 491 |
\ S = Server | S = Spy"; |
492 |
by (etac traces.induct 1); |
|
1893 | 493 |
by (ALLGOALS Asm_simp_tac); |
1885 | 494 |
(*We are left with NS3*) |
2032 | 495 |
by (subgoal_tac "S = Server | S = Spy" 1); |
1885 | 496 |
(*First justify this assumption!*) |
497 |
by (fast_tac (!claset addSEs [allE, mp] addss (!simpset)) 2); |
|
498 |
by (Step_tac 1); |
|
2032 | 499 |
by (dtac Says_Server_message_form 1); |
1885 | 500 |
by (ALLGOALS Full_simp_tac); |
501 |
(*Final case. Clear out needless quantifiers to speed the following step*) |
|
502 |
by (eres_inst_tac [("V","ALL x. ?P(x)")] thin_rl 1); |
|
2032 | 503 |
by (dtac encrypted_form 1); |
504 |
by (rtac (parts.Inj RS conjI) 1); |
|
1885 | 505 |
auto(); |
2032 | 506 |
qed_spec_mp "Server_or_Spy"; |
1885 | 507 |
|
508 |
||
509 |
(*Describes the form of X when the following message is sent; |
|
510 |
use Says_Server_message_form if applicable*) |
|
511 |
goal thy |
|
1942 | 512 |
"!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \ |
1913 | 513 |
\ : set_of_list evs; \ |
1885 | 514 |
\ evs : traces \ |
1893 | 515 |
\ |] ==> (EX evt:traces. K = newK evt & length evt < length evs & \ |
1942 | 516 |
\ X = (Crypt {|Key K, Agent A|} (shrK B)))"; |
2032 | 517 |
by (forward_tac [Server_or_Spy] 1); |
518 |
by (assume_tac 1); |
|
1885 | 519 |
by (Step_tac 1); |
520 |
by (fast_tac (!claset addSDs [Says_Server_message_form] addss (!simpset)) 1); |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
521 |
by (forward_tac [encrypted_form] 1); |
2032 | 522 |
by (rtac (parts.Inj RS conjI) 1); |
1893 | 523 |
by (auto_tac (!claset addIs [Says_imp_old_keys], !simpset)); |
1885 | 524 |
qed "Says_S_message_form"; |
525 |
||
1930 | 526 |
(*Currently unused. Needed only to reason about the VERY LAST message.*) |
1885 | 527 |
goal thy |
528 |
"!!evs. [| evs = Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} \ |
|
1942 | 529 |
\ (shrK A)) # evs'; \ |
1885 | 530 |
\ evs : traces \ |
1893 | 531 |
\ |] ==> (EX evt:traces. evs' : traces & length evt < length evs & \ |
1885 | 532 |
\ K = newK evt & \ |
1942 | 533 |
\ X = (Crypt {|Key K, Agent A|} (shrK B)))"; |
1885 | 534 |
by (forward_tac [traces_eq_ConsE] 1); |
1913 | 535 |
by (dtac (set_of_list_eqI1 RS Says_S_message_form) 2); |
2032 | 536 |
by (Auto_tac()); |
1885 | 537 |
qed "Says_S_message_form_eq"; |
538 |
||
539 |
||
540 |
||
541 |
(**** |
|
542 |
The following is to prove theorems of the form |
|
543 |
||
1913 | 544 |
Key K : analz (insert (Key (newK evt)) |
2032 | 545 |
(insert (Key (shrK C)) (sees Spy evs))) ==> |
546 |
Key K : analz (insert (Key (shrK C)) (sees Spy evs)) |
|
1885 | 547 |
|
548 |
A more general formula must be proved inductively. |
|
549 |
||
550 |
****) |
|
551 |
||
552 |
||
1933 | 553 |
(*NOT useful in this form, but it says that session keys are not used |
1885 | 554 |
to encrypt messages containing other keys, in the actual protocol. |
555 |
We require that agents should behave like this subsequently also.*) |
|
556 |
goal thy |
|
557 |
"!!evs. evs : traces ==> \ |
|
2032 | 558 |
\ (Crypt X (newK evt)) : parts (sees Spy evs) & \ |
559 |
\ Key K : parts {X} --> Key K : parts (sees Spy evs)"; |
|
560 |
by (etac traces.induct 1); |
|
561 |
by (dtac NS3_msg_in_parts_sees_Spy 5); |
|
1893 | 562 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes))); |
1885 | 563 |
(*Deals with Faked messages*) |
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
564 |
by (best_tac (!claset addSEs partsEs |
2032 | 565 |
addDs [impOfSubs analz_subset_parts, |
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
566 |
impOfSubs parts_insert_subset_Un] |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
567 |
addss (!simpset)) 1); |
1933 | 568 |
(*NS4 and NS5*) |
569 |
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); |
|
1885 | 570 |
result(); |
571 |
||
572 |
||
1893 | 573 |
(** Specialized rewriting for this proof **) |
1885 | 574 |
|
575 |
Delsimps [image_insert]; |
|
576 |
Addsimps [image_insert RS sym]; |
|
577 |
||
578 |
goal thy "insert (Key (newK x)) (sees A evs) = \ |
|
579 |
\ Key `` (newK``{x}) Un (sees A evs)"; |
|
580 |
by (Fast_tac 1); |
|
581 |
val insert_Key_singleton = result(); |
|
582 |
||
583 |
goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \ |
|
584 |
\ Key `` (f `` (insert x E)) Un C"; |
|
585 |
by (Fast_tac 1); |
|
586 |
val insert_Key_image = result(); |
|
587 |
||
588 |
||
1893 | 589 |
(** Session keys are not used to encrypt other session keys **) |
590 |
||
1885 | 591 |
goal thy |
592 |
"!!evs. evs : traces ==> \ |
|
1942 | 593 |
\ ALL K E. (Key K : analz (insert (Key (shrK C)) \ |
2032 | 594 |
\ (Key``(newK``E) Un (sees Spy evs)))) = \ |
1885 | 595 |
\ (K : newK``E | \ |
1942 | 596 |
\ Key K : analz (insert (Key (shrK C)) \ |
2032 | 597 |
\ (sees Spy evs)))"; |
598 |
by (etac traces.induct 1); |
|
599 |
by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); |
|
1885 | 600 |
by (REPEAT ((eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac) 5)); |
601 |
by (ALLGOALS |
|
1893 | 602 |
(asm_simp_tac |
1885 | 603 |
(!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK] |
2032 | 604 |
@ pushes) |
1885 | 605 |
setloop split_tac [expand_if]))); |
606 |
(*Cases NS2 and NS3!! Simple, thanks to auto case splits*) |
|
607 |
by (REPEAT (Fast_tac 3)); |
|
608 |
(*Base case*) |
|
609 |
by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); |
|
610 |
(** LEVEL 7 **) |
|
611 |
(*Fake case*) |
|
612 |
by (REPEAT (Safe_step_tac 1)); |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
613 |
by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 2); |
1885 | 614 |
by (subgoal_tac |
1913 | 615 |
"Key K : analz \ |
616 |
\ (synth \ |
|
1942 | 617 |
\ (analz (insert (Key (shrK C)) \ |
2032 | 618 |
\ (Key``(newK``E) Un (sees Spy evsa)))))" 1); |
1885 | 619 |
(*First, justify this subgoal*) |
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
620 |
(*Discard formulae for better speed*) |
1885 | 621 |
by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2); |
622 |
by (eres_inst_tac [("V","?Q ~: ?QQ")] thin_rl 2); |
|
1913 | 623 |
by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)] |
624 |
addSEs [impOfSubs analz_mono]) 2); |
|
1885 | 625 |
by (Asm_full_simp_tac 1); |
1913 | 626 |
by (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1); |
627 |
qed_spec_mp "analz_image_newK"; |
|
1885 | 628 |
|
629 |
||
630 |
goal thy |
|
631 |
"!!evs. evs : traces ==> \ |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
632 |
\ Key K : analz (insert (Key (newK evt)) \ |
1942 | 633 |
\ (insert (Key (shrK C)) \ |
2032 | 634 |
\ (sees Spy evs))) = \ |
1885 | 635 |
\ (K = newK evt | \ |
1942 | 636 |
\ Key K : analz (insert (Key (shrK C)) \ |
2032 | 637 |
\ (sees Spy evs)))"; |
1913 | 638 |
by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, |
2032 | 639 |
insert_Key_singleton]) 1); |
1885 | 640 |
by (Fast_tac 1); |
1913 | 641 |
qed "analz_insert_Key_newK"; |
1885 | 642 |
|
643 |
||
644 |
||
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
645 |
(*This says that the Key, K, uniquely identifies the message. |
2032 | 646 |
But if C=Spy then he could send all sorts of nonsense.*) |
1893 | 647 |
goal thy |
648 |
"!!evs. evs : traces ==> \ |
|
649 |
\ EX X'. ALL C S A Y N B X. \ |
|
2032 | 650 |
\ C ~= Spy --> \ |
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
651 |
\ Says S A Y : set_of_list evs --> \ |
1942 | 652 |
\ ((Crypt {|N, Agent B, Key K, X|} (shrK C)) : parts{Y} --> \ |
1893 | 653 |
\ (X = X'))"; |
2032 | 654 |
by (etac traces.induct 1); |
655 |
by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); |
|
1893 | 656 |
by (ALLGOALS |
657 |
(asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib]))); |
|
658 |
(*NS2: Case split propagates some context to other subgoal...*) |
|
659 |
by (excluded_middle_tac "K = newK evsa" 2); |
|
660 |
by (Asm_simp_tac 2); |
|
661 |
(*...we assume X is a very new message, and handle this case by contradiction*) |
|
662 |
by (fast_tac (!claset addIs [impOfSubs (subset_insertI RS parts_mono)] |
|
2032 | 663 |
addSEs partsEs |
664 |
addEs [Says_imp_old_keys RS less_irrefl] |
|
665 |
addss (!simpset)) 2); |
|
1893 | 666 |
(*NS3: No relevant messages*) |
667 |
by (fast_tac (!claset addSEs [exI] addss (!simpset)) 2); |
|
668 |
(*Fake*) |
|
669 |
by (Step_tac 1); |
|
2032 | 670 |
by (rtac exI 1); |
671 |
by (rtac conjI 1); |
|
672 |
by (assume_tac 2); |
|
1893 | 673 |
by (Step_tac 1); |
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
674 |
(** LEVEL 12 **) |
1942 | 675 |
by (subgoal_tac "Crypt {|N, Agent Ba, Key K, Xa|} (shrK C) \ |
2032 | 676 |
\ : parts (sees Spy evsa)" 1); |
1893 | 677 |
by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2); |
1913 | 678 |
by (best_tac (!claset addSEs [impOfSubs analz_subset_parts] |
2032 | 679 |
addDs [impOfSubs parts_insert_subset_Un] |
1893 | 680 |
addss (!simpset)) 2); |
681 |
by (eres_inst_tac [("V","?aa : parts {X}")] thin_rl 1); |
|
2032 | 682 |
by (dtac parts_singleton 1); |
1893 | 683 |
by (Step_tac 1); |
2032 | 684 |
by (dtac seesD 1); |
1893 | 685 |
by (Step_tac 1); |
686 |
by (Full_simp_tac 2); |
|
687 |
by (fast_tac (!claset addSDs [spec]) 1); |
|
688 |
val lemma = result(); |
|
1885 | 689 |
|
690 |
||
1893 | 691 |
(*In messages of this form, the session key uniquely identifies the rest*) |
1885 | 692 |
goal thy |
693 |
"!!evs. [| Says S A \ |
|
1942 | 694 |
\ (Crypt {|N, Agent B, Key K, X|} (shrK C)) \ |
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
695 |
\ : set_of_list evs; \ |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
696 |
\ Says S' A' \ |
1942 | 697 |
\ (Crypt {|N', Agent B', Key K, X'|} (shrK C')) \ |
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
698 |
\ : set_of_list evs; \ |
2032 | 699 |
\ evs : traces; C ~= Spy; C' ~= Spy |] ==> X = X'"; |
700 |
by (dtac lemma 1); |
|
701 |
by (etac exE 1); |
|
1893 | 702 |
by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1); |
703 |
by (Fast_tac 1); |
|
704 |
qed "unique_session_keys"; |
|
1885 | 705 |
|
706 |
||
707 |
||
2032 | 708 |
(*Crucial security property: Spy does not see the keys sent in msg NS2 |
1885 | 709 |
-- even if another key is compromised*) |
710 |
goal thy |
|
711 |
"!!evs. [| Says Server (Friend i) \ |
|
1913 | 712 |
\ (Crypt {|N, Agent(Friend j), K, X|} K') : set_of_list evs; \ |
1885 | 713 |
\ evs : traces; Friend i ~= C; Friend j ~= C \ |
714 |
\ |] ==> \ |
|
2032 | 715 |
\ K ~: analz (insert (Key (shrK C)) (sees Spy evs))"; |
716 |
by (etac rev_mp 1); |
|
717 |
by (etac traces.induct 1); |
|
1893 | 718 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes))); |
1885 | 719 |
(*Next 3 steps infer that K has the form "Key (newK evs'" ... *) |
720 |
by (REPEAT_FIRST (resolve_tac [conjI, impI])); |
|
721 |
by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac)); |
|
722 |
by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac)); |
|
723 |
by (ALLGOALS |
|
724 |
(asm_full_simp_tac |
|
1913 | 725 |
(!simpset addsimps ([analz_subset_parts RS contra_subsetD, |
2032 | 726 |
analz_insert_Key_newK] @ pushes) |
1885 | 727 |
setloop split_tac [expand_if]))); |
728 |
(*NS2*) |
|
1893 | 729 |
by (fast_tac (!claset addSEs [less_irrefl]) 2); |
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
730 |
(** LEVEL 8 **) |
1885 | 731 |
(*Now for the Fake case*) |
2032 | 732 |
by (rtac notI 1); |
1885 | 733 |
by (subgoal_tac |
1893 | 734 |
"Key (newK evt) : \ |
1942 | 735 |
\ analz (synth (analz (insert (Key (shrK C)) \ |
2032 | 736 |
\ (sees Spy evsa))))" 1); |
737 |
by (etac (impOfSubs analz_mono) 2); |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
738 |
by (deepen_tac (!claset addIs [analz_mono RS synth_mono RSN (2,rev_subsetD), |
2032 | 739 |
impOfSubs synth_increasing, |
740 |
impOfSubs analz_increasing]) 0 2); |
|
1885 | 741 |
(*Proves the Fake goal*) |
742 |
by (fast_tac (!claset addss (!simpset)) 1); |
|
743 |
||
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
744 |
(**LEVEL 13**) |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
745 |
(*NS3: that message from the Server was sent earlier*) |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
746 |
by (mp_tac 1); |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
747 |
by (forward_tac [Says_S_message_form] 1 THEN assume_tac 1); |
1885 | 748 |
by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac)); |
1893 | 749 |
by (asm_full_simp_tac |
1913 | 750 |
(!simpset addsimps (mem_if::analz_insert_Key_newK::pushes)) 1); |
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
751 |
by (Step_tac 1); |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
752 |
(**LEVEL 18 **) |
2032 | 753 |
by (dtac unique_session_keys 1); |
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
754 |
by (REPEAT_FIRST assume_tac); |
1893 | 755 |
by (ALLGOALS Full_simp_tac); |
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
756 |
by (Step_tac 1); |
1942 | 757 |
by (asm_full_simp_tac (!simpset addsimps [shrK_mem_analz]) 1); |
2032 | 758 |
qed "Spy_not_see_encrypted_key"; |
1885 | 759 |
|
760 |
||
761 |
||
762 |
||
1893 | 763 |
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX; |
1885 | 764 |
|
765 |
||
1893 | 766 |
goals_limit:=4; |
1885 | 767 |
|
768 |
||
769 |
||
1893 | 770 |
goal thy |
771 |
"!!evs. [| Says Server (Friend i) \ |
|
1913 | 772 |
\ (Crypt {|N, Agent B, K|} K') : set_of_list evs; \ |
1893 | 773 |
\ evs : traces; i~=j \ |
1913 | 774 |
\ |] ==> K ~: analz (sees (Friend j) evs)"; |
2032 | 775 |
by (rtac (sees_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1); |
776 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps [Spy_not_see_encrypted_key]))); |
|
1893 | 777 |
qed "Friend_not_see_encrypted_key"; |
1885 | 778 |
|
1893 | 779 |
goal thy |
780 |
"!!evs. [| Says Server (Friend i) \ |
|
1913 | 781 |
\ (Crypt {|N, Agent B, K|} K') : set_of_list evs; \ |
1893 | 782 |
\ A ~: {Friend i, Server}; \ |
783 |
\ evs : traces \ |
|
1913 | 784 |
\ |] ==> K ~: analz (sees A evs)"; |
1893 | 785 |
by (eres_inst_tac [("P", "A~:?X")] rev_mp 1); |
786 |
by (agent.induct_tac "A" 1); |
|
787 |
by (ALLGOALS Simp_tac); |
|
788 |
by (asm_simp_tac (!simpset addsimps [eq_sym_conv, |
|
2032 | 789 |
Friend_not_see_encrypted_key]) 1); |
790 |
by (rtac ([analz_mono, Spy_not_see_encrypted_key] MRS contra_subsetD) 1); |
|
1893 | 791 |
(* hyp_subst_tac would deletes the equality assumption... *) |
792 |
by (ALLGOALS (rtac n_not_Suc_n ORELSE' Fast_tac)); |
|
793 |
qed "Agent_not_see_encrypted_key"; |
|
1885 | 794 |
|
795 |
||
1893 | 796 |
(*Neatly packaged, perhaps in a useless form*) |
797 |
goalw thy [knownBy_def] |
|
798 |
"!!evs. [| Says Server (Friend i) \ |
|
1913 | 799 |
\ (Crypt {|N, Agent B, K|} K') : set_of_list evs; \ |
1893 | 800 |
\ evs : traces \ |
801 |
\ |] ==> knownBy evs K <= {Friend i, Server}"; |
|
1885 | 802 |
|
1893 | 803 |
by (Step_tac 1); |
2032 | 804 |
by (rtac ccontr 1); |
1893 | 805 |
by (fast_tac (!claset addDs [Agent_not_see_encrypted_key]) 1); |
806 |
qed "knownBy_encrypted_key"; |
|
1885 | 807 |
|
808 |
||
809 |
||
810 |
||
811 |
||
812 |
||
813 |
||
814 |
push_proof(); |
|
815 |
goal thy |
|
816 |
"!!evs. [| evs = Says S (Friend i) \ |
|
817 |
\ (Crypt {|N, Agent(Friend j), K, X|} K') # evs'; \ |
|
818 |
\ evs : traces; i~=k \ |
|
819 |
\ |] ==> \ |
|
2032 | 820 |
\ K ~: analz (insert (Key (shrK (Friend k))) (sees Spy evs))"; |
821 |
by (etac rev_mp 1); |
|
822 |
by (etac traces.induct 1); |
|
1885 | 823 |
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes))); |
824 |
by (Step_tac 1); |
|
1913 | 825 |
by (asm_full_simp_tac (!simpset addsimps[analz_subset_parts RS contra_subsetD]) 1); |
2032 | 826 |
val Spy_not_see_encrypted_key_lemma = result(); |
1885 | 827 |
|
828 |
||
829 |
||
830 |
||
831 |
||
832 |
||
833 |
||
1913 | 834 |
(*Precisely formulated as needed below. Perhaps redundant, as simplification |
835 |
with the aid of analz_subset_parts RS contra_subsetD might do the |
|
836 |
same thing.*) |
|
837 |
goal thy |
|
2032 | 838 |
"!!evs. [| evs : traces; A ~= Spy; A ~= Friend j |] ==> \ |
1942 | 839 |
\ Key (shrK A) ~: \ |
2032 | 840 |
\ analz (insert (Key (shrK (Friend j))) (sees Spy evs))"; |
841 |
by (rtac (analz_subset_parts RS contra_subsetD) 1); |
|
1913 | 842 |
by (Asm_simp_tac 1); |
1942 | 843 |
qed "insert_not_analz_shrK"; |
1885 | 844 |
|
845 |
||
846 |
||
847 |
||
848 |
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX; |
|
849 |
proof_timing:=true; |
|
850 |
||
1852 | 851 |
|
852 |
||
853 |
YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY; |
|
854 |
||
855 |
||
856 |
||
857 |
(*If a message is sent, encrypted with a Friend's server key, then either |
|
858 |
that Friend or the Server originally sent it.*) |
|
859 |
goal thy |
|
860 |
"!!evs. evs : traces ==> \ |
|
1942 | 861 |
\ ALL A B X i. Says A B (Crypt X (shrK (Friend i))) \ |
1913 | 862 |
\ : set_of_list evs --> \ |
1942 | 863 |
\ (EX B'. Says Server B' (Crypt X (shrK (Friend i))) : set_of_list evs | \ |
864 |
\ Says (Friend i) B' (Crypt X (shrK (Friend i))) : set_of_list evs)"; |
|
2032 | 865 |
by (etac traces.induct 1); |
1852 | 866 |
by (Step_tac 1); |
867 |
by (ALLGOALS Asm_full_simp_tac); |
|
868 |
(*Remaining cases are Fake, NS2 and NS3*) |
|
2032 | 869 |
by (Fast_tac 2); (*Proves the NS2 case*) |
1852 | 870 |
|
871 |
by (REPEAT (dtac spec 2)); |
|
872 |
fe conjE; |
|
2032 | 873 |
by (dtac mp 2); |
1852 | 874 |
|
875 |
by (REPEAT (resolve_tac [refl, conjI] 2)); |
|
876 |
by (ALLGOALS Asm_full_simp_tac); |
|
877 |
||
878 |
||
879 |
||
880 |
||
881 |
by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2); |
|
2032 | 882 |
by (etac conjE 2); |
1852 | 883 |
by ((dtac spec THEN' dtac spec THEN' dtac spec THEN' dtac spec)2); |
884 |
||
885 |
(*The NS3 case needs the induction hypothesis twice! |
|
886 |
One application is to the X component of the most recent message.*) |
|
1942 | 887 |
by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent A|} (shrK B)" 2); |
1852 | 888 |
by (Fast_tac 3); |
889 |
by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2); |
|
2032 | 890 |
by (etac conjE 2); |
1852 | 891 |
(*DELETE the first quantified formula: it's now useless*) |
892 |
by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2); |
|
893 |
by (fast_tac (!claset addss (!simpset)) 2); |
|
894 |
(*Now for the Fake case*) |
|
2032 | 895 |
by (etac disjE 1); |
1852 | 896 |
(*The subcase of Fake, where the message in question is NOT the most recent*) |
897 |
by (Best_tac 2); |
|
898 |
||
899 |
by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac)); |
|
2032 | 900 |
by (etac Crypt_synth 1); |
901 |
by (etac Key_synth 2); |
|
1852 | 902 |
|
1913 | 903 |
(*Split up the possibilities of that message being synthd...*) |
1852 | 904 |
by (Step_tac 1); |
905 |
by (Best_tac 6); |
|
906 |
||
907 |
||
908 |
||
909 |
||
910 |
||
1839 | 911 |
(*NEEDED??*) |
912 |
||
913 |
goal thy "!!A. X ~= Y ==> (X : sees A (Says B C Y # evs)) = (X : sees A evs)"; |
|
914 |
by (asm_simp_tac (!simpset addsimps [sees_Cons] |
|
915 |
setloop split_tac [expand_if]) 1); |
|
916 |
qed "in_sees_Says"; |
|
917 |
||
918 |
goal thy "!!A. X ~: parts {Y} ==> \ |
|
919 |
\ (X : parts (sees A (Says B C Y # evs))) = \ |
|
920 |
\ (X : parts (sees A evs))"; |
|
921 |
by (asm_simp_tac (!simpset addsimps [sees_Cons] |
|
922 |
setloop split_tac [expand_if]) 1); |
|
923 |
by (asm_simp_tac (!simpset addsimps [parts_Un]) 1); |
|
924 |
qed "in_parts_sees_Says"; |
|
925 |
||
1852 | 926 |
goal thy "!!evs. length evs < length evs' ==> newK evs ~= newK (A',evs')"; |
1839 | 927 |
by (fast_tac (!claset addSEs [less_irrefl]) 1); |
928 |
qed "length_less_newK_neq"; |
|
929 |
||
930 |
||
931 |
||
932 |
||
933 |
||
934 |
||
935 |
YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY; |
|
936 |
||
937 |
goalw thy [keysFor_def] |
|
938 |
"!!X. Crypt X K: H ==> invKey K : keysFor H"; |
|
939 |
by (Fast_tac 1); |
|
940 |
qed "keysFor_I"; |
|
941 |
AddSIs [keysFor_I]; |
|
942 |
||
943 |
goalw thy [keysFor_def] |
|
944 |
"!!K. K : keysFor H ==> EX X K'. K=invKey K' & Crypt X K': H"; |
|
945 |
by (Fast_tac 1); |
|
946 |
qed "keysFor_D"; |
|
947 |
AddSDs [keysFor_D]; |
|
948 |
||
949 |