equal
deleted
inserted
replaced
272 apply (case_tac "K:invKey`Ks") |
272 apply (case_tac "K:invKey`Ks") |
273 (* K:invKey`Ks *) |
273 (* K:invKey`Ks *) |
274 apply (clarsimp, blast) |
274 apply (clarsimp, blast) |
275 (* K ~:invKey`Ks *) |
275 (* K ~:invKey`Ks *) |
276 apply (subgoal_tac "Guard n Ks (set (decrypt' l' K Y))") |
276 apply (subgoal_tac "Guard n Ks (set (decrypt' l' K Y))") |
277 apply (drule_tac x="decrypt' l' K Y" in spec, simp add: set_mem_eq) |
277 apply (drule_tac x="decrypt' l' K Y" in spec, simp add: mem_iff) |
278 apply (subgoal_tac "Crypt K Y:parts (set l)") |
278 apply (subgoal_tac "Crypt K Y:parts (set l)") |
279 apply (drule parts_cnb, rotate_tac -1, simp) |
279 apply (drule parts_cnb, rotate_tac -1, simp) |
280 apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub) |
280 apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub) |
281 apply (rule insert_mono, rule set_minus) |
281 apply (rule insert_mono, rule set_minus) |
282 apply (simp add: analz_insertD, blast) |
282 apply (simp add: analz_insertD, blast) |