--- a/Co2sobj_prop.thy	Tue Oct 08 16:37:39 2013 +0800
+++ b/Co2sobj_prop.thy	Thu Oct 10 12:00:49 2013 +0800
@@ -2295,18 +2295,24 @@
              dest:is_file_in_current is_dir_in_current)
 done
 
+declare Product_Type.split_paired_Ex Product_Type.split_paired_All [simp del]
+
+lemma info_flow_shm_prop1:
+  "p \<in> current_procs s \<Longrightarrow> info_flow_shm s p p"
+by (simp add:info_flow_shm_def)
+
 lemma co2sobj_attach:
   "\<lbrakk>valid (Attach p h flag # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Attach p h flag # s) obj = (
       case obj of
-        O_proc p' \<Rightarrow> if (p' = p)
-                     then (case (cp2sproc (Attach p h flag # s) p) of
-                             Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s \<or> 
-              (\<exists> p'. O_proc p' \<in> Tainted s \<and> (p', SHM_RDWR) \<in> procs_of_shm s h)))
+        O_proc p' \<Rightarrow> if (info_flow_shm s p p')
+                     then (case (cp2sproc (Attach p h flag # s) p') of
+                             Some sp \<Rightarrow> Some (S_proc sp (O_proc p' \<in> Tainted s \<or> 
+              (\<exists> p''. O_proc p'' \<in> Tainted s \<and> (p'', SHM_RDWR) \<in> procs_of_shm s h)))
                            | _       \<Rightarrow> None)
-                     else if (\<exists> flag'. (p', flag') \<in> procs_of_shm s h)
+                     else if (\<exists> p'' flag'. (p'', flag') \<in> procs_of_shm s h \<and> flag = SHM_RDWR \<and> O_proc p \<in> Tainted s \<and>
+  info_flow_shm s p'' p')
                           then (case (cp2sproc s p') of 
-                                  Some sp \<Rightarrow> Some (S_proc sp (O_proc p' \<in> Tainted s \<or>
-              (O_proc p \<in> Tainted s \<and> flag = SHM_RDWR)))
+                                  Some sp \<Rightarrow> Some (S_proc sp True)
                                 | _       \<Rightarrow> None)
                           else co2sobj s obj
       | _         \<Rightarrow> co2sobj s obj)"
@@ -2314,19 +2320,21 @@
 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
 
 apply (rule conjI|rule impI|erule exE)+
-apply (simp split:option.splits)
+apply (simp split:option.splits del:split_paired_Ex)
 apply (rule impI, frule current_proc_has_sp, simp)
-apply ((erule exE)+, auto simp:cp2sproc_attach tainted_eq_Tainted)[1]
-apply (rule impI|rule conjI)+
-apply (subgoal_tac "p \<in> current_procs (Attach p h flag # s)")
-apply (drule_tac p = p in current_proc_has_sp, simp, erule exE)
-apply (auto simp:tainted_eq_Tainted)[1]
-apply (simp, rule impI)
-apply (subgoal_tac "nat \<in> current_procs (Attach p h flag # s)")
-apply (drule_tac p = nat in current_proc_has_sp, simp, erule exE)
-apply (drule_tac p = nat in current_proc_has_sp, simp, erule exE)
-apply (auto simp:cp2sproc_attach tainted_eq_Tainted)[1]
-apply simp
+apply ((erule exE)+, auto simp:tainted_eq_Tainted intro:info_flow_shm_Tainted)[1]
+apply (rule impI, simp add:tainted_eq_Tainted split:option.splits del:split_paired_Ex)
+apply (auto simp:info_flow_shm_prop1 cp2sproc_attach dest!:current_proc_has_sp')[1]
+
+apply (case_tac "cp2sproc (Attach p h flag # s) nat")
+apply (drule current_proc_has_sp', simp+)
+
+apply (rule conjI|erule exE|erule conjE|rule impI)+
+apply (simp add:tainted_eq_Tainted)
+apply (auto simp:info_flow_shm_prop1 cp2sproc_attach intro:info_flow_shm_Tainted dest!:current_proc_has_sp')[1]
+apply (auto simp:info_flow_shm_prop1 cp2sproc_attach tainted_eq_Tainted intro:info_flow_shm_Tainted dest!:current_proc_has_sp'
+split:option.splits if_splits)[1]
+
 
 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' 
              simp:current_files_simps cf2sfiles_simps cf2sfile_simps tainted_eq_Tainted

--- a/Static.thy	Tue Oct 08 16:37:39 2013 +0800
+++ b/Static.thy	Thu Oct 10 12:00:49 2013 +0800
@@ -482,7 +482,7 @@
      | _ \<Rightarrow> sobj = sobj')}"
 
 
-(* no del 
+
 (* all reachable static states(sobjects set) *)
 inductive_set static :: "t_static_state set"
 where
@@ -650,15 +650,19 @@
 | "init_obj_related (S_dir sf) (O_dir f) = (sfile_related sf f)"
 | "init_obj_related (S_msgq (qi, sec, sms)) (O_msgq q') = (qi = Init q')"
 | "init_obj_related (S_shm (hi, sec)) (O_shm h') = (hi = Init h')"
+(*
 | "init_obj_related (S_msg (qi, sec, sms) (mi, secm, tagm)) (O_msg q' m') = (qi = Init q' \<and> mi = Init m')"
+*)
 | "init_obj_related _ _ = False"
 
 fun tainted_s :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> bool"
 where
   "tainted_s ss (S_proc sp  tag) = (S_proc sp tag  \<in> ss \<and> tag = True)"
 | "tainted_s ss (S_file sfs tag) = (S_file sfs tag \<in> ss \<and> tag = True)"
+(*
 | "tainted_s ss (S_msg  (qi, sec, sms)  (mi, secm, tag)) = 
      (S_msgq (qi, sec, sms) \<in> ss \<and> (mi,secm,tag) \<in> set sms \<and> tag = True)"
+*)
 | "tainted_s ss _ = False"
 
 (*

--- a/Tainted_prop.thy	Tue Oct 08 16:37:39 2013 +0800
+++ b/Tainted_prop.thy	Thu Oct 10 12:00:49 2013 +0800
@@ -54,9 +54,9 @@
       else Tainted s)"
 | "Tainted (Attach p h flag # s) = 
      (if (O_proc p \<in> Tainted s \<and> flag = SHM_RDWR) 
-      then Tainted s \<union> {O_proc p' | p' flag'. (p', flag') \<in> procs_of_shm s h}
+      then Tainted s \<union> {O_proc p'' | p' flag' p''. (p', flag') \<in> procs_of_shm s h \<and> info_flow_shm s p' p''}
       else if (\<exists> p'. O_proc p' \<in> Tainted s \<and> (p', SHM_RDWR) \<in> procs_of_shm s h)
-           then Tainted s \<union> {O_proc p}
+           then Tainted s \<union> {O_proc p'| p'. info_flow_shm s p p'}
            else Tainted s)"
 | "Tainted (SendMsg p q m # s) = 
      (if (O_proc p \<in> Tainted s) then Tainted s \<union> {O_msg q m} else Tainted s)"