--- a/Dynamic2static.thy	Thu Jun 06 08:00:20 2013 +0800
+++ b/Dynamic2static.thy	Thu Jun 06 12:38:44 2013 +0800
@@ -112,8 +112,9 @@
 apply (rule notI)
 apply (clarsimp simp:s2ss_def)
 apply (case_tac obj, case_tac [!] obja, case_tac sobj)
-apply (auto split:option.splits if_splits dest!:cp2sproc_pi cq2smsgq_qi ch2sshm_hi cm2smsg_mi)
-
+apply (auto split:option.splits if_splits dest!:cp2sproc_pi cq2smsgq_qi ch2sshm_hi cm2smsg_mi cf2sfile_fi)
+apply (auto simp:cf2sfiles_def same_inode_files_def has_same_inode_prop1' is_file_def is_dir_def
+           split:option.splits t_inode_tag.splits dest!:cf2sfile_fi)
 done
 
 lemma deleted_imp_deletable_s:
@@ -167,16 +168,68 @@
 
 apply (erule exE|erule conjE)+
 
-apply (erule exE, erule conjE)+
+sorry
+
+lemma tainted_s_in_ss:
+  "tainted_s ss sobj \<Longrightarrow> sobj \<in> ss"
+apply (case_tac sobj, simp_all)
+apply (case_tac bool, simp+)
+apply (case_tac bool, simp+)
+apply (case_tac prod1, case_tac prod2, simp)
+thm tainted_s.simps
+oops
+
+lemma set_eq_D:
+  "\<lbrakk>x \<in> S; {x. P x} = S\<rbrakk> \<Longrightarrow> P x"
+by auto
+
+lemma cqm2sms_prop1:
+  "\<lbrakk>cqm2sms s q queue = Some sms; sm \<in> set sms\<rbrakk> \<Longrightarrow> \<exists> m. cm2smsg s q m = Some sm"
+apply (induct queue arbitrary:sms)
+apply (auto split:option.splits)
+done
 
-sorry
+lemma sq_sm_prop:
+  "\<lbrakk>sm \<in> set sms; cq2smsgq s q = Some (qi, qsec, sms); valid s\<rbrakk>
+   \<Longrightarrow> \<exists> m. cm2smsg s q m = Some sm"
+by (auto simp:cq2smsgq_def split: option.splits intro:cqm2sms_prop1)
+
+lemma tainted_s_imp_tainted:
+  "\<lbrakk>tainted_s ss sobj; ss \<in> static\<rbrakk> \<Longrightarrow> \<exists> s obj. valid s \<and> co2sobj s obj = Some sobj \<and> obj \<in> tainted s"
+apply (drule s2d_main)
+apply (erule exE, erule conjE, simp add:s2ss_def)
+apply (rule_tac x = s in exI, simp)
+apply (case_tac sobj, simp_all)
+apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) 
+apply (rule_tac x = obj in exI, simp)
+apply (case_tac obj, (simp split:option.splits if_splits)+)
+
+apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) 
+apply (rule_tac x = obj in exI, simp)
+apply (case_tac obj, (simp split:option.splits if_splits)+)
+
+apply (case_tac prod1, case_tac prod2, simp)
+apply ((erule conjE)+, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) 
+apply (case_tac obj, simp_all split:option.splits if_splits)
+apply (drule_tac sm = "(aa, ba, True)" in sq_sm_prop, simp+, erule exE)
+apply (rule_tac x = "O_msg nat m" in exI)
+apply (simp)
+
+apply (case_tac obj, (simp split:option.splits if_splits)+)
+apply (erule conjE, drule_tac )
 
 
 
-lemma tainted_s_imp_tainted:
-  "\<lbrakk>tainted_s ss sobj; ss \<in> static\<rbrakk> \<Longrightarrow> \<exists> obj s. s2ss s = ss \<and> valid s \<and> co2sobj s obj = Some sobj \<and> obj \<in> tainted s"
+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_same_inode_tainted:
+  "\<lbrakk>has_same_inode s f f'; O_file f' \<in> tainted s\<rbrakk> \<Longrightarrow> O_file f \<in> tainted s"
+by (drule has_inode_tainted_aux, auto simp:has_same_inode_def)
 
 theorem static_sound:
   assumes tbl_s: "taintable_s obj"
@@ -186,19 +239,19 @@
     and sobj: "tainted_s ss sobj" and related: "init_obj_related sobj obj"
     and init_alive: "init_alive obj" by (auto simp:taintable_s_def)
   from static sobj tainted_s_imp_tainted 
-  obtain s obj' where s2ss: "s2ss s = ss" and co2sobj: "co2sobj s obj' = Some sobj"
-    and tainted: "obj' \<in> tainted s" and vs: "valid s" by blast
+  obtain s obj' where co2sobj: "co2sobj s obj' = Some sobj"
+    and tainted': "obj' \<in> tainted s" and vs: "valid s" by blast
   
-  from co2sobj related
-  have eq:"obj = obj'"
-    apply (case_tac obj', case_tac [!] obj, case_tac [!] sobj)
-    apply auto
-    apply (auto split:option.splits if_splits)
-    apply (case_tac a, simp+)
-    apply (simp add:cp2sproc_def split:option.splits if_splits)
-    apply simp
-    sorry
-  with tainted vs init_alive
+  from co2sobj related vs
+  have eq:"obj = obj' \<or> (\<exists> f f'. obj = O_file f \<and> obj' = O_file f' \<and> has_same_inode s f f')"
+    apply (case_tac obj', case_tac [!] obj)
+    apply (auto split:option.splits if_splits dest!:cp2sproc_pi cq2smsgq_qi ch2sshm_hi cm2smsg_mi cf2sfile_fi)
+    apply (auto simp:cf2sfiles_def same_inode_files_def has_same_inode_def is_file_def is_dir_def
+               split:option.splits t_inode_tag.splits dest!:cf2sfile_fi)
+    done
+  with tainted' have tainted: "obj \<in> tainted s"
+    by (auto intro:has_same_inode_tainted)
+  with vs init_alive
   show ?thesis by (auto simp:taintable_def)
 qed
 

--- a/Static.thy	Thu Jun 06 08:00:20 2013 +0800
+++ b/Static.thy	Thu Jun 06 12:38:44 2013 +0800
@@ -653,7 +653,7 @@
   "tainted_s ss (S_proc sp  tag) = (S_proc sp tag  \<in> ss \<and> tag = True)"
 | "tainted_s ss (S_file sfs tag) = (S_file sfs tag \<in> ss \<and> tag = True)"
 | "tainted_s ss (S_msg  (qi, sec, sms)  (mi, secm, tag)) = 
-     (S_msgq (qi, sec, sms) \<in> ss \<and> (mi,sec,tag) \<in> set sms \<and> tag = True)"
+     (S_msgq (qi, sec, sms) \<in> ss \<and> (mi,secm,tag) \<in> set sms \<and> tag = True)"
 | "tainted_s ss _ = False"
 
 (*