equal
deleted
inserted
replaced
185 by (spy_analz_tac 1); |
185 by (spy_analz_tac 1); |
186 qed_spec_mp "analz_image_freshK"; |
186 qed_spec_mp "analz_image_freshK"; |
187 |
187 |
188 |
188 |
189 Goal "[| evs \\<in> kerberos_ban; KAB \\<notin> range shrK |] ==> \ |
189 Goal "[| evs \\<in> kerberos_ban; KAB \\<notin> range shrK |] ==> \ |
190 \ Key K \\<in> analz (insert (Key KAB) (spies evs)) = \ |
190 \ (Key K \\<in> analz (insert (Key KAB) (spies evs))) = \ |
191 \ (K = KAB | Key K \\<in> analz (spies evs))"; |
191 \ (K = KAB | Key K \\<in> analz (spies evs))"; |
192 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); |
192 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); |
193 qed "analz_insert_freshK"; |
193 qed "analz_insert_freshK"; |
194 |
194 |
195 |
195 |