--- a/Flask.thy	Tue Nov 19 09:27:25 2013 +0800
+++ b/Flask.thy	Tue Nov 19 12:31:56 2013 +0800
@@ -1115,19 +1115,27 @@
         (Some ctxts, Some ctxt) \<Rightarrow> Some (ctxt#ctxts)
       | _ \<Rightarrow> None)"
 
+definition search_check_ctxt:: 
+  "security_context_t \<Rightarrow> security_context_t \<Rightarrow> security_context_t set \<Rightarrow> bool \<Rightarrow> bool"
+where
+  "search_check_ctxt pctxt fctxt asecs if_file \<equiv> (
+      if if_file 
+      then search_check_file pctxt fctxt \<and> search_check_allp pctxt asecs
+      else search_check_dir  pctxt fctxt \<and> search_check_allp pctxt asecs )"
+
 fun search_check :: "t_state \<Rightarrow> security_context_t \<Rightarrow> t_file \<Rightarrow> bool"
 where
   "search_check s pctxt [] = 
      (case (sectxt_of_obj s (O_dir [])) of
-        Some fctxt \<Rightarrow> search_check_dir pctxt fctxt
+        Some fctxt \<Rightarrow> search_check_ctxt pctxt fctxt {} False 
       | _          \<Rightarrow> False)"
 | "search_check s pctxt (f#pf) = 
      (if (is_file s (f#pf)) 
       then (case (sectxt_of_obj s (O_file (f#pf)), get_parentfs_ctxts s pf) of
-              (Some fctxt, Some pfctxts) \<Rightarrow> (search_check_file pctxt fctxt \<and> search_check_allp pctxt (set pfctxts))
+              (Some fctxt, Some pfctxts) \<Rightarrow> search_check_ctxt pctxt fctxt (set pfctxts) True
             | _ \<Rightarrow> False)
       else (case (sectxt_of_obj s (O_dir (f#pf)), get_parentfs_ctxts s pf) of
-              (Some fctxt, Some pfctxts) \<Rightarrow> (search_check_dir pctxt fctxt \<and> search_check_allp pctxt (set pfctxts))
+              (Some fctxt, Some pfctxts) \<Rightarrow> search_check_ctxt pctxt fctxt (set pfctxts) False
             | _ \<Rightarrow> False))"
 
 (* this means we should prove every current fd has a security context! *)
@@ -1135,10 +1143,13 @@
 where
   "sectxts_of_fds s p fds \<equiv> {ctxt. \<exists> fd \<in> fds. sectxt_of_obj s (O_fd p fd) = Some ctxt}"
 
+definition inherit_fds_check_ctxt:: "security_context_t \<Rightarrow> security_context_t set \<Rightarrow> bool"
+where
+  "inherit_fds_check_ctxt p fds \<equiv> (\<forall> ctxt \<in> fds. permission_check p ctxt C_fd P_inherit)"
+
 definition inherit_fds_check :: "t_state \<Rightarrow> security_context_t \<Rightarrow> t_process \<Rightarrow> t_fd set \<Rightarrow> bool"
 where
-  "inherit_fds_check s npsectxt p fds \<equiv> 
-     (\<forall> ctxt \<in> sectxts_of_fds s p fds. permission_check npsectxt ctxt C_fd P_inherit)"
+  "inherit_fds_check s npsectxt p fds \<equiv> inherit_fds_check_ctxt npsectxt (sectxts_of_fds s p fds)"
 
 fun npctxt_execve :: "security_context_t \<Rightarrow> security_context_t \<Rightarrow> security_context_t option"
 where
@@ -1165,10 +1176,13 @@
 where
   "sectxts_of_shms s shms \<equiv> {ctxt. \<exists> h \<in> shms. sectxt_of_obj s (O_shm h) = Some ctxt}"
 
+definition inherit_shms_check_ctxt:: "security_context_t \<Rightarrow> security_context_t set \<Rightarrow> bool"
+where
+  "inherit_shms_check_ctxt p shms \<equiv> (\<forall> ctxt \<in> shms. permission_check p ctxt C_shm P_inherit)"
+
 definition inherit_shms_check :: "t_state \<Rightarrow> security_context_t \<Rightarrow> t_shm set \<Rightarrow> bool"
 where
-  "inherit_shms_check s npsectxt shms \<equiv> 
-     (\<forall> ctxt \<in> sectxts_of_shms s shms. permission_check npsectxt ctxt C_shm P_inherit)"
+  "inherit_shms_check s npsectxt shms \<equiv> inherit_shms_check_ctxt npsectxt (sectxts_of_shms s shms)"
 
 fun perm_of_mflag :: "t_open_must_flag \<Rightarrow> permission_t set"
 where