--- a/Current_prop.thy	Sun Jun 16 08:05:37 2013 +0800
+++ b/Current_prop.thy	Mon Jun 24 09:01:42 2013 +0800
@@ -49,7 +49,66 @@
 
 lemma info_shm_flow_in_procs:
   "\<lbrakk>info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s \<and> p' \<in> current_procs s"
-by (auto simp:info_flow_shm_def intro:procs_of_shm_prop2)
+apply (induct rule:info_flow_shm.induct )
+by (auto intro:procs_of_shm_prop2)
+
+(*********** simpset for info_flow_shm **************)
+
+lemma info_flow_shm_prop1: 
+  "\<lbrakk>info_flow_shm s p p'; p \<noteq> p'; valid s\<rbrakk> 
+   \<Longrightarrow> \<exists> h h' flag. (p, SHM_RDWR) \<in> procs_of_shm s h \<and> (p', flag) \<in> procs_of_shm s h'"
+by (induct rule: info_flow_shm.induct, auto)
+
+lemma info_flow_shm_cases:
+  "\<lbrakk>info_flow_shm \<tau> pa pb; \<And>p s. \<lbrakk>s = \<tau> ; pa = p; pb = p; p \<in> current_procs s\<rbrakk> \<Longrightarrow> P;
+  \<And>s p p' h p'' flag. \<lbrakk>s = \<tau>; pa = p; pb = p''; info_flow_shm s p p'; (p', SHM_RDWR) \<in> procs_of_shm s h;
+                       (p'', flag) \<in> procs_of_shm s h\<rbrakk>\<Longrightarrow> P\<rbrakk>
+  \<Longrightarrow> P"
+by (erule info_flow_shm.cases, auto)
+
+definition one_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
+where
+  "one_flow_shm s p p' \<equiv> p \<noteq> p' \<and> (\<exists> h flag. (p, SHM_RDWR) \<in> procs_of_shm s h \<and> (p', flag) \<in> procs_of_shm s h)"
+
+inductive flows_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
+where
+  "p \<in> current_procs s \<Longrightarrow> flows_shm s p p"
+| "\<lbrakk>flows_shm s p p'; one_flow_shm s p' p''\<rbrakk> \<Longrightarrow> flows_shm s p p''"
+
+definition attached_procs :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_process set"
+where
+  "attached_procs s h \<equiv> {p. \<exists> flag. (p, flag) \<in> procs_of_shm s h}"
+
+definition flowed_procs:: "t_state \<Rightarrow> t_shm \<Rightarrow> t_process set"
+where
+  "flowed_procs s h \<equiv> {p'. \<exists> p \<in> attached_procs s h. flows_shm s p p'}"
+
+fun Info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process set"
+where
+  "Info_flow_shm [] = (\<lambda> p. {p'. flows_shm [] p p'})"
+| "Info_flow_shm (Attach p h flag # s) = (\<lambda> p'. if (p' = p) then {p''. \<exists> }"
+
+
+lemma info_flow_shm_attach:
+  "valid (Attach p h flag # s) \<Longrightarrow> info_flow_shm (Attach p h flag # s) = (\<lambda> pa pb. (info_flow_shm s pa pb) \<or> 
+     (if (pa = p) 
+      then (if (flag = SHM_RDWR) 
+            then (\<exists> flag. (pb, flag) \<in> procs_of_shm s h)
+            else (pb = p)) 
+      else (if (pb = p) 
+            then (pa, SHM_RDWR) \<in> procs_of_shm s h
+            else info_flow_shm s pa pb)) )"
+apply (frule vd_cons, frule vt_grant_os, rule ext, rule ext)
+apply (case_tac "info_flow_shm s pa pb", simp)
+
+thm info_flow_shm.cases
+apply (auto split:if_splits intro:info_flow_shm.intros elim:info_flow_shm_cases)
+apply (erule info_flow_shm_cases, simp, simp split:if_splits)
+apply (rule_tac p = pa and p' = p' in info_flow_shm.intros(2), simp+)
+apply (rule notI, erule info_flow_shm.cases, simp+)
+pr 5
+
+lemmas info_flow_shm_simps = info_flow_shm_other
 
 lemma has_same_inode_in_current:
   "\<lbrakk>has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> f \<in> current_files s \<and> f' \<in> current_files s"

--- a/Flask.thy	Sun Jun 16 08:05:37 2013 +0800
+++ b/Flask.thy	Mon Jun 24 09:01:42 2013 +0800
@@ -473,10 +473,17 @@
     (\<lambda> h. (procs_of_shm s h) - {(p, flag) | flag. (p, flag) \<in> procs_of_shm s h})"
 | "procs_of_shm (e # \<tau>) = procs_of_shm \<tau>"
 
+inductive info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
+where
+  "p \<in> current_procs s \<Longrightarrow> info_flow_shm s p p"
+| "\<lbrakk>info_flow_shm s p p'; (p', SHM_RDWR) \<in> procs_of_shm s h; (p'', flag) \<in> procs_of_shm s h; p' \<noteq> p''\<rbrakk>
+   \<Longrightarrow> info_flow_shm s p p''"
+(*
 definition info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
 where
   "info_flow_shm \<tau> from to \<equiv> (from = to \<and> from \<in> current_procs \<tau>) \<or> (\<exists> h toflag. 
     (((from, SHM_RDWR) \<in> procs_of_shm \<tau> h) \<and> ((to, toflag) \<in> procs_of_shm \<tau> h)))" 
+*)
 
 fun current_msgqs :: "t_state \<Rightarrow> t_msg set"
 where

--- a/Static.thy	Sun Jun 16 08:05:37 2013 +0800
+++ b/Static.thy	Mon Jun 24 09:01:42 2013 +0800
@@ -463,9 +463,16 @@
 where
   "info_flow_sproc_sshms shms shms' \<equiv> (\<exists> sh flag'. (sh, SHM_RDWR) \<in> shms \<and> (sh, flag') \<in> shms')" 
 
+(*
 fun info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool"
 where
   "info_flow_sshm (pi,sec,fds,shms) (pi',sec',fds',shms') = info_flow_sproc_sshms shms shms'"
+*)
+inductive info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool"
+where
+  "info_flow_sshm sp sp"
+| "\<lbrakk>info_flow_sshm sp (pi,sec,fds,shms); info_flow_sproc_sshms shms shms'\<rbrakk>
+   \<Longrightarrow> info_flow_sshm sp (pi',sec',fds',shms')"
 
 definition update_ss_shms :: "t_static_state \<Rightarrow> t_sproc \<Rightarrow> bool \<Rightarrow> t_static_state"
 where

--- a/Tainted_prop.thy	Sun Jun 16 08:05:37 2013 +0800
+++ b/Tainted_prop.thy	Mon Jun 24 09:01:42 2013 +0800
@@ -95,6 +95,13 @@
 (*?? need simpset for tainted *)
 sorry
 
+lemma info_flow_shm_intro:
+  "\<lbrakk>(p, SHM_RDWR) \<in> procs_of_shm s h; (p', flag) \<in> procs_of_shm s h; valid s\<rbrakk>
+   \<Longrightarrow> info_flow_shm s p p'"
+apply (rule_tac p = p and p' = p in info_flow_shm.intros(2))
+apply (auto intro!:info_flow_shm.intros(1) procs_of_shm_prop2)
+done
+
 lemma info_flow_shm_Tainted:
   "\<lbrakk>O_proc p \<in> Tainted s; info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> O_proc p' \<in> Tainted s"
 proof (induct s arbitrary:p p')
@@ -109,7 +116,7 @@
   have p4': 
     "\<And> p p' h flag. \<lbrakk>O_proc p \<in> Tainted s; (p, SHM_RDWR) \<in> procs_of_shm s h; (p', flag) \<in> procs_of_shm s h\<rbrakk> 
                 \<Longrightarrow> O_proc p' \<in> Tainted s"
-    by (rule p4, auto simp:info_flow_shm_def)    
+    by (rule p4, auto intro!:info_flow_shm_intro p5)    
   from p2 p3 have p7: "p \<in> current_procs (e # s)" and p8: "p' \<in> current_procs (e # s)"
     by (auto dest:info_shm_flow_in_procs)
   show ?case
@@ -120,8 +127,12 @@
     with p1 p2 p5 p6 p7 p8 p3 show ?thesis
     apply (case_tac e)
     prefer 7
-    apply (simp add:info_flow_shm_def split:if_splits option.splits)
+    apply (simp split:if_splits option.splits)
     apply (rule allI|rule impI|rule conjI)+
+
+
+    apply (auto dest:p4'   procs_of_shm_prop2 Tainted_in_current split:if_splits option.splits)[1]
+
     apply (erule disjE, drule_tac p = p and p' = p' in p4', simp+)
     apply (erule disjE, rule disjI2, rule disjI2, rule_tac x = h in exI, simp, rule_tac x= toflag in exI, simp)
     apply ((erule exE|erule conjE)+)