--- 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*)