[STATEMENT]
lemma Spy_dont_know_TTPKey_parts [simp]:
     "evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> parts(spies evs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evs \<in> certified_mail \<Longrightarrow> Key (privateKey b TTP) \<notin> parts (knows Spy evs)
[PROOF STEP]
by simp