--- a/simple_selinux/Temp.thy	Tue Dec 03 22:42:48 2013 +0800
+++ b/simple_selinux/Temp.thy	Thu Dec 05 20:13:30 2013 +0800
@@ -69,9 +69,15 @@
          (S_proc (pi, pctxt, fds \<union> {(pctxt, flags, (Created, nfsec, Some fsec, asecs \<union> {fsec}))}, shms) tagp)
       ) \<in> static"
 | S_readf:   "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; (fdctxt,flags,sf) \<in> fds; 
-               permission_check pctxt fdctxt C_fd P_setattr; S_file sfs tagf \<in> ss; sf \<in> sfs;
-               permission_check pctxt (sectxt_of_sfile sf) C_file P_read; is_read_flag flags\<rbrakk>
+               permission_check pctxt fdctxt C_fd P_setattr; S_file sf tagf \<in> ss; 
+               permission_check pctxt (sectxt_of_sfile sf) C_file P_read\<rbrakk>
   \<Longrightarrow> (update_ss_shms ss (pi, pctxt,fds,shms) (tagp \<or> tagf)) \<in> static"
+(*add following to locale assumptions:
+     \<And> pctxt fctxt. permission_check pctxt fctxt C_file P_read/P_write \<Longrightarrow>
+       permission_check pctxt pctxt C_fd P_setattr \<and>
+       search_check_s pctxt sf True; not \<forall> sf, should be \<forall> sf \<in> static \<and> sectxt_of_sfile sf = fctxt. 
+
+ *)
 | S_writef:  "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; (fdctxt,flags,sf) \<in> fds; 
                permission_check pctxt fdctxt C_fd P_setattr; sf \<in> sfs; S_file sfs tagf \<in> ss; 
                permission_check pctxt (sectxt_of_sfile sf) C_file P_write; is_write_flag flags\<rbrakk>