334 \ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs --> \ |
334 \ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs --> \ |
335 \ Key K ~: analz (sees lost Spy evs)"; |
335 \ Key K ~: analz (sees lost Spy evs)"; |
336 by (etac otway.induct 1); |
336 by (etac otway.induct 1); |
337 by analz_Fake_tac; |
337 by analz_Fake_tac; |
338 by (ALLGOALS |
338 by (ALLGOALS |
339 (asm_full_simp_tac |
339 (asm_simp_tac (!simpset addsimps ([not_parts_not_analz, |
340 (!simpset addsimps ([analz_subset_parts RS contra_subsetD, |
340 analz_insert_Key_newK] @ pushes) |
341 analz_insert_Key_newK] @ pushes) |
341 setloop split_tac [expand_if]))); |
342 setloop split_tac [expand_if]))); |
|
343 (*OR3*) |
342 (*OR3*) |
344 by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl] |
343 by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl] |
345 addss (!simpset addsimps [parts_insert2])) 3); |
344 addss (!simpset addsimps [parts_insert2])) 3); |
346 (*OR4, OR2, Fake*) |
345 (*OR4, OR2, Fake*) |
347 by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac)); |
346 by (REPEAT_FIRST spy_analz_tac); |
348 (*Oops*) (** LEVEL 5 **) |
347 (*Oops*) (** LEVEL 5 **) |
349 by (fast_tac (!claset delrules [disjE] |
348 by (fast_tac (!claset delrules [disjE] |
350 addDs [unique_session_keys] addss (!simpset)) 1); |
349 addDs [unique_session_keys] addss (!simpset)) 1); |
351 val lemma = result() RS mp RS mp RSN(2,rev_notE); |
350 val lemma = result() RS mp RS mp RSN(2,rev_notE); |
352 |
351 |