# HG changeset patch
# User chunhan
# Date 1373352231 -28800
# Node ID fc749f19b8947ab1e4d9896c14d79084201682d2
# Parent  b6333712cb024e0c3ef2336cf27b50e9cd67de12
Info_flow_shm_attach_prop

diff -r b6333712cb02 -r fc749f19b894 Current_prop.thy
--- a/Current_prop.thy	Mon Jun 24 15:22:37 2013 +0800
+++ b/Current_prop.thy	Tue Jul 09 14:43:51 2013 +0800
@@ -55,15 +55,332 @@
   "\<lbrakk>info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s \<and> p' \<in> current_procs s"
 by (auto intro:procs_of_shm_prop2 simp:info_flow_shm_def one_flow_shm_def)
 
-(*********** simpset for info_flow_shm **************)
+lemma flag_of_proc_shm_prop1:
+  "\<lbrakk>flag_of_proc_shm s p h = Some flag; valid s\<rbrakk> \<Longrightarrow> (p, flag) \<in> procs_of_shm s h"
+apply (induct s arbitrary:p flag)
+apply (simp, drule init_shmflag_has_proc, simp)
+apply (frule vd_cons, frule vt_grant_os)
+apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2)
+done
+
+(*********** simpset for one_flow_shm **************)
+
+lemma one_flow_not_self:
+  "one_flow_shm s h p p \<Longrightarrow> False"
+by (simp add:one_flow_shm_def)
+
+lemma one_flow_shm_attach:
+  "valid (Attach p h flag # s) \<Longrightarrow> one_flow_shm (Attach p h flag # s) = (\<lambda> h' pa pb. 
+     if (h' = h) 
+     then (pa = p \<and> pb \<noteq> p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pb, flagb) \<in> procs_of_shm s h)) \<or>
+          (pb = p \<and> pa \<noteq> p \<and> (pa, SHM_RDWR) \<in> procs_of_shm s h) \<or>
+          (one_flow_shm s h pa pb)               
+     else one_flow_shm s h' pa pb        )"
+apply (rule ext, rule ext, rule ext, frule vd_cons, frule vt_grant_os)
+by (auto simp add: one_flow_shm_def)
+
+lemma one_flow_shm_detach:
+  "valid (Detach p h # s) \<Longrightarrow> one_flow_shm (Detach p h # s) = (\<lambda> h' pa pb.
+     if (h' = h) 
+     then (pa \<noteq> p \<and> pb \<noteq> p \<and> one_flow_shm s h' pa pb)
+     else one_flow_shm s h' pa pb)"
+apply (rule ext, rule ext, rule ext, frule vt_grant_os)
+by (auto simp:one_flow_shm_def)
+
+lemma one_flow_shm_deleteshm:
+  "valid (DeleteShM p h # s) \<Longrightarrow> one_flow_shm (DeleteShM p h # s) = (\<lambda> h' pa pb. 
+     if (h' = h) 
+     then False
+     else one_flow_shm s h' pa pb)"
+apply (rule ext, rule ext, rule ext, frule vt_grant_os)
+by (auto simp: one_flow_shm_def)
+
+lemma one_flow_shm_clone:
+  "valid (Clone p p' fds shms # s) \<Longrightarrow> one_flow_shm (Clone p p' fds shms # s) = (\<lambda> h pa pb. 
+     if (pa = p' \<and> pb \<noteq> p' \<and> h \<in> shms)
+     then (if (pb = p) then (flag_of_proc_shm s p h = Some SHM_RDWR) else one_flow_shm s h p pb)
+     else if (pb = p' \<and> pa \<noteq> p' \<and> h \<in> shms)
+          then (if (pa = p) then (flag_of_proc_shm s p h = Some SHM_RDWR) else one_flow_shm s h pa p)
+          else one_flow_shm s h pa pb)"
+apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons, clarsimp)
+apply (frule_tac p = p' in procs_of_shm_prop2', simp)
+apply (auto simp:one_flow_shm_def intro:procs_of_shm_prop4 flag_of_proc_shm_prop1)
+done
+
+lemma one_flow_shm_execve:
+  "valid (Execve p f fds # s) \<Longrightarrow> one_flow_shm (Execve p f fds # s) = (\<lambda> h pa pb. 
+     pa \<noteq> p \<and> pb \<noteq> p \<and> one_flow_shm s h pa pb    )"
+apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)
+by (auto simp:one_flow_shm_def)
+
+lemma one_flow_shm_kill:
+  "valid (Kill p p' # s) \<Longrightarrow> one_flow_shm (Kill p p' # s) = (\<lambda> h pa pb. 
+     pa \<noteq> p' \<and> pb \<noteq> p' \<and> one_flow_shm s h pa pb                 )"
+apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)
+by (auto simp:one_flow_shm_def)
+
+lemma one_flow_shm_exit:
+  "valid (Exit p # s) \<Longrightarrow> one_flow_shm (Exit p # s) = (\<lambda> h pa pb. 
+     pa \<noteq> p \<and> pb \<noteq> p \<and> one_flow_shm s h pa pb                          )"
+apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)
+by (auto simp:one_flow_shm_def)
+
+lemma one_flow_shm_other:
+  "\<lbrakk>valid (e # s); 
+    \<forall> p h flag. e \<noteq> Attach p h flag;
+    \<forall> p h. e \<noteq> Detach p h;
+    \<forall> p h. e \<noteq> DeleteShM p h;
+    \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;
+    \<forall> p f fds. e \<noteq> Execve p f fds;
+    \<forall> p p'. e \<noteq> Kill p p';
+    \<forall> p. e \<noteq> Exit p
+   \<rbrakk> \<Longrightarrow> one_flow_shm (e # s) = one_flow_shm s"
+apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)
+apply (case_tac e, auto simp:one_flow_shm_def dest:procs_of_shm_prop2)
+apply (drule procs_of_shm_prop1, auto)
+done
+
+lemmas one_flow_shm_simps = one_flow_shm_other one_flow_shm_attach one_flow_shm_detach one_flow_shm_deleteshm
+  one_flow_shm_clone one_flow_shm_execve one_flow_shm_kill one_flow_shm_exit
+
+
+inductive Info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
+where
+  ifs_self: "p \<in> current_procs s \<Longrightarrow> Info_flow_shm s p p"
+| ifs_flow:"\<lbrakk>Info_flow_shm s p p'; one_flow_shm s h p' p''\<rbrakk> \<Longrightarrow> Info_flow_shm s p p''"
+
+lemma Info_flow_trans_aux:
+  "Info_flow_shm s p' p'' \<Longrightarrow> \<forall>p. Info_flow_shm s p p' \<longrightarrow> Info_flow_shm s p p''"
+apply (erule Info_flow_shm.induct)
+by (auto intro:Info_flow_shm.intros)
+
+lemma Info_flow_trans:
+  "\<lbrakk>Info_flow_shm s p p'; Info_flow_shm s p' p''\<rbrakk> \<Longrightarrow> Info_flow_shm s p p''"
+by (auto dest:Info_flow_trans_aux)
+
+lemma one_flow_flows:
+  "\<lbrakk>one_flow_shm s h p p'; valid s\<rbrakk> \<Longrightarrow> Info_flow_shm s p p'"
+apply (rule Info_flow_shm.intros(2), simp_all)
+apply (rule Info_flow_shm.intros(1))
+apply (auto intro:procs_of_shm_prop2 simp:one_flow_shm_def)
+done
+
+lemma ifs_flow': "\<lbrakk>one_flow_shm s h p p'; Info_flow_shm s p' p''; valid s\<rbrakk> \<Longrightarrow> Info_flow_shm s p p''"
+apply (drule one_flow_flows, simp+)
+apply (erule Info_flow_trans, simp+)
+done
+
+lemma Info_flow_shm_cases1:
+  "\<lbrakk>Info_flow_shm s pa pb; 
+    \<And>p \<tau>. \<lbrakk>\<tau> = s; pa = p; pb = p; p \<in> current_procs \<tau>\<rbrakk> \<Longrightarrow> P;
+    \<And>\<tau> p p' h p''. \<lbrakk>\<tau> = s; pa = p; pb = p''; Info_flow_shm \<tau> p p'; one_flow_shm \<tau> h p' p''\<rbrakk> \<Longrightarrow> P\<rbrakk>
+   \<Longrightarrow> P"
+by (erule Info_flow_shm.cases, auto)
+
+
+lemma Info_flow_shm_prop1:
+  "\<not> Info_flow_shm s p p \<Longrightarrow> p \<notin> current_procs s" 
+by (rule notI, drule Info_flow_shm.intros(1), simp)
+
+lemma Info_flow_shm_intro4:
+  "\<lbrakk>(p, flagb) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> Info_flow_shm s p p"
+by (drule procs_of_shm_prop2, simp, simp add:Info_flow_shm.intros)
+
+(********* simpset for inductive Info_flow_shm **********)
 
-lemma info_flow_shm_attach:
-  "valid (Attach p h flag # s) \<Longrightarrow> info_flow_shm (Attach p h flag # s) = (\<lambda> pa pb. 
-     (pa = p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pb, flagb) \<in> procs_of_shm s h)) \<or>
-     (pb = p \<and> (pa, SHM_RDWR) \<in> procs_of_shm s h) \<or>
-     (info_flow_shm s pa pb)                       )"
-apply (rule ext, rule ext, frule vt_grant_os)
-by (auto simp add:info_flow_shm_def one_flow_shm_def)
+lemma Info_flow_shm_attach1:
+  "Info_flow_shm s' pa pb \<Longrightarrow> valid s' \<and> (s' = Attach p h flag # s) \<longrightarrow> 
+    ((Info_flow_shm s pa pb) \<or> 
+     (\<not> Info_flow_shm s pa pb \<and> pa = p \<and> pb \<noteq> p \<and> flag = SHM_RDWR \<and> 
+       (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)) \<or>
+     (\<not> Info_flow_shm s pa pb \<and> pb = p \<and> pa \<noteq> p \<and> 
+       (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p')))"
+proof (induct rule:Info_flow_shm.induct)
+  case (ifs_self proc \<tau>)
+  show ?case
+  proof (rule impI)
+    assume pre: "valid \<tau> \<and> \<tau> = Attach p h flag # s"
+    hence p1: "p \<in> current_procs s" and p2: "valid s" by (auto intro:vd_cons dest:vt_grant_os)
+    hence p3: "Info_flow_shm s p p" by (auto intro:Info_flow_shm.intros)
+    from ifs_self pre have "proc \<in> current_procs s" by simp 
+    hence p4: "Info_flow_shm s proc proc" by (auto intro:Info_flow_shm.intros)
+    show "Info_flow_shm s proc proc \<or>
+          (\<not> Info_flow_shm s proc proc \<and> proc = p \<and> proc \<noteq> p \<and> flag = SHM_RDWR \<and> 
+           (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' proc)) \<or>
+          (\<not> Info_flow_shm s proc proc \<and> proc = p \<and> proc \<noteq> p \<and> 
+           (\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s proc p'))"
+      using p4 p3 by auto
+  qed
+next
+  case (ifs_flow \<tau> pa pb h' pc)
+  thus ?case
+  proof (rule_tac impI)
+    assume p1:"Info_flow_shm \<tau> pa pb" and p2: "valid \<tau> \<and> (\<tau> = Attach p h flag # s) \<longrightarrow> Info_flow_shm s pa pb \<or>
+     \<not> Info_flow_shm s pa pb \<and> pa = p \<and>
+     pb \<noteq> p \<and> flag = SHM_RDWR \<and> (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb) \<or>
+     \<not> Info_flow_shm s pa pb \<and> pb = p \<and> pa \<noteq> p \<and> (\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p')"
+    and p3: "one_flow_shm \<tau> h' pb pc" and p4: "valid \<tau> \<and> \<tau> = Attach p h flag # s" 
+    from p2 and p4 have p2': "Info_flow_shm s pa pb \<or> 
+      (\<not> Info_flow_shm s pa pb \<and> pa = p \<and> pb \<noteq> p \<and> flag = SHM_RDWR \<and> 
+       (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)) \<or>
+      (\<not> Info_flow_shm s pa pb \<and> pb = p \<and> pa \<noteq> p \<and> 
+       (\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'))"
+      by (erule_tac impE, simp)
+    from p4 have p5: "valid s" and p6: "os_grant s (Attach p h flag)" by (auto intro:vd_cons dest:vt_grant_os)
+    from p6 have "p \<in> current_procs s" by simp hence p7:"Info_flow_shm s p p" by (erule_tac Info_flow_shm.intros)
+    from p3 p4 have p8: "if (h' = h) 
+     then (pb = p \<and> pc \<noteq> p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pc, flagb) \<in> procs_of_shm s h)) \<or>
+          (pc = p \<and> pb \<noteq> p \<and> (pb, SHM_RDWR) \<in> procs_of_shm s h) \<or>
+          (one_flow_shm s h pb pc)               
+     else one_flow_shm s h' pb pc        " by (auto simp add:one_flow_shm_attach) 
+    
+    have "\<lbrakk>pa = p; pc = p\<rbrakk> \<Longrightarrow> Info_flow_shm s pa pc " using p7 by simp
+    moreover have "\<lbrakk>pa = p; pc \<noteq> p; flag = SHM_RDWR; \<not> Info_flow_shm s pa pc\<rbrakk> 
+      \<Longrightarrow> \<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc"
+      sorry
+    moreover have "\<lbrakk>pa = p; pc \<noteq> p; flag \<noteq> SHM_RDWR; \<not> Info_flow_shm s pa pc\<rbrakk>
+      \<Longrightarrow> Info_flow_shm s pa pc"
+      sorry
+    moreover have "\<lbrakk>pc = p; pa \<noteq> p; \<not> Info_flow_shm s pa pc\<rbrakk>
+      \<Longrightarrow> \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'"
+      sorry
+    ultimately 
+
+      
+    
+    show "Info_flow_shm s pa pc \<or>
+      (\<not> Info_flow_shm s pa pc \<and> pa = p \<and> pc \<noteq> p \<and> flag = SHM_RDWR \<and> 
+       (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc)) \<or>
+      (\<not> Info_flow_shm s pa pc \<and> pc = p \<and> pa \<noteq> p \<and> 
+       (\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'))"
+      apply auto
+      sorry
+  qed
+qed
+
+lemma Info_flow_shm_intro3:
+  "\<lbrakk>Info_flow_shm s p from; (from, SHM_RDWR) \<in> procs_of_shm s h; (to, flag) \<in> procs_of_shm s h\<rbrakk>
+   \<Longrightarrow> Info_flow_shm s p to"
+apply (case_tac "from = to", simp)
+apply (erule_tac h = h in Info_flow_shm.intros(2), simp add:one_flow_shm_def)
+by (rule_tac x = flag in exI, simp)
+
+lemma Info_flow_shm_attach1:
+  "Info_flow_shm s' pa pb \<Longrightarrow> valid s' \<and> (s' = Attach p h flag # s) \<longrightarrow> 
+     (if Info_flow_shm s pa pb then True else
+     (if (pa = p \<and> flag = SHM_RDWR) 
+      then (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)
+      else if (pb = p) 
+           then (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p')
+           else (\<exists> p' flag'. Info_flow_shm s pa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> 
+                             Info_flow_shm s p' pb) \<or>
+                (\<exists> p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pb)
+     )  )"
+proof (induct rule:Info_flow_shm.induct)
+  case (ifs_self proc \<tau>)
+  show ?case
+  proof (rule impI)
+    assume pre: "valid \<tau> \<and> \<tau> = Attach p h flag # s"
+    hence p1: "p \<in> current_procs s" and p2: "valid s" by (auto intro:vd_cons dest:vt_grant_os)
+    hence p3: "Info_flow_shm s p p" by (auto intro:Info_flow_shm.intros)
+    from ifs_self pre have "proc \<in> current_procs s" by simp 
+    hence p4: "Info_flow_shm s proc proc" by (auto intro:Info_flow_shm.intros)
+    show "if Info_flow_shm s proc proc then True
+    else if proc = p \<and> flag = SHM_RDWR then \<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' proc
+         else if proc = p then \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s proc p'
+              else (\<exists>p' flag'. Info_flow_shm s proc p \<and>
+                       flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' proc) \<or>
+                   (\<exists>p'. Info_flow_shm s proc p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p proc)"      using p4 p3 by auto
+  qed
+next
+  case (ifs_flow \<tau> pa pb h' pc)
+  thus ?case
+  proof (rule_tac impI)
+    assume p1:"Info_flow_shm \<tau> pa pb" and p2: "valid \<tau> \<and> \<tau> = Attach p h flag # s \<longrightarrow>
+     (if Info_flow_shm s pa pb then True
+      else if pa = p \<and> flag = SHM_RDWR then \<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb
+           else if pb = p then \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'
+                else (\<exists>p' flag'. Info_flow_shm s pa p \<and>
+                         flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb) \<or>
+                     (\<exists>p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pb))"
+      and p3: "one_flow_shm \<tau> h' pb pc" and p4: "valid \<tau> \<and> \<tau> = Attach p h flag # s"
+
+    from p2 and p4 have p2': "(if Info_flow_shm s pa pb then True
+      else if pa = p \<and> flag = SHM_RDWR then \<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb
+           else if pb = p then \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'
+                else (\<exists>p' flag'. Info_flow_shm s pa p \<and>
+                         flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb) \<or>
+                     (\<exists>p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pb))"
+      by (erule_tac impE, simp)
+    from p4 have p5: "valid s" and p6: "os_grant s (Attach p h flag)" by (auto intro:vd_cons dest:vt_grant_os)
+    from p6 have "p \<in> current_procs s" by simp hence p7:"Info_flow_shm s p p" by (erule_tac Info_flow_shm.intros)
+    from p3 p4 have p8: "if (h' = h) 
+     then (pb = p \<and> pc \<noteq> p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pc, flagb) \<in> procs_of_shm s h)) \<or>
+          (pc = p \<and> pb \<noteq> p \<and> (pb, SHM_RDWR) \<in> procs_of_shm s h) \<or>
+          (one_flow_shm s h pb pc)               
+     else one_flow_shm s h' pb pc        " by (auto simp add:one_flow_shm_attach) 
+
+    have "\<And> flagb. (pc, flagb) \<in> procs_of_shm s h 
+      \<Longrightarrow> \<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc"
+      apply (rule_tac x= pc in exI, rule_tac x = flagb in exI, frule procs_of_shm_prop2)
+      by (simp add:p5, simp add:Info_flow_shm.intros(1))
+    hence p10: "\<not> Info_flow_shm s p pc \<Longrightarrow> (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc) \<or>
+      Info_flow_shm s pa pc"
+      using p2' p7 p8 p5
+      by (auto split:if_splits dest:Info_flow_shm.intros(2))      
+  (*     apply (rule_tac x = pb in exI, simp add:one_flow_flows, rule_tac x = flagb in exI, simp)+  *)
+    moreover have "pc = p \<Longrightarrow> (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p') 
+                            \<or> Info_flow_shm s pa pc"
+      using p2' p7 p8 p5
+      by (auto split:if_splits intro:Info_flow_shm_intro3 simp:one_flow_shm_def)
+    moreover have "\<lbrakk>pc \<noteq> p; pa \<noteq> p \<or> flag \<noteq> SHM_RDWR\<rbrakk> \<Longrightarrow> (\<exists>p' flag'. Info_flow_shm s pa p \<and>
+                          flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc) \<or>
+                      (\<exists>p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pc) \<or>
+                      Info_flow_shm s pa pc"
+      using p2' p7 p8 p5
+      apply (auto split:if_splits intro:Info_flow_shm_intro3 simp:one_flow_shm_def)
+      apply (rule_tac x = pc in exI, simp add:Info_flow_shm_intro4)
+      apply (rule_tac x = flagb in exI, simp)      
+      done
+    ultimately  show "if Info_flow_shm s pa pc then True
+       else if pa = p \<and> flag = SHM_RDWR then \<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc
+            else if pc = p then \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'
+                 else (\<exists>p' flag'. Info_flow_shm s pa p \<and>
+                          flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc) \<or>
+                      (\<exists>p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pc)"
+      using p7 by auto
+  qed
+qed
+
+      
+
+
+
+
+
+
+
+
+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>
+     (pa = p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)) \<or>
+     (pb = p \<and> (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pa)) )"
+apply (rule ext, rule ext, rule iffI)
+apply (case_tac "Info_flow_shm s pa pb", simp)
+apply (case_tac "pa = p \<and> flag = SHM_RDWR \<and> (\<exists>flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)", simp)
+
+apply (erule Info_flow_shm_cases1, simp, drule_tac p = pc in Info_flow_shm.intros(1), simp)
+apply (simp add:one_flow_shm_simps split:if_splits, erule disjE, simp)
+
+
+
+apply (simp split:if_splits, (rule impI|rule allI|rule conjI|erule conjE|erule exE)+, simp)
+apply (simp)
+apply (simp, erule Info_flow_shm_cases', simp, simp)
+apply (rule_tac x = 
+apply (auto dest:Info_flow_shm.cases)
+apply (auto simp add:one_flow_shm_simps)
 
 lemma info_flow_shm_detach:
   "valid (Detach p h # s) \<Longrightarrow> info_flow_shm (Detach p h # s) = (\<lambda> pa pb. 
diff -r b6333712cb02 -r fc749f19b894 Flask.thy
--- 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>
diff -r b6333712cb02 -r fc749f19b894 Tainted_prop.thy
--- 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)+