--- a/Tainted_prop.thy	Thu Oct 24 09:42:35 2013 +0800
+++ b/Tainted_prop.thy	Wed Oct 30 08:18:40 2013 +0800
@@ -36,7 +36,7 @@
 | "Tainted (WriteFile p fd # s) = 
      (case (file_of_proc_fd s p fd) of 
         Some f \<Rightarrow> if (O_proc p) \<in> Tainted s
-                  then Tainted s \<union> {O_file f' | f'. has_same_inode s f f'}
+                  then Tainted s \<union> {O_file f' | f'. f' \<in> same_inode_files s f}
                   else Tainted s
       | None   \<Rightarrow> Tainted s)"
 | "Tainted (CloseFd p fd # s) = 
@@ -50,7 +50,7 @@
      (if (O_file f \<in> Tainted s) then Tainted s \<union> {O_file f'} else Tainted s)"
 | "Tainted (Truncate p f len # s) = 
      (if (len > 0 \<and> O_proc p \<in> Tainted s)
-      then Tainted s \<union> {O_file f' | f'. has_same_inode s f f'}
+      then Tainted s \<union> {O_file f' | f'. f' \<in> same_inode_files s f}
       else Tainted s)"
 | "Tainted (Attach p h flag # s) = 
      (if (O_proc p \<in> Tainted s \<and> flag = SHM_RDWR) 
@@ -80,8 +80,9 @@
 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 procs_of_shm_prop2 
+           intro:same_inode_files_prop1 procs_of_shm_prop2 
             dest:info_shm_flow_in_procs)
+apply (auto simp:same_inode_files_def is_file_def split:if_splits)
 done 
 
 lemma Tainted_proc_in_current:
@@ -161,6 +162,10 @@
 qed
 qed
 
+lemma has_same_inode_comm:
+  "has_same_inode s f f' = has_same_inode s f' f"
+by (auto simp add:has_same_inode_def same_inode_files_def is_file_def)
+
 lemma tainted_imp_Tainted:
   "obj \<in> tainted s \<Longrightarrow> obj \<in> Tainted s"
 apply (induct rule:tainted.induct)  (*
@@ -170,7 +175,7 @@
 apply (rule disjI2, rule_tac x = flag' in exI, simp)
 apply ((rule impI)+, erule_tac x = p' in allE, simp)
 *)
-apply (auto intro:info_flow_shm_Tainted dest:vd_cons)
+apply (auto intro:info_flow_shm_Tainted simp:has_same_inode_def dest:vd_cons)
 apply (case_tac e, auto split:option.splits if_splits simp:alive_simps)
 done
 
@@ -184,7 +189,8 @@
 apply (induct s arbitrary:obj, simp add:t_init)
 apply (frule Tainted_in_current, simp+)
 apply (frule vt_grant_os, frule vd_cons, case_tac a)
-apply (auto split:if_splits option.splits elim:Tainted_imp_tainted_aux_remain intro:tainted.intros)
+apply (auto split:if_splits option.splits elim:Tainted_imp_tainted_aux_remain intro:tainted.intros
+  simp:has_same_inode_def)
 done
 
 lemma tainted_eq_Tainted:
@@ -195,19 +201,43 @@
   "\<lbrakk>O_proc p \<in> tainted s; info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> O_proc p' \<in> tainted s"
 by (simp only:tainted_eq_Tainted info_flow_shm_Tainted)
 
+
+lemma same_inode_files_Tainted:
+  "\<lbrakk>O_file f \<in> Tainted s; f' \<in> same_inode_files s f; valid s\<rbrakk> \<Longrightarrow> O_file f' \<in> Tainted s"
+apply (induct s arbitrary:f f', simp add:same_inode_in_seeds has_same_inode_def)
+apply (frule vt_grant_os, frule vd_cons, case_tac a)
+prefer 6
+apply (simp split:if_splits option.splits add:same_inode_files_open current_files_simps)
+prefer 8
+apply (frule Tainted_in_current, simp, simp add:alive.simps, drule is_file_in_current)
+apply (auto simp add:same_inode_files_closefd split:option.splits if_splits)[1]
+prefer 8
+apply (frule Tainted_in_current, simp, simp add:alive.simps, drule is_file_in_current)
+apply (auto simp add:same_inode_files_unlink split:option.splits if_splits)[1]
+prefer 10
+apply (auto split:if_splits option.splits simp:same_inode_files_linkhard current_files_simps)[1]
+apply (drule Tainted_in_current, simp, simp add:alive.simps is_file_in_current)
+apply (drule same_inode_files_prop5, simp)
+apply (drule same_inode_files_prop5, drule_tac f' = list1 and f'' = f' in same_inode_files_prop4, simp, simp)
+
+apply (auto simp:same_inode_files_other split:if_splits)
+apply (drule_tac f'' = f' and f' = f and f = fa in same_inode_files_prop4, simp+)
+apply (drule_tac f'' = f' and f' = f and f = list in same_inode_files_prop4, simp+)
+done
+
 lemma has_same_inode_Tainted:
   "\<lbrakk>O_file f \<in> Tainted s; has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> O_file f' \<in> Tainted s"
-apply (induct s arbitrary:f f', simp add:same_inode_in_seeds)
-apply (frule vt_grant_os, frule vd_cons, case_tac a)
-apply (auto split:if_splits option.splits simp:has_same_inode_def dest:iof's_im_in_cim)
-apply (drule_tac obj = "O_file list2" in Tainted_in_current, simp, simp add:is_file_in_current) 
-done
+by (simp add:has_same_inode_def same_inode_files_Tainted)
 
 lemma has_same_inode_tainted:
   "\<lbrakk>O_file f \<in> tainted s; has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> O_file f' \<in> tainted s"
 by (simp add:has_same_inode_Tainted tainted_eq_Tainted)
 
-
+lemma same_inodes_Tainted:
+  "\<lbrakk>f \<in> same_inode_files s f'; valid s\<rbrakk> \<Longrightarrow> (O_file f \<in> Tainted s) = (O_file f' \<in> Tainted s)"
+apply (frule same_inode_files_prop8, frule same_inode_files_prop7)
+apply (auto intro:has_same_inode_Tainted)
+done