src/HOL/Auth/Yahalom2.thy

 (*Nobody can have used non-existent keys!  Needed to apply analz_insert_Key*)
 lemma new_keys_not_used [rule_format, simp]:
  "evs \<in> yahalom ==> Key K \<notin> used evs --> K \<notin> keysFor (parts (knows Spy evs))"
 apply (erule yahalom.induct, force,
        frule_tac [6] YM4_parts_knows_Spy, simp_all)
-(*Fake, YM3, YM4*)
-apply (blast dest!: keysFor_parts_insert)+
+txt{*Fake*}
+apply (force dest!: keysFor_parts_insert)
+txt{*YM3, YM4*}
+apply blast+
 done
 
 
 (*Describes the form of K when the Server sends this message.  Useful for
   Oops as well as main secrecy property.*)

 apply blast
 (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
 apply (force dest!: Crypt_imp_keysFor)
 (*YM4: was Crypt K (Nonce NB) the very last message?  If so, apply unicity
   of session keys; if not, use ind. hyp.*)
-apply (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys  )
+apply (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys )
 done
 
 
 text{*If B receives YM4 then A has used nonce NB (and therefore is alive).
   Moreover, A associates K with NB (thus is talking about the same run).