110 qed "respond_imp_responses"; |
110 qed "respond_imp_responses"; |
111 |
111 |
112 |
112 |
113 (** For reasoning about the encrypted portion of messages **) |
113 (** For reasoning about the encrypted portion of messages **) |
114 |
114 |
115 val RA2_analz_sees_Spy = Says_imp_sees_Spy RS analz.Inj |> standard; |
115 val RA2_analz_spies = Says_imp_spies RS analz.Inj |> standard; |
116 |
116 |
117 goal thy "!!evs. Says C' B {|Crypt K X, X', RA|} : set evs \ |
117 goal thy "!!evs. Says C' B {|Crypt K X, X', RA|} : set evs \ |
118 \ ==> RA : analz (sees Spy evs)"; |
118 \ ==> RA : analz (spies evs)"; |
119 by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); |
119 by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1); |
120 qed "RA4_analz_sees_Spy"; |
120 qed "RA4_analz_spies"; |
121 |
121 |
122 (*RA2_analz... and RA4_analz... let us treat those cases using the same |
122 (*RA2_analz... and RA4_analz... let us treat those cases using the same |
123 argument as for the Fake case. This is possible for most, but not all, |
123 argument as for the Fake case. This is possible for most, but not all, |
124 proofs: Fake does not invent new nonces (as in RA2), and of course Fake |
124 proofs: Fake does not invent new nonces (as in RA2), and of course Fake |
125 messages originate from the Spy. *) |
125 messages originate from the Spy. *) |
126 |
126 |
127 bind_thm ("RA2_parts_sees_Spy", |
127 bind_thm ("RA2_parts_spies", |
128 RA2_analz_sees_Spy RS (impOfSubs analz_subset_parts)); |
128 RA2_analz_spies RS (impOfSubs analz_subset_parts)); |
129 bind_thm ("RA4_parts_sees_Spy", |
129 bind_thm ("RA4_parts_spies", |
130 RA4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); |
130 RA4_analz_spies RS (impOfSubs analz_subset_parts)); |
131 |
131 |
132 (*For proving the easier theorems about X ~: parts (sees Spy evs).*) |
132 (*For proving the easier theorems about X ~: parts (spies evs).*) |
133 fun parts_induct_tac i = |
133 fun parts_induct_tac i = |
134 etac recur.induct i THEN |
134 etac recur.induct i THEN |
135 forward_tac [RA2_parts_sees_Spy] (i+3) THEN |
135 forward_tac [RA2_parts_spies] (i+3) THEN |
136 etac subst (i+3) (*RA2: DELETE needless definition of PA!*) THEN |
136 etac subst (i+3) (*RA2: DELETE needless definition of PA!*) THEN |
137 forward_tac [respond_imp_responses] (i+4) THEN |
137 forward_tac [respond_imp_responses] (i+4) THEN |
138 forward_tac [RA4_parts_sees_Spy] (i+5) THEN |
138 forward_tac [RA4_parts_spies] (i+5) THEN |
139 prove_simple_subgoals_tac i; |
139 prove_simple_subgoals_tac i; |
140 |
140 |
141 |
141 |
142 (** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY |
142 (** Theorems of the form X ~: parts (spies evs) imply that NOBODY |
143 sends messages containing X! **) |
143 sends messages containing X! **) |
144 |
144 |
145 |
145 |
146 (** Spy never sees another agent's shared key! (unless it's lost at start) **) |
146 (** Spy never sees another agent's shared key! (unless it's bad at start) **) |
147 |
147 |
148 goal thy |
148 goal thy |
149 "!!evs. evs : recur ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)"; |
149 "!!evs. evs : recur ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; |
150 by (parts_induct_tac 1); |
150 by (parts_induct_tac 1); |
151 by (Fake_parts_insert_tac 1); |
151 by (Fake_parts_insert_tac 1); |
152 by (ALLGOALS |
152 by (ALLGOALS |
153 (asm_simp_tac (!simpset addsimps [parts_insert2, parts_insert_sees]))); |
153 (asm_simp_tac (!simpset addsimps [parts_insert2, parts_insert_spies]))); |
154 (*RA3*) |
154 (*RA3*) |
155 by (blast_tac (!claset addDs [Key_in_parts_respond]) 2); |
155 by (blast_tac (!claset addDs [Key_in_parts_respond]) 2); |
156 (*RA2*) |
156 (*RA2*) |
157 by (blast_tac (!claset addSEs partsEs addDs [parts_cut]) 1); |
157 by (blast_tac (!claset addSEs partsEs addDs [parts_cut]) 1); |
158 qed "Spy_see_shrK"; |
158 qed "Spy_see_shrK"; |
159 Addsimps [Spy_see_shrK]; |
159 Addsimps [Spy_see_shrK]; |
160 |
160 |
161 goal thy |
161 goal thy |
162 "!!evs. evs : recur ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)"; |
162 "!!evs. evs : recur ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; |
163 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); |
163 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); |
164 qed "Spy_analz_shrK"; |
164 qed "Spy_analz_shrK"; |
165 Addsimps [Spy_analz_shrK]; |
165 Addsimps [Spy_analz_shrK]; |
166 |
166 |
167 goal thy "!!A. [| Key (shrK A) : parts (sees Spy evs); \ |
167 goal thy "!!A. [| Key (shrK A) : parts (spies evs); evs : recur |] ==> A:bad"; |
168 \ evs : recur |] ==> A:lost"; |
|
169 by (blast_tac (!claset addDs [Spy_see_shrK]) 1); |
168 by (blast_tac (!claset addDs [Spy_see_shrK]) 1); |
170 qed "Spy_see_shrK_D"; |
169 qed "Spy_see_shrK_D"; |
171 |
170 |
172 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); |
171 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); |
173 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; |
172 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; |
209 |
208 |
210 |
209 |
211 (*** Proofs involving analz ***) |
210 (*** Proofs involving analz ***) |
212 |
211 |
213 (*For proofs involving analz.*) |
212 (*For proofs involving analz.*) |
214 val analz_sees_tac = |
213 val analz_spies_tac = |
215 etac subst 4 (*RA2: DELETE needless definition of PA!*) THEN |
214 etac subst 4 (*RA2: DELETE needless definition of PA!*) THEN |
216 dtac RA2_analz_sees_Spy 4 THEN |
215 dtac RA2_analz_spies 4 THEN |
217 forward_tac [respond_imp_responses] 5 THEN |
216 forward_tac [respond_imp_responses] 5 THEN |
218 dtac RA4_analz_sees_Spy 6; |
217 dtac RA4_analz_spies 6; |
219 |
218 |
220 |
219 |
221 (** Session keys are not used to encrypt other session keys **) |
220 (** Session keys are not used to encrypt other session keys **) |
222 |
221 |
223 (*Version for "responses" relation. Handles case RA3 in the theorem below. |
222 (*Version for "responses" relation. Handles case RA3 in the theorem below. |
224 Note that it holds for *any* set H (not just "sees Spy evs") |
223 Note that it holds for *any* set H (not just "spies evs") |
225 satisfying the inductive hypothesis.*) |
224 satisfying the inductive hypothesis.*) |
226 goal thy |
225 goal thy |
227 "!!evs. [| RB : responses evs; \ |
226 "!!evs. [| RB : responses evs; \ |
228 \ ALL K KK. KK <= Compl (range shrK) --> \ |
227 \ ALL K KK. KK <= Compl (range shrK) --> \ |
229 \ (Key K : analz (Key``KK Un H)) = \ |
228 \ (Key K : analz (Key``KK Un H)) = \ |
237 |
236 |
238 (*Version for the protocol. Proof is almost trivial, thanks to the lemma.*) |
237 (*Version for the protocol. Proof is almost trivial, thanks to the lemma.*) |
239 goal thy |
238 goal thy |
240 "!!evs. evs : recur ==> \ |
239 "!!evs. evs : recur ==> \ |
241 \ ALL K KK. KK <= Compl (range shrK) --> \ |
240 \ ALL K KK. KK <= Compl (range shrK) --> \ |
242 \ (Key K : analz (Key``KK Un (sees Spy evs))) = \ |
241 \ (Key K : analz (Key``KK Un (spies evs))) = \ |
243 \ (K : KK | Key K : analz (sees Spy evs))"; |
242 \ (K : KK | Key K : analz (spies evs))"; |
244 by (etac recur.induct 1); |
243 by (etac recur.induct 1); |
245 by analz_sees_tac; |
244 by analz_spies_tac; |
246 by (REPEAT_FIRST (resolve_tac [allI, impI])); |
245 by (REPEAT_FIRST (resolve_tac [allI, impI])); |
247 by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); |
246 by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); |
248 by (ALLGOALS |
247 by (ALLGOALS |
249 (asm_simp_tac |
248 (asm_simp_tac |
250 (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma]))); |
249 (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma]))); |
254 by (spy_analz_tac 1); |
253 by (spy_analz_tac 1); |
255 val raw_analz_image_freshK = result(); |
254 val raw_analz_image_freshK = result(); |
256 qed_spec_mp "analz_image_freshK"; |
255 qed_spec_mp "analz_image_freshK"; |
257 |
256 |
258 |
257 |
259 (*Instance of the lemma with H replaced by (sees Spy evs): |
258 (*Instance of the lemma with H replaced by (spies evs): |
260 [| RB : responses evs; evs : recur; |] |
259 [| RB : responses evs; evs : recur; |] |
261 ==> KK <= Compl (range shrK) --> |
260 ==> KK <= Compl (range shrK) --> |
262 Key K : analz (insert RB (Key``KK Un sees Spy evs)) = |
261 Key K : analz (insert RB (Key``KK Un spies evs)) = |
263 (K : KK | Key K : analz (insert RB (sees Spy evs))) |
262 (K : KK | Key K : analz (insert RB (spies evs))) |
264 *) |
263 *) |
265 bind_thm ("resp_analz_image_freshK", |
264 bind_thm ("resp_analz_image_freshK", |
266 raw_analz_image_freshK RSN |
265 raw_analz_image_freshK RSN |
267 (2, resp_analz_image_freshK_lemma) RS spec RS spec); |
266 (2, resp_analz_image_freshK_lemma) RS spec RS spec); |
268 |
267 |
269 goal thy |
268 goal thy |
270 "!!evs. [| evs : recur; KAB ~: range shrK |] ==> \ |
269 "!!evs. [| evs : recur; KAB ~: range shrK |] ==> \ |
271 \ Key K : analz (insert (Key KAB) (sees Spy evs)) = \ |
270 \ Key K : analz (insert (Key KAB) (spies evs)) = \ |
272 \ (K = KAB | Key K : analz (sees Spy evs))"; |
271 \ (K = KAB | Key K : analz (spies evs))"; |
273 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); |
272 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); |
274 qed "analz_insert_freshK"; |
273 qed "analz_insert_freshK"; |
275 |
274 |
276 |
275 |
277 (*Everything that's hashed is already in past traffic. *) |
276 (*Everything that's hashed is already in past traffic. *) |
278 goal thy "!!evs. [| Hash {|Key(shrK A), X|} : parts (sees Spy evs); \ |
277 goal thy "!!evs. [| Hash {|Key(shrK A), X|} : parts (spies evs); \ |
279 \ evs : recur; A ~: lost |] \ |
278 \ evs : recur; A ~: bad |] \ |
280 \ ==> X : parts (sees Spy evs)"; |
279 \ ==> X : parts (spies evs)"; |
281 by (etac rev_mp 1); |
280 by (etac rev_mp 1); |
282 by (parts_induct_tac 1); |
281 by (parts_induct_tac 1); |
283 (*RA3 requires a further induction*) |
282 (*RA3 requires a further induction*) |
284 by (etac responses.induct 2); |
283 by (etac responses.induct 2); |
285 by (ALLGOALS Asm_simp_tac); |
284 by (ALLGOALS Asm_simp_tac); |
286 (*Fake*) |
285 (*Fake*) |
287 by (simp_tac (!simpset addsimps [parts_insert_sees]) 1); |
286 by (simp_tac (!simpset addsimps [parts_insert_spies]) 1); |
288 by (Fake_parts_insert_tac 1); |
287 by (Fake_parts_insert_tac 1); |
289 qed "Hash_imp_body"; |
288 qed "Hash_imp_body"; |
290 |
289 |
291 |
290 |
292 (** The Nonce NA uniquely identifies A's message. |
291 (** The Nonce NA uniquely identifies A's message. |
294 |
293 |
295 Unicity is not used in other proofs but is desirable in its own right. |
294 Unicity is not used in other proofs but is desirable in its own right. |
296 **) |
295 **) |
297 |
296 |
298 goal thy |
297 goal thy |
299 "!!evs. [| evs : recur; A ~: lost |] \ |
298 "!!evs. [| evs : recur; A ~: bad |] \ |
300 \ ==> EX B' P'. ALL B P. \ |
299 \ ==> EX B' P'. ALL B P. \ |
301 \ Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (sees Spy evs) \ |
300 \ Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (spies evs) \ |
302 \ --> B=B' & P=P'"; |
301 \ --> B=B' & P=P'"; |
303 by (parts_induct_tac 1); |
302 by (parts_induct_tac 1); |
304 by (Fake_parts_insert_tac 1); |
303 by (Fake_parts_insert_tac 1); |
305 by (etac responses.induct 3); |
304 by (etac responses.induct 3); |
306 by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib]))); |
305 by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib]))); |
307 by (step_tac (!claset addSEs partsEs) 1); |
306 by (step_tac (!claset addSEs partsEs) 1); |
308 (*RA1,2: creation of new Nonce. Move assertion into global context*) |
307 (*RA1,2: creation of new Nonce. Move assertion into global context*) |
309 by (ALLGOALS (expand_case_tac "NA = ?y")); |
308 by (ALLGOALS (expand_case_tac "NA = ?y")); |
310 by (REPEAT_FIRST (ares_tac [exI])); |
309 by (REPEAT_FIRST (ares_tac [exI])); |
311 by (REPEAT (blast_tac (!claset addSDs [Hash_imp_body] |
310 by (REPEAT (blast_tac (!claset addSDs [Hash_imp_body] |
312 addSEs sees_Spy_partsEs) 1)); |
311 addSEs spies_partsEs) 1)); |
313 val lemma = result(); |
312 val lemma = result(); |
314 |
313 |
315 goalw thy [HPair_def] |
314 goalw thy [HPair_def] |
316 "!!A.[| Hash[Key(shrK A)] {|Agent A, B,NA,P|} : parts(sees Spy evs); \ |
315 "!!A.[| Hash[Key(shrK A)] {|Agent A, B,NA,P|} : parts(spies evs); \ |
317 \ Hash[Key(shrK A)] {|Agent A, B',NA,P'|} : parts(sees Spy evs); \ |
316 \ Hash[Key(shrK A)] {|Agent A, B',NA,P'|} : parts(spies evs); \ |
318 \ evs : recur; A ~: lost |] \ |
317 \ evs : recur; A ~: bad |] \ |
319 \ ==> B=B' & P=P'"; |
318 \ ==> B=B' & P=P'"; |
320 by (REPEAT (eresolve_tac partsEs 1)); |
319 by (REPEAT (eresolve_tac partsEs 1)); |
321 by (prove_unique_tac lemma 1); |
320 by (prove_unique_tac lemma 1); |
322 qed "unique_NA"; |
321 qed "unique_NA"; |
323 |
322 |
415 Does not in itself guarantee security: an attack could violate |
414 Does not in itself guarantee security: an attack could violate |
416 the premises, e.g. by having A=Spy **) |
415 the premises, e.g. by having A=Spy **) |
417 |
416 |
418 goal thy |
417 goal thy |
419 "!!evs. [| (PB,RB,KAB) : respond evs; evs : recur |] \ |
418 "!!evs. [| (PB,RB,KAB) : respond evs; evs : recur |] \ |
420 \ ==> ALL A A' N. A ~: lost & A' ~: lost --> \ |
419 \ ==> ALL A A' N. A ~: bad & A' ~: bad --> \ |
421 \ Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} --> \ |
420 \ Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} --> \ |
422 \ Key K ~: analz (insert RB (sees Spy evs))"; |
421 \ Key K ~: analz (insert RB (spies evs))"; |
423 by (etac respond.induct 1); |
422 by (etac respond.induct 1); |
424 by (forward_tac [respond_imp_responses] 2); |
423 by (forward_tac [respond_imp_responses] 2); |
425 by (forward_tac [respond_imp_not_used] 2); |
424 by (forward_tac [respond_imp_not_used] 2); |
426 by (ALLGOALS (*12 seconds*) |
425 by (ALLGOALS (*12 seconds*) |
427 (asm_simp_tac |
426 (asm_simp_tac |
435 addDs [resp_analz_insert] |
434 addDs [resp_analz_insert] |
436 addIs [impOfSubs analz_subset_parts]) 4)); |
435 addIs [impOfSubs analz_subset_parts]) 4)); |
437 by (Blast_tac 3); |
436 by (Blast_tac 3); |
438 by (blast_tac (!claset addSEs partsEs |
437 by (blast_tac (!claset addSEs partsEs |
439 addDs [Key_in_parts_respond]) 2); |
438 addDs [Key_in_parts_respond]) 2); |
440 (*by unicity, either B=Aa or B=A', a contradiction since B: lost*) |
439 (*by unicity, either B=Aa or B=A', a contradiction since B: bad*) |
441 by (dtac unique_session_keys 1); |
440 by (dtac unique_session_keys 1); |
442 by (etac respond_certificate 1); |
441 by (etac respond_certificate 1); |
443 by (assume_tac 1); |
442 by (assume_tac 1); |
444 by (Blast_tac 1); |
443 by (Blast_tac 1); |
445 qed_spec_mp "respond_Spy_not_see_session_key"; |
444 qed_spec_mp "respond_Spy_not_see_session_key"; |
446 |
445 |
447 |
446 |
448 goal thy |
447 goal thy |
449 "!!evs. [| Crypt (shrK A) {|Key K, Agent A', N|} \ |
448 "!!evs. [| Crypt (shrK A) {|Key K, Agent A', N|} : parts (spies evs); \ |
450 \ : parts (sees Spy evs); \ |
449 \ A ~: bad; A' ~: bad; evs : recur |] \ |
451 \ A ~: lost; A' ~: lost; evs : recur |] \ |
450 \ ==> Key K ~: analz (spies evs)"; |
452 \ ==> Key K ~: analz (sees Spy evs)"; |
|
453 by (etac rev_mp 1); |
451 by (etac rev_mp 1); |
454 by (etac recur.induct 1); |
452 by (etac recur.induct 1); |
455 by analz_sees_tac; |
453 by analz_spies_tac; |
456 by (ALLGOALS |
454 by (ALLGOALS |
457 (asm_simp_tac |
455 (asm_simp_tac |
458 (!simpset addsimps [parts_insert_sees, analz_insert_freshK] |
456 (!simpset addsimps [parts_insert_spies, analz_insert_freshK] |
459 setloop split_tac [expand_if]))); |
457 setloop split_tac [expand_if]))); |
460 (*RA4*) |
458 (*RA4*) |
461 by (spy_analz_tac 5); |
459 by (spy_analz_tac 5); |
462 (*RA2*) |
460 (*RA2*) |
463 by (spy_analz_tac 3); |
461 by (spy_analz_tac 3); |
492 (*Only RA1 or RA2 can have caused such a part of a message to appear. |
490 (*Only RA1 or RA2 can have caused such a part of a message to appear. |
493 This result is of no use to B, who cannot verify the Hash. Moreover, |
491 This result is of no use to B, who cannot verify the Hash. Moreover, |
494 it can say nothing about how recent A's message is. It might later be |
492 it can say nothing about how recent A's message is. It might later be |
495 used to prove B's presence to A at the run's conclusion.*) |
493 used to prove B's presence to A at the run's conclusion.*) |
496 goalw thy [HPair_def] |
494 goalw thy [HPair_def] |
497 "!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} \ |
495 "!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} : parts(spies evs); \ |
498 \ : parts (sees Spy evs); \ |
496 \ A ~: bad; evs : recur |] \ |
499 \ A ~: lost; evs : recur |] \ |
|
500 \ ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) : set evs"; |
497 \ ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) : set evs"; |
501 by (etac rev_mp 1); |
498 by (etac rev_mp 1); |
502 by (parts_induct_tac 1); |
499 by (parts_induct_tac 1); |
503 by (Fake_parts_insert_tac 1); |
500 by (Fake_parts_insert_tac 1); |
504 (*RA3*) |
501 (*RA3*) |