src/HOL/Auth/Yahalom2.thy
changeset 13926 6e62e5357a10
parent 13907 2bc462b99e70
child 13956 8fe7e12290e1
     1.1 --- a/src/HOL/Auth/Yahalom2.thy	Sat Apr 26 12:38:17 2003 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom2.thy	Sat Apr 26 12:38:42 2003 +0200
     1.3 @@ -137,8 +137,10 @@
     1.4   "evs \<in> yahalom ==> Key K \<notin> used evs --> K \<notin> keysFor (parts (knows Spy evs))"
     1.5  apply (erule yahalom.induct, force,
     1.6         frule_tac [6] YM4_parts_knows_Spy, simp_all)
     1.7 -(*Fake, YM3, YM4*)
     1.8 -apply (blast dest!: keysFor_parts_insert)+
     1.9 +txt{*Fake*}
    1.10 +apply (force dest!: keysFor_parts_insert)
    1.11 +txt{*YM3, YM4*}
    1.12 +apply blast+
    1.13  done
    1.14  
    1.15  
    1.16 @@ -394,7 +396,7 @@
    1.17  apply (force dest!: Crypt_imp_keysFor)
    1.18  (*YM4: was Crypt K (Nonce NB) the very last message?  If so, apply unicity
    1.19    of session keys; if not, use ind. hyp.*)
    1.20 -apply (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys  )
    1.21 +apply (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys )
    1.22  done
    1.23  
    1.24