theory Noninterference

lemma sameFor_reads_f_g_affects_equiv:
  "\<lbrakk> pas_cur_domain aag (internal_state_if s); silc_inv aag st (internal_state_if s);
     (s,s') \<in> same_for aag (Partition (label_of (pasSubject aag)));
     Partition l \<in> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag));
     (s,s') \<in> same_for aag (Partition l) \<rbrakk>
     \<Longrightarrow> reads_equiv_f_g aag (internal_state_if s) (internal_state_if s') \<and>
         affects_equiv aag (OrdinaryLabel l) (internal_state_if s) (internal_state_if s')" apply (rule conjI) apply (rule sameFor_reads_equiv_f_g') apply blast apply blast apply (rule_tac s=s in observable_if_cases) apply (erule_tac s=s' in observable_if_cases) apply (simp add: partsSubjectAffects_def) apply (frule pasSubject_not_SilcLabel) apply clarsimp apply (clarsimp simp: affects_equiv_def2 sameFor_def) apply (clarsimp simp: sameFor_subject_def[where l=l]) apply (blast intro: states_equiv_for_guard_imp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_cur_domain aag (internal_state_if s); silc_inv aag st (internal_state_if s); (s, s') \<in> same_for aag (Partition (label_of (pasSubject aag))); Partition l \<in> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag)); (s, s') \<in> same_for aag (Partition l)\<rbrakk> \<Longrightarrow> reads_equiv_f_g aag (internal_state_if s) (internal_state_if s') \<and> affects_equiv aag (OrdinaryLabel l) (internal_state_if s) (internal_state_if s') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_cur_domain aag (internal_state_if s); silc_inv aag st (internal_state_if s); (s, s') \<in> same_for aag (Partition (label_of (pasSubject aag))); Partition l \<in> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag)); (s, s') \<in> same_for aag (Partition l)\<rbrakk> \<Longrightarrow> reads_equiv_f_g aag (internal_state_if s) (internal_state_if s')
 2. \<lbrakk>pas_cur_domain aag (internal_state_if s); silc_inv aag st (internal_state_if s); (s, s') \<in> same_for aag (Partition (label_of (pasSubject aag))); Partition l \<in> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag)); (s, s') \<in> same_for aag (Partition l)\<rbrakk> \<Longrightarrow> affects_equiv aag (OrdinaryLabel l) (internal_state_if s) (internal_state_if s') proof (prove)
goal (4 subgoals):
 1. \<lbrakk>pas_cur_domain aag (internal_state_if s); silc_inv aag st (internal_state_if s); (s, s') \<in> same_for aag (Partition (label_of (pasSubject aag))); Partition l \<in> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag)); (s, s') \<in> same_for aag (Partition l)\<rbrakk> \<Longrightarrow> pas_cur_domain aag (internal_state_if s) \<or> pas_cur_domain aag (internal_state_if s')
 2. \<lbrakk>pas_cur_domain aag (internal_state_if s); silc_inv aag st (internal_state_if s); (s, s') \<in> same_for aag (Partition (label_of (pasSubject aag))); Partition l \<in> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag)); (s, s') \<in> same_for aag (Partition l)\<rbrakk> \<Longrightarrow> silc_inv aag ?st3 (internal_state_if s)
 3. \<lbrakk>pas_cur_domain aag (internal_state_if s); silc_inv aag st (internal_state_if s); (s, s') \<in> same_for aag (Partition (label_of (pasSubject aag))); Partition l \<in> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag)); (s, s') \<in> same_for aag (Partition l)\<rbrakk> \<Longrightarrow> (((?uc3, internal_state_if s), ?mode3), (?uc'3, internal_state_if s'), ?mode'3) \<in> same_for aag (Partition (label_of (pasSubject aag)))
 4. \<lbrakk>pas_cur_domain aag (internal_state_if s); silc_inv aag st (internal_state_if s); (s, s') \<in> same_for aag (Partition (label_of (pasSubject aag))); Partition l \<in> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag)); (s, s') \<in> same_for aag (Partition l)\<rbrakk> \<Longrightarrow> affects_equiv aag (OrdinaryLabel l) (internal_state_if s) (internal_state_if s') proof (prove)
goal (3 subgoals):
 1. \<lbrakk>pas_cur_domain aag (internal_state_if s); silc_inv aag st (internal_state_if s); (s, s') \<in> same_for aag (Partition (label_of (pasSubject aag))); Partition l \<in> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag)); (s, s') \<in> same_for aag (Partition l)\<rbrakk> \<Longrightarrow> silc_inv aag ?st3 (internal_state_if s)
 2. \<lbrakk>pas_cur_domain aag (internal_state_if s); silc_inv aag st (internal_state_if s); (s, s') \<in> same_for aag (Partition (label_of (pasSubject aag))); Partition l \<in> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag)); (s, s') \<in> same_for aag (Partition l)\<rbrakk> \<Longrightarrow> (((?uc3, internal_state_if s), ?mode3), (?uc'3, internal_state_if s'), ?mode'3) \<in> same_for aag (Partition (label_of (pasSubject aag)))
 3. \<lbrakk>pas_cur_domain aag (internal_state_if s); silc_inv aag st (internal_state_if s); (s, s') \<in> same_for aag (Partition (label_of (pasSubject aag))); Partition l \<in> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag)); (s, s') \<in> same_for aag (Partition l)\<rbrakk> \<Longrightarrow> affects_equiv aag (OrdinaryLabel l) (internal_state_if s) (internal_state_if s') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_cur_domain aag (internal_state_if s); silc_inv aag st (internal_state_if s); (s, s') \<in> same_for aag (Partition (label_of (pasSubject aag))); Partition l \<in> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag)); (s, s') \<in> same_for aag (Partition l)\<rbrakk> \<Longrightarrow> (((?uc3, internal_state_if s), ?mode3), (?uc'3, internal_state_if s'), ?mode'3) \<in> same_for aag (Partition (label_of (pasSubject aag)))
 2. \<lbrakk>pas_cur_domain aag (internal_state_if s); silc_inv aag st (internal_state_if s); (s, s') \<in> same_for aag (Partition (label_of (pasSubject aag))); Partition l \<in> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag)); (s, s') \<in> same_for aag (Partition l)\<rbrakk> \<Longrightarrow> affects_equiv aag (OrdinaryLabel l) (internal_state_if s) (internal_state_if s') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_cur_domain aag (internal_state_if s); silc_inv aag st (internal_state_if s); (s, s') \<in> same_for aag (Partition (label_of (pasSubject aag))); Partition l \<in> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag)); (s, s') \<in> same_for aag (Partition l)\<rbrakk> \<Longrightarrow> (s, (?uc'14 s, internal_state_if s'), ?mode'13 s) \<in> same_for aag (Partition (label_of (pasSubject aag)))
 2. \<lbrakk>pas_cur_domain aag (internal_state_if s); silc_inv aag st (internal_state_if s); (s, s') \<in> same_for aag (Partition (label_of (pasSubject aag))); Partition l \<in> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag)); (s, s') \<in> same_for aag (Partition l)\<rbrakk> \<Longrightarrow> affects_equiv aag (OrdinaryLabel l) (internal_state_if s) (internal_state_if s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_cur_domain aag (internal_state_if s); silc_inv aag st (internal_state_if s); (s, s') \<in> same_for aag (Partition (label_of (pasSubject aag))); Partition l \<in> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag)); (s, s') \<in> same_for aag (Partition l)\<rbrakk> \<Longrightarrow> affects_equiv aag (OrdinaryLabel l) (internal_state_if s) (internal_state_if s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_cur_domain aag (internal_state_if s); silc_inv aag st (internal_state_if s); (s, s') \<in> same_for aag (Partition (label_of (pasSubject aag))); Partition l \<in> Partition ` {x. label_can_affect_partition (pasPolicy aag) (OrdinaryLabel (label_of (pasSubject aag))) (OrdinaryLabel x)}; (s, s') \<in> same_for aag (Partition l)\<rbrakk> \<Longrightarrow> affects_equiv aag (OrdinaryLabel l) (internal_state_if s) (internal_state_if s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_cur_domain aag (internal_state_if s); silc_inv aag st (internal_state_if s); (s, s') \<in> same_for aag (Partition (label_of (pasSubject aag))); Partition l \<in> Partition ` {x. label_can_affect_partition (pasPolicy aag) (OrdinaryLabel (label_of (pasSubject aag))) (OrdinaryLabel x)}; (s, s') \<in> same_for aag (Partition l); pasSubject aag \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> affects_equiv aag (OrdinaryLabel l) (internal_state_if s) (internal_state_if s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_cur_domain aag (internal_state_if s); silc_inv aag st (internal_state_if s); (s, s') \<in> same_for aag (Partition (label_of (pasSubject aag))); (s, s') \<in> same_for aag (Partition l); pasSubject aag \<noteq> SilcLabel; label_can_affect_partition (pasPolicy aag) (pasSubject aag) (OrdinaryLabel l)\<rbrakk> \<Longrightarrow> affects_equiv aag (OrdinaryLabel l) (internal_state_if s) (internal_state_if s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_cur_domain aag (internal_state_if s); silc_inv aag st (internal_state_if s); (s, s') \<in> sameFor_subject (pasPolicy aag) (pasObjectAbs aag) (pasIRQAbs aag) (pasASIDAbs aag) (pasDomainAbs aag) (label_of (pasSubject aag)); (s, s') \<in> sameFor_subject (pasPolicy aag) (pasObjectAbs aag) (pasIRQAbs aag) (pasASIDAbs aag) (pasDomainAbs aag) l; pasSubject aag \<noteq> SilcLabel; label_can_affect_partition (pasPolicy aag) (pasSubject aag) (OrdinaryLabel l)\<rbrakk> \<Longrightarrow> states_equiv_for (aag_can_affect aag (OrdinaryLabel l)) (aag_can_affect_irq aag (OrdinaryLabel l)) (aag_can_affect_asid aag (OrdinaryLabel l)) (aag_can_affect_domain aag (OrdinaryLabel l)) (internal_state_if s) (internal_state_if s') proof (prove)
goal (1 subgoal):
 1. \<And>a b ba aa bb bc. \<lbrakk>pas_cur_domain aag b; silc_inv aag st b; (((a, b), ba), (aa, bb), bc) \<in> sameFor_subject (pasPolicy aag) (pasObjectAbs aag) (pasIRQAbs aag) (pasASIDAbs aag) (pasDomainAbs aag) (label_of (pasSubject aag)); pasSubject aag \<noteq> SilcLabel; label_can_affect_partition (pasPolicy aag) (pasSubject aag) (OrdinaryLabel l); s = ((a, b), ba); s' = ((aa, bb), bc); states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) (\<lambda>x. pasIRQAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) (\<lambda>x. pasASIDAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) (\<lambda>x. pasDomainAbs aag x \<inter> subjectReads (pasPolicy aag) (OrdinaryLabel l) \<noteq> {}) b bb; (pasDomainAbs aag (cur_domain b) \<inter> subjectReads (pasPolicy aag) (OrdinaryLabel l) = {} \<longrightarrow> pasDomainAbs aag (cur_domain bb) \<inter> subjectReads (pasPolicy aag) (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap b bb\<rbrakk> \<Longrightarrow> states_equiv_for (aag_can_affect aag (OrdinaryLabel l)) (aag_can_affect_irq aag (OrdinaryLabel l)) (aag_can_affect_asid aag (OrdinaryLabel l)) (aag_can_affect_domain aag (OrdinaryLabel l)) b bb proof (prove)
goal:
No subgoals!