[STATEMENT]
lemma B_trusts_WL5:
     "[| Says S B (Crypt (shrK B) \<lbrace>Agent A, Nonce NB\<rbrace>) \<in> set evs;
         A \<notin> bad;  B \<notin> bad;  evs \<in> woolam  |]
      ==> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Says S B (Crypt (shrK B) \<lbrace>Agent A, Nonce NB\<rbrace>) \<in> set evs; A \<notin> bad; B \<notin> bad; evs \<in> woolam\<rbrakk> \<Longrightarrow> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs
[PROOF STEP]
by (blast dest!: NB_Crypt_imp_Server_msg)