equal
deleted
inserted
replaced
194 done |
194 done |
195 |
195 |
196 |
196 |
197 lemma analz_insert_freshK: |
197 lemma analz_insert_freshK: |
198 "[| evs \<in> otway; KAB \<notin> range shrK |] ==> |
198 "[| evs \<in> otway; KAB \<notin> range shrK |] ==> |
199 Key K \<in> analz (insert (Key KAB) (knows Spy evs)) = |
199 (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = |
200 (K = KAB | Key K \<in> analz (knows Spy evs))" |
200 (K = KAB | Key K \<in> analz (knows Spy evs))" |
201 by (simp only: analz_image_freshK analz_image_freshK_simps) |
201 by (simp only: analz_image_freshK analz_image_freshK_simps) |
202 |
202 |
203 |
203 |
204 (*** The Key K uniquely identifies the Server's message. **) |
204 (*** The Key K uniquely identifies the Server's message. **) |