[STATEMENT]
lemma PO_m2_inv9_M5_step3:
  "{m2_inv9_M5 \<inter> m2_inv2_keys_for} m2_step3 Rs A B Na Kab {> m2_inv9_M5}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {m2_inv9_M5 \<inter> m2_inv2_keys_for} m2_step3 Rs A B Na Kab {> m2_inv9_M5}
[PROOF STEP]
apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv9_M5I)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>Nb xa. \<lbrakk>xa \<in> m2_inv9_M5; xa \<in> m2_inv2_keys_for; Rs \<notin> dom (runs xa); Kab = sesK (Rs $ sk); Insec A B (Msg [aNon Na]) \<in> chan xa; dAuth (sesK (Rs $ sk)) (Msg [aNon Nb, aNon Nb]) \<in> chan xa; A \<in> bad; B \<in> bad; aKey (sesK (Rs $ sk)) \<notin> extr (insert (aKey (sesK (Rs $ sk))) (insert (aAgt A) ik0)) (chan xa)\<rbrakk> \<Longrightarrow> \<exists>Ra. Ra \<noteq> Rs \<and> (Ra \<noteq> Rs \<longrightarrow> runs xa Ra = Some (Init, [A, B], [aKey (sesK (Rs $ sk)), aNon Nb]))
 2. \<And>Kaba Aa Ba Nb xa. \<lbrakk>xa \<in> m2_inv9_M5; xa \<in> m2_inv2_keys_for; Rs \<notin> dom (runs xa); Kab = sesK (Rs $ sk); Insec A B (Msg [aNon Na]) \<in> chan xa; dAuth Kaba (Msg [aNon Nb, aNon Nb]) \<in> chan xa; A \<in> bad; B \<in> bad; aKey Kaba \<notin> extr (insert (aKey (sesK (Rs $ sk))) (insert (aAgt A) ik0)) (chan xa); StatCh secure Sv Ba (Msg [aKey Kaba, aAgt Aa]) \<in> chan xa\<rbrakk> \<Longrightarrow> \<exists>Ra. Ra \<noteq> Rs \<and> (Ra \<noteq> Rs \<longrightarrow> runs xa Ra = Some (Init, [Aa, Ba], [aKey Kaba, aNon Nb]))
 3. \<And>Nb xa. \<lbrakk>xa \<in> m2_inv9_M5; xa \<in> m2_inv2_keys_for; Rs \<notin> dom (runs xa); Kab = sesK (Rs $ sk); Insec A B (Msg [aNon Na]) \<in> chan xa; dAuth (sesK (Rs $ sk)) (Msg [aNon Nb, aNon Nb]) \<in> chan xa; A \<in> bad; B \<notin> bad; aKey (sesK (Rs $ sk)) \<notin> extr (insert (aKey (sesK (Rs $ sk))) ik0) (chan xa)\<rbrakk> \<Longrightarrow> \<exists>Ra. Ra \<noteq> Rs \<and> (Ra \<noteq> Rs \<longrightarrow> runs xa Ra = Some (Init, [A, B], [aKey (sesK (Rs $ sk)), aNon Nb]))
 4. \<And>Kaba Aa Ba Nb xa. \<lbrakk>xa \<in> m2_inv9_M5; xa \<in> m2_inv2_keys_for; Rs \<notin> dom (runs xa); Kab = sesK (Rs $ sk); Insec A B (Msg [aNon Na]) \<in> chan xa; dAuth Kaba (Msg [aNon Nb, aNon Nb]) \<in> chan xa; A \<in> bad; B \<notin> bad; aKey Kaba \<notin> extr (insert (aKey (sesK (Rs $ sk))) ik0) (chan xa); StatCh secure Sv Ba (Msg [aKey Kaba, aAgt Aa]) \<in> chan xa\<rbrakk> \<Longrightarrow> \<exists>Ra. Ra \<noteq> Rs \<and> (Ra \<noteq> Rs \<longrightarrow> runs xa Ra = Some (Init, [Aa, Ba], [aKey Kaba, aNon Nb]))
 5. \<And>Nb xa. \<lbrakk>xa \<in> m2_inv9_M5; xa \<in> m2_inv2_keys_for; Rs \<notin> dom (runs xa); Kab = sesK (Rs $ sk); Insec A B (Msg [aNon Na]) \<in> chan xa; dAuth (sesK (Rs $ sk)) (Msg [aNon Nb, aNon Nb]) \<in> chan xa; A \<notin> bad; B \<in> bad; aKey (sesK (Rs $ sk)) \<notin> extr (insert (aKey (sesK (Rs $ sk))) (insert (aAgt A) ik0)) (chan xa)\<rbrakk> \<Longrightarrow> \<exists>Ra. Ra \<noteq> Rs \<and> (Ra \<noteq> Rs \<longrightarrow> runs xa Ra = Some (Init, [A, B], [aKey (sesK (Rs $ sk)), aNon Nb]))
 6. \<And>Kaba Aa Ba Nb xa. \<lbrakk>xa \<in> m2_inv9_M5; xa \<in> m2_inv2_keys_for; Rs \<notin> dom (runs xa); Kab = sesK (Rs $ sk); Insec A B (Msg [aNon Na]) \<in> chan xa; dAuth Kaba (Msg [aNon Nb, aNon Nb]) \<in> chan xa; A \<notin> bad; B \<in> bad; aKey Kaba \<notin> extr (insert (aKey (sesK (Rs $ sk))) (insert (aAgt A) ik0)) (chan xa); StatCh secure Sv Ba (Msg [aKey Kaba, aAgt Aa]) \<in> chan xa\<rbrakk> \<Longrightarrow> \<exists>Ra. Ra \<noteq> Rs \<and> (Ra \<noteq> Rs \<longrightarrow> runs xa Ra = Some (Init, [Aa, Ba], [aKey Kaba, aNon Nb]))
 7. \<And>Nb xa. \<lbrakk>xa \<in> m2_inv9_M5; xa \<in> m2_inv2_keys_for; Rs \<notin> dom (runs xa); Kab = sesK (Rs $ sk); Insec A B (Msg [aNon Na]) \<in> chan xa; dAuth (sesK (Rs $ sk)) (Msg [aNon Nb, aNon Nb]) \<in> chan xa; A \<notin> bad; B \<notin> bad; aKey (sesK (Rs $ sk)) \<notin> extr ik0 (chan xa)\<rbrakk> \<Longrightarrow> \<exists>Ra. Ra \<noteq> Rs \<and> (Ra \<noteq> Rs \<longrightarrow> runs xa Ra = Some (Init, [A, B], [aKey (sesK (Rs $ sk)), aNon Nb]))
 8. \<And>Kaba Aa Ba Nb xa. \<lbrakk>xa \<in> m2_inv9_M5; xa \<in> m2_inv2_keys_for; Rs \<notin> dom (runs xa); Kab = sesK (Rs $ sk); Insec A B (Msg [aNon Na]) \<in> chan xa; dAuth Kaba (Msg [aNon Nb, aNon Nb]) \<in> chan xa; A \<notin> bad; B \<notin> bad; aKey Kaba \<notin> extr ik0 (chan xa); StatCh secure Sv Ba (Msg [aKey Kaba, aAgt Aa]) \<in> chan xa\<rbrakk> \<Longrightarrow> \<exists>Ra. Ra \<noteq> Rs \<and> (Ra \<noteq> Rs \<longrightarrow> runs xa Ra = Some (Init, [Aa, Ba], [aKey Kaba, aNon Nb]))
[PROOF STEP]
apply (auto simp add: m2_inv2_keys_for__extr_insert_key dest!: m2_inv9_M5D dest: dom_lemmas)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done