46 |
47 |
47 (** For reasoning about the encrypted portion of messages **) |
48 (** For reasoning about the encrypted portion of messages **) |
48 |
49 |
49 goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs ==> \ |
50 goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs ==> \ |
50 \ X : analz (sees lost Spy evs)"; |
51 \ X : analz (sees lost Spy evs)"; |
51 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); |
52 by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); |
52 qed "OR2_analz_sees_Spy"; |
53 qed "OR2_analz_sees_Spy"; |
53 |
54 |
54 goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set_of_list evs ==> \ |
55 goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set_of_list evs ==> \ |
55 \ X : analz (sees lost Spy evs)"; |
56 \ X : analz (sees lost Spy evs)"; |
56 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); |
57 by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); |
57 qed "OR4_analz_sees_Spy"; |
58 qed "OR4_analz_sees_Spy"; |
58 |
59 |
59 goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \ |
60 goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \ |
60 \ ==> K : parts (sees lost Spy evs)"; |
61 \ ==> K : parts (sees lost Spy evs)"; |
61 by (fast_tac (!claset addSEs sees_Spy_partsEs) 1); |
62 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); |
62 qed "Oops_parts_sees_Spy"; |
63 qed "Oops_parts_sees_Spy"; |
63 |
64 |
64 (*OR2_analz... and OR4_analz... let us treat those cases using the same |
65 (*OR2_analz... and OR4_analz... let us treat those cases using the same |
65 argument as for the Fake case. This is possible for most, but not all, |
66 argument as for the Fake case. This is possible for most, but not all, |
66 proofs: Fake does not invent new nonces (as in OR2), and of course Fake |
67 proofs: Fake does not invent new nonces (as in OR2), and of course Fake |
107 qed "Spy_analz_shrK"; |
108 qed "Spy_analz_shrK"; |
108 Addsimps [Spy_analz_shrK]; |
109 Addsimps [Spy_analz_shrK]; |
109 |
110 |
110 goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \ |
111 goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \ |
111 \ evs : otway |] ==> A:lost"; |
112 \ evs : otway |] ==> A:lost"; |
112 by (fast_tac (!claset addDs [Spy_see_shrK]) 1); |
113 by (blast_tac (!claset addDs [Spy_see_shrK]) 1); |
113 qed "Spy_see_shrK_D"; |
114 qed "Spy_see_shrK_D"; |
114 |
115 |
115 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); |
116 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); |
116 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; |
117 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; |
117 |
118 |
183 by analz_Fake_tac; |
184 by analz_Fake_tac; |
184 by (REPEAT_FIRST (resolve_tac [allI, impI])); |
185 by (REPEAT_FIRST (resolve_tac [allI, impI])); |
185 by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); |
186 by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); |
186 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); |
187 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); |
187 (*Base*) |
188 (*Base*) |
188 by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); |
189 by (blast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); |
189 (*Fake, OR2, OR4*) |
190 (*Fake, OR2, OR4*) |
190 by (REPEAT (spy_analz_tac 1)); |
191 by (REPEAT (spy_analz_tac 1)); |
191 qed_spec_mp "analz_image_freshK"; |
192 qed_spec_mp "analz_image_freshK"; |
192 |
193 |
193 |
194 |
209 by (etac otway.induct 1); |
210 by (etac otway.induct 1); |
210 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); |
211 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); |
211 by (Step_tac 1); |
212 by (Step_tac 1); |
212 (*Remaining cases: OR3 and OR4*) |
213 (*Remaining cases: OR3 and OR4*) |
213 by (ex_strip_tac 2); |
214 by (ex_strip_tac 2); |
214 by (Fast_tac 2); |
215 by (Blast_tac 2); |
215 by (expand_case_tac "K = ?y" 1); |
216 by (expand_case_tac "K = ?y" 1); |
216 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); |
217 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); |
217 (*...we assume X is a recent message, and handle this case by contradiction*) |
218 (*...we assume X is a recent message, and handle this case by contradiction*) |
218 by (fast_tac (!claset addSEs sees_Spy_partsEs |
219 by (blast_tac (!claset addSEs sees_Spy_partsEs |
219 delrules [conjI] (*prevent split-up into 4 subgoals*) |
220 delrules [conjI] (*prevent split-up into 4 subgoals*) |
220 addss (!simpset addsimps [parts_insertI])) 1); |
221 addss (!simpset addsimps [parts_insertI])) 1); |
221 val lemma = result(); |
222 val lemma = result(); |
222 |
223 |
223 goal thy |
224 goal thy |
243 by (ALLGOALS |
244 by (ALLGOALS |
244 (asm_simp_tac (!simpset addcongs [conj_cong] |
245 (asm_simp_tac (!simpset addcongs [conj_cong] |
245 addsimps [not_parts_not_analz, analz_insert_freshK] |
246 addsimps [not_parts_not_analz, analz_insert_freshK] |
246 setloop split_tac [expand_if]))); |
247 setloop split_tac [expand_if]))); |
247 (*OR3*) |
248 (*OR3*) |
248 by (fast_tac (!claset delrules [impCE] |
249 by (blast_tac (!claset delrules [impCE] |
249 addSEs sees_Spy_partsEs |
250 addSEs sees_Spy_partsEs |
250 addIs [impOfSubs analz_subset_parts] |
251 addIs [impOfSubs analz_subset_parts]) 3); |
251 addss (!simpset addsimps [parts_insert2])) 3); |
|
252 (*OR4, OR2, Fake*) |
252 (*OR4, OR2, Fake*) |
253 by (REPEAT_FIRST spy_analz_tac); |
253 by (REPEAT_FIRST spy_analz_tac); |
254 (*Oops*) (** LEVEL 5 **) |
254 (*Oops*) (** LEVEL 5 **) |
255 by (fast_tac (!claset delrules [disjE] |
255 by (blast_tac (!claset addSDs [unique_session_keys]) 1); |
256 addDs [unique_session_keys] addss (!simpset)) 1); |
|
257 val lemma = result() RS mp RS mp RSN(2,rev_notE); |
256 val lemma = result() RS mp RS mp RSN(2,rev_notE); |
258 |
257 |
259 goal thy |
258 goal thy |
260 "!!evs. [| Says Server B \ |
259 "!!evs. [| Says Server B \ |
261 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
260 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
262 \ Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs; \ |
261 \ Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs; \ |
263 \ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs; \ |
262 \ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs; \ |
264 \ A ~: lost; B ~: lost; evs : otway |] \ |
263 \ A ~: lost; B ~: lost; evs : otway |] \ |
265 \ ==> Key K ~: analz (sees lost Spy evs)"; |
264 \ ==> Key K ~: analz (sees lost Spy evs)"; |
266 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); |
265 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); |
267 by (fast_tac (!claset addSEs [lemma]) 1); |
266 by (blast_tac (!claset addSEs [lemma]) 1); |
268 qed "Spy_not_see_encrypted_key"; |
267 qed "Spy_not_see_encrypted_key"; |
269 |
268 |
270 |
269 |
271 (*** Attempting to prove stronger properties ***) |
270 (*** Attempting to prove stronger properties ***) |
272 |
271 |
280 \ : parts (sees lost Spy evs) --> \ |
279 \ : parts (sees lost Spy evs) --> \ |
281 \ Says A B {|NA, Agent A, Agent B, \ |
280 \ Says A B {|NA, Agent A, Agent B, \ |
282 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ |
281 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ |
283 \ : set_of_list evs"; |
282 \ : set_of_list evs"; |
284 by (parts_induct_tac 1); |
283 by (parts_induct_tac 1); |
285 by (Fast_tac 1); |
284 by (Blast_tac 1); |
286 qed_spec_mp "Crypt_imp_OR1"; |
285 qed_spec_mp "Crypt_imp_OR1"; |
287 |
286 |
288 |
287 |
289 (*Crucial property: If the encrypted message appears, and A has used NA |
288 (*Crucial property: If the encrypted message appears, and A has used NA |
290 to start a run, then it originated with the Server!*) |
289 to start a run, then it originated with the Server!*) |
301 \ Crypt (shrK A) {|NA, Key K|}, \ |
300 \ Crypt (shrK A) {|NA, Key K|}, \ |
302 \ Crypt (shrK B) {|NB, Key K|}|} \ |
301 \ Crypt (shrK B) {|NB, Key K|}|} \ |
303 \ : set_of_list evs)"; |
302 \ : set_of_list evs)"; |
304 by (parts_induct_tac 1); |
303 by (parts_induct_tac 1); |
305 (*OR1: it cannot be a new Nonce, contradiction.*) |
304 (*OR1: it cannot be a new Nonce, contradiction.*) |
306 by (fast_tac (!claset addSIs [parts_insertI] |
305 by (blast_tac (!claset addSIs [parts_insertI] |
307 addSEs sees_Spy_partsEs |
306 addSEs sees_Spy_partsEs) 1); |
308 addss (!simpset)) 1); |
|
309 (*OR4*) |
307 (*OR4*) |
310 by (REPEAT (Safe_step_tac 2)); |
308 by (REPEAT (Safe_step_tac 2)); |
311 by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3)); |
309 by (REPEAT (blast_tac (!claset addSDs [parts_cut]) 3)); |
312 by (fast_tac (!claset addSIs [Crypt_imp_OR1] |
310 by (blast_tac (!claset addSIs [Crypt_imp_OR1] |
313 addEs sees_Spy_partsEs) 2); |
311 addEs sees_Spy_partsEs) 2); |
314 (*OR3*) (** LEVEL 5 **) |
312 (*OR3*) (** LEVEL 5 **) |
315 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib]))); |
313 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib]))); |
316 by (step_tac (!claset delrules [disjCI, impCE]) 1); |
314 by (step_tac (!claset delrules [disjCI, impCE]) 1); |
317 (*The hypotheses at this point suggest an attack in which nonce NA is used |
315 (*The hypotheses at this point suggest an attack in which nonce NA is used |
318 in two different roles: |
316 in two different roles: |