176 |
176 |
177 (*Pushing Unions into parts; one of the A's equals B, and thus sees Y*) |
177 (*Pushing Unions into parts; one of the A's equals B, and thus sees Y*) |
178 goal thy "(UN A. parts (sees A (Says B C Y # evs))) = \ |
178 goal thy "(UN A. parts (sees A (Says B C Y # evs))) = \ |
179 \ parts {Y} Un (UN A. parts (sees A evs))"; |
179 \ parts {Y} Un (UN A. parts (sees A evs))"; |
180 by (Step_tac 1); |
180 by (Step_tac 1); |
181 be rev_mp 1; (*for some reason, split_tac does not work on assumptions*) |
181 by (etac rev_mp 1); (*for some reason, split_tac does not work on assumptions*) |
182 val ss = (!simpset addsimps [parts_Un, sees_Cons] |
182 val ss = (!simpset addsimps [parts_Un, sees_Cons] |
183 setloop split_tac [expand_if]); |
183 setloop split_tac [expand_if]); |
184 by (ALLGOALS (fast_tac (!claset addss ss))); |
184 by (ALLGOALS (fast_tac (!claset addss ss))); |
185 qed "UN_parts_sees_Says"; |
185 qed "UN_parts_sees_Says"; |
186 |
186 |
187 goal thy "Says A B X : set_of_list evs --> X : sees Enemy evs"; |
187 goal thy "Says A B X : set_of_list evs --> X : sees Spy evs"; |
188 by (list.induct_tac "evs" 1); |
188 by (list.induct_tac "evs" 1); |
189 by (Auto_tac ()); |
189 by (Auto_tac ()); |
190 qed_spec_mp "Says_imp_sees_Enemy"; |
190 qed_spec_mp "Says_imp_sees_Spy"; |
191 |
191 |
192 Addsimps [Says_imp_sees_Enemy]; |
192 Addsimps [Says_imp_sees_Spy]; |
193 AddIs [Says_imp_sees_Enemy]; |
193 AddIs [Says_imp_sees_Spy]; |
194 |
194 |
195 goal thy "initState C <= Key `` range shrK"; |
195 goal thy "initState C <= Key `` range shrK"; |
196 by (agent.induct_tac "C" 1); |
196 by (agent.induct_tac "C" 1); |
197 by (Auto_tac ()); |
197 by (Auto_tac ()); |
198 qed "initState_subset"; |
198 qed "initState_subset"; |
202 \ (EX A. Notes A X : set_of_list evs) | \ |
202 \ (EX A. Notes A X : set_of_list evs) | \ |
203 \ (EX A. X = Key (shrK A))"; |
203 \ (EX A. X = Key (shrK A))"; |
204 by (list.induct_tac "evs" 1); |
204 by (list.induct_tac "evs" 1); |
205 by (ALLGOALS Asm_simp_tac); |
205 by (ALLGOALS Asm_simp_tac); |
206 by (fast_tac (!claset addDs [impOfSubs initState_subset]) 1); |
206 by (fast_tac (!claset addDs [impOfSubs initState_subset]) 1); |
207 br conjI 1; |
207 by (rtac conjI 1); |
208 by (Fast_tac 2); |
208 by (Fast_tac 2); |
209 by (event.induct_tac "a" 1); |
209 by (event.induct_tac "a" 1); |
210 by (ALLGOALS (asm_simp_tac (!simpset addsimps [mem_if]))); |
210 by (ALLGOALS (asm_simp_tac (!simpset addsimps [mem_if]))); |
211 by (ALLGOALS Fast_tac); |
211 by (ALLGOALS Fast_tac); |
212 qed_spec_mp "seesD"; |
212 qed_spec_mp "seesD"; |
213 |
213 |
214 |
214 |
215 Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Enemy]; |
215 Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Spy]; |
216 Delsimps [sees_Cons]; (**** NOTE REMOVAL -- laws above are cleaner ****) |
216 Delsimps [sees_Cons]; (**** NOTE REMOVAL -- laws above are cleaner ****) |
217 |
217 |
218 |
218 |
219 (**** Inductive proofs about traces ****) |
219 (**** Inductive proofs about traces ****) |
220 |
220 |
221 (*The Enemy can see more than anybody else, except for their initial state*) |
221 (*The Spy can see more than anybody else, except for their initial state*) |
222 goal thy |
222 goal thy |
223 "!!evs. evs : traces ==> \ |
223 "!!evs. evs : traces ==> \ |
224 \ sees A evs <= initState A Un sees Enemy evs"; |
224 \ sees A evs <= initState A Un sees Spy evs"; |
225 be traces.induct 1; |
225 by (etac traces.induct 1); |
226 by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] |
226 by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] |
227 addss (!simpset)))); |
227 addss (!simpset)))); |
228 qed "sees_agent_subset_sees_Enemy"; |
228 qed "sees_agent_subset_sees_Spy"; |
229 |
229 |
230 |
230 |
231 (*Nobody sends themselves messages*) |
231 (*Nobody sends themselves messages*) |
232 goal thy "!!evs. evs : traces ==> ALL A X. Says A A X ~: set_of_list evs"; |
232 goal thy "!!evs. evs : traces ==> ALL A X. Says A A X ~: set_of_list evs"; |
233 be traces.induct 1; |
233 by (etac traces.induct 1); |
234 by (Auto_tac()); |
234 by (Auto_tac()); |
235 qed_spec_mp "not_Says_to_self"; |
235 qed_spec_mp "not_Says_to_self"; |
236 Addsimps [not_Says_to_self]; |
236 Addsimps [not_Says_to_self]; |
237 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
237 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
238 |
238 |
239 goal thy "!!evs. evs : traces ==> Notes A X ~: set_of_list evs"; |
239 goal thy "!!evs. evs : traces ==> Notes A X ~: set_of_list evs"; |
240 be traces.induct 1; |
240 by (etac traces.induct 1); |
241 by (Auto_tac()); |
241 by (Auto_tac()); |
242 qed "not_Notes"; |
242 qed "not_Notes"; |
243 Addsimps [not_Notes]; |
243 Addsimps [not_Notes]; |
244 AddSEs [not_Notes RSN (2, rev_notE)]; |
244 AddSEs [not_Notes RSN (2, rev_notE)]; |
245 |
245 |
246 |
246 |
247 goal thy "!!evs. (Says S A (Crypt {|N, B, K, X|} KA)) : set_of_list evs ==> \ |
247 goal thy "!!evs. (Says S A (Crypt {|N, B, K, X|} KA)) : set_of_list evs ==> \ |
248 \ X : parts (sees Enemy evs)"; |
248 \ X : parts (sees Spy evs)"; |
249 by (fast_tac (!claset addSEs partsEs |
249 by (fast_tac (!claset addSEs partsEs |
250 addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1); |
250 addSDs [Says_imp_sees_Spy RS parts.Inj]) 1); |
251 qed "NS3_msg_in_parts_sees_Enemy"; |
251 qed "NS3_msg_in_parts_sees_Spy"; |
252 |
252 |
253 |
253 |
254 (*** Server keys are not betrayed ***) |
254 (*** Server keys are not betrayed ***) |
255 |
255 |
256 (*Enemy never sees another agent's server key!*) |
256 (*Spy never sees another agent's server key!*) |
257 goal thy |
257 goal thy |
258 "!!evs. [| evs : traces; A ~= Enemy |] ==> \ |
258 "!!evs. [| evs : traces; A ~= Spy |] ==> \ |
259 \ Key (shrK A) ~: parts (sees Enemy evs)"; |
259 \ Key (shrK A) ~: parts (sees Spy evs)"; |
260 be traces.induct 1; |
260 by (etac traces.induct 1); |
261 bd NS3_msg_in_parts_sees_Enemy 5; |
261 by (dtac NS3_msg_in_parts_sees_Spy 5); |
262 by (Auto_tac()); |
262 by (Auto_tac()); |
263 (*Deals with Fake message*) |
263 (*Deals with Fake message*) |
264 by (best_tac (!claset addDs [impOfSubs analz_subset_parts, |
264 by (best_tac (!claset addDs [impOfSubs analz_subset_parts, |
265 impOfSubs synth_analz_parts_insert_subset_Un]) 1); |
265 impOfSubs synth_analz_parts_insert_subset_Un]) 1); |
266 qed "Enemy_not_see_shrK"; |
266 qed "Spy_not_see_shrK"; |
267 |
267 |
268 bind_thm ("Enemy_not_analz_shrK", |
268 bind_thm ("Spy_not_analz_shrK", |
269 [analz_subset_parts, Enemy_not_see_shrK] MRS contra_subsetD); |
269 [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD); |
270 |
270 |
271 Addsimps [Enemy_not_see_shrK, |
271 Addsimps [Spy_not_see_shrK, |
272 not_sym RSN (2, Enemy_not_see_shrK), |
272 not_sym RSN (2, Spy_not_see_shrK), |
273 Enemy_not_analz_shrK, |
273 Spy_not_analz_shrK, |
274 not_sym RSN (2, Enemy_not_analz_shrK)]; |
274 not_sym RSN (2, Spy_not_analz_shrK)]; |
275 |
275 |
276 (*We go to some trouble to preserve R in the 3rd subgoal*) |
276 (*We go to some trouble to preserve R in the 3rd subgoal*) |
277 val major::prems = |
277 val major::prems = |
278 goal thy "[| Key (shrK A) : parts (sees Enemy evs); \ |
278 goal thy "[| Key (shrK A) : parts (sees Spy evs); \ |
279 \ evs : traces; \ |
279 \ evs : traces; \ |
280 \ A=Enemy ==> R \ |
280 \ A=Spy ==> R \ |
281 \ |] ==> R"; |
281 \ |] ==> R"; |
282 br ccontr 1; |
282 by (rtac ccontr 1); |
283 br ([major, Enemy_not_see_shrK] MRS rev_notE) 1; |
283 by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1); |
284 by (swap_res_tac prems 2); |
284 by (swap_res_tac prems 2); |
285 by (ALLGOALS (fast_tac (!claset addIs prems))); |
285 by (ALLGOALS (fast_tac (!claset addIs prems))); |
286 qed "Enemy_see_shrK_E"; |
286 qed "Spy_see_shrK_E"; |
287 |
287 |
288 bind_thm ("Enemy_analz_shrK_E", |
288 bind_thm ("Spy_analz_shrK_E", |
289 analz_subset_parts RS subsetD RS Enemy_see_shrK_E); |
289 analz_subset_parts RS subsetD RS Spy_see_shrK_E); |
290 |
290 |
291 (*Classical reasoner doesn't need the not_sym versions (with swapped ~=) *) |
291 (*Classical reasoner doesn't need the not_sym versions (with swapped ~=) *) |
292 AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E]; |
292 AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E]; |
293 |
293 |
294 |
294 |
295 (*No Friend will ever see another agent's server key |
295 (*No Friend will ever see another agent's server key |
296 (excluding the Enemy, who might transmit his). |
296 (excluding the Spy, who might transmit his). |
297 The Server, of course, knows all server keys.*) |
297 The Server, of course, knows all server keys.*) |
298 goal thy |
298 goal thy |
299 "!!evs. [| evs : traces; A ~= Enemy; A ~= Friend j |] ==> \ |
299 "!!evs. [| evs : traces; A ~= Spy; A ~= Friend j |] ==> \ |
300 \ Key (shrK A) ~: parts (sees (Friend j) evs)"; |
300 \ Key (shrK A) ~: parts (sees (Friend j) evs)"; |
301 br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1; |
301 by (rtac (sees_agent_subset_sees_Spy RS parts_mono RS contra_subsetD) 1); |
302 by (ALLGOALS Asm_simp_tac); |
302 by (ALLGOALS Asm_simp_tac); |
303 qed "Friend_not_see_shrK"; |
303 qed "Friend_not_see_shrK"; |
304 |
304 |
305 |
305 |
306 (*Not for Addsimps -- it can cause goals to blow up!*) |
306 (*Not for Addsimps -- it can cause goals to blow up!*) |
307 goal thy |
307 goal thy |
308 "!!evs. evs : traces ==> \ |
308 "!!evs. evs : traces ==> \ |
309 \ (Key (shrK A) \ |
309 \ (Key (shrK A) \ |
310 \ : analz (insert (Key (shrK B)) (sees Enemy evs))) = \ |
310 \ : analz (insert (Key (shrK B)) (sees Spy evs))) = \ |
311 \ (A=B | A=Enemy)"; |
311 \ (A=B | A=Spy)"; |
312 by (best_tac (!claset addDs [impOfSubs analz_subset_parts] |
312 by (best_tac (!claset addDs [impOfSubs analz_subset_parts] |
313 addIs [impOfSubs (subset_insertI RS analz_mono)] |
313 addIs [impOfSubs (subset_insertI RS analz_mono)] |
314 addss (!simpset)) 1); |
314 addss (!simpset)) 1); |
315 qed "shrK_mem_analz"; |
315 qed "shrK_mem_analz"; |
316 |
316 |
317 |
317 |
318 |
318 |
319 |
319 |
369 (*Nobody can have USED keys that will be generated in the future. |
369 (*Nobody can have USED keys that will be generated in the future. |
370 ...very like new_keys_not_seen*) |
370 ...very like new_keys_not_seen*) |
371 goal thy "!!evs. evs : traces ==> \ |
371 goal thy "!!evs. evs : traces ==> \ |
372 \ length evs <= length evs' --> \ |
372 \ length evs <= length evs' --> \ |
373 \ newK evs' ~: keysFor (UN C. parts (sees C evs))"; |
373 \ newK evs' ~: keysFor (UN C. parts (sees C evs))"; |
374 be traces.induct 1; |
374 by (etac traces.induct 1); |
375 bd NS3_msg_in_parts_sees_Enemy 5; |
375 by (dtac NS3_msg_in_parts_sees_Spy 5); |
376 by (ALLGOALS Asm_simp_tac); |
376 by (ALLGOALS Asm_simp_tac); |
377 (*NS1 and NS2*) |
377 (*NS1 and NS2*) |
378 map (by o fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [3,2]; |
378 map (by o fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [3,2]; |
379 (*Fake and NS3*) |
379 (*Fake and NS3*) |
380 map (by o best_tac |
380 map (by o best_tac |
381 (!claset addSDs [newK_invKey] |
381 (!claset addSDs [newK_invKey] |
382 addDs [impOfSubs (analz_subset_parts RS keysFor_mono), |
382 addDs [impOfSubs (analz_subset_parts RS keysFor_mono), |
383 impOfSubs (parts_insert_subset_Un RS keysFor_mono), |
383 impOfSubs (parts_insert_subset_Un RS keysFor_mono), |
384 Suc_leD] |
384 Suc_leD] |
385 addEs [new_keys_not_seen RS not_parts_not_analz RSN (2,rev_notE)] |
385 addEs [new_keys_not_seen RS not_parts_not_analz RSN (2,rev_notE)] |
386 addss (!simpset))) |
386 addss (!simpset))) |
387 [2,1]; |
387 [2,1]; |
388 (*NS4 and NS5: nonce exchange*) |
388 (*NS4 and NS5: nonce exchange*) |
389 by (ALLGOALS (deepen_tac (!claset addSDs [newK_invKey, Says_imp_old_keys] |
389 by (ALLGOALS (deepen_tac (!claset addSDs [newK_invKey, Says_imp_old_keys] |
390 addIs [less_SucI, impOfSubs keysFor_mono] |
390 addIs [less_SucI, impOfSubs keysFor_mono] |
391 addss (!simpset addsimps [le_def])) 0)); |
391 addss (!simpset addsimps [le_def])) 0)); |
392 val lemma = result(); |
392 val lemma = result(); |
393 |
393 |
394 goal thy |
394 goal thy |
395 "!!evs. [| evs : traces; length evs <= length evs' |] ==> \ |
395 "!!evs. [| evs : traces; length evs <= length evs' |] ==> \ |
396 \ newK evs' ~: keysFor (parts (sees C evs))"; |
396 \ newK evs' ~: keysFor (parts (sees C evs))"; |
397 by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1); |
397 by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1); |
398 qed "new_keys_not_used"; |
398 qed "new_keys_not_used"; |
399 |
399 |
400 bind_thm ("new_keys_not_analzd", |
400 bind_thm ("new_keys_not_analzd", |
401 [analz_subset_parts RS keysFor_mono, |
401 [analz_subset_parts RS keysFor_mono, |
402 new_keys_not_used] MRS contra_subsetD); |
402 new_keys_not_used] MRS contra_subsetD); |
403 |
403 |
404 Addsimps [new_keys_not_used, new_keys_not_analzd]; |
404 Addsimps [new_keys_not_used, new_keys_not_analzd]; |
405 |
405 |
406 |
406 |
407 (** Rewrites to push in Key and Crypt messages, so that other messages can |
407 (** Rewrites to push in Key and Crypt messages, so that other messages can |
432 \ |] ==> (EX evt:traces. \ |
432 \ |] ==> (EX evt:traces. \ |
433 \ K = Key(newK evt) & \ |
433 \ K = Key(newK evt) & \ |
434 \ X = (Crypt {|K, Agent A|} (shrK B)) & \ |
434 \ X = (Crypt {|K, Agent A|} (shrK B)) & \ |
435 \ K' = shrK A & \ |
435 \ K' = shrK A & \ |
436 \ length evt < length evs)"; |
436 \ length evt < length evs)"; |
437 be rev_mp 1; |
437 by (etac rev_mp 1); |
438 be traces.induct 1; |
438 by (etac traces.induct 1); |
439 by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset)))); |
439 by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset)))); |
440 qed "Says_Server_message_form"; |
440 qed "Says_Server_message_form"; |
441 |
441 |
442 (* c ~: keysFor (parts H) ==> c ~: keysFor (analz H) *) |
442 (* c ~: keysFor (parts H) ==> c ~: keysFor (analz H) *) |
443 bind_thm ("not_parts_not_keysFor_analz", |
443 bind_thm ("not_parts_not_keysFor_analz", |
444 analz_subset_parts RS keysFor_mono RS contra_subsetD); |
444 analz_subset_parts RS keysFor_mono RS contra_subsetD); |
445 |
445 |
446 |
446 |
447 |
447 |
448 (*USELESS for NS3, case 1, as the ind hyp says the same thing! |
448 (*USELESS for NS3, case 1, as the ind hyp says the same thing! |
449 goal thy |
449 goal thy |
450 "!!evs. [| evs = Says Server (Friend i) \ |
450 "!!evs. [| evs = Says Server (Friend i) \ |
451 \ (Crypt {|N, Agent(Friend j), K, X|} K') # evs'; \ |
451 \ (Crypt {|N, Agent(Friend j), K, X|} K') # evs'; \ |
452 \ evs : traces; i~=k \ |
452 \ evs : traces; i~=k \ |
453 \ |] ==> \ |
453 \ |] ==> \ |
454 \ K ~: analz (insert (Key (shrK (Friend k))) (sees Enemy evs))"; |
454 \ K ~: analz (insert (Key (shrK (Friend k))) (sees Spy evs))"; |
455 be rev_mp 1; |
455 by (etac rev_mp 1); |
456 be traces.induct 1; |
456 by (etac traces.induct 1); |
457 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes))); |
457 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes))); |
458 by (Step_tac 1); |
458 by (Step_tac 1); |
459 by (asm_full_simp_tac (!simpset addsimps[analz_subset_parts RS contra_subsetD]) 1); |
459 by (asm_full_simp_tac (!simpset addsimps[analz_subset_parts RS contra_subsetD]) 1); |
460 val Enemy_not_see_encrypted_key_lemma = result(); |
460 val Spy_not_see_encrypted_key_lemma = result(); |
461 *) |
461 *) |
462 |
462 |
463 |
463 |
464 (*Describes the form of X when the following message is sent*) |
464 (*Describes the form of X when the following message is sent*) |
465 goal thy |
465 goal thy |
466 "!!evs. evs : traces ==> \ |
466 "!!evs. evs : traces ==> \ |
467 \ ALL A NA B K X. \ |
467 \ ALL A NA B K X. \ |
468 \ (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \ |
468 \ (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \ |
469 \ : parts (sees Enemy evs) & A ~= Enemy --> \ |
469 \ : parts (sees Spy evs) & A ~= Spy --> \ |
470 \ (EX evt:traces. K = newK evt & \ |
470 \ (EX evt:traces. K = newK evt & \ |
471 \ X = (Crypt {|Key K, Agent A|} (shrK B)))"; |
471 \ X = (Crypt {|Key K, Agent A|} (shrK B)))"; |
472 be traces.induct 1; |
472 by (etac traces.induct 1); |
473 bd NS3_msg_in_parts_sees_Enemy 5; |
473 by (dtac NS3_msg_in_parts_sees_Spy 5); |
474 by (Step_tac 1); |
474 by (Step_tac 1); |
475 by (ALLGOALS Asm_full_simp_tac); |
475 by (ALLGOALS Asm_full_simp_tac); |
476 (*Remaining cases are Fake and NS2*) |
476 (*Remaining cases are Fake and NS2*) |
477 by (fast_tac (!claset addSDs [spec]) 2); |
477 by (fast_tac (!claset addSDs [spec]) 2); |
478 (*Now for the Fake case*) |
478 (*Now for the Fake case*) |
479 by (best_tac (!claset addDs [impOfSubs analz_subset_parts, |
479 by (best_tac (!claset addDs [impOfSubs analz_subset_parts, |
480 impOfSubs synth_analz_parts_insert_subset_Un] |
480 impOfSubs synth_analz_parts_insert_subset_Un] |
481 addss (!simpset)) 1); |
481 addss (!simpset)) 1); |
482 qed_spec_mp "encrypted_form"; |
482 qed_spec_mp "encrypted_form"; |
483 |
483 |
484 |
484 |
485 (*For eliminating the A ~= Enemy condition from the previous result*) |
485 (*For eliminating the A ~= Spy condition from the previous result*) |
486 goal thy |
486 goal thy |
487 "!!evs. evs : traces ==> \ |
487 "!!evs. evs : traces ==> \ |
488 \ ALL S A NA B K X. \ |
488 \ ALL S A NA B K X. \ |
489 \ Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \ |
489 \ Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \ |
490 \ : set_of_list evs --> \ |
490 \ : set_of_list evs --> \ |
491 \ S = Server | S = Enemy"; |
491 \ S = Server | S = Spy"; |
492 be traces.induct 1; |
492 by (etac traces.induct 1); |
493 by (ALLGOALS Asm_simp_tac); |
493 by (ALLGOALS Asm_simp_tac); |
494 (*We are left with NS3*) |
494 (*We are left with NS3*) |
495 by (subgoal_tac "S = Server | S = Enemy" 1); |
495 by (subgoal_tac "S = Server | S = Spy" 1); |
496 (*First justify this assumption!*) |
496 (*First justify this assumption!*) |
497 by (fast_tac (!claset addSEs [allE, mp] addss (!simpset)) 2); |
497 by (fast_tac (!claset addSEs [allE, mp] addss (!simpset)) 2); |
498 by (Step_tac 1); |
498 by (Step_tac 1); |
499 bd Says_Server_message_form 1; |
499 by (dtac Says_Server_message_form 1); |
500 by (ALLGOALS Full_simp_tac); |
500 by (ALLGOALS Full_simp_tac); |
501 (*Final case. Clear out needless quantifiers to speed the following step*) |
501 (*Final case. Clear out needless quantifiers to speed the following step*) |
502 by (eres_inst_tac [("V","ALL x. ?P(x)")] thin_rl 1); |
502 by (eres_inst_tac [("V","ALL x. ?P(x)")] thin_rl 1); |
503 bd encrypted_form 1; |
503 by (dtac encrypted_form 1); |
504 br (parts.Inj RS conjI) 1; |
504 by (rtac (parts.Inj RS conjI) 1); |
505 auto(); |
505 auto(); |
506 qed_spec_mp "Server_or_Enemy"; |
506 qed_spec_mp "Server_or_Spy"; |
507 |
507 |
508 |
508 |
509 (*Describes the form of X when the following message is sent; |
509 (*Describes the form of X when the following message is sent; |
510 use Says_Server_message_form if applicable*) |
510 use Says_Server_message_form if applicable*) |
511 goal thy |
511 goal thy |
512 "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \ |
512 "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \ |
513 \ : set_of_list evs; \ |
513 \ : set_of_list evs; \ |
514 \ evs : traces \ |
514 \ evs : traces \ |
515 \ |] ==> (EX evt:traces. K = newK evt & length evt < length evs & \ |
515 \ |] ==> (EX evt:traces. K = newK evt & length evt < length evs & \ |
516 \ X = (Crypt {|Key K, Agent A|} (shrK B)))"; |
516 \ X = (Crypt {|Key K, Agent A|} (shrK B)))"; |
517 by (forward_tac [Server_or_Enemy] 1); |
517 by (forward_tac [Server_or_Spy] 1); |
518 ba 1; |
518 by (assume_tac 1); |
519 by (Step_tac 1); |
519 by (Step_tac 1); |
520 by (fast_tac (!claset addSDs [Says_Server_message_form] addss (!simpset)) 1); |
520 by (fast_tac (!claset addSDs [Says_Server_message_form] addss (!simpset)) 1); |
521 by (forward_tac [encrypted_form] 1); |
521 by (forward_tac [encrypted_form] 1); |
522 br (parts.Inj RS conjI) 1; |
522 by (rtac (parts.Inj RS conjI) 1); |
523 by (auto_tac (!claset addIs [Says_imp_old_keys], !simpset)); |
523 by (auto_tac (!claset addIs [Says_imp_old_keys], !simpset)); |
524 qed "Says_S_message_form"; |
524 qed "Says_S_message_form"; |
525 |
525 |
526 (*Currently unused. Needed only to reason about the VERY LAST message.*) |
526 (*Currently unused. Needed only to reason about the VERY LAST message.*) |
527 goal thy |
527 goal thy |
553 (*NOT useful in this form, but it says that session keys are not used |
553 (*NOT useful in this form, but it says that session keys are not used |
554 to encrypt messages containing other keys, in the actual protocol. |
554 to encrypt messages containing other keys, in the actual protocol. |
555 We require that agents should behave like this subsequently also.*) |
555 We require that agents should behave like this subsequently also.*) |
556 goal thy |
556 goal thy |
557 "!!evs. evs : traces ==> \ |
557 "!!evs. evs : traces ==> \ |
558 \ (Crypt X (newK evt)) : parts (sees Enemy evs) & \ |
558 \ (Crypt X (newK evt)) : parts (sees Spy evs) & \ |
559 \ Key K : parts {X} --> Key K : parts (sees Enemy evs)"; |
559 \ Key K : parts {X} --> Key K : parts (sees Spy evs)"; |
560 be traces.induct 1; |
560 by (etac traces.induct 1); |
561 bd NS3_msg_in_parts_sees_Enemy 5; |
561 by (dtac NS3_msg_in_parts_sees_Spy 5); |
562 by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes))); |
562 by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes))); |
563 (*Deals with Faked messages*) |
563 (*Deals with Faked messages*) |
564 by (best_tac (!claset addSEs partsEs |
564 by (best_tac (!claset addSEs partsEs |
565 addDs [impOfSubs analz_subset_parts, |
565 addDs [impOfSubs analz_subset_parts, |
566 impOfSubs parts_insert_subset_Un] |
566 impOfSubs parts_insert_subset_Un] |
567 addss (!simpset)) 1); |
567 addss (!simpset)) 1); |
568 (*NS4 and NS5*) |
568 (*NS4 and NS5*) |
569 by (ALLGOALS (fast_tac (!claset addss (!simpset)))); |
569 by (ALLGOALS (fast_tac (!claset addss (!simpset)))); |
570 result(); |
570 result(); |
629 |
629 |
630 goal thy |
630 goal thy |
631 "!!evs. evs : traces ==> \ |
631 "!!evs. evs : traces ==> \ |
632 \ Key K : analz (insert (Key (newK evt)) \ |
632 \ Key K : analz (insert (Key (newK evt)) \ |
633 \ (insert (Key (shrK C)) \ |
633 \ (insert (Key (shrK C)) \ |
634 \ (sees Enemy evs))) = \ |
634 \ (sees Spy evs))) = \ |
635 \ (K = newK evt | \ |
635 \ (K = newK evt | \ |
636 \ Key K : analz (insert (Key (shrK C)) \ |
636 \ Key K : analz (insert (Key (shrK C)) \ |
637 \ (sees Enemy evs)))"; |
637 \ (sees Spy evs)))"; |
638 by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, |
638 by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, |
639 insert_Key_singleton]) 1); |
639 insert_Key_singleton]) 1); |
640 by (Fast_tac 1); |
640 by (Fast_tac 1); |
641 qed "analz_insert_Key_newK"; |
641 qed "analz_insert_Key_newK"; |
642 |
642 |
643 |
643 |
644 |
644 |
645 (*This says that the Key, K, uniquely identifies the message. |
645 (*This says that the Key, K, uniquely identifies the message. |
646 But if C=Enemy then he could send all sorts of nonsense.*) |
646 But if C=Spy then he could send all sorts of nonsense.*) |
647 goal thy |
647 goal thy |
648 "!!evs. evs : traces ==> \ |
648 "!!evs. evs : traces ==> \ |
649 \ EX X'. ALL C S A Y N B X. \ |
649 \ EX X'. ALL C S A Y N B X. \ |
650 \ C ~= Enemy --> \ |
650 \ C ~= Spy --> \ |
651 \ Says S A Y : set_of_list evs --> \ |
651 \ Says S A Y : set_of_list evs --> \ |
652 \ ((Crypt {|N, Agent B, Key K, X|} (shrK C)) : parts{Y} --> \ |
652 \ ((Crypt {|N, Agent B, Key K, X|} (shrK C)) : parts{Y} --> \ |
653 \ (X = X'))"; |
653 \ (X = X'))"; |
654 be traces.induct 1; |
654 by (etac traces.induct 1); |
655 by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); |
655 by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); |
656 by (ALLGOALS |
656 by (ALLGOALS |
657 (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib]))); |
657 (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib]))); |
658 (*NS2: Case split propagates some context to other subgoal...*) |
658 (*NS2: Case split propagates some context to other subgoal...*) |
659 by (excluded_middle_tac "K = newK evsa" 2); |
659 by (excluded_middle_tac "K = newK evsa" 2); |
660 by (Asm_simp_tac 2); |
660 by (Asm_simp_tac 2); |
661 (*...we assume X is a very new message, and handle this case by contradiction*) |
661 (*...we assume X is a very new message, and handle this case by contradiction*) |
662 by (fast_tac (!claset addIs [impOfSubs (subset_insertI RS parts_mono)] |
662 by (fast_tac (!claset addIs [impOfSubs (subset_insertI RS parts_mono)] |
663 addSEs partsEs |
663 addSEs partsEs |
664 addEs [Says_imp_old_keys RS less_irrefl] |
664 addEs [Says_imp_old_keys RS less_irrefl] |
665 addss (!simpset)) 2); |
665 addss (!simpset)) 2); |
666 (*NS3: No relevant messages*) |
666 (*NS3: No relevant messages*) |
667 by (fast_tac (!claset addSEs [exI] addss (!simpset)) 2); |
667 by (fast_tac (!claset addSEs [exI] addss (!simpset)) 2); |
668 (*Fake*) |
668 (*Fake*) |
669 by (Step_tac 1); |
669 by (Step_tac 1); |
670 br exI 1; |
670 by (rtac exI 1); |
671 br conjI 1; |
671 by (rtac conjI 1); |
672 ba 2; |
672 by (assume_tac 2); |
673 by (Step_tac 1); |
673 by (Step_tac 1); |
674 (** LEVEL 12 **) |
674 (** LEVEL 12 **) |
675 by (subgoal_tac "Crypt {|N, Agent Ba, Key K, Xa|} (shrK C) \ |
675 by (subgoal_tac "Crypt {|N, Agent Ba, Key K, Xa|} (shrK C) \ |
676 \ : parts (sees Enemy evsa)" 1); |
676 \ : parts (sees Spy evsa)" 1); |
677 by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2); |
677 by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2); |
678 by (best_tac (!claset addSEs [impOfSubs analz_subset_parts] |
678 by (best_tac (!claset addSEs [impOfSubs analz_subset_parts] |
679 addDs [impOfSubs parts_insert_subset_Un] |
679 addDs [impOfSubs parts_insert_subset_Un] |
680 addss (!simpset)) 2); |
680 addss (!simpset)) 2); |
681 by (eres_inst_tac [("V","?aa : parts {X}")] thin_rl 1); |
681 by (eres_inst_tac [("V","?aa : parts {X}")] thin_rl 1); |
682 bd parts_singleton 1; |
682 by (dtac parts_singleton 1); |
683 by (Step_tac 1); |
683 by (Step_tac 1); |
684 bd seesD 1; |
684 by (dtac seesD 1); |
685 by (Step_tac 1); |
685 by (Step_tac 1); |
686 by (Full_simp_tac 2); |
686 by (Full_simp_tac 2); |
687 by (fast_tac (!claset addSDs [spec]) 1); |
687 by (fast_tac (!claset addSDs [spec]) 1); |
688 val lemma = result(); |
688 val lemma = result(); |
689 |
689 |
694 \ (Crypt {|N, Agent B, Key K, X|} (shrK C)) \ |
694 \ (Crypt {|N, Agent B, Key K, X|} (shrK C)) \ |
695 \ : set_of_list evs; \ |
695 \ : set_of_list evs; \ |
696 \ Says S' A' \ |
696 \ Says S' A' \ |
697 \ (Crypt {|N', Agent B', Key K, X'|} (shrK C')) \ |
697 \ (Crypt {|N', Agent B', Key K, X'|} (shrK C')) \ |
698 \ : set_of_list evs; \ |
698 \ : set_of_list evs; \ |
699 \ evs : traces; C ~= Enemy; C' ~= Enemy |] ==> X = X'"; |
699 \ evs : traces; C ~= Spy; C' ~= Spy |] ==> X = X'"; |
700 bd lemma 1; |
700 by (dtac lemma 1); |
701 be exE 1; |
701 by (etac exE 1); |
702 by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1); |
702 by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1); |
703 by (Fast_tac 1); |
703 by (Fast_tac 1); |
704 qed "unique_session_keys"; |
704 qed "unique_session_keys"; |
705 |
705 |
706 |
706 |
707 |
707 |
708 (*Crucial security property: Enemy does not see the keys sent in msg NS2 |
708 (*Crucial security property: Spy does not see the keys sent in msg NS2 |
709 -- even if another key is compromised*) |
709 -- even if another key is compromised*) |
710 goal thy |
710 goal thy |
711 "!!evs. [| Says Server (Friend i) \ |
711 "!!evs. [| Says Server (Friend i) \ |
712 \ (Crypt {|N, Agent(Friend j), K, X|} K') : set_of_list evs; \ |
712 \ (Crypt {|N, Agent(Friend j), K, X|} K') : set_of_list evs; \ |
713 \ evs : traces; Friend i ~= C; Friend j ~= C \ |
713 \ evs : traces; Friend i ~= C; Friend j ~= C \ |
714 \ |] ==> \ |
714 \ |] ==> \ |
715 \ K ~: analz (insert (Key (shrK C)) (sees Enemy evs))"; |
715 \ K ~: analz (insert (Key (shrK C)) (sees Spy evs))"; |
716 be rev_mp 1; |
716 by (etac rev_mp 1); |
717 be traces.induct 1; |
717 by (etac traces.induct 1); |
718 by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes))); |
718 by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes))); |
719 (*Next 3 steps infer that K has the form "Key (newK evs'" ... *) |
719 (*Next 3 steps infer that K has the form "Key (newK evs'" ... *) |
720 by (REPEAT_FIRST (resolve_tac [conjI, impI])); |
720 by (REPEAT_FIRST (resolve_tac [conjI, impI])); |
721 by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac)); |
721 by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac)); |
722 by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac)); |
722 by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac)); |
723 by (ALLGOALS |
723 by (ALLGOALS |
724 (asm_full_simp_tac |
724 (asm_full_simp_tac |
725 (!simpset addsimps ([analz_subset_parts RS contra_subsetD, |
725 (!simpset addsimps ([analz_subset_parts RS contra_subsetD, |
726 analz_insert_Key_newK] @ pushes) |
726 analz_insert_Key_newK] @ pushes) |
727 setloop split_tac [expand_if]))); |
727 setloop split_tac [expand_if]))); |
728 (*NS2*) |
728 (*NS2*) |
729 by (fast_tac (!claset addSEs [less_irrefl]) 2); |
729 by (fast_tac (!claset addSEs [less_irrefl]) 2); |
730 (** LEVEL 8 **) |
730 (** LEVEL 8 **) |
731 (*Now for the Fake case*) |
731 (*Now for the Fake case*) |
732 br notI 1; |
732 by (rtac notI 1); |
733 by (subgoal_tac |
733 by (subgoal_tac |
734 "Key (newK evt) : \ |
734 "Key (newK evt) : \ |
735 \ analz (synth (analz (insert (Key (shrK C)) \ |
735 \ analz (synth (analz (insert (Key (shrK C)) \ |
736 \ (sees Enemy evsa))))" 1); |
736 \ (sees Spy evsa))))" 1); |
737 be (impOfSubs analz_mono) 2; |
737 by (etac (impOfSubs analz_mono) 2); |
738 by (deepen_tac (!claset addIs [analz_mono RS synth_mono RSN (2,rev_subsetD), |
738 by (deepen_tac (!claset addIs [analz_mono RS synth_mono RSN (2,rev_subsetD), |
739 impOfSubs synth_increasing, |
739 impOfSubs synth_increasing, |
740 impOfSubs analz_increasing]) 0 2); |
740 impOfSubs analz_increasing]) 0 2); |
741 (*Proves the Fake goal*) |
741 (*Proves the Fake goal*) |
742 by (fast_tac (!claset addss (!simpset)) 1); |
742 by (fast_tac (!claset addss (!simpset)) 1); |
743 |
743 |
744 (**LEVEL 13**) |
744 (**LEVEL 13**) |
745 (*NS3: that message from the Server was sent earlier*) |
745 (*NS3: that message from the Server was sent earlier*) |
860 "!!evs. evs : traces ==> \ |
860 "!!evs. evs : traces ==> \ |
861 \ ALL A B X i. Says A B (Crypt X (shrK (Friend i))) \ |
861 \ ALL A B X i. Says A B (Crypt X (shrK (Friend i))) \ |
862 \ : set_of_list evs --> \ |
862 \ : set_of_list evs --> \ |
863 \ (EX B'. Says Server B' (Crypt X (shrK (Friend i))) : set_of_list evs | \ |
863 \ (EX B'. Says Server B' (Crypt X (shrK (Friend i))) : set_of_list evs | \ |
864 \ Says (Friend i) B' (Crypt X (shrK (Friend i))) : set_of_list evs)"; |
864 \ Says (Friend i) B' (Crypt X (shrK (Friend i))) : set_of_list evs)"; |
865 be traces.induct 1; |
865 by (etac traces.induct 1); |
866 by (Step_tac 1); |
866 by (Step_tac 1); |
867 by (ALLGOALS Asm_full_simp_tac); |
867 by (ALLGOALS Asm_full_simp_tac); |
868 (*Remaining cases are Fake, NS2 and NS3*) |
868 (*Remaining cases are Fake, NS2 and NS3*) |
869 by (Fast_tac 2); (*Proves the NS2 case*) |
869 by (Fast_tac 2); (*Proves the NS2 case*) |
870 |
870 |
871 by (REPEAT (dtac spec 2)); |
871 by (REPEAT (dtac spec 2)); |
872 fe conjE; |
872 fe conjE; |
873 bd mp 2; |
873 by (dtac mp 2); |
874 |
874 |
875 by (REPEAT (resolve_tac [refl, conjI] 2)); |
875 by (REPEAT (resolve_tac [refl, conjI] 2)); |
876 by (ALLGOALS Asm_full_simp_tac); |
876 by (ALLGOALS Asm_full_simp_tac); |
877 |
877 |
878 |
878 |
879 |
879 |
880 |
880 |
881 by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2); |
881 by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2); |
882 be conjE 2; |
882 by (etac conjE 2); |
883 by ((dtac spec THEN' dtac spec THEN' dtac spec THEN' dtac spec)2); |
883 by ((dtac spec THEN' dtac spec THEN' dtac spec THEN' dtac spec)2); |
884 |
884 |
885 (*The NS3 case needs the induction hypothesis twice! |
885 (*The NS3 case needs the induction hypothesis twice! |
886 One application is to the X component of the most recent message.*) |
886 One application is to the X component of the most recent message.*) |
887 by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent A|} (shrK B)" 2); |
887 by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent A|} (shrK B)" 2); |
888 by (Fast_tac 3); |
888 by (Fast_tac 3); |
889 by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2); |
889 by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2); |
890 be conjE 2; |
890 by (etac conjE 2); |
891 (*DELETE the first quantified formula: it's now useless*) |
891 (*DELETE the first quantified formula: it's now useless*) |
892 by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2); |
892 by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2); |
893 by (fast_tac (!claset addss (!simpset)) 2); |
893 by (fast_tac (!claset addss (!simpset)) 2); |
894 (*Now for the Fake case*) |
894 (*Now for the Fake case*) |
895 be disjE 1; |
895 by (etac disjE 1); |
896 (*The subcase of Fake, where the message in question is NOT the most recent*) |
896 (*The subcase of Fake, where the message in question is NOT the most recent*) |
897 by (Best_tac 2); |
897 by (Best_tac 2); |
898 |
898 |
899 by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac)); |
899 by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac)); |
900 be Crypt_synth 1; |
900 by (etac Crypt_synth 1); |
901 be Key_synth 2; |
901 by (etac Key_synth 2); |
902 |
902 |
903 (*Split up the possibilities of that message being synthd...*) |
903 (*Split up the possibilities of that message being synthd...*) |
904 by (Step_tac 1); |
904 by (Step_tac 1); |
905 by (Best_tac 6); |
905 by (Best_tac 6); |
906 |
906 |