|
1 (* Title: HOL/Auth/NS_Public |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1996 University of Cambridge |
|
5 |
|
6 Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol. |
|
7 Version incorporating Lowe's fix (inclusion of B's identify in round 2). |
|
8 *) |
|
9 |
|
10 open NS_Public; |
|
11 |
|
12 proof_timing:=true; |
|
13 HOL_quantifiers := false; |
|
14 Pretty.setdepth 20; |
|
15 |
|
16 AddIffs [Spy_in_lost]; |
|
17 |
|
18 (*Replacing the variable by a constant improves search speed by 50%!*) |
|
19 val Says_imp_sees_Spy' = |
|
20 read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy; |
|
21 |
|
22 |
|
23 (*A "possibility property": there are traces that reach the end*) |
|
24 goal thy |
|
25 "!!A B. A ~= B ==> EX NB. EX evs: ns_public. \ |
|
26 \ Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs"; |
|
27 by (REPEAT (resolve_tac [exI,bexI] 1)); |
|
28 by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2); |
|
29 by (ALLGOALS (simp_tac (!simpset setsolver safe_solver))); |
|
30 by (REPEAT_FIRST (resolve_tac [refl, conjI])); |
|
31 by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver)))); |
|
32 result(); |
|
33 |
|
34 |
|
35 (**** Inductive proofs about ns_public ****) |
|
36 |
|
37 (*Nobody sends themselves messages*) |
|
38 goal thy "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set_of_list evs"; |
|
39 by (etac ns_public.induct 1); |
|
40 by (Auto_tac()); |
|
41 qed_spec_mp "not_Says_to_self"; |
|
42 Addsimps [not_Says_to_self]; |
|
43 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
|
44 |
|
45 |
|
46 (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) |
|
47 fun parts_induct_tac i = SELECT_GOAL |
|
48 (DETERM (etac ns_public.induct 1 THEN |
|
49 (*Fake message*) |
|
50 TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, |
|
51 impOfSubs Fake_parts_insert] |
|
52 addss (!simpset)) 2)) THEN |
|
53 (*Base case*) |
|
54 fast_tac (!claset addss (!simpset)) 1 THEN |
|
55 ALLGOALS Asm_simp_tac) i; |
|
56 |
|
57 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY |
|
58 sends messages containing X! **) |
|
59 |
|
60 (*Spy never sees another agent's private key! (unless it's lost at start)*) |
|
61 goal thy |
|
62 "!!evs. evs : ns_public \ |
|
63 \ ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)"; |
|
64 by (parts_induct_tac 1); |
|
65 by (Auto_tac()); |
|
66 qed "Spy_see_priK"; |
|
67 Addsimps [Spy_see_priK]; |
|
68 |
|
69 goal thy |
|
70 "!!evs. evs : ns_public \ |
|
71 \ ==> (Key (priK A) : analz (sees lost Spy evs)) = (A : lost)"; |
|
72 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); |
|
73 qed "Spy_analz_priK"; |
|
74 Addsimps [Spy_analz_priK]; |
|
75 |
|
76 goal thy "!!A. [| Key (priK A) : parts (sees lost Spy evs); \ |
|
77 \ evs : ns_public |] ==> A:lost"; |
|
78 by (fast_tac (!claset addDs [Spy_see_priK]) 1); |
|
79 qed "Spy_see_priK_D"; |
|
80 |
|
81 bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D); |
|
82 AddSDs [Spy_see_priK_D, Spy_analz_priK_D]; |
|
83 |
|
84 |
|
85 (*** Future nonces can't be seen or used! ***) |
|
86 |
|
87 goal thy "!!evs. evs : ns_public ==> \ |
|
88 \ length evs <= length evt --> \ |
|
89 \ Nonce (newN evt) ~: parts (sees lost Spy evs)"; |
|
90 by (parts_induct_tac 1); |
|
91 by (REPEAT_FIRST (fast_tac (!claset |
|
92 addSEs partsEs |
|
93 addSDs [Says_imp_sees_Spy' RS parts.Inj] |
|
94 addEs [leD RS notE] |
|
95 addDs [impOfSubs analz_subset_parts, |
|
96 impOfSubs parts_insert_subset_Un, |
|
97 Suc_leD] |
|
98 addss (!simpset)))); |
|
99 qed_spec_mp "new_nonces_not_seen"; |
|
100 Addsimps [new_nonces_not_seen]; |
|
101 |
|
102 val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE); |
|
103 |
|
104 |
|
105 (**** Authenticity properties obtained from NS2 ****) |
|
106 |
|
107 (*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce |
|
108 is secret. (Honest users generate fresh nonces.)*) |
|
109 goal thy |
|
110 "!!evs. evs : ns_public \ |
|
111 \ ==> Nonce NA ~: analz (sees lost Spy evs) --> \ |
|
112 \ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \ |
|
113 \ Crypt (pubK C) {|X, Nonce NA, Agent D|} ~: parts (sees lost Spy evs)"; |
|
114 by (etac ns_public.induct 1); |
|
115 by (ALLGOALS |
|
116 (asm_simp_tac |
|
117 (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes) |
|
118 setloop split_tac [expand_if]))); |
|
119 (*NS3*) |
|
120 by (fast_tac (!claset addSEs partsEs |
|
121 addEs [nonce_not_seen_now]) 4); |
|
122 (*NS2*) |
|
123 by (fast_tac (!claset addSEs partsEs |
|
124 addEs [nonce_not_seen_now]) 3); |
|
125 (*Fake*) |
|
126 by (best_tac (!claset addIs [impOfSubs (subset_insertI RS analz_mono)] |
|
127 addDs [impOfSubs analz_subset_parts, |
|
128 impOfSubs Fake_parts_insert] |
|
129 addss (!simpset)) 2); |
|
130 (*Base*) |
|
131 by (fast_tac (!claset addDs [impOfSubs analz_subset_parts] |
|
132 addss (!simpset)) 1); |
|
133 bind_thm ("no_nonce_NS1_NS2", result() RSN (2, rev_mp) RSN (2, rev_mp)); |
|
134 |
|
135 |
|
136 (*Uniqueness for NS1: nonce NA identifies agents A and B*) |
|
137 goal thy |
|
138 "!!evs. evs : ns_public \ |
|
139 \ ==> Nonce NA ~: analz (sees lost Spy evs) --> \ |
|
140 \ (EX A' B'. ALL A B. \ |
|
141 \ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \ |
|
142 \ A=A' & B=B')"; |
|
143 by (etac ns_public.induct 1); |
|
144 by (ALLGOALS |
|
145 (asm_simp_tac |
|
146 (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes) |
|
147 setloop split_tac [expand_if]))); |
|
148 (*NS1*) |
|
149 by (expand_case_tac "NA = ?y" 3 THEN |
|
150 REPEAT (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 3)); |
|
151 (*Base*) |
|
152 by (fast_tac (!claset addss (!simpset)) 1); |
|
153 (*Fake*) |
|
154 by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1); |
|
155 by (step_tac (!claset addSIs [impOfSubs (subset_insertI RS analz_mono)]) 1); |
|
156 by (ex_strip_tac 1); |
|
157 by (best_tac (!claset delrules [conjI] |
|
158 addDs [impOfSubs analz_subset_parts, |
|
159 impOfSubs Fake_parts_insert] |
|
160 addss (!simpset)) 1); |
|
161 val lemma = result(); |
|
162 |
|
163 goal thy |
|
164 "!!evs. [| Crypt(pubK B) {|Nonce NA, Agent A|} : parts(sees lost Spy evs); \ |
|
165 \ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(sees lost Spy evs); \ |
|
166 \ Nonce NA ~: analz (sees lost Spy evs); \ |
|
167 \ evs : ns_public |] \ |
|
168 \ ==> A=A' & B=B'"; |
|
169 by (dtac lemma 1); |
|
170 by (mp_tac 1); |
|
171 by (REPEAT (etac exE 1)); |
|
172 (*Duplicate the assumption*) |
|
173 by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1); |
|
174 by (fast_tac (!claset addSDs [spec]) 1); |
|
175 qed "unique_NA"; |
|
176 |
|
177 |
|
178 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*) |
|
179 goal thy |
|
180 "!!evs. [| A ~: lost; B ~: lost; evs : ns_public |] \ |
|
181 \ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs \ |
|
182 \ --> Nonce NA ~: analz (sees lost Spy evs)"; |
|
183 by (etac ns_public.induct 1); |
|
184 by (ALLGOALS |
|
185 (asm_simp_tac |
|
186 (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes) |
|
187 setloop split_tac [expand_if]))); |
|
188 (*NS3*) |
|
189 by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
|
190 addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4); |
|
191 (*NS1*) |
|
192 by (fast_tac (!claset addSEs partsEs |
|
193 addSDs [new_nonces_not_seen, |
|
194 Says_imp_sees_Spy' RS parts.Inj]) 2); |
|
195 (*Fake*) |
|
196 by (REPEAT_FIRST (rtac conjI ORELSE' spy_analz_tac)); |
|
197 (*NS2*) |
|
198 by (Step_tac 1); |
|
199 by (fast_tac (!claset addSEs partsEs |
|
200 addSDs [new_nonces_not_seen, |
|
201 Says_imp_sees_Spy' RS parts.Inj]) 2); |
|
202 by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
|
203 addDs [unique_NA]) 1); |
|
204 bind_thm ("Spy_not_see_NA", result() RSN (2, rev_mp)); |
|
205 |
|
206 |
|
207 (*Authentication for A: if she receives message 2 and has used NA |
|
208 to start a run, then B has sent message 2.*) |
|
209 goal thy |
|
210 "!!evs. [| A ~: lost; B ~: lost; evs : ns_public |] \ |
|
211 \ ==> Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|} \ |
|
212 \ : parts (sees lost Spy evs) \ |
|
213 \ --> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs \ |
|
214 \ --> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ |
|
215 \ : set_of_list evs"; |
|
216 by (etac ns_public.induct 1); |
|
217 by (ALLGOALS Asm_simp_tac); |
|
218 (*NS1*) |
|
219 by (fast_tac (!claset addSEs partsEs |
|
220 addSDs [new_nonces_not_seen, |
|
221 Says_imp_sees_Spy' RS parts.Inj]) 2); |
|
222 (*Fake*) |
|
223 by (REPEAT_FIRST (resolve_tac [impI, conjI])); |
|
224 by (fast_tac (!claset addss (!simpset)) 1); |
|
225 by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1)); |
|
226 by (best_tac (!claset addSIs [disjI2] |
|
227 addDs [impOfSubs analz_subset_parts, |
|
228 impOfSubs Fake_parts_insert] |
|
229 addss (!simpset)) 1); |
|
230 qed_spec_mp "NA_decrypt_imp_B_msg"; |
|
231 |
|
232 (*Corollary: if A receives B's message NS2 and the nonce NA agrees |
|
233 then that message really originated with B.*) |
|
234 goal thy |
|
235 "!!evs. [| Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ |
|
236 \ : set_of_list evs;\ |
|
237 \ Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs;\ |
|
238 \ A ~: lost; B ~: lost; evs : ns_public |] \ |
|
239 \ ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ |
|
240 \ : set_of_list evs"; |
|
241 by (fast_tac (!claset addSIs [NA_decrypt_imp_B_msg] |
|
242 addEs partsEs |
|
243 addDs [Says_imp_sees_Spy' RS parts.Inj]) 1); |
|
244 qed "A_trusts_NS2"; |
|
245 |
|
246 (*If the encrypted message appears then it originated with Alice in NS1*) |
|
247 goal thy |
|
248 "!!evs. evs : ns_public \ |
|
249 \ ==> Nonce NA ~: analz (sees lost Spy evs) --> \ |
|
250 \ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \ |
|
251 \ Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs"; |
|
252 by (etac ns_public.induct 1); |
|
253 by (ALLGOALS |
|
254 (asm_simp_tac |
|
255 (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes) |
|
256 setloop split_tac [expand_if]))); |
|
257 (*Fake*) |
|
258 by (best_tac (!claset addSIs [disjI2] |
|
259 addIs [impOfSubs (subset_insertI RS analz_mono)] |
|
260 addDs [impOfSubs analz_subset_parts, |
|
261 impOfSubs Fake_parts_insert] |
|
262 addss (!simpset)) 2); |
|
263 (*Base*) |
|
264 by (fast_tac (!claset addss (!simpset)) 1); |
|
265 qed_spec_mp "B_trusts_NS1"; |
|
266 |
|
267 |
|
268 |
|
269 (**** Authenticity properties obtained from NS2 ****) |
|
270 |
|
271 (*Uniqueness for NS2: nonce NB identifies nonce NA and agents A, B |
|
272 [unicity of B makes Lowe's fix work] |
|
273 [proof closely follows that for unique_NA] *) |
|
274 goal thy |
|
275 "!!evs. evs : ns_public \ |
|
276 \ ==> Nonce NB ~: analz (sees lost Spy evs) --> \ |
|
277 \ (EX A' NA' B'. ALL A NA B. \ |
|
278 \ Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|} \ |
|
279 \ : parts (sees lost Spy evs) --> A=A' & NA=NA' & B=B')"; |
|
280 by (etac ns_public.induct 1); |
|
281 by (ALLGOALS |
|
282 (asm_simp_tac |
|
283 (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes) |
|
284 setloop split_tac [expand_if]))); |
|
285 (*NS2*) |
|
286 by (expand_case_tac "NB = ?y" 3 THEN |
|
287 REPEAT (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 3)); |
|
288 (*Base*) |
|
289 by (fast_tac (!claset addss (!simpset)) 1); |
|
290 (*Fake*) |
|
291 by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1); |
|
292 by (step_tac (!claset addSIs [impOfSubs (subset_insertI RS analz_mono)]) 1); |
|
293 by (ex_strip_tac 1); |
|
294 by (best_tac (!claset delrules [conjI] |
|
295 addDs [impOfSubs analz_subset_parts, |
|
296 impOfSubs Fake_parts_insert] |
|
297 addss (!simpset)) 1); |
|
298 val lemma = result(); |
|
299 |
|
300 goal thy |
|
301 "!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|} \ |
|
302 \ : parts(sees lost Spy evs); \ |
|
303 \ Crypt(pubK A') {|Nonce NA', Nonce NB, Agent B'|} \ |
|
304 \ : parts(sees lost Spy evs); \ |
|
305 \ Nonce NB ~: analz (sees lost Spy evs); \ |
|
306 \ evs : ns_public |] \ |
|
307 \ ==> A=A' & NA=NA' & B=B'"; |
|
308 by (dtac lemma 1); |
|
309 by (mp_tac 1); |
|
310 by (REPEAT (etac exE 1)); |
|
311 (*Duplicate the assumption*) |
|
312 by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1); |
|
313 by (fast_tac (!claset addSDs [spec]) 1); |
|
314 qed "unique_NB"; |
|
315 |
|
316 |
|
317 (*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*) |
|
318 goal thy |
|
319 "!!evs. [| A ~: lost; B ~: lost; evs : ns_public |] \ |
|
320 \ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ |
|
321 \ : set_of_list evs \ |
|
322 \ --> Nonce NB ~: analz (sees lost Spy evs)"; |
|
323 by (etac ns_public.induct 1); |
|
324 by (ALLGOALS |
|
325 (asm_simp_tac |
|
326 (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes) |
|
327 setloop split_tac [expand_if]))); |
|
328 (*NS3*) |
|
329 by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
|
330 addDs [unique_NB]) 4); |
|
331 (*NS1*) |
|
332 by (fast_tac (!claset addSEs partsEs |
|
333 addSDs [new_nonces_not_seen, |
|
334 Says_imp_sees_Spy' RS parts.Inj]) 2); |
|
335 (*Fake*) |
|
336 by (REPEAT_FIRST (rtac conjI ORELSE' spy_analz_tac)); |
|
337 (*NS2*) |
|
338 by (Step_tac 1); |
|
339 by (fast_tac (!claset addSEs partsEs |
|
340 addSDs [new_nonces_not_seen, |
|
341 Says_imp_sees_Spy' RS parts.Inj]) 2); |
|
342 by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
|
343 addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1); |
|
344 bind_thm ("Spy_not_see_NB", result() RSN (2, rev_mp)); |
|
345 |
|
346 |
|
347 (*Matches only NS2, not NS1 (or NS3)*) |
|
348 val Says_imp_sees_Spy'' = |
|
349 read_instantiate [("X","Crypt ?K {|?XX,?YY,?ZZ|}")] Says_imp_sees_Spy'; |
|
350 |
|
351 |
|
352 (*Authentication for B: if he receives message 3 and has used NB |
|
353 in message 2, then A has sent message 3.*) |
|
354 goal thy |
|
355 "!!evs. [| A ~: lost; B ~: lost; evs : ns_public |] \ |
|
356 \ ==> Crypt (pubK B) (Nonce NB) : parts (sees lost Spy evs) \ |
|
357 \ --> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ |
|
358 \ : set_of_list evs \ |
|
359 \ --> Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs"; |
|
360 by (etac ns_public.induct 1); |
|
361 by (ALLGOALS Asm_simp_tac); |
|
362 (*NS1*) |
|
363 by (fast_tac (!claset addSEs partsEs |
|
364 addSDs [new_nonces_not_seen, |
|
365 Says_imp_sees_Spy' RS parts.Inj]) 2); |
|
366 (*Fake*) |
|
367 by (REPEAT_FIRST (resolve_tac [impI, conjI])); |
|
368 by (fast_tac (!claset addss (!simpset)) 1); |
|
369 by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); |
|
370 by (best_tac (!claset addSIs [disjI2] |
|
371 addDs [impOfSubs analz_subset_parts, |
|
372 impOfSubs Fake_parts_insert] |
|
373 addss (!simpset)) 1); |
|
374 (*NS3*) |
|
375 by (Step_tac 1); |
|
376 by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); |
|
377 by (best_tac (!claset addSDs [Says_imp_sees_Spy'' RS parts.Inj] |
|
378 addDs [unique_NB]) 1); |
|
379 qed_spec_mp "NB_decrypt_imp_A_msg"; |
|
380 |
|
381 (*Corollary: if B receives message NS3 and the nonce NB agrees |
|
382 then that message really originated with A.*) |
|
383 goal thy |
|
384 "!!evs. [| Says A' B (Crypt (pubK B) (Nonce NB)): set_of_list evs; \ |
|
385 \ Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ |
|
386 \ : set_of_list evs; \ |
|
387 \ A ~: lost; B ~: lost; evs : ns_public |] \ |
|
388 \ ==> Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs"; |
|
389 by (fast_tac (!claset addSIs [NB_decrypt_imp_A_msg] |
|
390 addEs partsEs |
|
391 addDs [Says_imp_sees_Spy' RS parts.Inj]) 1); |
|
392 qed "B_trusts_NS3"; |
|
393 |
|
394 |
|
395 (**** Overall guarantee for B*) |
|
396 |
|
397 (*If B receives NS3 and the nonce NB agrees with the nonce he joined with |
|
398 NA, then A initiated the run using NA. |
|
399 SAME PROOF AS NB_decrypt_imp_A_msg*) |
|
400 goal thy |
|
401 "!!evs. [| A ~: lost; B ~: lost; evs : ns_public |] \ |
|
402 \ ==> Crypt (pubK B) (Nonce NB) : parts (sees lost Spy evs) \ |
|
403 \ --> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ |
|
404 \ : set_of_list evs \ |
|
405 \ --> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs"; |
|
406 by (etac ns_public.induct 1); |
|
407 by (ALLGOALS Asm_simp_tac); |
|
408 (*Fake, NS2, NS3*) |
|
409 (*NS1*) |
|
410 by (fast_tac (!claset addSEs partsEs |
|
411 addSDs [new_nonces_not_seen, |
|
412 Says_imp_sees_Spy' RS parts.Inj]) 2); |
|
413 (*Fake*) |
|
414 by (REPEAT_FIRST (resolve_tac [impI, conjI])); |
|
415 by (fast_tac (!claset addss (!simpset)) 1); |
|
416 by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); |
|
417 by (best_tac (!claset addSIs [disjI2] |
|
418 addDs [impOfSubs analz_subset_parts, |
|
419 impOfSubs Fake_parts_insert] |
|
420 addss (!simpset)) 1); |
|
421 (*NS3*) |
|
422 by (Step_tac 1); |
|
423 by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); |
|
424 by (best_tac (!claset addSDs [Says_imp_sees_Spy'' RS parts.Inj] |
|
425 addDs [unique_NB]) 1); |
|
426 val lemma = result() RSN (2, rev_mp) RSN (2, rev_mp); |
|
427 |
|
428 goal thy |
|
429 "!!evs. [| Says A' B (Crypt (pubK B) (Nonce NB)): set_of_list evs; \ |
|
430 \ Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ |
|
431 \ : set_of_list evs; \ |
|
432 \ A ~: lost; B ~: lost; evs : ns_public |] \ |
|
433 \ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs"; |
|
434 by (fast_tac (!claset addSIs [lemma] |
|
435 addEs partsEs |
|
436 addDs [Says_imp_sees_Spy' RS parts.Inj]) 1); |
|
437 qed_spec_mp "B_trusts_protocol"; |
|
438 |