theory Noninterference_Base

lemma Nonleakage_gen_confidentiality_u:
  "Nonleakage_gen \<Longrightarrow> confidentiality_u" apply (clarsimp simp: Nonleakage_gen_def confidentiality_u_def) apply (drule_tac x="[a]" in spec, drule_tac x=s in spec) apply (drule_tac x=u in spec, drule_tac x=t in spec) apply (case_tac "dom a s \<leadsto> u") apply (simp add: sources_Step_2 uwr_equiv_def sameFor_dom_def Step_def) apply (simp add: sources_Step uwr_equiv_def sameFor_dom_def Step_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Nonleakage_gen \<Longrightarrow> confidentiality_u proof (prove)
goal (1 subgoal):
 1. \<And>a u s t s' t'. \<lbrakk>\<forall>as s u t. reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> s \<approx>sources as s u\<approx> t \<longrightarrow> uwr_equiv s as t as u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; dom a s \<leadsto> u \<longrightarrow> s \<sim>dom a s\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t' proof (prove)
goal (1 subgoal):
 1. \<And>a u s t s' t'. \<lbrakk>reachable s; reachable t; s \<sim>schedDomain\<sim> t; dom a s \<leadsto> u \<longrightarrow> s \<sim>dom a s\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; \<forall>u t. reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> s \<approx>sources [a] s u\<approx> t \<longrightarrow> uwr_equiv s [a] t [a] u\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t' proof (prove)
goal (1 subgoal):
 1. \<And>a u s t s' t'. \<lbrakk>reachable s; reachable t; s \<sim>schedDomain\<sim> t; dom a s \<leadsto> u \<longrightarrow> s \<sim>dom a s\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> s \<approx>sources [a] s u\<approx> t \<longrightarrow> uwr_equiv s [a] t [a] u\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t' proof (prove)
goal (2 subgoals):
 1. \<And>a u s t s' t'. \<lbrakk>reachable s; reachable t; s \<sim>schedDomain\<sim> t; dom a s \<leadsto> u \<longrightarrow> s \<sim>dom a s\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> s \<approx>sources [a] s u\<approx> t \<longrightarrow> uwr_equiv s [a] t [a] u; dom a s \<leadsto> u\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t'
 2. \<And>a u s t s' t'. \<lbrakk>reachable s; reachable t; s \<sim>schedDomain\<sim> t; dom a s \<leadsto> u \<longrightarrow> s \<sim>dom a s\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> s \<approx>sources [a] s u\<approx> t \<longrightarrow> uwr_equiv s [a] t [a] u; (dom a s, u) \<notin> policy\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t' proof (prove)
goal (1 subgoal):
 1. \<And>a u s t s' t'. \<lbrakk>reachable s; reachable t; s \<sim>schedDomain\<sim> t; dom a s \<leadsto> u \<longrightarrow> s \<sim>dom a s\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> s \<approx>sources [a] s u\<approx> t \<longrightarrow> uwr_equiv s [a] t [a] u; (dom a s, u) \<notin> policy\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t' proof (prove)
goal:
No subgoals!