[STATEMENT]
lemma Notes_TTP_imp_Says_A:
     "[|Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace>
           \<in> set evs;
        sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
        A \<notin> broken; evs \<in> zg|]
     ==> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set evs; sub_K = Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>; A \<notin> broken; evs \<in> zg\<rbrakk> \<Longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set evs; A \<notin> broken; evs \<in> zg; sub_K = Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrakk> \<Longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set evs
[PROOF STEP]
apply (erule rev_mp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<notin> broken; evs \<in> zg; sub_K = Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrakk> \<Longrightarrow> Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set evs \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set evs
[PROOF STEP]
apply (erule zg.induct)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>A \<notin> broken; sub_K = Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrakk> \<Longrightarrow> Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set [] \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set []
 2. \<And>evsf X Ba. \<lbrakk>A \<notin> broken; sub_K = Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>; evsf \<in> zg; Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set evsf \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set evsf; X \<in> synth (analz (knows Spy evsf))\<rbrakk> \<Longrightarrow> Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set (Says Spy Ba X # evsf) \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set (Says Spy Ba X # evsf)
 3. \<And>evsr Aa Ba X. \<lbrakk>A \<notin> broken; sub_K = Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>; evsr \<in> zg; Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set evsr \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set evsr; Says Aa Ba X \<in> set evsr\<rbrakk> \<Longrightarrow> Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set (Gets Ba X # evsr) \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set (Gets Ba X # evsr)
 4. \<And>evs1 La C Ka m NRO Aa Ba. \<lbrakk>A \<notin> broken; sub_K = Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>; evs1 \<in> zg; Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set evs1 \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set evs1; Nonce La \<notin> used evs1; C = Crypt Ka (Number m); Ka \<in> symKeys; NRO = Crypt (priEK Aa) \<lbrace>Number f_nro, Agent Ba, Nonce La, C\<rbrace>\<rbrakk> \<Longrightarrow> Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set (Says Aa Ba \<lbrace>Number f_nro, Agent Ba, Nonce La, C, NRO\<rbrace> # evs1) \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set (Says Aa Ba \<lbrace>Number f_nro, Agent Ba, Nonce La, C, NRO\<rbrace> # evs1)
 5. \<And>evs2 Ba La C NRO Aa NRR. \<lbrakk>A \<notin> broken; sub_K = Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>; evs2 \<in> zg; Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set evs2 \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set evs2; Gets Ba \<lbrace>Number f_nro, Agent Ba, Nonce La, C, NRO\<rbrace> \<in> set evs2; NRO = Crypt (priEK Aa) \<lbrace>Number f_nro, Agent Ba, Nonce La, C\<rbrace>; NRR = Crypt (priEK Ba) \<lbrace>Number f_nrr, Agent Aa, Nonce La, C\<rbrace>\<rbrakk> \<Longrightarrow> Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set (Says Ba Aa \<lbrace>Number f_nrr, Agent Aa, Nonce La, NRR\<rbrace> # evs2) \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set (Says Ba Aa \<lbrace>Number f_nrr, Agent Aa, Nonce La, NRR\<rbrace> # evs2)
 6. \<And>evs3 C Ka M Aa Ba La NRO NRR sub_Ka. \<lbrakk>A \<notin> broken; sub_K = Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>; evs3 \<in> zg; Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set evs3 \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set evs3; C = Crypt Ka M; Ka \<in> symKeys; Says Aa Ba \<lbrace>Number f_nro, Agent Ba, Nonce La, C, NRO\<rbrace> \<in> set evs3; Gets Aa \<lbrace>Number f_nrr, Agent Aa, Nonce La, NRR\<rbrace> \<in> set evs3; NRR = Crypt (priEK Ba) \<lbrace>Number f_nrr, Agent Aa, Nonce La, C\<rbrace>; sub_Ka = Crypt (priEK Aa) \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka\<rbrace>\<rbrakk> \<Longrightarrow> Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set (Says Aa TTP \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka, sub_Ka\<rbrace> # evs3) \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set (Says Aa TTP \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka, sub_Ka\<rbrace> # evs3)
 7. \<And>evs4 Ka Ba La sub_Ka Aa con_Ka. \<lbrakk>A \<notin> broken; sub_K = Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>; evs4 \<in> zg; Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set evs4 \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set evs4; Ka \<in> symKeys; Gets TTP \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka, sub_Ka\<rbrace> \<in> set evs4; sub_Ka = Crypt (priEK Aa) \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka\<rbrace>; con_Ka = Crypt (priEK TTP) \<lbrace>Number f_con, Agent Aa, Agent Ba, Nonce La, Key Ka\<rbrace>\<rbrakk> \<Longrightarrow> Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set (Says TTP Spy con_Ka # Notes TTP \<lbrace>Number f_con, Agent Aa, Agent Ba, Nonce La, Key Ka, con_Ka\<rbrace> # evs4) \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set (Says TTP Spy con_Ka # Notes TTP \<lbrace>Number f_con, Agent Aa, Agent Ba, Nonce La, Key Ka, con_Ka\<rbrace> # evs4)
[PROOF STEP]
apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>evs4 Ka Ba La sub_Ka Aa con_Ka. \<lbrakk>A \<in> bad \<longrightarrow> A = Spy; sub_K = Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>; evs4 \<in> zg; Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set evs4 \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set evs4; Ka \<in> symKeys; Gets TTP \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka, Crypt (priEK Aa) \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka\<rbrace>\<rbrace> \<in> set evs4; sub_Ka = Crypt (priEK Aa) \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka\<rbrace>; con_Ka = Crypt (priEK TTP) \<lbrace>Number f_con, Agent Aa, Agent Ba, Nonce La, Key Ka\<rbrace>\<rbrakk> \<Longrightarrow> A = Aa \<and> B = Ba \<and> L = La \<and> K = Ka \<and> con_K = Crypt (priEK TTP) \<lbrace>Number f_con, Agent Aa, Agent Ba, Nonce La, Key Ka\<rbrace> \<longrightarrow> Says Aa TTP \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka, Crypt (priEK Aa) \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka\<rbrace>\<rbrace> \<in> set evs4
[PROOF STEP]
txt\<open>ZG4\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>evs4 Ka Ba La sub_Ka Aa con_Ka. \<lbrakk>A \<in> bad \<longrightarrow> A = Spy; sub_K = Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>; evs4 \<in> zg; Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set evs4 \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set evs4; Ka \<in> symKeys; Gets TTP \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka, Crypt (priEK Aa) \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka\<rbrace>\<rbrace> \<in> set evs4; sub_Ka = Crypt (priEK Aa) \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka\<rbrace>; con_Ka = Crypt (priEK TTP) \<lbrace>Number f_con, Agent Aa, Agent Ba, Nonce La, Key Ka\<rbrace>\<rbrakk> \<Longrightarrow> A = Aa \<and> B = Ba \<and> L = La \<and> K = Ka \<and> con_K = Crypt (priEK TTP) \<lbrace>Number f_con, Agent Aa, Agent Ba, Nonce La, Key Ka\<rbrace> \<longrightarrow> Says Aa TTP \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka, Crypt (priEK Aa) \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka\<rbrace>\<rbrace> \<in> set evs4
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>evs4 Ka Ba La sub_Ka Aa con_Ka. \<lbrakk>A \<in> bad \<longrightarrow> A = Spy; sub_K = Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>; evs4 \<in> zg; K \<in> symKeys; Gets TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set evs4; con_K = Crypt (priEK TTP) \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K\<rbrace>; Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, Crypt (priEK TTP) \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<notin> set evs4\<rbrakk> \<Longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set evs4
[PROOF STEP]
apply (rule sub_K_validity, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done