--- a/Co2sobj_prop.thy	Mon Aug 05 12:30:26 2013 +0800
+++ b/Co2sobj_prop.thy	Tue Aug 27 08:50:53 2013 +0800
@@ -1,28 +1,248 @@
 (*<*)
 theory Co2sobj_prop
-imports Main Flask Flask_type Static Static_type Sectxt_prop Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop
+imports Main Flask Flask_type Static Static_type Sectxt_prop Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop Tainted_prop Valid_prop Init_prop
 begin
 (*<*)
 
+ML {*
+fun print_ss ss =
+let
+val {simps, congs, procs, ...} = Raw_Simplifier.dest_ss ss
+in
+simps
+end
+*}
+
+
 context tainting_s begin
 
 (********************* cm2smsg simpset ***********************)
 
-lemma cm2smsg_other: "\<lbrakk>valid (e # s); \<forall> p q m. e \<noteq> SendMsg p q m\<rbrakk> \<Longrightarrow> cm2smsg (e # s) = cm2smsg s"
+lemma cm2smsg_other: 
+  "\<lbrakk>valid (e # s); \<forall> p q m. e \<noteq> SendMsg p q m; \<forall> p q m. e \<noteq> RecvMsg p q m; \<forall> p q. e \<noteq> RemoveMsgq p q\<rbrakk> 
+   \<Longrightarrow> cm2smsg (e # s) = cm2smsg s"
 apply (frule vt_grant_os, frule vd_cons, rule ext, rule ext)
+unfolding cm2smsg_def
 apply (case_tac e)
-apply (auto simp:cm2smsg_def sectxt_of_obj_simps split:option.splits if_splits
-intro:tainted.intro
+apply (auto simp:sectxt_of_obj_simps tainted_eq_Tainted 
+           split:t_object.splits option.splits if_splits 
+            dest:not_deleted_init_msg  dest!:current_has_sec')
+done
+
+lemma cm2smsg_sendmsg:
+  "valid (SendMsg p q m # s) \<Longrightarrow> cm2smsg (SendMsg p q m # s) = (\<lambda> q' m'. 
+     if (q' = q \<and> m' = m)
+     then (case (sectxt_of_obj (SendMsg p q m # s) (O_msg q m)) of
+             Some sec \<Rightarrow> Some (Created, sec, O_msg q m \<in> tainted (SendMsg p q m # s))
+           | _ \<Rightarrow> None)
+     else cm2smsg s q' m') "
+apply (frule vd_cons, frule vt_grant_os, rule ext, rule ext)
+apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps 
+  split:if_splits option.splits
+  dest:not_deleted_init_msg  dest!:current_has_sec')
+done
+
+lemma cm2smsg_recvmsg1:
+  "\<lbrakk>q' \<noteq> q; valid (RecvMsg p q m # s)\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q' = cm2smsg s q'"
+apply (frule vd_cons, frule vt_grant_os, rule ext)
+apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps 
+  split:if_splits option.splits)
+done
+
+lemma cm2smsg_recvmsg2:
+  "\<lbrakk>m' \<noteq> m; valid (RecvMsg p q m # s)\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q m' = cm2smsg s q m'"
+apply (frule vd_cons, frule vt_grant_os)
+apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps 
+  split:if_splits option.splits)
+done
+
+lemma cm2smsg_recvmsg1':
+  "\<lbrakk>valid (RecvMsg p q m # s); q' \<noteq> q\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q' = cm2smsg s q'"
+apply (frule vd_cons, frule vt_grant_os, rule ext)
+apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps 
+  split:if_splits option.splits)
+done
+
+lemma cm2smsg_recvmsg2':
+  "\<lbrakk>valid (RecvMsg p q m # s); m' \<noteq> m\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q m' = cm2smsg s q m'"
+apply (frule vd_cons, frule vt_grant_os)
+apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps 
+  split:if_splits option.splits)
+done
+
+lemma cm2smsg_removemsgq:
+  "\<lbrakk>q' \<noteq> q; valid (RemoveMsgq p q # s)\<rbrakk> \<Longrightarrow> cm2smsg (RemoveMsgq p q # s) q' = cm2smsg s q'"
+apply (frule vd_cons, frule vt_grant_os, rule ext)
+apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps 
+  split:if_splits option.splits)
+done
+
+lemmas cm2smsg_simps = cm2smsg_nil_prop cm2smsg_sendmsg cm2smsg_recvmsg1' cm2smsg_recvmsg2'
+  cm2smsg_removemsgq cm2smsg_other
+
+lemma init_cm2smsg_has_smsg:
+  "\<lbrakk>m \<in> set (init_msgs_of_queue q); q \<in> init_msgqs\<rbrakk> \<Longrightarrow> \<exists> sm. init_cm2smsg q m = Some sm"
+by (auto simp:init_cm2smsg_def split:option.splits dest:init_msg_has_ctxt)
+
+lemma hd_set_prop1:
+  "hd l \<notin> set l \<Longrightarrow> l = []"
+by (case_tac l, auto)
+
+lemma tl_set_prop1:
+  "a \<in> set (tl l) \<Longrightarrow> a \<in> set l"
+by (case_tac l, auto)
+
+lemma current_has_smsg:
+  "\<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sm. cm2smsg s q m = Some sm"
+apply (induct s)
+apply (simp only:cm2smsg_nil_prop msgs_of_queue.simps current_msgqs.simps init_cm2smsg_has_smsg)
+
+apply (frule vt_grant_os, frule vd_cons, case_tac a)
+apply (auto simp:cm2smsg_def sectxt_of_obj_simps split:if_splits option.splits
+  dest!:current_has_sec' hd_set_prop1 dest:not_deleted_init_msg tl_set_prop1)
+done 
+
+lemma current_has_smsg':
+  "\<lbrakk>cm2smsg s q m = None; q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> m \<notin> set (msgs_of_queue s q)"
+by (auto dest:current_has_smsg)
+
+lemma cqm2sms_has_sms_aux:
+  "\<forall> m \<in> set ms. sectxt_of_obj s (O_msg q m) \<noteq> None \<Longrightarrow> (\<exists> sms. cqm2sms s q ms = Some sms)"
+by (induct ms, auto split:option.splits simp:cm2smsg_def)
+
+lemma current_has_sms:
+  "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sms. cqm2sms s q (msgs_of_queue s q) = Some sms"
+apply (rule cqm2sms_has_sms_aux)
+apply (auto dest:current_msg_has_sec)
+done
+
+lemma current_has_sms':
+  "\<lbrakk>cqm2sms s q (msgs_of_queue s q) = None; valid s\<rbrakk> \<Longrightarrow> q \<notin> current_msgqs s"
+by (auto dest:current_has_sms)
+
+(********************* cqm2sms simpset ***********************) 
+
+lemma cqm2sms_other:
+  "\<lbrakk>valid (e # s); \<forall> p m. e \<noteq> CreateMsgq p q; \<forall> p q m. e \<noteq> SendMsg p q m; 
+    \<forall> p q m. e \<noteq> RecvMsg p q m; \<forall> p q. e \<noteq> RemoveMsgq p q\<rbrakk> 
+   \<Longrightarrow> cqm2sms (e # s) = cqm2sms s"
+apply (rule ext, rule ext)
+apply (induct_tac xa, simp)
+apply (frule vt_grant_os, frule vd_cons, case_tac e)
+apply (auto split:option.splits dest:cm2smsg_other) 
+done
 
-lemmas cm2smsg_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other
+lemma cqm2sms_createmsgq:
+  "valid (CreateMsgq p q # s) \<Longrightarrow> cqm2sms (CreateMsgq p q # s) = (\<lambda> q' ms'. 
+     if (q' = q \<and> ms' = []) then Some []
+     else cqm2sms s q' ms')"
+apply (rule ext, rule ext)
+apply (frule vt_grant_os, frule vd_cons, induct_tac ms')
+apply (auto split:if_splits option.splits dest:cm2smsg_other)
+done
+
+lemma cqm2sms_2:
+  "cqm2sms s q (ms @ [m]) = 
+     (case (cqm2sms s q ms, cm2smsg s q m) of 
+       (Some sms, Some sm) \<Rightarrow> Some (sms @ [sm]) 
+     | _ \<Rightarrow> None)"
+apply (induct ms, simp split:option.splits)
+by (auto split:option.splits)
+
+lemmas cqm2sms_simps2 = cqm2sms.simps(1) cqm2sms_2
+
+declare cqm2sms.simps [simp del]
+
+lemma cqm2sms_prop1:
+  "cqm2sms s q ms = None \<Longrightarrow> \<exists> m \<in> set ms. cm2smsg s q m = None"
+by (induct ms, auto simp:cqm2sms.simps split:option.splits)
+
+lemma cqm2sms_sendmsg1:
+  "\<lbrakk>valid (SendMsg p q m # s); m \<notin> set ms\<rbrakk>
+   \<Longrightarrow> cqm2sms (SendMsg p q m # s) q' ms = cqm2sms s q' ms"
+apply (frule vt_grant_os, frule vd_cons)
+apply (frule cm2smsg_sendmsg)
+apply (induct ms rule:rev_induct)
+apply (auto split:if_splits option.splits  simp:cqm2sms_simps2)
+done
+
+lemma cqm2sms_sendmsg2:
+  "\<lbrakk>valid (SendMsg p q m # s); q' \<noteq> q\<rbrakk>
+   \<Longrightarrow> cqm2sms (SendMsg p q m # s) q' ms = cqm2sms s q' ms"
+apply (frule vt_grant_os, frule vd_cons)
+apply (frule cm2smsg_sendmsg)
+apply (induct ms rule:rev_induct)
+apply (auto split:if_splits option.splits  simp:cqm2sms_simps2)
+done
+
+lemma cqm2sms_sendmsg3:
+  "\<lbrakk>valid (SendMsg p q m # s); ms' = msgs_of_queue (SendMsg p q m # s) q\<rbrakk>
+   \<Longrightarrow> cqm2sms (SendMsg p q m # s) q ms' = 
+     (case (cqm2sms s q (msgs_of_queue s q), sectxt_of_obj (SendMsg p q m # s) (O_msg q m)) of
+       (Some sms, Some sec) \<Rightarrow> Some (sms @ [(Created, sec, O_msg q m \<in> tainted (SendMsg p q m # s))])
+     | _ \<Rightarrow> None)"
+apply (frule vt_grant_os, frule vd_cons)
+apply (frule cm2smsg_sendmsg)
+apply (auto split:if_splits option.splits  simp:cqm2sms_simps2 cqm2sms_sendmsg1)
+done
+
+lemma cqm2sms_sendmsg:
+  "\<lbrakk>valid (SendMsg p q m # s); ms' = msgs_of_queue (SendMsg p q m # s) q'\<rbrakk> 
+   \<Longrightarrow> cqm2sms (SendMsg p q m # s) q' ms' = (
+     if (q' = q) 
+     then (case (cqm2sms s q (msgs_of_queue s q), sectxt_of_obj (SendMsg p q m # s) (O_msg q m)) of
+             (Some sms, Some sec) \<Rightarrow> Some (sms @ [(Created, sec, O_msg q m \<in> tainted (SendMsg p q m # s))])
+           | _ \<Rightarrow> None)
+     else cqm2sms s q' ms' )"
+apply (simp split:if_splits add:cqm2sms_sendmsg2 cqm2sms_sendmsg3)
+done
+
+lemma cqm2sms_recvmsg1:
+  "\<lbrakk>valid (RecvMsg p q m # s); m \<notin> set ms\<rbrakk> 
+   \<Longrightarrow> cqm2sms (RecvMsg p q m # s) q ms = cqm2sms s q ms"
+apply (frule vt_grant_os, frule vd_cons)
+apply (induct ms rule:rev_induct)
+apply (auto split:if_splits option.splits simp:cqm2sms_simps2 cm2smsg_recvmsg2')
+done
+
+lemma cqm2sms_recvmsg2:
+  "\<lbrakk>valid (RecvMsg p q m # s); q' \<noteq> q\<rbrakk>
+   \<Longrightarrow> cqm2sms (RecvMsg p q m # s) q' ms = cqm2sms s q' ms"
+apply (frule vt_grant_os, frule vd_cons)
+apply (induct ms rule:rev_induct)
+apply (auto split:if_splits option.splits simp:cqm2sms_simps2 cm2smsg_recvmsg1')
+done
+
+lemma cqm2sms_recvmsg:
+  "\<lbrakk>valid (RecvMsg p q m # s); ms = msgs_of_queue (RecvMsg p q m # s) q'\<rbrakk>
+   \<Longrightarrow> cqm2sms (RecvMsg p q m # s) q' ms = (
+     if (q' = q) 
+     then (case (cqm2sms s q (msgs_of_queue s q)) of
+             Some sms \<Rightarrow> Some (tl sms)
+           | _ \<Rightarrow> None)
+     else cqm2sms s q' ms)"
+apply (frule vt_grant_os, frule vd_cons)
+apply (auto split:if_splits option.splits simp:cqm2sms_recvmsg1 cqm2sms_recvmsg2)
+using cm2smsg_recvmsg1 cm2smsg_recvmsg2
+apply (auto split:if_splits option.splits)
+
+  
+lemmas cqm2sms_simps = cqm2sms_other cqm2sms_createmsgq cqm2sms_sendmsg cqm2sms_recvmsg
+
+(********************* cq2smsgq simpset ***********************) 
+ 
+lemma cq2smsgq_other: 
+  "\<lbrakk>valid (e # s); \<forall> p m. e \<noteq> CreateMsgq p q; \<forall> p q m. e \<noteq> SendMsg p q m; 
+    \<forall> p q m. e \<noteq> RecvMsg p q m; \<forall> p q. e \<noteq> RemoveMsgq p q\<rbrakk> 
+   \<Longrightarrow> cq2smsgq (e # s) = cq2smsgq s" 
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac e) 
+apply (auto simp:cq2smsgq_def sectxt_of_obj_simps 
+           split:t_object.splits option.splits if_splits 
+            dest:not_deleted_init_msg  dest!:current_has_sec') 
 
 
-
-(********************* cq2smsgq simpset ***********************) 
+  
 
-lemma cq2smsgq_other: "\<forall> p m. e \<noteq> CreateMsg p m \<Longrightarrow> cm2smsg (e # \<tau>) m' = cm2smsg \<tau> m'" 
-apply (case_tac e) 
-by (auto simp:cm2smsg_def index_of_msg.simps d2s_aux.simps) 
 
 lemmas cq2smsgq_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other 
 

--- a/Dynamic2static.thy	Mon Aug 05 12:30:26 2013 +0800
+++ b/Dynamic2static.thy	Tue Aug 27 08:50:53 2013 +0800
@@ -13,6 +13,9 @@
 apply 
 induct s, case tac e, every event analysis
 *)
+thm s2ss_def
+
+
 sorry
 
 lemma d2s_main':

--- a/Flask.thy	Mon Aug 05 12:30:26 2013 +0800
+++ b/Flask.thy	Tue Aug 27 08:50:53 2013 +0800
@@ -705,7 +705,7 @@
 | "os_grant \<tau> (SendMsg p q m)                 = 
     (p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau> \<and> m \<notin> (set (msgs_of_queue \<tau> q)))"
 | "os_grant \<tau> (RecvMsg p q m)                 = 
-    (p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau> \<and> m = hd (msgs_of_queue \<tau> q))"
+    (p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau> \<and> m = hd (msgs_of_queue \<tau> q) \<and> msgs_of_queue \<tau> q \<noteq> [])"
 | "os_grant \<tau> (RemoveMsgq p q)                = 
     (p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau>)"
 | "os_grant \<tau> (CreateShM p h)                 = 
@@ -1475,7 +1475,7 @@
 | t_attach1:"\<lbrakk>O_proc p \<in> tainted s; valid (Attach p h SHM_RDWR # s); (p', flag') \<in> procs_of_shm s h\<rbrakk>
              \<Longrightarrow> O_proc p' \<in> tainted (Attach p h SHM_RDWR # s)"
 | t_attach2:"\<lbrakk>O_proc p' \<in> tainted s; valid (Attach p h flag # s); (p', SHM_RDWR) \<in> procs_of_shm s h\<rbrakk>
-             \<Longrightarrow> O_proc p \<in> tainted (Attach p h SHM_RDWR # s)"
+             \<Longrightarrow> O_proc p \<in> tainted (Attach p h flag # s)"
 | t_sendmsg:"\<lbrakk>O_proc p \<in> tainted s; valid (SendMsg p q m # s)\<rbrakk>
              \<Longrightarrow> O_msg q m \<in> tainted (SendMsg p q m # s)"
 | t_recvmsg:"\<lbrakk>O_msg q m \<in> tainted s; valid (RecvMsg p q m # s); info_flow_shm s p p'\<rbrakk>

--- a/Sectxt_prop.thy	Mon Aug 05 12:30:26 2013 +0800
+++ b/Sectxt_prop.thy	Tue Aug 27 08:50:53 2013 +0800
@@ -600,8 +600,92 @@
            dest!:current_has_type' current_proc_has_role' current_has_user')
 done
 
+lemma sec_kill: 
+  "valid (Kill p p' # s) \<Longrightarrow> sectxt_of_obj (Kill p p' # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_ptrace:
+  "valid (Ptrace p p' # s) \<Longrightarrow> sectxt_of_obj (Ptrace p p' # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_exit:
+  "valid (Exit p # s) \<Longrightarrow> sectxt_of_obj (Exit p # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_readfile:
+  "valid (ReadFile p fd # s) \<Longrightarrow> sectxt_of_obj (ReadFile p fd # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_writefile:
+  "valid (WriteFile p fd # s) \<Longrightarrow> sectxt_of_obj (WriteFile p fd # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_closefd:
+  "valid (CloseFd p fd # s) \<Longrightarrow> sectxt_of_obj (CloseFd p fd # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_unlink:
+  "valid (UnLink p f # s) \<Longrightarrow> sectxt_of_obj (UnLink p f # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_Rmdir:
+  "valid (Rmdir p f # s) \<Longrightarrow> sectxt_of_obj (Rmdir p f # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_truncate:
+  "valid (Truncate p f len # s) \<Longrightarrow> sectxt_of_obj (Truncate p f len # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_recvmsg:
+  "valid (RecvMsg p q m # s) \<Longrightarrow> sectxt_of_obj (RecvMsg p q m # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_removemsgq:
+  "valid (RemoveMsgq p q # s) \<Longrightarrow> sectxt_of_obj (RemoveMsgq p q # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_attach:
+  "valid (Attach p h flag # s) \<Longrightarrow> sectxt_of_obj (Attach p h flag # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_detach:
+  "valid (Detach p h # s) \<Longrightarrow> sectxt_of_obj (Detach p h # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_deleteshm:
+  "valid (DeleteShM p h # s) \<Longrightarrow> sectxt_of_obj (DeleteShM p h # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_bind:
+  "valid (Bind p fd addr # s) \<Longrightarrow> sectxt_of_obj (Bind p fd addr # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_connect:
+  "valid (Connect p fd addr # s) \<Longrightarrow> sectxt_of_obj (Connect p fd addr # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_listen:
+  "valid (Listen p fd # s) \<Longrightarrow> sectxt_of_obj (Listen p fd # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_sendsock:
+  "valid (SendSock p fd # s) \<Longrightarrow> sectxt_of_obj (SendSock p fd # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_recvsock:
+  "valid (RecvSock p fd # s) \<Longrightarrow> sectxt_of_obj (RecvSock p fd # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_shutdown:
+  "valid (Shutdown p fd how # s) \<Longrightarrow> sectxt_of_obj (Shutdown p fd how # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
 lemmas sectxt_of_obj_simps = sec_execve sec_open sec_mkdir sec_linkhard sec_createmsgq sec_sendmsg
-  sec_createshm sec_createsock sec_accept sec_clone sec_others (* init_sectxt_prop *)
+  sec_createshm sec_createsock sec_accept sec_clone sec_kill sec_ptrace sec_exit sec_readfile
+  sec_writefile sec_closefd sec_unlink sec_Rmdir sec_truncate sec_recvmsg sec_removemsgq
+  sec_attach sec_detach sec_deleteshm sec_bind sec_connect sec_listen sec_sendsock
+  sec_recvsock sec_shutdown
+(* init_sectxt_prop *)
 
 (**************** get_parentfs_ctxts simpset **************)
 

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