--- a/Tainted_prop.thy	Mon Aug 05 12:30:26 2013 +0800
+++ b/Tainted_prop.thy	Tue Aug 27 08:50:53 2013 +0800
@@ -1,5 +1,5 @@
 theory Tainted_prop 
-imports Main Flask Flask_type Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop Current_prop 
+imports Main Flask Flask_type Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop Current_prop Alive_prop
 begin
 
 context tainting begin
@@ -86,27 +86,6 @@
   "\<lbrakk>O_proc p \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
 by (drule Tainted_in_current, simp+)
 
-lemma has_inode_tainted_aux:
-  "O_file f \<in> tainted s \<Longrightarrow> \<forall> f'. has_same_inode s f f' \<longrightarrow> O_file f' \<in> tainted s"
-apply (erule tainted.induct)
-apply (auto intro:tainted.intros simp:has_same_inode_def)
-(*?? need simpset for tainted *)
-
-
-sorry
-
-lemma has_inode_Tainted_aux:
-  "\<lbrakk>O_file f \<in> Tainted s; has_same_inode s f f'\<rbrakk> \<Longrightarrow> O_file f' \<in> Tainted s"
-apply (induct s, auto)
-apply (auto intro:tainted.intros simp:has_same_inode_def)
-(*?? need simpset for tainted *)
-sorry
-
-lemma "\<lbrakk>info_flow_shm s pa pb; info_flow_shm s pb pc; valid s\<rbrakk> \<Longrightarrow> info_flow_shm s pa pc"
-apply (auto simp add:info_flow_shm_def one_flow_shm_def procs_of_shm_prop2)
-apply (erule_tac x = h in allE, simp)
-apply (case_tac "h = ha", simp+)
-sorry
 
 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"
@@ -122,17 +101,16 @@
   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"
-    apply (rule p4, auto simp:info_flow_shm_def one_flow_shm_def ) (* procs_of_shm_prop2 *)    
-    sorry
-  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) *) sorry
+    by (rule p4, auto simp:info_flow_shm_def one_flow_shm_def procs_of_shm_prop2 p5)    
+  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 "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)
+    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)+
@@ -153,9 +131,6 @@
 
 
 
-
-
-
     prefer 7
     apply (simp split:if_splits option.splits)
     apply (rule allI|rule impI|rule conjI)+
@@ -175,47 +150,60 @@
     apply (drule_tac p = "nat1" and p' = p' in p4')
     apply (auto dest:p4'[where p = nat1 and p' = p'])
     
-apply (induct s) (*
+apply (induct s) 
 apply simp defer
 apply (frule vd_cons, frule vt_grant_os, case_tac a)
 apply (auto simp:info_flow_shm_def elim!:disjE)
 sorry *)
   sorry
-next 
-  case (Cons e s)
-  show ?case 
-    sorry
+qed
 qed
 
 lemma tainted_imp_Tainted:
   "obj \<in> tainted s \<Longrightarrow> obj \<in> Tainted s"
-apply (induct rule:tainted.induct)
+apply (induct rule:tainted.induct)  (*
+apply (simp_all add:vd_cons) 
+apply (rule impI)
+
+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 (case_tac e, auto split:option.splits if_splits simp:alive_simps)
 done
 
+lemma Tainted_imp_tainted_aux_remain:
+  "\<lbrakk>obj \<in> Tainted s; valid (e # s); alive (e # s) obj; \<And> obj. obj \<in> Tainted s \<Longrightarrow> obj \<in> tainted s\<rbrakk>
+   \<Longrightarrow> obj \<in> tainted (e # s)"
+by (rule t_remain, auto)
+
 lemma Tainted_imp_tainted:
   "\<lbrakk>obj \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> obj \<in> tainted s"
-proof (induct s arbitrary:obj)
-  case Nil
-  thus ?case by (auto intro:t_init)
-next
-  case (Cons e s)
-  hence p1: "\<And> obj. obj \<in> Tainted s \<Longrightarrow> obj \<in> tainted s"
-    and p2: "obj \<in> Tainted (e # s)" and p3: "valid (e # s)" 
-    and p4: "valid s" and p5: "os_grant s e"
-    by (auto dest:vd_cons intro:vd_cons vt_grant_os)
-  from p1 have p6: ""
-apply (frule vd_cons, frule vt_grant_os, frule valid_Tainted_obj, simp)
-apply (case_tac a)
-apply (auto intro!:t_init t_clone t_execve t_cfile t_read t_write t_link t_trunc t_sendmsg t_recvmsg
-            intro:t_remain
-             split:if_splits option.splits dest:Tainted_in_current)
-pr 25
+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)
+done
+
+lemma tainted_eq_Tainted:
+  "valid s \<Longrightarrow> (obj \<in> tainted s) = (obj \<in> Tainted s)"
+by (rule iffI, auto intro:Tainted_imp_tainted tainted_imp_Tainted)
 
-lemma tainted_imp_Tainted:
-  "obj \<in> tainted s \<Longrightarrow> obj \<in> Tainted s"
+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"
+by (simp only:tainted_eq_Tainted info_flow_shm_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"
+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
+
+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)
 
 
 
@@ -223,7 +211,8 @@
 
 lemma tainted_in_current:
   "obj \<in> tainted s \<Longrightarrow> alive s obj"
-apply (erule tainted.induct, auto dest:vt_grant_os vd_cons simp:is_file_simps)
+apply (erule tainted.induct)
+apply (auto dest:vt_grant_os vd_cons info_shm_flow_in_procs procs_of_shm_prop2 simp:is_file_simps)
 apply (drule seeds_in_init, simp add:tobj_in_alive)
 apply (erule has_same_inode_prop2, simp, simp add:vd_cons)
 apply (frule vt_grant_os, simp)