equal
deleted
inserted
replaced
274 (asm_simp_tac |
274 (asm_simp_tac |
275 (!simpset addsimps ([analz_insert_eq, analz_insert_freshK] @ pushes) |
275 (!simpset addsimps ([analz_insert_eq, analz_insert_freshK] @ pushes) |
276 setloop split_tac [expand_if]))); |
276 setloop split_tac [expand_if]))); |
277 (*Oops*) |
277 (*Oops*) |
278 by (blast_tac (!claset addDs [unique_session_keys]) 5); |
278 by (blast_tac (!claset addDs [unique_session_keys]) 5); |
279 (*NS4*) |
279 (*NS3, replay sub-case*) |
280 by (Blast_tac 4); |
280 by (Blast_tac 4); |
281 (*NS2*) |
281 (*NS2*) |
282 by (blast_tac (!claset addSEs sees_Spy_partsEs |
282 by (blast_tac (!claset addSEs sees_Spy_partsEs |
283 addIs [parts_insertI, impOfSubs analz_subset_parts]) 2); |
283 addIs [parts_insertI, impOfSubs analz_subset_parts]) 2); |
284 (*Fake*) |
284 (*Fake*) |
285 by (spy_analz_tac 1); |
285 by (spy_analz_tac 1); |
286 (*NS3*) (**LEVEL 6 **) |
286 (*NS3, Server sub-case*) (**LEVEL 6 **) |
287 by (step_tac (!claset delrules [impCE]) 1); |
287 by (step_tac (!claset delrules [impCE]) 1); |
288 by (forward_tac [Says_imp_sees_Spy RS parts.Inj RS A_trusts_NS2] 1); |
288 by (forward_tac [Says_imp_sees_Spy RS parts.Inj RS A_trusts_NS2] 1); |
289 by (assume_tac 2); |
289 by (assume_tac 2); |
290 by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj RS |
290 by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj RS |
291 Crypt_Spy_analz_lost]) 1); |
291 Crypt_Spy_analz_lost]) 1); |