--- a/Tainted_prop.thy	Mon Jun 24 15:22:37 2013 +0800
+++ b/Tainted_prop.thy	Tue Jul 09 14:43:51 2013 +0800
@@ -50,6 +50,12 @@
      (if (len > 0 \<and> O_proc p \<in> Tainted s)
       then Tainted s \<union> {O_file f' | f'. has_same_inode s f f'}
       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}
+      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}
+           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)"
 | "Tainted (RecvMsg p q m # s) = 
@@ -72,7 +78,8 @@
 apply (drule seeds_in_init, case_tac obj, simp_all add:is_file_nil)
 apply (frule vd_cons, frule valid_Tainted_obj, simp, frule vt_grant_os, case_tac a)
 apply (auto simp:alive_simps split:if_splits option.splits t_object.splits
-           intro:has_same_inode_prop2 has_same_inode_prop1 dest:info_shm_flow_in_procs)
+           intro:has_same_inode_prop2 has_same_inode_prop1 procs_of_shm_prop2 
+            dest:info_shm_flow_in_procs)
 done
 
 lemma Tainted_proc_in_current:
@@ -95,12 +102,6 @@
 (*?? 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"
@@ -116,17 +117,40 @@
   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 intro!:info_flow_shm_intro p5)    
+    by (rule p4, auto simp:info_flow_shm_def one_flow_shm_def)    
   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
-  proof (cases "p = p'")
+  proof (cases "self_shm s p p'")
     case True with p1 show ?thesis by simp
   next
     case False
     with p1 p2 p5 p6 p7 p8 p3 show ?thesis
     apply (case_tac e)
     prefer 7
+    apply (simp add:info_flow_shm_simps split:if_splits option.splits)
+    apply (rule allI|rule impI|rule conjI)+
+    apply simp
+    apply (case_tac "O_proc p \<in> Tainted s", drule_tac p'=p' in p4, simp+)
+    apply simp
+
+
+
+
+    apply (auto simp:info_flow_shm_simps one_flow_shm_def dest:Tainted_in_current 
+  intro:p4 p4' split:if_splits option.splits)
+    apply (auto simp:info_flow_shm_def one_flow_shm_def)
+
+
+
+    apply (auto simp:one_flow_shm_def intro:p4 p4' split:if_splits option.splits)
+
+
+
+
+
+
+    prefer 7
     apply (simp split:if_splits option.splits)
     apply (rule allI|rule impI|rule conjI)+