src/HOL/Auth/NS_Shared.thy
changeset 11251 a6816d47f41d
parent 11188 5d539f1682c3
child 11280 6fdc4c4ccec1
     1.1 --- a/src/HOL/Auth/NS_Shared.thy	Wed Apr 11 11:53:54 2001 +0200
     1.2 +++ b/src/HOL/Auth/NS_Shared.thy	Thu Apr 12 12:45:05 2001 +0200
     1.3 @@ -20,8 +20,8 @@
     1.4  	(*The spy MAY say anything he CAN say.  We do not expect him to
     1.5  	  invent new nonces here, but he can also use NS1.  Common to
     1.6  	  all similar protocols.*)
     1.7 -  Fake: "\<lbrakk>evs \<in> ns_shared;  X \<in> synth (analz (spies evs))\<rbrakk>
     1.8 -	 \<Longrightarrow> Says Spy B X # evs \<in> ns_shared"
     1.9 +  Fake: "\<lbrakk>evsf \<in> ns_shared;  X \<in> synth (analz (spies evsf))\<rbrakk>
    1.10 +	 \<Longrightarrow> Says Spy B X # evsf \<in> ns_shared"
    1.11  
    1.12  	(*Alice initiates a protocol run, requesting to talk to any B*)
    1.13    NS1:  "\<lbrakk>evs1 \<in> ns_shared;  Nonce NA \<notin> used evs1\<rbrakk>
    1.14 @@ -74,10 +74,8 @@
    1.15  
    1.16  declare Says_imp_knows_Spy [THEN parts.Inj, dest]
    1.17  declare parts.Body  [dest]
    1.18 -declare MPair_parts [elim!]    (*can speed up some proofs*)
    1.19 -
    1.20 -declare analz_subset_parts [THEN subsetD, dest]
    1.21 -declare Fake_parts_insert  [THEN subsetD, dest]
    1.22 +declare Fake_parts_insert_in_Un  [dest]
    1.23 +declare analz_into_parts [dest]
    1.24  declare image_eq_UN [simp]  (*accelerates proofs involving nested images*)
    1.25  
    1.26  
    1.27 @@ -123,7 +121,6 @@
    1.28  apply blast+;
    1.29  done
    1.30  
    1.31 -
    1.32  lemma Spy_analz_shrK [simp]:
    1.33       "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
    1.34  by auto
    1.35 @@ -310,8 +307,7 @@
    1.36        Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
    1.37        Says B A (Crypt K (Nonce NB)) \<in> set evs"
    1.38  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
    1.39 -apply analz_mono_contra
    1.40 -apply simp_all
    1.41 +apply (analz_mono_contra, simp_all)
    1.42  apply blast     (*Fake*)
    1.43  (*NS2: contradiction from the assumptions  
    1.44    Key K \<notin> used evs2  and Crypt K (Nonce NB) \<in> parts (spies evs2) *)