--- a/no_shm_selinux/Enrich2.thy	Mon Dec 30 12:01:09 2013 +0800
+++ b/no_shm_selinux/Enrich2.thy	Mon Dec 30 14:04:23 2013 +0800
@@ -648,6 +648,29 @@
       apply (auto simp:is_created_proc_simps split:if_splits)
       done
   qed
+  have sf_cons:
+    "\<forall>f. f \<in> current_files (e # s) \<longrightarrow> cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
+  proof clarify
+    fix f 
+    assume a1: "f \<in> current_files (e # s)"
+    from pre have pre_sf: "\<And> f. \<lbrakk>f \<in> current_files s; is_created_proc s p\<rbrakk>
+      \<Longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f"
+      by auto
+    from a1 have a1': "f \<in> current_files (enrich_proc (e # s) p p')"
+      using vd_cons' nodel_cons
+      by (simp add:enrich_proc_cur_files)
+      
+    show "cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
+        apply (case_tac e)
+        using vd created_cons nodel_cons vd_enrich_cons vd_cons' a1 a1'
+        apply (auto intro!:pre_sf simp:cf2sfile_simps is_created_proc_simps 
+          split:if_splits dest:vd_cons)
+        thm cf2sfile_other
+        apply (simp_all)
+        done
+      
+    
+    sorry
   moreover have "\<forall>tp fd. fd \<in> proc_file_fds (e # s) tp \<longrightarrow> 
     cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
   proof clarify
@@ -673,6 +696,18 @@
       using a1' nodel_cons all_procs_cons a1' created_cons vd_cons'
       apply (frule_tac enrich_proc_filefd, simp_all)
       done
+    have sec_proc:
+      "\<And> tp. \<lbrakk>tp \<in> current_procs s; is_created_proc s p\<rbrakk> 
+       \<Longrightarrow> sectxt_of_obj (enrich_proc s p p') (O_proc tp) = sectxt_of_obj s (O_proc tp)"
+      using pre 
+      apply (clarsimp)
+      apply (erule_tac x = tp in allE, auto simp:cp2sproc_def split:option.splits)
+      done
+    have sec_proc':
+      "\<And> tp. \<lbrakk>tp \<in> current_procs s; is_created_proc s p; p = tp\<rbrakk> 
+       \<Longrightarrow> sectxt_of_obj (enrich_proc s tp p') (O_proc tp) = sectxt_of_obj s (O_proc tp)"
+      apply (drule_tac sec_proc, simp+)
+      done
     show "cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
     proof-
       have b1: "\<And> proc f' fds. e = Execve proc f' fds
@@ -701,9 +736,48 @@
         done 
       have b3: "\<And> proc f' flags fd' opt. e = Open proc f' flags fd' opt 
          \<Longrightarrow> cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
+        using a4 a1' vd_enrich_cons vd_cons' created_cons 
+        apply (simp split:if_splits del:file_of_proc_fd.simps) 
+        
+        apply (simp add:cfd2sfd_open sec_open is_created_proc_simps a2 del:file_of_proc_fd.simps)
+        apply (tactic {*my_clarify_tac 1*})
+        apply (drule vd_cons)
+        apply (simp add:cfd2sfd_open sec_open a3 a2 split:if_splits)
+        apply (case_tac "proc \<in> current_procs s")
+        apply (simp add:sec_proc')
+        apply (case_tac "sectxt_of_obj s (O_proc proc)", simp+)        
+        apply (case_tac "f \<in> current_files (e # s)")
+        apply (drule sf_cons[rule_format], simp)
+        using vd_enrich_cons
+        apply (simp add:cf2sfile_open_none)
+        using os
+        apply (simp add:current_files_simps is_file_in_current split:option.splits)
+        using os
+        apply (simp split:option.splits)
+        apply (rule impI)
+        apply (simp add:cfd2sfd_open sec_open a3 a2 split:if_splits)
+        apply (drule vd_cons)
+        apply (drule_tac p' = tp and fd' = fd and f' = f and s = "enrich_proc s proc p'" in cfd2sfd_open)
+        apply (simp, rule impI, simp)
+        apply (simp split:if_splits, rule conjI, rule impI, simp)
+        apply (drule pre_sfd', simp, simp)
+
+        apply (simp add:cfd2sfd_open sec_open is_created_proc_simps a2 del:file_of_proc_fd.simps)
+        apply (case_tac "proc \<in> current_procs s")
+        apply (simp add:sec_proc)
+        apply (case_tac "f' \<in> current_files (e # s)")
+        apply (drule sf_cons[rule_format], simp)
+        apply (simp split:option.splits)
+        apply (rule impI|rule conjI)+
+        apply (drule current_has_sec', simp add:vd, simp add:os)
+        apply (rule impI, rule impI)
         apply (simp split:if_splits)
-        thm cfd2sfd_open
-        sorry
+        apply (simp add:pre_sfd')
+        using os
+        apply (simp add:current_files_simps is_file_in_current split:option.splits)
+        using os
+        apply (simp split:option.splits)
+        done
       have b4: "\<And> proc fd'. e = ReadFile proc fd' 
          \<Longrightarrow> cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
         using a4 vd_enrich_cons a1' vd_cons' created_cons
@@ -727,8 +801,6 @@
   qed
   moreover have "\<forall>tp. tp \<in> current_procs (e # s) \<longrightarrow> cp2sproc (enrich_proc (e # s) p p') tp = cp2sproc (e # s) tp"
     sorry
-  moreover have "\<forall>f. f \<in> current_files (e # s) \<longrightarrow> cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
-    sorry
   moreover have "\<forall>q. q \<in> current_msgqs (e # s) \<longrightarrow> cq2smsgq (enrich_proc (e # s) p p') q = cq2smsgq (e # s) q"
     sorry
   moreover have "cp2sproc (enrich_proc (e # s) p p') p' = cp2sproc (e # s) p"