296 by (EVERY (map spy_analz_tac [4,1])); |
296 by (EVERY (map spy_analz_tac [4,1])); |
297 (*NS2*) |
297 (*NS2*) |
298 by (fast_tac (!claset addSEs sees_Spy_partsEs |
298 by (fast_tac (!claset addSEs sees_Spy_partsEs |
299 addIs [parts_insertI, impOfSubs analz_subset_parts] |
299 addIs [parts_insertI, impOfSubs analz_subset_parts] |
300 addss (!simpset)) 1); |
300 addss (!simpset)) 1); |
301 (*NS3 and Oops subcases*) (**LEVEL 5 **) |
301 (*Oops*) |
|
302 by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 2); |
|
303 (*NS3*) (**LEVEL 6 **) |
302 by (step_tac (!claset delrules [impCE]) 1); |
304 by (step_tac (!claset delrules [impCE]) 1); |
303 by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2); |
|
304 by (etac conjE 2); |
|
305 by (mp_tac 2); |
|
306 (**LEVEL 9 **) |
|
307 by (forward_tac [Says_imp_sees_Spy RS parts.Inj RS A_trusts_NS2] 2); |
|
308 by (assume_tac 3); |
|
309 by (fast_tac (!claset addSEs [Says_Crypt_not_lost]) 2); |
|
310 by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 2); |
|
311 (*NS3*) |
|
312 by (forward_tac [Says_imp_sees_Spy RS parts.Inj RS A_trusts_NS2] 1); |
305 by (forward_tac [Says_imp_sees_Spy RS parts.Inj RS A_trusts_NS2] 1); |
313 by (assume_tac 2); |
306 by (assume_tac 2); |
314 by (fast_tac (!claset addSEs [Says_Crypt_not_lost]) 1); |
307 by (fast_tac (!claset addSEs [Says_Crypt_not_lost]) 1); |
315 by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1); |
308 by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1); |
316 val lemma = result() RS mp RS mp RSN(2,rev_notE); |
309 val lemma = result() RS mp RS mp RSN(2,rev_notE); |