theory Noninterference

lemma confidentiality_u:
  notes split_paired_All[simp del]
  shows "ni.confidentiality_u" apply (simp add: ni.confidentiality_u_def | intro allI impI | elim conjE)+ apply (case_tac "(part s, u) \<in> policyFlows (pasPolicy initial_aag)") apply (simp) apply (fastforce intro: confidentiality_part schedNotGlobalChannel simp: big_Step2) apply (case_tac "u = PSched") apply (subgoal_tac "part s \<noteq> PSched") apply (blast intro: confidentiality_for_sched big_Step2) apply (fastforce intro: policyFlows_refl[THEN refl_onD]) apply (metis integrity_part uwr_sym uwr_trans schedIncludesCurrentDom not_PSched big_Step2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. confidentiality_u proof (prove)
goal (1 subgoal):
 1. \<And>u s t s' t'. \<lbrakk>uwr2 s PSched t; policy2 (part s) u \<longrightarrow> uwr2 s (part s) t; uwr2 s u t; reachable s; reachable t; (s, s') \<in> ni.Step (); (t, t') \<in> ni.Step ()\<rbrakk> \<Longrightarrow> uwr2 s' u t' proof (prove)
goal (2 subgoals):
 1. \<And>u s t s' t'. \<lbrakk>uwr2 s PSched t; policy2 (part s) u \<longrightarrow> uwr2 s (part s) t; uwr2 s u t; reachable s; reachable t; (s, s') \<in> ni.Step (); (t, t') \<in> ni.Step (); policy2 (part s) u\<rbrakk> \<Longrightarrow> uwr2 s' u t'
 2. \<And>u s t s' t'. \<lbrakk>uwr2 s PSched t; policy2 (part s) u \<longrightarrow> uwr2 s (part s) t; uwr2 s u t; reachable s; reachable t; (s, s') \<in> ni.Step (); (t, t') \<in> ni.Step (); (part s, u) \<notin> policyFlows (pasPolicy initial_aag)\<rbrakk> \<Longrightarrow> uwr2 s' u t' proof (prove)
goal (2 subgoals):
 1. \<And>u s t s' t'. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; reachable s; reachable t; (s, s') \<in> ni.Step (); (t, t') \<in> ni.Step (); policy2 (part s) u\<rbrakk> \<Longrightarrow> uwr2 s' u t'
 2. \<And>u s t s' t'. \<lbrakk>uwr2 s PSched t; policy2 (part s) u \<longrightarrow> uwr2 s (part s) t; uwr2 s u t; reachable s; reachable t; (s, s') \<in> ni.Step (); (t, t') \<in> ni.Step (); (part s, u) \<notin> policyFlows (pasPolicy initial_aag)\<rbrakk> \<Longrightarrow> uwr2 s' u t' proof (prove)
goal (1 subgoal):
 1. \<And>u s t s' t'. \<lbrakk>uwr2 s PSched t; policy2 (part s) u \<longrightarrow> uwr2 s (part s) t; uwr2 s u t; reachable s; reachable t; (s, s') \<in> ni.Step (); (t, t') \<in> ni.Step (); (part s, u) \<notin> policyFlows (pasPolicy initial_aag)\<rbrakk> \<Longrightarrow> uwr2 s' u t' proof (prove)
goal (2 subgoals):
 1. \<And>u s t s' t'. \<lbrakk>uwr2 s PSched t; policy2 (part s) u \<longrightarrow> uwr2 s (part s) t; uwr2 s u t; reachable s; reachable t; (s, s') \<in> ni.Step (); (t, t') \<in> ni.Step (); (part s, u) \<notin> policyFlows (pasPolicy initial_aag); u = PSched\<rbrakk> \<Longrightarrow> uwr2 s' u t'
 2. \<And>u s t s' t'. \<lbrakk>uwr2 s PSched t; policy2 (part s) u \<longrightarrow> uwr2 s (part s) t; uwr2 s u t; reachable s; reachable t; (s, s') \<in> ni.Step (); (t, t') \<in> ni.Step (); (part s, u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 s' u t' proof (prove)
goal (3 subgoals):
 1. \<And>u s t s' t'. \<lbrakk>uwr2 s PSched t; policy2 (part s) u \<longrightarrow> uwr2 s (part s) t; uwr2 s u t; reachable s; reachable t; (s, s') \<in> ni.Step (); (t, t') \<in> ni.Step (); (part s, u) \<notin> policyFlows (pasPolicy initial_aag); u = PSched; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 s' u t'
 2. \<And>u s t s' t'. \<lbrakk>uwr2 s PSched t; policy2 (part s) u \<longrightarrow> uwr2 s (part s) t; uwr2 s u t; reachable s; reachable t; (s, s') \<in> ni.Step (); (t, t') \<in> ni.Step (); (part s, u) \<notin> policyFlows (pasPolicy initial_aag); u = PSched\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 3. \<And>u s t s' t'. \<lbrakk>uwr2 s PSched t; policy2 (part s) u \<longrightarrow> uwr2 s (part s) t; uwr2 s u t; reachable s; reachable t; (s, s') \<in> ni.Step (); (t, t') \<in> ni.Step (); (part s, u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 s' u t' proof (prove)
goal (2 subgoals):
 1. \<And>u s t s' t'. \<lbrakk>uwr2 s PSched t; policy2 (part s) u \<longrightarrow> uwr2 s (part s) t; uwr2 s u t; reachable s; reachable t; (s, s') \<in> ni.Step (); (t, t') \<in> ni.Step (); (part s, u) \<notin> policyFlows (pasPolicy initial_aag); u = PSched\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 2. \<And>u s t s' t'. \<lbrakk>uwr2 s PSched t; policy2 (part s) u \<longrightarrow> uwr2 s (part s) t; uwr2 s u t; reachable s; reachable t; (s, s') \<in> ni.Step (); (t, t') \<in> ni.Step (); (part s, u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 s' u t' proof (prove)
goal (1 subgoal):
 1. \<And>u s t s' t'. \<lbrakk>uwr2 s PSched t; policy2 (part s) u \<longrightarrow> uwr2 s (part s) t; uwr2 s u t; reachable s; reachable t; (s, s') \<in> ni.Step (); (t, t') \<in> ni.Step (); (part s, u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 s' u t' proof (prove)
goal:
No subgoals!