--- 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