theory Noninterference

lemma partitionIntegrity_subjectAffects_eobj:
  "\<lbrakk> partitionIntegrity aag s s'; pas_refined aag s;
     valid_objs s; einvs s; einvs s'; pas_wellformed_noninterference aag;
     silc_inv aag st s; silc_inv aag st' s'; ekheap s x \<noteq> ekheap s' x \<rbrakk>
     \<Longrightarrow> pasObjectAbs aag x \<in> subjectAffects (pasPolicy aag) (pasSubject aag)" apply (drule partitionIntegrity_integrity) apply (drule integrity_subjects_eobj) apply (drule_tac x=x in spec) apply (erule integrity_eobj.cases) apply simp apply (rule subjectAffects.affects_lrefl) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; einvs s; einvs s'; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; ekheap s x \<noteq> ekheap s' x\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; valid_objs s; einvs s; einvs s'; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; ekheap s x \<noteq> ekheap s' x; integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {} s s'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; valid_objs s; einvs s; einvs s'; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; ekheap s x \<noteq> ekheap s' x; \<forall>x. integrity_eobj (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) x) (ekheap s x) (ekheap s' x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; valid_objs s; einvs s; einvs s'; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; ekheap s x \<noteq> ekheap s' x; integrity_eobj (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) x) (ekheap s x) (ekheap s' x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_refined aag s; valid_objs s; einvs s; einvs s'; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; ekheap s x \<noteq> ekheap s' x; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) x \<in> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<lbrakk>pas_refined aag s; valid_objs s; einvs s; einvs s'; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; ekheap s x \<noteq> ekheap s' x; ekheap s x = ekheap s' x\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_refined aag s; valid_objs s; invs s \<and> valid_list s \<and> valid_sched s; invs s' \<and> valid_list s' \<and> valid_sched s'; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; ekheap s x \<noteq> ekheap s' x; is_subject aag x\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasSubject aag)
 2. \<lbrakk>pas_refined aag s; valid_objs s; einvs s; einvs s'; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; ekheap s x \<noteq> ekheap s' x; ekheap s x = ekheap s' x\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; valid_objs s; einvs s; einvs s'; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; ekheap s x \<noteq> ekheap s' x; ekheap s x = ekheap s' x\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal:
No subgoals!