34 |
38 |
35 (*Monotonicity*) |
39 (*Monotonicity*) |
36 goal thy "!!evs. lost' <= lost ==> otway lost' <= otway lost"; |
40 goal thy "!!evs. lost' <= lost ==> otway lost' <= otway lost"; |
37 by (rtac subsetI 1); |
41 by (rtac subsetI 1); |
38 by (etac otway.induct 1); |
42 by (etac otway.induct 1); |
39 by (REPEAT_FIRST |
43 by (ALLGOALS |
40 (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono) |
44 (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono) |
41 :: otway.intrs)))); |
45 :: otway.intrs)))); |
42 qed "otway_mono"; |
46 qed "otway_mono"; |
43 |
47 |
44 (*Nobody sends themselves messages*) |
48 (*Nobody sends themselves messages*) |
45 goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set_of_list evs"; |
49 goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set_of_list evs"; |
52 |
56 |
53 (** For reasoning about the encrypted portion of messages **) |
57 (** For reasoning about the encrypted portion of messages **) |
54 |
58 |
55 goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs \ |
59 goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs \ |
56 \ ==> X : analz (sees lost Spy evs)"; |
60 \ ==> X : analz (sees lost Spy evs)"; |
57 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); |
61 by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1); |
58 qed "OR2_analz_sees_Spy"; |
62 qed "OR2_analz_sees_Spy"; |
59 |
63 |
60 goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set_of_list evs \ |
64 goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set_of_list evs \ |
61 \ ==> X : analz (sees lost Spy evs)"; |
65 \ ==> X : analz (sees lost Spy evs)"; |
62 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); |
66 by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1); |
63 qed "OR4_analz_sees_Spy"; |
67 qed "OR4_analz_sees_Spy"; |
64 |
68 |
65 goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \ |
69 goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \ |
66 \ ==> K : parts (sees lost Spy evs)"; |
70 \ ==> K : parts (sees lost Spy evs)"; |
67 by (fast_tac (!claset addSEs sees_Spy_partsEs) 1); |
71 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); |
68 qed "Oops_parts_sees_Spy"; |
72 qed "Oops_parts_sees_Spy"; |
69 |
73 |
70 (*OR2_analz... and OR4_analz... let us treat those cases using the same |
74 (*OR2_analz... and OR4_analz... let us treat those cases using the same |
71 argument as for the Fake case. This is possible for most, but not all, |
75 argument as for the Fake case. This is possible for most, but not all, |
72 proofs: Fake does not invent new nonces (as in OR2), and of course Fake |
76 proofs: Fake does not invent new nonces (as in OR2), and of course Fake |
116 qed "Spy_analz_shrK"; |
120 qed "Spy_analz_shrK"; |
117 Addsimps [Spy_analz_shrK]; |
121 Addsimps [Spy_analz_shrK]; |
118 |
122 |
119 goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \ |
123 goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \ |
120 \ evs : otway lost |] ==> A:lost"; |
124 \ evs : otway lost |] ==> A:lost"; |
121 by (fast_tac (!claset addDs [Spy_see_shrK]) 1); |
125 by (blast_tac (!claset addDs [Spy_see_shrK]) 1); |
122 qed "Spy_see_shrK_D"; |
126 qed "Spy_see_shrK_D"; |
123 |
127 |
124 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); |
128 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); |
125 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; |
129 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; |
126 |
130 |
133 by (best_tac |
137 by (best_tac |
134 (!claset addIs [impOfSubs analz_subset_parts] |
138 (!claset addIs [impOfSubs analz_subset_parts] |
135 addDs [impOfSubs (analz_subset_parts RS keysFor_mono), |
139 addDs [impOfSubs (analz_subset_parts RS keysFor_mono), |
136 impOfSubs (parts_insert_subset_Un RS keysFor_mono)] |
140 impOfSubs (parts_insert_subset_Un RS keysFor_mono)] |
137 unsafe_addss (!simpset)) 1); |
141 unsafe_addss (!simpset)) 1); |
138 (*OR1-3*) |
142 by (ALLGOALS Blast_tac); |
139 by (REPEAT (fast_tac (!claset addss (!simpset)) 1)); |
|
140 qed_spec_mp "new_keys_not_used"; |
143 qed_spec_mp "new_keys_not_used"; |
141 |
144 |
142 bind_thm ("new_keys_not_analzd", |
145 bind_thm ("new_keys_not_analzd", |
143 [analz_subset_parts RS keysFor_mono, |
146 [analz_subset_parts RS keysFor_mono, |
144 new_keys_not_used] MRS contra_subsetD); |
147 new_keys_not_used] MRS contra_subsetD); |
156 \ {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs; \ |
159 \ {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs; \ |
157 \ evs : otway lost |] \ |
160 \ evs : otway lost |] \ |
158 \ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; |
161 \ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; |
159 by (etac rev_mp 1); |
162 by (etac rev_mp 1); |
160 by (etac otway.induct 1); |
163 by (etac otway.induct 1); |
161 by (ALLGOALS (fast_tac (!claset addss (!simpset)))); |
164 by (ALLGOALS Simp_tac); |
|
165 by (ALLGOALS Blast_tac); |
162 qed "Says_Server_message_form"; |
166 qed "Says_Server_message_form"; |
163 |
167 |
164 |
168 |
165 (*For proofs involving analz. We again instantiate the variable to "lost".*) |
169 (*For proofs involving analz. We again instantiate the variable to "lost".*) |
166 val analz_Fake_tac = |
170 val analz_Fake_tac = |
193 by analz_Fake_tac; |
197 by analz_Fake_tac; |
194 by (REPEAT_FIRST (resolve_tac [allI, impI])); |
198 by (REPEAT_FIRST (resolve_tac [allI, impI])); |
195 by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); |
199 by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); |
196 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); |
200 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); |
197 (*Base*) |
201 (*Base*) |
198 by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); |
202 by (Blast_tac 1); |
199 (*Fake, OR2, OR4*) |
203 (*Fake, OR2, OR4*) |
200 by (REPEAT (spy_analz_tac 1)); |
204 by (REPEAT (spy_analz_tac 1)); |
201 qed_spec_mp "analz_image_freshK"; |
205 qed_spec_mp "analz_image_freshK"; |
202 |
206 |
203 |
207 |
219 by (etac otway.induct 1); |
223 by (etac otway.induct 1); |
220 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); |
224 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); |
221 by (Step_tac 1); |
225 by (Step_tac 1); |
222 (*Remaining cases: OR3 and OR4*) |
226 (*Remaining cases: OR3 and OR4*) |
223 by (ex_strip_tac 2); |
227 by (ex_strip_tac 2); |
224 by (Fast_tac 2); |
228 by (Best_tac 2); |
225 by (expand_case_tac "K = ?y" 1); |
229 by (expand_case_tac "K = ?y" 1); |
226 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); |
230 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); |
227 (*...we assume X is a recent message, and handle this case by contradiction*) |
231 (*...we assume X is a recent message, and handle this case by contradiction*) |
228 by (fast_tac (!claset addSEs sees_Spy_partsEs |
232 by (blast_tac (!claset addSEs sees_Spy_partsEs |
229 delrules [conjI] (*prevent split-up into 4 subgoals*) |
233 delrules [conjI] (*no split-up into 4 subgoals*)) 1); |
230 addss (!simpset addsimps [parts_insertI])) 1); |
|
231 val lemma = result(); |
234 val lemma = result(); |
232 |
235 |
233 goal thy |
236 goal thy |
234 "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} \ |
237 "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} \ |
235 \ : set_of_list evs; \ |
238 \ : set_of_list evs; \ |
264 \ --> B = B'"; |
267 \ --> B = B'"; |
265 by (parts_induct_tac 1); |
268 by (parts_induct_tac 1); |
266 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); |
269 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); |
267 (*OR1: creation of new Nonce. Move assertion into global context*) |
270 (*OR1: creation of new Nonce. Move assertion into global context*) |
268 by (expand_case_tac "NA = ?y" 1); |
271 by (expand_case_tac "NA = ?y" 1); |
269 by (best_tac (!claset addSEs sees_Spy_partsEs) 1); |
272 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); |
270 val lemma = result(); |
273 val lemma = result(); |
271 |
274 |
272 goal thy |
275 goal thy |
273 "!!evs.[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts(sees lost Spy evs); \ |
276 "!!evs.[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts(sees lost Spy evs); \ |
274 \ Crypt (shrK A) {|NA, Agent A, Agent C|}: parts(sees lost Spy evs); \ |
277 \ Crypt (shrK A) {|NA, Agent A, Agent C|}: parts(sees lost Spy evs); \ |
286 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \ |
289 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \ |
287 \ : parts (sees lost Spy evs) --> \ |
290 \ : parts (sees lost Spy evs) --> \ |
288 \ Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \ |
291 \ Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \ |
289 \ ~: parts (sees lost Spy evs)"; |
292 \ ~: parts (sees lost Spy evs)"; |
290 by (parts_induct_tac 1); |
293 by (parts_induct_tac 1); |
291 by (REPEAT (fast_tac (!claset addSEs sees_Spy_partsEs |
294 by (REPEAT (blast_tac (!claset addSEs sees_Spy_partsEs |
292 addSDs [impOfSubs parts_insert_subset_Un] |
295 addSDs [impOfSubs parts_insert_subset_Un]) 1)); |
293 addss (!simpset)) 1)); |
|
294 qed_spec_mp"no_nonce_OR1_OR2"; |
296 qed_spec_mp"no_nonce_OR1_OR2"; |
295 |
297 |
296 |
298 |
297 (*Crucial property: If the encrypted message appears, and A has used NA |
299 (*Crucial property: If the encrypted message appears, and A has used NA |
298 to start a run, then it originated with the Server!*) |
300 to start a run, then it originated with the Server!*) |
307 \ Crypt (shrK A) {|NA, Key K|}, \ |
309 \ Crypt (shrK A) {|NA, Key K|}, \ |
308 \ Crypt (shrK B) {|NB, Key K|}|} \ |
310 \ Crypt (shrK B) {|NB, Key K|}|} \ |
309 \ : set_of_list evs)"; |
311 \ : set_of_list evs)"; |
310 by (parts_induct_tac 1); |
312 by (parts_induct_tac 1); |
311 (*OR1: it cannot be a new Nonce, contradiction.*) |
313 (*OR1: it cannot be a new Nonce, contradiction.*) |
312 by (fast_tac (!claset addSIs [parts_insertI] |
314 by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1); |
313 addSEs sees_Spy_partsEs |
|
314 addss (!simpset)) 1); |
|
315 (*OR3 and OR4*) |
315 (*OR3 and OR4*) |
316 (*OR4*) |
316 (*OR4*) |
317 by (REPEAT (Safe_step_tac 2)); |
317 by (REPEAT (Safe_step_tac 2)); |
318 by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3)); |
318 by (REPEAT (blast_tac (!claset addSDs [parts_cut]) 3)); |
319 by (fast_tac (!claset addSIs [Crypt_imp_OR1] |
319 by (fast_tac (!claset addSIs [Crypt_imp_OR1] |
320 addEs sees_Spy_partsEs) 2); |
320 addEs sees_Spy_partsEs) 2); |
321 (*OR3*) (** LEVEL 5 **) |
321 (*OR3*) (** LEVEL 5 **) |
322 by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1); |
322 by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1); |
323 by (step_tac (!claset delrules [disjCI, impCE]) 1); |
323 by (step_tac (!claset delrules [disjCI, impCE]) 1); |
324 by (fast_tac (!claset addSEs [MPair_parts] |
324 by (blast_tac (!claset addSEs [MPair_parts] |
325 addSDs [Says_imp_sees_Spy RS parts.Inj] |
325 addSDs [Says_imp_sees_Spy' RS parts.Inj] |
326 addEs [no_nonce_OR1_OR2 RSN (2, rev_notE)] |
326 addEs [no_nonce_OR1_OR2 RSN (2, rev_notE)] |
327 delrules [conjI] (*stop split-up into 4 subgoals*)) 2); |
327 delrules [conjI] (*stop split-up into 4 subgoals*)) 2); |
328 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj] |
328 by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
329 addSEs [MPair_parts] |
329 addSEs [MPair_parts] |
330 addEs [unique_NA]) 1); |
330 addIs [unique_NA]) 1); |
331 qed_spec_mp "NA_Crypt_imp_Server_msg"; |
331 qed_spec_mp "NA_Crypt_imp_Server_msg"; |
332 |
332 |
333 |
333 |
334 (*Corollary: if A receives B's OR4 message and the nonce NA agrees |
334 (*Corollary: if A receives B's OR4 message and the nonce NA agrees |
335 then the key really did come from the Server! CANNOT prove this of the |
335 then the key really did come from the Server! CANNOT prove this of the |
345 \ ==> EX NB. Says Server B \ |
345 \ ==> EX NB. Says Server B \ |
346 \ {|NA, \ |
346 \ {|NA, \ |
347 \ Crypt (shrK A) {|NA, Key K|}, \ |
347 \ Crypt (shrK A) {|NA, Key K|}, \ |
348 \ Crypt (shrK B) {|NB, Key K|}|} \ |
348 \ Crypt (shrK B) {|NB, Key K|}|} \ |
349 \ : set_of_list evs"; |
349 \ : set_of_list evs"; |
350 by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg] |
350 by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg] |
351 addEs sees_Spy_partsEs) 1); |
351 addEs sees_Spy_partsEs) 1); |
352 qed "A_trusts_OR4"; |
352 qed "A_trusts_OR4"; |
353 |
353 |
354 |
354 |
355 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3 |
355 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3 |
356 Does not in itself guarantee security: an attack could violate |
356 Does not in itself guarantee security: an attack could violate |
368 by (ALLGOALS |
368 by (ALLGOALS |
369 (asm_simp_tac (!simpset addcongs [conj_cong] |
369 (asm_simp_tac (!simpset addcongs [conj_cong] |
370 addsimps [not_parts_not_analz, analz_insert_freshK] |
370 addsimps [not_parts_not_analz, analz_insert_freshK] |
371 setloop split_tac [expand_if]))); |
371 setloop split_tac [expand_if]))); |
372 (*OR3*) |
372 (*OR3*) |
373 by (fast_tac (!claset delrules [impCE] |
373 by (blast_tac (!claset delrules [impCE] |
374 addSEs sees_Spy_partsEs |
374 addSEs sees_Spy_partsEs |
375 addIs [impOfSubs analz_subset_parts] |
375 addIs [impOfSubs analz_subset_parts]) 3); |
376 addss (!simpset addsimps [parts_insert2])) 3); |
|
377 (*OR4, OR2, Fake*) |
376 (*OR4, OR2, Fake*) |
378 by (REPEAT_FIRST spy_analz_tac); |
377 by (REPEAT_FIRST spy_analz_tac); |
379 (*Oops*) (** LEVEL 5 **) |
378 (*Oops*) (** LEVEL 5 **) |
380 by (fast_tac (!claset delrules [disjE] |
379 by (blast_tac (!claset addSDs [unique_session_keys]) 1); |
381 addDs [unique_session_keys] addss (!simpset)) 1); |
|
382 val lemma = result() RS mp RS mp RSN(2,rev_notE); |
380 val lemma = result() RS mp RS mp RSN(2,rev_notE); |
383 |
381 |
384 goal thy |
382 goal thy |
385 "!!evs. [| Says Server B \ |
383 "!!evs. [| Says Server B \ |
386 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
384 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
387 \ Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs; \ |
385 \ Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs; \ |
388 \ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs; \ |
386 \ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs; \ |
389 \ A ~: lost; B ~: lost; evs : otway lost |] \ |
387 \ A ~: lost; B ~: lost; evs : otway lost |] \ |
390 \ ==> Key K ~: analz (sees lost Spy evs)"; |
388 \ ==> Key K ~: analz (sees lost Spy evs)"; |
391 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); |
389 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); |
392 by (fast_tac (!claset addSEs [lemma]) 1); |
390 by (blast_tac (!claset addSEs [lemma]) 1); |
393 qed "Spy_not_see_encrypted_key"; |
391 qed "Spy_not_see_encrypted_key"; |
394 |
392 |
395 |
393 |
396 goal thy |
394 goal thy |
397 "!!evs. [| C ~: {A,B,Server}; \ |
395 "!!evs. [| C ~: {A,B,Server}; \ |
402 \ A ~: lost; B ~: lost; evs : otway lost |] \ |
400 \ A ~: lost; B ~: lost; evs : otway lost |] \ |
403 \ ==> Key K ~: analz (sees lost C evs)"; |
401 \ ==> Key K ~: analz (sees lost C evs)"; |
404 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1); |
402 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1); |
405 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1); |
403 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1); |
406 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key)); |
404 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key)); |
407 by (REPEAT_FIRST (fast_tac (!claset addIs [otway_mono RS subsetD]))); |
405 by (REPEAT_FIRST (blast_tac (!claset addIs [otway_mono RS subsetD]))); |
408 qed "Agent_not_see_encrypted_key"; |
406 qed "Agent_not_see_encrypted_key"; |
409 |
407 |
410 |
408 |
411 (**** Authenticity properties relating to NB ****) |
409 (**** Authenticity properties relating to NB ****) |
412 |
410 |
419 \ (EX X. Says B Server \ |
417 \ (EX X. Says B Server \ |
420 \ {|NA, Agent A, Agent B, X, \ |
418 \ {|NA, Agent A, Agent B, X, \ |
421 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \ |
419 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \ |
422 \ : set_of_list evs)"; |
420 \ : set_of_list evs)"; |
423 by (parts_induct_tac 1); |
421 by (parts_induct_tac 1); |
424 by (auto_tac (!claset, !simpset addcongs [conj_cong])); |
422 by (ALLGOALS Blast_tac); |
425 bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE); |
423 bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE); |
426 |
424 |
427 |
425 |
428 (** The Nonce NB uniquely identifies B's message. **) |
426 (** The Nonce NB uniquely identifies B's message. **) |
429 |
427 |
434 \ --> NA = NA' & A = A'"; |
432 \ --> NA = NA' & A = A'"; |
435 by (parts_induct_tac 1); |
433 by (parts_induct_tac 1); |
436 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); |
434 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); |
437 (*OR2: creation of new Nonce. Move assertion into global context*) |
435 (*OR2: creation of new Nonce. Move assertion into global context*) |
438 by (expand_case_tac "NB = ?y" 1); |
436 by (expand_case_tac "NB = ?y" 1); |
439 by (deepen_tac (!claset addSEs sees_Spy_partsEs) 3 1); |
437 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); |
440 val lemma = result(); |
438 val lemma = result(); |
441 |
439 |
442 goal thy |
440 goal thy |
443 "!!evs.[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \ |
441 "!!evs.[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \ |
444 \ : parts(sees lost Spy evs); \ |
442 \ : parts(sees lost Spy evs); \ |
463 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
461 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
464 \ Crypt (shrK B) {|NB, Key K|}|} \ |
462 \ Crypt (shrK B) {|NB, Key K|}|} \ |
465 \ : set_of_list evs)"; |
463 \ : set_of_list evs)"; |
466 by (parts_induct_tac 1); |
464 by (parts_induct_tac 1); |
467 (*OR1: it cannot be a new Nonce, contradiction.*) |
465 (*OR1: it cannot be a new Nonce, contradiction.*) |
468 by (fast_tac (!claset addSIs [parts_insertI] |
466 by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1); |
469 addSEs sees_Spy_partsEs |
|
470 addss (!simpset)) 1); |
|
471 (*OR4*) |
467 (*OR4*) |
472 by (fast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2); |
468 by (blast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2); |
473 (*OR3*) |
469 (*OR3*) |
474 by (step_tac (!claset delrules [disjCI, impCE]) 1); |
470 by (step_tac (!claset delrules [disjCI, impCE]) 1); |
475 by (fast_tac (!claset delrules [conjI] (*stop split-up*)) 3); |
471 by (blast_tac (!claset delrules [conjI] (*stop split-up*)) 3); |
476 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj] |
472 by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
477 addSEs [MPair_parts] |
473 addSEs [MPair_parts] |
478 addDs [unique_NB]) 2); |
474 addDs [unique_NB]) 2); |
479 by (fast_tac (!claset addSEs [MPair_parts] |
475 by (blast_tac (!claset addSEs [MPair_parts, no_nonce_OR1_OR2 RSN (2, rev_notE)] |
480 addSDs [Says_imp_sees_Spy RS parts.Inj] |
476 addSDs [Says_imp_sees_Spy' RS parts.Inj] |
481 addSEs [no_nonce_OR1_OR2 RSN (2, rev_notE)] |
477 delrules [conjI, impCE] (*stop split-up*)) 1); |
482 delrules [conjI, impCE] (*stop split-up*)) 1); |
|
483 qed_spec_mp "NB_Crypt_imp_Server_msg"; |
478 qed_spec_mp "NB_Crypt_imp_Server_msg"; |
484 |
479 |
485 |
480 |
486 (*Guarantee for B: if it gets a message with matching NB then the Server |
481 (*Guarantee for B: if it gets a message with matching NB then the Server |
487 has sent the correct message.*) |
482 has sent the correct message.*) |
495 \ ==> Says Server B \ |
490 \ ==> Says Server B \ |
496 \ {|NA, \ |
491 \ {|NA, \ |
497 \ Crypt (shrK A) {|NA, Key K|}, \ |
492 \ Crypt (shrK A) {|NA, Key K|}, \ |
498 \ Crypt (shrK B) {|NB, Key K|}|} \ |
493 \ Crypt (shrK B) {|NB, Key K|}|} \ |
499 \ : set_of_list evs"; |
494 \ : set_of_list evs"; |
500 by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg] |
495 by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg] |
501 addEs sees_Spy_partsEs) 1); |
496 addSEs sees_Spy_partsEs) 1); |
502 qed "B_trusts_OR3"; |
497 qed "B_trusts_OR3"; |
503 |
498 |
504 |
499 |
505 B_trusts_OR3 RS Spy_not_see_encrypted_key; |
500 B_trusts_OR3 RS Spy_not_see_encrypted_key; |
506 |
501 |
512 \ Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs --> \ |
507 \ Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs --> \ |
513 \ (EX X. Says B Server {|NA, Agent A, Agent B, X, \ |
508 \ (EX X. Says B Server {|NA, Agent A, Agent B, X, \ |
514 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ |
509 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ |
515 \ : set_of_list evs)"; |
510 \ : set_of_list evs)"; |
516 by (etac otway.induct 1); |
511 by (etac otway.induct 1); |
517 by (Auto_tac()); |
512 by (ALLGOALS Asm_simp_tac); |
518 by (dtac (Says_imp_sees_Spy RS parts.Inj) 1); |
513 by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj] |
519 by (fast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 1); |
514 addSEs [MPair_parts, Crypt_imp_OR2]) 3); |
|
515 by (ALLGOALS Blast_tac); |
520 bind_thm ("OR3_imp_OR2", result() RSN (2,rev_mp) RS exE); |
516 bind_thm ("OR3_imp_OR2", result() RSN (2,rev_mp) RS exE); |
521 |
517 |
522 |
518 |
523 (*After getting and checking OR4, agent A can trust that B has been active. |
519 (*After getting and checking OR4, agent A can trust that B has been active. |
524 We could probably prove that X has the expected form, but that is not |
520 We could probably prove that X has the expected form, but that is not |
531 \ : set_of_list evs; \ |
527 \ : set_of_list evs; \ |
532 \ A ~: lost; A ~= Spy; B ~: lost; evs : otway lost |] \ |
528 \ A ~: lost; A ~= Spy; B ~: lost; evs : otway lost |] \ |
533 \ ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X, \ |
529 \ ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X, \ |
534 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}\ |
530 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}\ |
535 \ : set_of_list evs"; |
531 \ : set_of_list evs"; |
536 by (fast_tac (!claset addSDs [A_trusts_OR4] |
532 by (blast_tac (!claset addSDs [A_trusts_OR4] |
537 addSEs [OR3_imp_OR2]) 1); |
533 addSEs [OR3_imp_OR2]) 1); |
538 qed "A_auths_B"; |
534 qed "A_auths_B"; |