src/HOL/Auth/NS_Public_Bad.thy
changeset 13507 febb8e5d2a9d
parent 11366 b42287eb20cf
child 13922 75ae4244a596
     1.1 --- a/src/HOL/Auth/NS_Public_Bad.thy	Fri Aug 16 17:19:43 2002 +0200
     1.2 +++ b/src/HOL/Auth/NS_Public_Bad.thy	Sat Aug 17 14:55:08 2002 +0200
     1.3 @@ -106,8 +106,7 @@
     1.4          A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                     
     1.5         \<Longrightarrow> Nonce NA \<notin> analz (spies evs)"
     1.6  apply (erule rev_mp)   
     1.7 -apply (erule ns_public.induct, simp_all)
     1.8 -apply spy_analz
     1.9 +apply (erule ns_public.induct, simp_all, spy_analz)
    1.10  apply (blast dest: unique_NA intro: no_nonce_NS1_NS2)+
    1.11  done
    1.12  
    1.13 @@ -167,8 +166,7 @@
    1.14         A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                      
    1.15       \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
    1.16  apply (erule rev_mp, erule rev_mp)
    1.17 -apply (erule ns_public.induct, simp_all)
    1.18 -apply spy_analz
    1.19 +apply (erule ns_public.induct, simp_all, spy_analz)
    1.20  apply (simp_all add: all_conj_distrib) (*speeds up the next step*)
    1.21  apply (blast intro: no_nonce_NS1_NS2)+
    1.22  done
    1.23 @@ -197,17 +195,15 @@
    1.24  lemma "\<lbrakk>A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>            
    1.25         \<Longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs  
    1.26             \<longrightarrow> Nonce NB \<notin> analz (spies evs)"
    1.27 -apply (erule ns_public.induct, simp_all)
    1.28 -apply spy_analz
    1.29 +apply (erule ns_public.induct, simp_all, spy_analz)
    1.30  (*NS1: by freshness*)
    1.31  apply blast
    1.32  (*NS2: by freshness and unicity of NB*)
    1.33  apply (blast intro: no_nonce_NS1_NS2)
    1.34  (*NS3: unicity of NB identifies A and NA, but not B*)
    1.35  apply clarify
    1.36 -apply (frule_tac A' = "A" in 
    1.37 -       Says_imp_knows_Spy [THEN parts.Inj, THEN unique_NB])
    1.38 -apply auto
    1.39 +apply (frule_tac A' = A in 
    1.40 +       Says_imp_knows_Spy [THEN parts.Inj, THEN unique_NB], auto)
    1.41  apply (rename_tac C B' evs3)
    1.42  oops
    1.43