|
1 (* Title: HOL/Auth/NS_Shared |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1996 University of Cambridge |
|
5 |
|
6 Inductive relation "ns_shared" for Needham-Schroeder Shared-Key protocol. |
|
7 |
|
8 From page 247 of |
|
9 Burrows, Abadi and Needham. A Logic of Authentication. |
|
10 Proc. Royal Soc. 426 (1989) |
|
11 *) |
|
12 |
|
13 open NS_Shared; |
|
14 |
|
15 (**** Inductive proofs about ns_shared ****) |
|
16 |
|
17 (*The Enemy can see more than anybody else, except for their initial state*) |
|
18 goal thy |
|
19 "!!evs. evs : ns_shared ==> \ |
|
20 \ sees A evs <= initState A Un sees Enemy evs"; |
|
21 be ns_shared.induct 1; |
|
22 by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] |
|
23 addss (!simpset)))); |
|
24 qed "sees_agent_subset_sees_Enemy"; |
|
25 |
|
26 |
|
27 (*Nobody sends themselves messages*) |
|
28 goal thy "!!evs. evs : ns_shared ==> ALL A X. Says A A X ~: set_of_list evs"; |
|
29 be ns_shared.induct 1; |
|
30 by (Auto_tac()); |
|
31 qed_spec_mp "not_Says_to_self"; |
|
32 Addsimps [not_Says_to_self]; |
|
33 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
|
34 |
|
35 goal thy "!!evs. evs : ns_shared ==> Notes A X ~: set_of_list evs"; |
|
36 be ns_shared.induct 1; |
|
37 by (Auto_tac()); |
|
38 qed "not_Notes"; |
|
39 Addsimps [not_Notes]; |
|
40 AddSEs [not_Notes RSN (2, rev_notE)]; |
|
41 |
|
42 |
|
43 (*For reasoning about message NS3*) |
|
44 goal thy "!!evs. (Says S A (Crypt {|N, B, K, X|} KA)) : set_of_list evs ==> \ |
|
45 \ X : parts (sees Enemy evs)"; |
|
46 by (fast_tac (!claset addSEs partsEs |
|
47 addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1); |
|
48 qed "NS3_msg_in_parts_sees_Enemy"; |
|
49 |
|
50 |
|
51 (*** Server keys are not betrayed ***) |
|
52 |
|
53 (*Enemy never sees another agent's server key!*) |
|
54 goal thy |
|
55 "!!evs. [| evs : ns_shared; A ~= Enemy |] ==> \ |
|
56 \ Key (serverKey A) ~: parts (sees Enemy evs)"; |
|
57 be ns_shared.induct 1; |
|
58 bd NS3_msg_in_parts_sees_Enemy 5; |
|
59 by (Auto_tac()); |
|
60 (*Deals with Fake message*) |
|
61 by (best_tac (!claset addDs [impOfSubs analz_subset_parts, |
|
62 impOfSubs synth_analz_parts_insert_subset_Un]) 1); |
|
63 qed "Enemy_not_see_serverKey"; |
|
64 |
|
65 bind_thm ("Enemy_not_analz_serverKey", |
|
66 [analz_subset_parts, Enemy_not_see_serverKey] MRS contra_subsetD); |
|
67 |
|
68 Addsimps [Enemy_not_see_serverKey, |
|
69 not_sym RSN (2, Enemy_not_see_serverKey), |
|
70 Enemy_not_analz_serverKey, |
|
71 not_sym RSN (2, Enemy_not_analz_serverKey)]; |
|
72 |
|
73 (*We go to some trouble to preserve R in the 3rd subgoal*) |
|
74 val major::prems = |
|
75 goal thy "[| Key (serverKey A) : parts (sees Enemy evs); \ |
|
76 \ evs : ns_shared; \ |
|
77 \ A=Enemy ==> R \ |
|
78 \ |] ==> R"; |
|
79 br ccontr 1; |
|
80 br ([major, Enemy_not_see_serverKey] MRS rev_notE) 1; |
|
81 by (swap_res_tac prems 2); |
|
82 by (ALLGOALS (fast_tac (!claset addIs prems))); |
|
83 qed "Enemy_see_serverKey_E"; |
|
84 |
|
85 bind_thm ("Enemy_analz_serverKey_E", |
|
86 analz_subset_parts RS subsetD RS Enemy_see_serverKey_E); |
|
87 |
|
88 (*Classical reasoner doesn't need the not_sym versions (with swapped ~=) *) |
|
89 AddSEs [Enemy_see_serverKey_E, Enemy_analz_serverKey_E]; |
|
90 |
|
91 |
|
92 (*No Friend will ever see another agent's server key |
|
93 (excluding the Enemy, who might transmit his). |
|
94 The Server, of course, knows all server keys.*) |
|
95 goal thy |
|
96 "!!evs. [| evs : ns_shared; A ~= Enemy; A ~= Friend j |] ==> \ |
|
97 \ Key (serverKey A) ~: parts (sees (Friend j) evs)"; |
|
98 br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1; |
|
99 by (ALLGOALS Asm_simp_tac); |
|
100 qed "Friend_not_see_serverKey"; |
|
101 |
|
102 |
|
103 (*Not for Addsimps -- it can cause goals to blow up!*) |
|
104 goal thy |
|
105 "!!evs. evs : ns_shared ==> \ |
|
106 \ (Key (serverKey A) \ |
|
107 \ : analz (insert (Key (serverKey B)) (sees Enemy evs))) = \ |
|
108 \ (A=B | A=Enemy)"; |
|
109 by (best_tac (!claset addDs [impOfSubs analz_subset_parts] |
|
110 addIs [impOfSubs (subset_insertI RS analz_mono)] |
|
111 addss (!simpset)) 1); |
|
112 qed "serverKey_mem_analz"; |
|
113 |
|
114 |
|
115 (*** Future keys can't be seen or used! ***) |
|
116 |
|
117 (*Nobody can have SEEN keys that will be generated in the future. |
|
118 This has to be proved anew for each protocol description, |
|
119 but should go by similar reasoning every time. Hardest case is the |
|
120 standard Fake rule. |
|
121 The length comparison, and Union over C, are essential for the |
|
122 induction! *) |
|
123 goal thy "!!evs. evs : ns_shared ==> \ |
|
124 \ length evs <= length evs' --> \ |
|
125 \ Key (newK evs') ~: (UN C. parts (sees C evs))"; |
|
126 be ns_shared.induct 1; |
|
127 bd NS3_msg_in_parts_sees_Enemy 5; |
|
128 (*auto_tac does not work here, as it performs safe_tac first*) |
|
129 by (ALLGOALS Asm_simp_tac); |
|
130 by (ALLGOALS (best_tac (!claset addDs [impOfSubs analz_subset_parts, |
|
131 impOfSubs parts_insert_subset_Un, |
|
132 Suc_leD] |
|
133 addss (!simpset)))); |
|
134 val lemma = result(); |
|
135 |
|
136 (*Variant needed for the main theorem below*) |
|
137 goal thy |
|
138 "!!evs. [| evs : ns_shared; length evs <= length evs' |] ==> \ |
|
139 \ Key (newK evs') ~: parts (sees C evs)"; |
|
140 by (fast_tac (!claset addDs [lemma]) 1); |
|
141 qed "new_keys_not_seen"; |
|
142 Addsimps [new_keys_not_seen]; |
|
143 |
|
144 (*Another variant: old messages must contain old keys!*) |
|
145 goal thy |
|
146 "!!evs. [| Says A B X : set_of_list evs; \ |
|
147 \ Key (newK evt) : parts {X}; \ |
|
148 \ evs : ns_shared \ |
|
149 \ |] ==> length evt < length evs"; |
|
150 br ccontr 1; |
|
151 by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy] |
|
152 addIs [impOfSubs parts_mono, leI]) 1); |
|
153 qed "Says_imp_old_keys"; |
|
154 |
|
155 |
|
156 (*Nobody can have USED keys that will be generated in the future. |
|
157 ...very like new_keys_not_seen*) |
|
158 goal thy "!!evs. evs : ns_shared ==> \ |
|
159 \ length evs <= length evs' --> \ |
|
160 \ newK evs' ~: keysFor (UN C. parts (sees C evs))"; |
|
161 be ns_shared.induct 1; |
|
162 bd NS3_msg_in_parts_sees_Enemy 5; |
|
163 by (ALLGOALS Asm_simp_tac); |
|
164 (*NS1 and NS2*) |
|
165 map (by o fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [3,2]; |
|
166 (*Fake and NS3*) |
|
167 map (by o best_tac |
|
168 (!claset addSDs [newK_invKey] |
|
169 addDs [impOfSubs (analz_subset_parts RS keysFor_mono), |
|
170 impOfSubs (parts_insert_subset_Un RS keysFor_mono), |
|
171 Suc_leD] |
|
172 addEs [new_keys_not_seen RS not_parts_not_analz RSN (2,rev_notE)] |
|
173 addss (!simpset))) |
|
174 [2,1]; |
|
175 (*NS4 and NS5: nonce exchange*) |
|
176 by (ALLGOALS (deepen_tac (!claset addSDs [newK_invKey, Says_imp_old_keys] |
|
177 addIs [less_SucI, impOfSubs keysFor_mono] |
|
178 addss (!simpset addsimps [le_def])) 0)); |
|
179 val lemma = result(); |
|
180 |
|
181 goal thy |
|
182 "!!evs. [| evs : ns_shared; length evs <= length evs' |] ==> \ |
|
183 \ newK evs' ~: keysFor (parts (sees C evs))"; |
|
184 by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1); |
|
185 qed "new_keys_not_used"; |
|
186 |
|
187 bind_thm ("new_keys_not_analzd", |
|
188 [analz_subset_parts RS keysFor_mono, |
|
189 new_keys_not_used] MRS contra_subsetD); |
|
190 |
|
191 Addsimps [new_keys_not_used, new_keys_not_analzd]; |
|
192 |
|
193 |
|
194 (** Lemmas concerning the form of items passed in messages **) |
|
195 |
|
196 (*Describes the form *and age* of K, and the form of X, |
|
197 when the following message is sent*) |
|
198 goal thy |
|
199 "!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') : set_of_list evs; \ |
|
200 \ evs : ns_shared \ |
|
201 \ |] ==> (EX evt:ns_shared. \ |
|
202 \ K = Key(newK evt) & \ |
|
203 \ X = (Crypt {|K, Agent A|} (serverKey B)) & \ |
|
204 \ K' = serverKey A & \ |
|
205 \ length evt < length evs)"; |
|
206 be rev_mp 1; |
|
207 be ns_shared.induct 1; |
|
208 by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset)))); |
|
209 qed "Says_Server_message_form"; |
|
210 |
|
211 |
|
212 (*Describes the form of X when the following message is sent*) |
|
213 goal thy |
|
214 "!!evs. evs : ns_shared ==> \ |
|
215 \ ALL A NA B K X. \ |
|
216 \ (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \ |
|
217 \ : parts (sees Enemy evs) & A ~= Enemy --> \ |
|
218 \ (EX evt:ns_shared. K = newK evt & \ |
|
219 \ X = (Crypt {|Key K, Agent A|} (serverKey B)))"; |
|
220 be ns_shared.induct 1; |
|
221 bd NS3_msg_in_parts_sees_Enemy 5; |
|
222 by (Step_tac 1); |
|
223 by (ALLGOALS Asm_full_simp_tac); |
|
224 (*Remaining cases are Fake and NS2*) |
|
225 by (fast_tac (!claset addSDs [spec]) 2); |
|
226 (*Now for the Fake case*) |
|
227 by (best_tac (!claset addDs [impOfSubs analz_subset_parts, |
|
228 impOfSubs synth_analz_parts_insert_subset_Un] |
|
229 addss (!simpset)) 1); |
|
230 qed_spec_mp "encrypted_form"; |
|
231 |
|
232 |
|
233 (*For eliminating the A ~= Enemy condition from the previous result*) |
|
234 goal thy |
|
235 "!!evs. evs : ns_shared ==> \ |
|
236 \ ALL S A NA B K X. \ |
|
237 \ Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \ |
|
238 \ : set_of_list evs --> \ |
|
239 \ S = Server | S = Enemy"; |
|
240 be ns_shared.induct 1; |
|
241 by (ALLGOALS Asm_simp_tac); |
|
242 (*We are left with NS3*) |
|
243 by (subgoal_tac "S = Server | S = Enemy" 1); |
|
244 (*First justify this assumption!*) |
|
245 by (fast_tac (!claset addSEs [allE, mp] addss (!simpset)) 2); |
|
246 by (Step_tac 1); |
|
247 bd Says_Server_message_form 1; |
|
248 by (ALLGOALS Full_simp_tac); |
|
249 (*Final case. Clear out needless quantifiers to speed the following step*) |
|
250 by (eres_inst_tac [("V","ALL x. ?P(x)")] thin_rl 1); |
|
251 bd encrypted_form 1; |
|
252 br (parts.Inj RS conjI) 1; |
|
253 auto(); |
|
254 qed_spec_mp "Server_or_Enemy"; |
|
255 |
|
256 |
|
257 (*Describes the form of X when the following message is sent; |
|
258 use Says_Server_message_form if applicable*) |
|
259 goal thy |
|
260 "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \ |
|
261 \ : set_of_list evs; \ |
|
262 \ evs : ns_shared \ |
|
263 \ |] ==> (EX evt:ns_shared. K = newK evt & length evt < length evs & \ |
|
264 \ X = (Crypt {|Key K, Agent A|} (serverKey B)))"; |
|
265 by (forward_tac [Server_or_Enemy] 1); |
|
266 ba 1; |
|
267 by (Step_tac 1); |
|
268 by (fast_tac (!claset addSDs [Says_Server_message_form] addss (!simpset)) 1); |
|
269 by (forward_tac [encrypted_form] 1); |
|
270 br (parts.Inj RS conjI) 1; |
|
271 by (auto_tac (!claset addIs [Says_imp_old_keys], !simpset)); |
|
272 qed "Says_S_message_form"; |
|
273 |
|
274 |
|
275 |
|
276 (**** |
|
277 The following is to prove theorems of the form |
|
278 |
|
279 Key K : analz (insert (Key (newK evt)) |
|
280 (insert (Key (serverKey C)) (sees Enemy evs))) ==> |
|
281 Key K : analz (insert (Key (serverKey C)) (sees Enemy evs)) |
|
282 |
|
283 A more general formula must be proved inductively. |
|
284 |
|
285 ****) |
|
286 |
|
287 |
|
288 (*NOT useful in this form, but it says that session keys are not used |
|
289 to encrypt messages containing other keys, in the actual protocol. |
|
290 We require that agents should behave like this subsequently also.*) |
|
291 goal thy |
|
292 "!!evs. evs : ns_shared ==> \ |
|
293 \ (Crypt X (newK evt)) : parts (sees Enemy evs) & \ |
|
294 \ Key K : parts {X} --> Key K : parts (sees Enemy evs)"; |
|
295 be ns_shared.induct 1; |
|
296 bd NS3_msg_in_parts_sees_Enemy 5; |
|
297 by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes))); |
|
298 (*Deals with Faked messages*) |
|
299 by (best_tac (!claset addSEs partsEs |
|
300 addDs [impOfSubs analz_subset_parts, |
|
301 impOfSubs parts_insert_subset_Un] |
|
302 addss (!simpset)) 1); |
|
303 (*NS4 and NS5*) |
|
304 by (ALLGOALS (fast_tac (!claset addss (!simpset)))); |
|
305 result(); |
|
306 |
|
307 |
|
308 (** Specialized rewriting for this proof **) |
|
309 |
|
310 Delsimps [image_insert]; |
|
311 Addsimps [image_insert RS sym]; |
|
312 |
|
313 goal thy "insert (Key (newK x)) (sees A evs) = \ |
|
314 \ Key `` (newK``{x}) Un (sees A evs)"; |
|
315 by (Fast_tac 1); |
|
316 val insert_Key_singleton = result(); |
|
317 |
|
318 goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \ |
|
319 \ Key `` (f `` (insert x E)) Un C"; |
|
320 by (Fast_tac 1); |
|
321 val insert_Key_image = result(); |
|
322 |
|
323 |
|
324 (** Session keys are not used to encrypt other session keys **) |
|
325 |
|
326 goal thy |
|
327 "!!evs. evs : ns_shared ==> \ |
|
328 \ ALL K E. (Key K : analz (insert (Key (serverKey C)) \ |
|
329 \ (Key``(newK``E) Un (sees Enemy evs)))) = \ |
|
330 \ (K : newK``E | \ |
|
331 \ Key K : analz (insert (Key (serverKey C)) \ |
|
332 \ (sees Enemy evs)))"; |
|
333 be ns_shared.induct 1; |
|
334 by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); |
|
335 by (REPEAT ((eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac) 5)); |
|
336 by (ALLGOALS |
|
337 (asm_simp_tac |
|
338 (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK] |
|
339 @ pushes) |
|
340 setloop split_tac [expand_if]))); |
|
341 (*Cases NS2 and NS3!! Simple, thanks to auto case splits*) |
|
342 by (REPEAT (Fast_tac 3)); |
|
343 (*Base case*) |
|
344 by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); |
|
345 (** LEVEL 7 **) |
|
346 (*Fake case*) |
|
347 by (REPEAT (Safe_step_tac 1)); |
|
348 by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 2); |
|
349 by (subgoal_tac |
|
350 "Key K : analz \ |
|
351 \ (synth \ |
|
352 \ (analz (insert (Key (serverKey C)) \ |
|
353 \ (Key``(newK``E) Un (sees Enemy evsa)))))" 1); |
|
354 (*First, justify this subgoal*) |
|
355 (*Discard formulae for better speed*) |
|
356 by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2); |
|
357 by (eres_inst_tac [("V","?Q ~: ?QQ")] thin_rl 2); |
|
358 by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)] |
|
359 addSEs [impOfSubs analz_mono]) 2); |
|
360 by (Asm_full_simp_tac 1); |
|
361 by (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1); |
|
362 qed_spec_mp "analz_image_newK"; |
|
363 |
|
364 |
|
365 goal thy |
|
366 "!!evs. evs : ns_shared ==> \ |
|
367 \ Key K : analz (insert (Key (newK evt)) \ |
|
368 \ (insert (Key (serverKey C)) \ |
|
369 \ (sees Enemy evs))) = \ |
|
370 \ (K = newK evt | \ |
|
371 \ Key K : analz (insert (Key (serverKey C)) \ |
|
372 \ (sees Enemy evs)))"; |
|
373 by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, |
|
374 insert_Key_singleton]) 1); |
|
375 by (Fast_tac 1); |
|
376 qed "analz_insert_Key_newK"; |
|
377 |
|
378 |
|
379 |
|
380 (*This says that the Key, K, uniquely identifies the message. |
|
381 But if C=Enemy then he could send all sorts of nonsense.*) |
|
382 goal thy |
|
383 "!!evs. evs : ns_shared ==> \ |
|
384 \ EX X'. ALL C S A Y N B X. \ |
|
385 \ C ~= Enemy --> \ |
|
386 \ Says S A Y : set_of_list evs --> \ |
|
387 \ ((Crypt {|N, Agent B, Key K, X|} (serverKey C)) : parts{Y} --> \ |
|
388 \ (X = X'))"; |
|
389 be ns_shared.induct 1; |
|
390 by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); |
|
391 by (ALLGOALS |
|
392 (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib]))); |
|
393 (*NS2: Case split propagates some context to other subgoal...*) |
|
394 by (excluded_middle_tac "K = newK evsa" 2); |
|
395 by (Asm_simp_tac 2); |
|
396 (*...we assume X is a very new message, and handle this case by contradiction*) |
|
397 by (fast_tac (!claset addIs [impOfSubs (subset_insertI RS parts_mono)] |
|
398 addSEs partsEs |
|
399 addEs [Says_imp_old_keys RS less_irrefl] |
|
400 addss (!simpset)) 2); |
|
401 (*NS3: No relevant messages*) |
|
402 by (fast_tac (!claset addSEs [exI] addss (!simpset)) 2); |
|
403 (*Fake*) |
|
404 by (Step_tac 1); |
|
405 br exI 1; |
|
406 br conjI 1; |
|
407 ba 2; |
|
408 by (Step_tac 1); |
|
409 (** LEVEL 12 **) |
|
410 by (subgoal_tac "Crypt {|N, Agent Ba, Key K, Xa|} (serverKey C) \ |
|
411 \ : parts (sees Enemy evsa)" 1); |
|
412 by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2); |
|
413 by (best_tac (!claset addSEs [impOfSubs analz_subset_parts] |
|
414 addDs [impOfSubs parts_insert_subset_Un] |
|
415 addss (!simpset)) 2); |
|
416 by (eres_inst_tac [("V","?aa : parts {X}")] thin_rl 1); |
|
417 bd parts_singleton 1; |
|
418 by (Step_tac 1); |
|
419 bd seesD 1; |
|
420 by (Step_tac 1); |
|
421 by (Full_simp_tac 2); |
|
422 by (fast_tac (!claset addSDs [spec]) 1); |
|
423 val lemma = result(); |
|
424 |
|
425 |
|
426 (*In messages of this form, the session key uniquely identifies the rest*) |
|
427 goal thy |
|
428 "!!evs. [| Says S A \ |
|
429 \ (Crypt {|N, Agent B, Key K, X|} (serverKey C)) \ |
|
430 \ : set_of_list evs; \ |
|
431 \ Says S' A' \ |
|
432 \ (Crypt {|N', Agent B', Key K, X'|} (serverKey C')) \ |
|
433 \ : set_of_list evs; \ |
|
434 \ evs : ns_shared; C ~= Enemy; C' ~= Enemy |] ==> X = X'"; |
|
435 bd lemma 1; |
|
436 be exE 1; |
|
437 by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1); |
|
438 by (Fast_tac 1); |
|
439 qed "unique_session_keys"; |
|
440 |
|
441 |
|
442 |
|
443 (*Crucial secrecy property: Enemy does not see the keys sent in msg NS2 |
|
444 -- even if another key is compromised*) |
|
445 goal thy |
|
446 "!!evs. [| Says Server (Friend i) \ |
|
447 \ (Crypt {|N, Agent(Friend j), K, X|} K') : set_of_list evs; \ |
|
448 \ evs : ns_shared; Friend i ~= C; Friend j ~= C \ |
|
449 \ |] ==> \ |
|
450 \ K ~: analz (insert (Key (serverKey C)) (sees Enemy evs))"; |
|
451 be rev_mp 1; |
|
452 be ns_shared.induct 1; |
|
453 by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes))); |
|
454 (*Next 3 steps infer that K has the form "Key (newK evs'" ... *) |
|
455 by (REPEAT_FIRST (resolve_tac [conjI, impI])); |
|
456 by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac)); |
|
457 by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac)); |
|
458 by (ALLGOALS |
|
459 (asm_full_simp_tac |
|
460 (!simpset addsimps ([analz_subset_parts RS contra_subsetD, |
|
461 analz_insert_Key_newK] @ pushes) |
|
462 setloop split_tac [expand_if]))); |
|
463 (*NS2*) |
|
464 by (fast_tac (!claset addSEs [less_irrefl]) 2); |
|
465 (** LEVEL 8 **) |
|
466 (*Now for the Fake case*) |
|
467 br notI 1; |
|
468 by (subgoal_tac |
|
469 "Key (newK evt) : \ |
|
470 \ analz (synth (analz (insert (Key (serverKey C)) \ |
|
471 \ (sees Enemy evsa))))" 1); |
|
472 be (impOfSubs analz_mono) 2; |
|
473 by (deepen_tac (!claset addIs [analz_mono RS synth_mono RSN (2,rev_subsetD), |
|
474 impOfSubs synth_increasing, |
|
475 impOfSubs analz_increasing]) 0 2); |
|
476 (*Proves the Fake goal*) |
|
477 by (fast_tac (!claset addss (!simpset)) 1); |
|
478 |
|
479 (**LEVEL 13**) |
|
480 (*NS3: that message from the Server was sent earlier*) |
|
481 by (mp_tac 1); |
|
482 by (forward_tac [Says_S_message_form] 1 THEN assume_tac 1); |
|
483 by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac)); |
|
484 by (asm_full_simp_tac |
|
485 (!simpset addsimps (mem_if::analz_insert_Key_newK::pushes)) 1); |
|
486 by (Step_tac 1); |
|
487 (**LEVEL 18 **) |
|
488 bd unique_session_keys 1; |
|
489 by (REPEAT_FIRST assume_tac); |
|
490 by (ALLGOALS Full_simp_tac); |
|
491 by (Step_tac 1); |
|
492 by (asm_full_simp_tac (!simpset addsimps [serverKey_mem_analz]) 1); |
|
493 qed "Enemy_not_see_encrypted_key"; |
|
494 |
|
495 |
|
496 |
|
497 |