--- a/S2ss_prop.thy	Mon Sep 02 11:12:42 2013 +0800
+++ b/S2ss_prop.thy	Tue Sep 03 07:25:39 2013 +0800
@@ -365,10 +365,84 @@
 apply (simp add:is_dir_in_current)
 done
 
-lemma co2sobj_
+lemma co2sobj_clone:
+  "\<lbrakk>valid (Clone p p' fds shms # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Clone p p' fds shms # s) obj = (
+      if (obj = O_proc p')
+      then (case (cp2sproc (Clone p p' fds shms # s) p') of
+              Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))
+            | _       \<Rightarrow> None)
+      else co2sobj s obj )"
+apply (frule vt_grant_os, frule vd_cons, case_tac obj)
+apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (case_tac "cp2sproc (Clone p p' fds shms # s) p'")
+apply (drule current_proc_has_sp', simp, simp)
+apply ((erule conjE)+, frule_tac p = p in current_proc_has_sec, simp, erule exE, simp)
+apply (rule conjI, rule impI, simp)
+apply (simp (no_asm_simp) add:cp2sproc_clone tainted_eq_Tainted split:option.splits)
+
+apply (rule impI, simp add:cf2sfiles_other) 
+apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp)
+apply (frule_tac ff = list in cf2sfile_other', simp_all)
+apply (simp add:is_dir_in_current)
+done
+
+lemma co2sobj_ptrace:
+  "\<lbrakk>valid (Ptrace p p' # s); alive s obj\<rbrakk>\<Longrightarrow> co2sobj (Ptrace p p' # s) obj = (
+     case obj of
+       O_proc p'' \<Rightarrow> if (info_flow_shm s p' p'') 
+                     then (case (cp2sproc s p'') of 
+                             Some sp \<Rightarrow> Some (S_proc sp (O_proc p'' \<in> Tainted s \<or> O_proc p \<in> Tainted s))
+                           | _       \<Rightarrow> None)
+                     else if (info_flow_shm s p p'')
+                          then (case (cp2sproc s p'') of 
+                                  Some sp \<Rightarrow> Some (S_proc sp (O_proc p'' \<in> Tainted s \<or> O_proc p' \<in> Tainted s))
+                                | _       \<Rightarrow> None)
+                          else co2sobj s (O_proc p'')
+    | _          \<Rightarrow> co2sobj s obj)"
+apply (frule vt_grant_os, frule vd_cons, case_tac obj)
+apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other cf2sfiles_other tainted_eq_Tainted)
+apply (auto simp:cp2sproc_other tainted_eq_Tainted split:option.splits
+  dest!:current_proc_has_sec' current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
 
+apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp)
+apply (frule_tac ff = list in cf2sfile_other', simp_all)
+apply (simp add:is_dir_in_current)
+done
 
-end
+lemma co2sobj_open:
+  "\<lbrakk>valid (Open p f flag fd opt # s); alive (Open p f flag fd opt # s) obj\<rbrakk> 
+   \<Longrightarrow> co2sobj (Open p f flag fd opt # s) obj = (case obj of 
+     O_file f' \<Rightarrow> if (f' = f \<and> opt \<noteq> None)
+                  then (case (cf2sfile (Open p f flag fd opt # s) f) of
+                          Some sf \<Rightarrow> Some (S_file {sf} (O_proc p \<in> Tainted s))
+                        | _       \<Rightarrow> None)
+                  else co2sobj s (O_file f')
+   | O_proc p' \<Rightarrow> if (p' = p) 
+                  then (case (cp2sproc (Open p f flag fd opt # s) p) of
+                          Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))
+                        | _       \<Rightarrow> None)
+                  else co2sobj s (O_proc p')
+   | _         \<Rightarrow> co2sobj s obj )"
+apply (frule vt_grant_os, frule vd_cons, case_tac obj)
+apply (auto simp:cp2sproc_simps cf2sfiles_simps cf2sfile_simps current_files_simps 
+is_file_simps tainted_eq_Tainted split:option.splits
+           dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)
+apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (auto simp:cp2sproc_simps cf2sfiles_simps cf2sfile_simps current_files_simps 
+is_file_simps tainted_eq_Tainted split:option.splits
+           dest!:current_proc_has_sp' current_file_has_sfile' intro:info_flow_shm_Tainted)
+apply (
+apply 
+
+lemma co2sobj_other:
+  "\<lbrakk>valid (e # s); alive (e # s) obj; 
+    \<forall> p f fds. e \<noteq> Execve p f fds;
+    \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;
+    \<forall> p p'. e \<noteq> Ptrace p p';
+    \<forall> 
+   \<rbrakk> \<Longrightarrow> co2sobj (e # s) obj = co2sobj s obj"
+
+lemmas co2sobj_simps = co2sobj_execve co2sobj_clone co2sobj_ptrace
 
 (* simpset for s2ss*)
 

--- a/Static.thy	Mon Sep 02 11:12:42 2013 +0800
+++ b/Static.thy	Tue Sep 03 07:25:39 2013 +0800
@@ -99,16 +99,12 @@
        Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> seeds))
      | _ \<Rightarrow> None)"
 | "init_obj2sobj (O_file f) = 
-     (if (f \<in> init_files \<and> is_init_file f) 
-      then Some (S_file (init_cf2sfiles f) 
-                        (\<exists> f'. f' \<in> (init_same_inode_files f) \<and> O_file f \<in> seeds))
-      else None)"
-| "init_obj2sobj (O_dir f) = 
-     (if (is_init_dir f) then 
-        (case (init_cf2sfile f) of
-           Some sf \<Rightarrow> Some (S_dir sf) 
-         | _ \<Rightarrow> None)
-      else None)"
+     Some (S_file (init_cf2sfiles f) 
+                  (\<exists> f'. f' \<in> (init_same_inode_files f) \<and> O_file f \<in> seeds))"
+| "init_obj2sobj (O_dir f) =
+     (case (init_cf2sfile f) of
+        Some sf \<Rightarrow> Some (S_dir sf) 
+      | _ \<Rightarrow> None)"
 | "init_obj2sobj (O_msgq q) = 
      (case (init_cq2smsgq q) of
        Some sq \<Rightarrow> Some (S_msgq sq)
@@ -773,9 +769,7 @@
         Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
       | _       \<Rightarrow> None)"
 | "co2sobj s (O_file f) = 
-     (if (f \<in> current_files s) then 
-        Some (S_file (cf2sfiles s f) (O_file f \<in> tainted s))
-      else None)"
+     Some (S_file (cf2sfiles s f) (O_file f \<in> tainted s))"
 | "co2sobj s (O_dir f) = 
      (case (cf2sfile s f) of
         Some sf  \<Rightarrow> Some (S_dir sf)