theory Noninterference

lemma partitionIntegrity_subjectAffects_device:
  "\<lbrakk> partitionIntegrity aag s s'; pas_refined aag s; invs s; invs s';
     device_state (machine_state s) x \<noteq> device_state (machine_state s') x \<rbrakk>
     \<Longrightarrow> pasObjectAbs aag x \<in> subjectAffects (pasPolicy aag) (pasSubject aag)" apply (drule partitionIntegrity_integrity) apply (frule integrity_subjects_device) apply (drule_tac x=x in spec) apply (erule integrity_device.cases) apply (fastforce intro: affects_lrefl) apply blast apply (fastforce intro: affects_write) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; invs s; invs s'; device_state (machine_state s) x \<noteq> device_state (machine_state s') x\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; invs s; invs s'; device_state (machine_state s) x \<noteq> device_state (machine_state 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; invs s; invs s'; device_state (machine_state s) x \<noteq> device_state (machine_state s') x; integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {} s s'; \<forall>x. integrity_device (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; invs s; invs s'; device_state (machine_state s) x \<noteq> device_state (machine_state s') x; integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {} s s'; integrity_device (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>pas_refined aag s; invs s; invs s'; device_state (machine_state s) x \<noteq> device_state (machine_state s') x; integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {} s s'; 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; invs s; invs s'; device_state (machine_state s) x \<noteq> device_state (machine_state s') x; integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {} s s'; device_state (machine_state s) x = device_state (machine_state s') x\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<lbrakk>pas_refined aag s; invs s; invs s'; device_state (machine_state s) x \<noteq> device_state (machine_state s') x; integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {} s s'; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Write x\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_refined aag s; invs s; invs s'; device_state (machine_state s) x \<noteq> device_state (machine_state s') x; integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {} s s'; device_state (machine_state s) x = device_state (machine_state s') x\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<lbrakk>pas_refined aag s; invs s; invs s'; device_state (machine_state s) x \<noteq> device_state (machine_state s') x; integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {} s s'; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Write x\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; invs s; invs s'; device_state (machine_state s) x \<noteq> device_state (machine_state s') x; integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {} s s'; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Write x\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal:
No subgoals!