equal
deleted
inserted
replaced
228 done |
228 done |
229 |
229 |
230 |
230 |
231 lemma analz_insert_freshK: |
231 lemma analz_insert_freshK: |
232 "\\<lbrakk>evs \\<in> ns_shared; KAB \\<notin> range shrK\\<rbrakk> \\<Longrightarrow> |
232 "\\<lbrakk>evs \\<in> ns_shared; KAB \\<notin> range shrK\\<rbrakk> \\<Longrightarrow> |
233 Key K \\<in> analz (insert (Key KAB) (spies evs)) = |
233 (Key K \\<in> analz (insert (Key KAB) (spies evs))) = |
234 (K = KAB \\<or> Key K \\<in> analz (spies evs))" |
234 (K = KAB \\<or> Key K \\<in> analz (spies evs))" |
235 by (simp only: analz_image_freshK analz_image_freshK_simps) |
235 by (simp only: analz_image_freshK analz_image_freshK_simps) |
236 |
236 |
237 |
237 |
238 (** The session key K uniquely identifies the message **) |
238 (** The session key K uniquely identifies the message **) |