[STATEMENT]
lemma Auth_A_to_B_lemma [rule_format]:
     "evs \<in> yahalom
      \<Longrightarrow> Key K \<notin> analz (knows Spy evs) \<longrightarrow>
          K \<in> symKeys \<longrightarrow>
          Crypt K (Nonce NB) \<in> parts (knows Spy evs) \<longrightarrow>
          Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>
            \<in> parts (knows Spy evs) \<longrightarrow>
          B \<notin> bad \<longrightarrow>
          (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evs \<in> yahalom \<Longrightarrow> Key K \<notin> analz (knows Spy evs) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs)
[PROOF STEP]
apply (erule yahalom.induct, force,
       frule_tac [6] YM4_parts_knows_Spy)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>evsf X Ba. \<lbrakk>evsf \<in> yahalom; Key K \<notin> analz (knows Spy evsf) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evsf) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evsf) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evsf); X \<in> synth (analz (knows Spy evsf))\<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy (Says Spy Ba X # evsf)) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy (Says Spy Ba X # evsf)) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy (Says Spy Ba X # evsf)) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>Xa. Says A B \<lbrace>Xa, Crypt K (Nonce NB)\<rbrace> \<in> set (Says Spy Ba X # evsf))
 2. \<And>evsr Aa Ba X. \<lbrakk>evsr \<in> yahalom; Key K \<notin> analz (knows Spy evsr) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evsr) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evsr) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evsr); Says Aa Ba X \<in> set evsr\<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy (Gets Ba X # evsr)) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy (Gets Ba X # evsr)) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy (Gets Ba X # evsr)) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>Xa. Says A B \<lbrace>Xa, Crypt K (Nonce NB)\<rbrace> \<in> set (Gets Ba X # evsr))
 3. \<And>evs1 NA Aa Ba. \<lbrakk>evs1 \<in> yahalom; Key K \<notin> analz (knows Spy evs1) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs1) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs1) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs1); Nonce NA \<notin> used evs1\<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy (Says Aa Ba \<lbrace>Agent Aa, Nonce NA\<rbrace> # evs1)) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy (Says Aa Ba \<lbrace>Agent Aa, Nonce NA\<rbrace> # evs1)) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy (Says Aa Ba \<lbrace>Agent Aa, Nonce NA\<rbrace> # evs1)) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set (Says Aa Ba \<lbrace>Agent Aa, Nonce NA\<rbrace> # evs1))
 4. \<And>evs2 NBa Ba Aa NA. \<lbrakk>evs2 \<in> yahalom; Key K \<notin> analz (knows Spy evs2) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs2) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs2) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs2); Nonce NBa \<notin> used evs2; Gets Ba \<lbrace>Agent Aa, Nonce NA\<rbrace> \<in> set evs2\<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy (Says Ba Server \<lbrace>Agent Ba, Nonce NBa, Crypt (shrK Ba) \<lbrace>Agent Aa, Nonce NA\<rbrace>\<rbrace> # evs2)) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy (Says Ba Server \<lbrace>Agent Ba, Nonce NBa, Crypt (shrK Ba) \<lbrace>Agent Aa, Nonce NA\<rbrace>\<rbrace> # evs2)) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy (Says Ba Server \<lbrace>Agent Ba, Nonce NBa, Crypt (shrK Ba) \<lbrace>Agent Aa, Nonce NA\<rbrace>\<rbrace> # evs2)) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set (Says Ba Server \<lbrace>Agent Ba, Nonce NBa, Crypt (shrK Ba) \<lbrace>Agent Aa, Nonce NA\<rbrace>\<rbrace> # evs2))
 5. \<And>evs3 KAB Ba NBa Aa NA. \<lbrakk>evs3 \<in> yahalom; Key K \<notin> analz (knows Spy evs3) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs3) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs3) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs3); Key KAB \<notin> used evs3; Gets Server \<lbrace>Agent Ba, Nonce NBa, Crypt (shrK Ba) \<lbrace>Agent Aa, Nonce NA\<rbrace>\<rbrace> \<in> set evs3\<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy (Says Server Aa \<lbrace>Nonce NBa, Crypt (shrK Aa) \<lbrace>Agent Ba, Key KAB, Nonce NA\<rbrace>, Crypt (shrK Ba) \<lbrace>Agent Aa, Agent Ba, Key KAB, Nonce NBa\<rbrace>\<rbrace> # evs3)) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy (Says Server Aa \<lbrace>Nonce NBa, Crypt (shrK Aa) \<lbrace>Agent Ba, Key KAB, Nonce NA\<rbrace>, Crypt (shrK Ba) \<lbrace>Agent Aa, Agent Ba, Key KAB, Nonce NBa\<rbrace>\<rbrace> # evs3)) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy (Says Server Aa \<lbrace>Nonce NBa, Crypt (shrK Aa) \<lbrace>Agent Ba, Key KAB, Nonce NA\<rbrace>, Crypt (shrK Ba) \<lbrace>Agent Aa, Agent Ba, Key KAB, Nonce NBa\<rbrace>\<rbrace> # evs3)) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set (Says Server Aa \<lbrace>Nonce NBa, Crypt (shrK Aa) \<lbrace>Agent Ba, Key KAB, Nonce NA\<rbrace>, Crypt (shrK Ba) \<lbrace>Agent Aa, Agent Ba, Key KAB, Nonce NBa\<rbrace>\<rbrace> # evs3))
 6. \<And>evs4 Aa NBa Ba Ka NA X. \<lbrakk>evs4 \<in> yahalom; Key K \<notin> analz (knows Spy evs4) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs4) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs4); Gets Aa \<lbrace>Nonce NBa, Crypt (shrK Aa) \<lbrace>Agent Ba, Key Ka, Nonce NA\<rbrace>, X\<rbrace> \<in> set evs4; Says Aa Ba \<lbrace>Agent Aa, Nonce NA\<rbrace> \<in> set evs4\<rbrakk> \<Longrightarrow> evs4 \<in> yahalom
 7. \<And>evs4 Aa NBa Ba Ka NA X. \<lbrakk>evs4 \<in> yahalom; Key K \<notin> analz (knows Spy evs4) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs4) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs4); Gets Aa \<lbrace>Nonce NBa, Crypt (shrK Aa) \<lbrace>Agent Ba, Key Ka, Nonce NA\<rbrace>, X\<rbrace> \<in> set evs4; Says Aa Ba \<lbrace>Agent Aa, Nonce NA\<rbrace> \<in> set evs4; X \<in> parts (knows Spy evs4)\<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy (Says Aa Ba \<lbrace>X, Crypt Ka (Nonce NBa)\<rbrace> # evs4)) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy (Says Aa Ba \<lbrace>X, Crypt Ka (Nonce NBa)\<rbrace> # evs4)) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy (Says Aa Ba \<lbrace>X, Crypt Ka (Nonce NBa)\<rbrace> # evs4)) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>Xa. Says A B \<lbrace>Xa, Crypt K (Nonce NB)\<rbrace> \<in> set (Says Aa Ba \<lbrace>X, Crypt Ka (Nonce NBa)\<rbrace> # evs4))
 8. \<And>evso Aa NBa Ba Ka NA X. \<lbrakk>evso \<in> yahalom; Key K \<notin> analz (knows Spy evso) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evso) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evso) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evso); Says Server Aa \<lbrace>Nonce NBa, Crypt (shrK Aa) \<lbrace>Agent Ba, Key Ka, Nonce NA\<rbrace>, X\<rbrace> \<in> set evso\<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy (Notes Spy \<lbrace>Nonce NA, Nonce NBa, Key Ka\<rbrace> # evso)) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy (Notes Spy \<lbrace>Nonce NA, Nonce NBa, Key Ka\<rbrace> # evso)) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy (Notes Spy \<lbrace>Nonce NA, Nonce NBa, Key Ka\<rbrace> # evso)) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set (Notes Spy \<lbrace>Nonce NA, Nonce NBa, Key Ka\<rbrace> # evso))
[PROOF STEP]
apply (analz_mono_contra, simp_all)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>evsf X Ba. \<lbrakk>evsf \<in> yahalom; X \<in> synth (analz (knows Spy evsf)); Key K \<notin> analz (knows Spy evsf); K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evsf) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evsf) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evsf)\<rbrakk> \<Longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (insert X (knows Spy evsf)) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (insert X (knows Spy evsf)) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>Xa. A = Spy \<and> B = Ba \<and> \<lbrace>Xa, Crypt K (Nonce NB)\<rbrace> = X \<or> Says A B \<lbrace>Xa, Crypt K (Nonce NB)\<rbrace> \<in> set evsf)
 2. \<And>evs3 KAB Ba NBa Aa NA. \<lbrakk>evs3 \<in> yahalom; Key KAB \<notin> used evs3; Gets Server \<lbrace>Agent Ba, Nonce NBa, Crypt (shrK Ba) \<lbrace>Agent Aa, Nonce NA\<rbrace>\<rbrace> \<in> set evs3; Key K \<notin> analz (knows Spy evs3); K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs3) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs3) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs3)\<rbrakk> \<Longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs3) \<longrightarrow> B = Ba \<and> A = Aa \<and> B = Ba \<and> K = KAB \<and> NB = NBa \<longrightarrow> Ba \<notin> bad \<longrightarrow> (\<exists>X. Says Aa Ba \<lbrace>X, Crypt KAB (Nonce NBa)\<rbrace> \<in> set evs3)
 3. \<And>evs4 Aa NBa Ba Ka NA X. \<lbrakk>evs4 \<in> yahalom; Gets Aa \<lbrace>Nonce NBa, Crypt (shrK Aa) \<lbrace>Agent Ba, Key Ka, Nonce NA\<rbrace>, X\<rbrace> \<in> set evs4; Says Aa Ba \<lbrace>Agent Aa, Nonce NA\<rbrace> \<in> set evs4; X \<in> parts (knows Spy evs4); Key K \<notin> analz (knows Spy evs4); K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs4) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs4)\<rbrakk> \<Longrightarrow> K \<in> symKeys \<longrightarrow> (K = Ka \<and> NB = NBa \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key Ka, Nonce NBa\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>Xa. A = Aa \<and> B = Ba \<and> Xa = X \<or> Says A B \<lbrace>Xa, Crypt Ka (Nonce NBa)\<rbrace> \<in> set evs4)) \<and> (Crypt K (Nonce NB) \<in> parts (knows Spy evs4) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>Xa. A = Aa \<and> B = Ba \<and> Xa = X \<and> K = Ka \<and> NB = NBa \<or> Says A B \<lbrace>Xa, Crypt K (Nonce NB)\<rbrace> \<in> set evs4))
[PROOF STEP]
subgoal \<comment> \<open>Fake\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evsf_ \<in> yahalom; X_ \<in> synth (analz (knows Spy evsf_)); Key K \<notin> analz (knows Spy evsf_); K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evsf_) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evsf_) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evsf_)\<rbrakk> \<Longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (insert X_ (knows Spy evsf_)) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (insert X_ (knows Spy evsf_)) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>Xa. A = Spy \<and> B = Ba_ \<and> \<lbrace>Xa, Crypt K (Nonce NB)\<rbrace> = X_ \<or> Says A B \<lbrace>Xa, Crypt K (Nonce NB)\<rbrace> \<in> set evsf_)
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>evs3 KAB Ba NBa Aa NA. \<lbrakk>evs3 \<in> yahalom; Key KAB \<notin> used evs3; Gets Server \<lbrace>Agent Ba, Nonce NBa, Crypt (shrK Ba) \<lbrace>Agent Aa, Nonce NA\<rbrace>\<rbrace> \<in> set evs3; Key K \<notin> analz (knows Spy evs3); K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs3) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs3) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs3)\<rbrakk> \<Longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs3) \<longrightarrow> B = Ba \<and> A = Aa \<and> B = Ba \<and> K = KAB \<and> NB = NBa \<longrightarrow> Ba \<notin> bad \<longrightarrow> (\<exists>X. Says Aa Ba \<lbrace>X, Crypt KAB (Nonce NBa)\<rbrace> \<in> set evs3)
 2. \<And>evs4 Aa NBa Ba Ka NA X. \<lbrakk>evs4 \<in> yahalom; Gets Aa \<lbrace>Nonce NBa, Crypt (shrK Aa) \<lbrace>Agent Ba, Key Ka, Nonce NA\<rbrace>, X\<rbrace> \<in> set evs4; Says Aa Ba \<lbrace>Agent Aa, Nonce NA\<rbrace> \<in> set evs4; X \<in> parts (knows Spy evs4); Key K \<notin> analz (knows Spy evs4); K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs4) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs4)\<rbrakk> \<Longrightarrow> K \<in> symKeys \<longrightarrow> (K = Ka \<and> NB = NBa \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key Ka, Nonce NBa\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>Xa. A = Aa \<and> B = Ba \<and> Xa = X \<or> Says A B \<lbrace>Xa, Crypt Ka (Nonce NBa)\<rbrace> \<in> set evs4)) \<and> (Crypt K (Nonce NB) \<in> parts (knows Spy evs4) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>Xa. A = Aa \<and> B = Ba \<and> Xa = X \<and> K = Ka \<and> NB = NBa \<or> Says A B \<lbrace>Xa, Crypt K (Nonce NB)\<rbrace> \<in> set evs4))
[PROOF STEP]
subgoal \<comment> \<open>YM3 because the message \<^term>\<open>Crypt K (Nonce NB)\<close> could not exist\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evs3_ \<in> yahalom; Key KAB_ \<notin> used evs3_; Gets Server \<lbrace>Agent Ba_, Nonce NBa_, Crypt (shrK Ba_) \<lbrace>Agent Aa_, Nonce NA_\<rbrace>\<rbrace> \<in> set evs3_; Key K \<notin> analz (knows Spy evs3_); K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs3_) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs3_) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs3_)\<rbrakk> \<Longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs3_) \<longrightarrow> B = Ba_ \<and> A = Aa_ \<and> B = Ba_ \<and> K = KAB_ \<and> NB = NBa_ \<longrightarrow> Ba_ \<notin> bad \<longrightarrow> (\<exists>X. Says Aa_ Ba_ \<lbrace>X, Crypt KAB_ (Nonce NBa_)\<rbrace> \<in> set evs3_)
[PROOF STEP]
by (force dest!: Crypt_imp_keysFor)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>evs4 Aa NBa Ba Ka NA X. \<lbrakk>evs4 \<in> yahalom; Gets Aa \<lbrace>Nonce NBa, Crypt (shrK Aa) \<lbrace>Agent Ba, Key Ka, Nonce NA\<rbrace>, X\<rbrace> \<in> set evs4; Says Aa Ba \<lbrace>Agent Aa, Nonce NA\<rbrace> \<in> set evs4; X \<in> parts (knows Spy evs4); Key K \<notin> analz (knows Spy evs4); K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs4) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs4)\<rbrakk> \<Longrightarrow> K \<in> symKeys \<longrightarrow> (K = Ka \<and> NB = NBa \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key Ka, Nonce NBa\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>Xa. A = Aa \<and> B = Ba \<and> Xa = X \<or> Says A B \<lbrace>Xa, Crypt Ka (Nonce NBa)\<rbrace> \<in> set evs4)) \<and> (Crypt K (Nonce NB) \<in> parts (knows Spy evs4) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>Xa. A = Aa \<and> B = Ba \<and> Xa = X \<and> K = Ka \<and> NB = NBa \<or> Says A B \<lbrace>Xa, Crypt K (Nonce NB)\<rbrace> \<in> set evs4))
[PROOF STEP]
subgoal \<comment> \<open>YM4: was \<^term>\<open>Crypt K (Nonce NB)\<close> the very last message? If not, use the induction hypothesis,
             otherwise by unicity of session keys\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evs4_ \<in> yahalom; Gets Aa_ \<lbrace>Nonce NBa_, Crypt (shrK Aa_) \<lbrace>Agent Ba_, Key Ka_, Nonce NA_\<rbrace>, X_\<rbrace> \<in> set evs4_; Says Aa_ Ba_ \<lbrace>Agent Aa_, Nonce NA_\<rbrace> \<in> set evs4_; X_ \<in> parts (knows Spy evs4_); Key K \<notin> analz (knows Spy evs4_); K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs4_) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs4_) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs4_)\<rbrakk> \<Longrightarrow> K \<in> symKeys \<longrightarrow> (K = Ka_ \<and> NB = NBa_ \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key Ka_, Nonce NBa_\<rbrace> \<in> parts (knows Spy evs4_) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>Xa. A = Aa_ \<and> B = Ba_ \<and> Xa = X_ \<or> Says A B \<lbrace>Xa, Crypt Ka_ (Nonce NBa_)\<rbrace> \<in> set evs4_)) \<and> (Crypt K (Nonce NB) \<in> parts (knows Spy evs4_) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs4_) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>Xa. A = Aa_ \<and> B = Ba_ \<and> Xa = X_ \<and> K = Ka_ \<and> NB = NBa_ \<or> Says A B \<lbrace>Xa, Crypt K (Nonce NB)\<rbrace> \<in> set evs4_))
[PROOF STEP]
by (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done