[STATEMENT]
theorem Spy_not_see_NB [dest]:
     "\<lbrakk>Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs;   
       \<forall>C. Says A C (Crypt (pubEK C) (Nonce NB)) \<notin> set evs;       
       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                      
     \<Longrightarrow> Nonce NB \<notin> analz (knows Spy evs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs; \<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs; A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> \<Longrightarrow> Nonce NB \<notin> analz (knows Spy evs)
[PROOF STEP]
apply (erule rev_mp, erule rev_mp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> \<Longrightarrow> (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs \<longrightarrow> Nonce NB \<notin> analz (knows Spy evs)
[PROOF STEP]
apply (erule ns_public.induct, simp_all, spy_analz)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>evs1 NAa Ba. \<lbrakk>A \<notin> bad; B \<notin> bad; evs1 \<in> ns_public; (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs1) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs1 \<longrightarrow> Nonce NB \<notin> analz (knows Spy evs1); Nonce NAa \<notin> used evs1\<rbrakk> \<Longrightarrow> Ba \<in> bad \<longrightarrow> (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs1) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs1 \<longrightarrow> NB \<noteq> NAa
 2. \<And>evs2 NBa Ba NAa Aa. \<lbrakk>A \<notin> bad; B \<notin> bad; evs2 \<in> ns_public; (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs2) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs2 \<longrightarrow> Nonce NB \<notin> analz (knows Spy evs2); Nonce NBa \<notin> used evs2; Gets Ba (Crypt (pubK Ba) \<lbrace>Nonce NAa, Agent Aa\<rbrace>) \<in> set evs2\<rbrakk> \<Longrightarrow> (Aa \<in> bad \<longrightarrow> (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs2) \<longrightarrow> (NA = NAa \<longrightarrow> A = Aa \<longrightarrow> B = Ba \<longrightarrow> NB \<noteq> NBa) \<and> (Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs2 \<longrightarrow> NB \<noteq> NAa \<and> NB \<noteq> NBa)) \<and> (Aa \<notin> bad \<longrightarrow> (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs2) \<longrightarrow> B = Ba \<and> A = Aa \<and> NA = NAa \<and> NB = NBa \<longrightarrow> Nonce NBa \<notin> analz (knows Spy evs2))
 3. \<And>evs3 Aa Ba NAa NBa. \<lbrakk>A \<notin> bad; B \<notin> bad; evs3 \<in> ns_public; (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs3) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3 \<longrightarrow> Nonce NB \<notin> analz (knows Spy evs3); Says Aa Ba (Crypt (pubK Ba) \<lbrace>Nonce NAa, Agent Aa\<rbrace>) \<in> set evs3; Gets Aa (Crypt (pubK Aa) \<lbrace>Nonce NAa, Nonce NBa\<rbrace>) \<in> set evs3\<rbrakk> \<Longrightarrow> Ba \<in> bad \<longrightarrow> (\<forall>C. (C = Ba \<longrightarrow> A = Aa \<longrightarrow> NB \<noteq> NBa) \<and> Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs3) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3 \<longrightarrow> NB \<noteq> NBa
[PROOF STEP]
apply (simp_all add: all_conj_distrib)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>evs1 NAa Ba. \<lbrakk>A \<notin> bad; B \<notin> bad; evs1 \<in> ns_public; (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs1) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs1 \<longrightarrow> Nonce NB \<notin> analz (knows Spy evs1); Nonce NAa \<notin> used evs1\<rbrakk> \<Longrightarrow> Ba \<in> bad \<longrightarrow> (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs1) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs1 \<longrightarrow> NB \<noteq> NAa
 2. \<And>evs2 NBa Ba NAa Aa. \<lbrakk>A \<notin> bad; B \<notin> bad; evs2 \<in> ns_public; (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs2) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs2 \<longrightarrow> Nonce NB \<notin> analz (knows Spy evs2); Nonce NBa \<notin> used evs2; Gets Ba (Crypt (pubK Ba) \<lbrace>Nonce NAa, Agent Aa\<rbrace>) \<in> set evs2\<rbrakk> \<Longrightarrow> (Aa \<in> bad \<longrightarrow> (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs2) \<longrightarrow> (NA = NAa \<longrightarrow> A = Aa \<longrightarrow> B = Ba \<longrightarrow> NB \<noteq> NBa) \<and> (Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs2 \<longrightarrow> NB \<noteq> NAa \<and> NB \<noteq> NBa)) \<and> (Aa \<notin> bad \<longrightarrow> (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs2) \<longrightarrow> B = Ba \<and> A = Aa \<and> NA = NAa \<and> NB = NBa \<longrightarrow> Nonce NBa \<notin> analz (knows Spy evs2))
 3. \<And>evs3 Aa Ba NAa NBa. \<lbrakk>A \<notin> bad; B \<notin> bad; evs3 \<in> ns_public; (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs3) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3 \<longrightarrow> Nonce NB \<notin> analz (knows Spy evs3); Says Aa Ba (Crypt (pubK Ba) \<lbrace>Nonce NAa, Agent Aa\<rbrace>) \<in> set evs3; Gets Aa (Crypt (pubK Aa) \<lbrace>Nonce NAa, Nonce NBa\<rbrace>) \<in> set evs3\<rbrakk> \<Longrightarrow> Ba \<in> bad \<longrightarrow> (A = Aa \<longrightarrow> NB \<noteq> NBa) \<and> (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs3) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3 \<longrightarrow> NB \<noteq> NBa
[PROOF STEP]
(*speeds up the next step*)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>evs1 NAa Ba. \<lbrakk>A \<notin> bad; B \<notin> bad; evs1 \<in> ns_public; (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs1) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs1 \<longrightarrow> Nonce NB \<notin> analz (knows Spy evs1); Nonce NAa \<notin> used evs1\<rbrakk> \<Longrightarrow> Ba \<in> bad \<longrightarrow> (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs1) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs1 \<longrightarrow> NB \<noteq> NAa
 2. \<And>evs2 NBa Ba NAa Aa. \<lbrakk>A \<notin> bad; B \<notin> bad; evs2 \<in> ns_public; (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs2) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs2 \<longrightarrow> Nonce NB \<notin> analz (knows Spy evs2); Nonce NBa \<notin> used evs2; Gets Ba (Crypt (pubK Ba) \<lbrace>Nonce NAa, Agent Aa\<rbrace>) \<in> set evs2\<rbrakk> \<Longrightarrow> (Aa \<in> bad \<longrightarrow> (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs2) \<longrightarrow> (NA = NAa \<longrightarrow> A = Aa \<longrightarrow> B = Ba \<longrightarrow> NB \<noteq> NBa) \<and> (Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs2 \<longrightarrow> NB \<noteq> NAa \<and> NB \<noteq> NBa)) \<and> (Aa \<notin> bad \<longrightarrow> (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs2) \<longrightarrow> B = Ba \<and> A = Aa \<and> NA = NAa \<and> NB = NBa \<longrightarrow> Nonce NBa \<notin> analz (knows Spy evs2))
 3. \<And>evs3 Aa Ba NAa NBa. \<lbrakk>A \<notin> bad; B \<notin> bad; evs3 \<in> ns_public; (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs3) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3 \<longrightarrow> Nonce NB \<notin> analz (knows Spy evs3); Says Aa Ba (Crypt (pubK Ba) \<lbrace>Nonce NAa, Agent Aa\<rbrace>) \<in> set evs3; Gets Aa (Crypt (pubK Aa) \<lbrace>Nonce NAa, Nonce NBa\<rbrace>) \<in> set evs3\<rbrakk> \<Longrightarrow> Ba \<in> bad \<longrightarrow> (A = Aa \<longrightarrow> NB \<noteq> NBa) \<and> (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs3) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3 \<longrightarrow> NB \<noteq> NBa
[PROOF STEP]
apply (blast intro: no_nonce_NS1_NS2)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done