1.1 --- a/src/HOL/Auth/NS_Shared.thy	Thu Aug 27 09:28:52 2009 +0200
     1.2 +++ b/src/HOL/Auth/NS_Shared.thy	Thu Aug 27 15:49:45 2009 +0100
     1.3 @@ -318,9 +318,7 @@
     1.4      @{term "Crypt K (Nonce NB) \<in> parts (spies evs2)"} *} 
     1.5  apply (force dest!: Crypt_imp_keysFor)
     1.6  txt{*NS4*}
     1.7 -apply (blast dest: B_trusts_NS3
     1.8 -	           Says_imp_knows_Spy [THEN analz.Inj]
     1.9 -                   Crypt_Spy_analz_bad unique_session_keys)
    1.10 +apply (metis B_trusts_NS3 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst unique_session_keys)
    1.11  done
    1.12  
    1.13  text{*This version no longer assumes that K is secure*}
    1.14 @@ -349,9 +347,7 @@
    1.15  txt{*NS2*}
    1.16  apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
    1.17  txt{*NS4*}
    1.18 -apply (blast dest: B_trusts_NS3
    1.19 -	     dest: Says_imp_knows_Spy [THEN analz.Inj]
    1.20 -                   unique_session_keys Crypt_Spy_analz_bad)
    1.21 +apply (metis B_trusts_NS3 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst unique_session_keys)
    1.22  done
    1.23  
    1.24  
    1.25 @@ -475,18 +471,15 @@
    1.26  apply (erule rev_mp)
    1.27  apply (erule rev_mp)
    1.28  apply (erule ns_shared.induct, analz_mono_contra)
    1.29 -apply (frule_tac [5] Says_S_message_form)
    1.30  apply (simp_all)
    1.31  txt{*Fake*}
    1.32  apply blast
    1.33  txt{*NS2*}
    1.34  apply (force dest!: Crypt_imp_keysFor)
    1.35 -txt{*NS3, much quicker having installed @{term Says_S_message_form} before simplication*}
    1.36 -apply fastsimp
    1.37 +txt{*NS3*}
    1.38 +apply (metis NS3_msg_in_parts_spies parts_cut_eq)
    1.39  txt{*NS5, the most important case, can be solved by unicity*}
    1.40 -apply (case_tac "Aa \<in> bad")
    1.41 -apply (force dest!: Says_imp_spies [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Snd, THEN analz.Snd, THEN analz.Fst])
    1.42 -apply (blast dest: A_trusts_NS2 unique_session_keys)
    1.43 +apply (metis A_trusts_NS2 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst analz.Snd unique_session_keys)
    1.44  done
    1.45  
    1.46  lemma A_Issues_B: