--- a/Flask.thy	Mon Jun 24 15:22:37 2013 +0800
+++ b/Flask.thy	Tue Jul 09 14:43:51 2013 +0800
@@ -482,7 +482,8 @@
 *)
 definition one_flow_shm :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
 where
-  "one_flow_shm s h from to \<equiv> (from, SHM_RDWR) \<in> procs_of_shm s h \<and> (\<exists> flag. (to, flag) \<in> procs_of_shm s h)"
+  "one_flow_shm s h from to \<equiv> from \<noteq> to \<and> (from, SHM_RDWR) \<in> procs_of_shm s h \<and> 
+                              (\<exists> flag. (to, flag) \<in> procs_of_shm s h)"
 
 fun self_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
 where
@@ -1471,6 +1472,10 @@
 | t_rename':"\<lbrakk>O_dir f'' \<in> tainted s; valid (Rename p f f' # s);f \<preceq> f''\<rbrakk>
              \<Longrightarrow> O_dir (file_after_rename f f' f'') \<in> tainted (Rename p f f' # s)"
 *)
+| t_attach1:"\<lbrakk>O_proc p \<in> tainted s; valid (Attach p h SHM_RDWR # s); (p', flag') \<in> procs_of_shm s h\<rbrakk>
+             \<Longrightarrow> O_proc p' \<in> tainted (Attach p h SHM_RDWR # s)"
+| t_attach2:"\<lbrakk>O_proc p' \<in> tainted s; valid (Attach p h flag # s); (p', SHM_RDWR) \<in> procs_of_shm s h\<rbrakk>
+             \<Longrightarrow> O_proc p \<in> tainted (Attach p h SHM_RDWR # s)"
 | t_sendmsg:"\<lbrakk>O_proc p \<in> tainted s; valid (SendMsg p q m # s)\<rbrakk>
              \<Longrightarrow> O_msg q m \<in> tainted (SendMsg p q m # s)"
 | t_recvmsg:"\<lbrakk>O_msg q m \<in> tainted s; valid (RecvMsg p q m # s); info_flow_shm s p p'\<rbrakk>