--- a/no_shm_selinux/Alive_prop.thy	Tue Dec 31 14:57:13 2013 +0800
+++ b/no_shm_selinux/Alive_prop.thy	Wed Jan 01 23:00:24 2014 +0800
@@ -6,8 +6,7 @@
 
 lemma distinct_queue_msgs:
   "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> distinct (msgs_of_queue s q)"
-apply (induct s)
-apply (simp add:init_msgs_distinct)
+apply (induct s, simp)
 apply (frule vd_cons, frule vt_grant_os, case_tac a)
 apply auto
 apply (case_tac "msgs_of_queue s q", simp+)

--- a/no_shm_selinux/Co2sobj_prop.thy	Tue Dec 31 14:57:13 2013 +0800
+++ b/no_shm_selinux/Co2sobj_prop.thy	Wed Jan 01 23:00:24 2014 +0800
@@ -38,8 +38,7 @@
      else cm2smsg s q' m') "
 apply (frule vd_cons, frule vt_grant_os, rule ext, rule ext)
 apply (auto simp:cm2smsg_def sectxt_of_obj_simps 
-  split:if_splits option.splits dest:not_died_init_msg
-  dest!:current_has_sec')
+  split:if_splits option.splits dest!:current_has_sec')
 done
 
 lemma cm2smsg_recvmsg1:
@@ -77,7 +76,7 @@
   split:if_splits option.splits)
 done
 
-lemmas cm2smsg_simps = cm2smsg_nil_prop cm2smsg_sendmsg cm2smsg_recvmsg1' cm2smsg_recvmsg2'
+lemmas cm2smsg_simps = cm2smsg_sendmsg cm2smsg_recvmsg1' cm2smsg_recvmsg2'
   cm2smsg_removemsgq cm2smsg_other
 
 (*
@@ -97,11 +96,11 @@
 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 (simp add:msgs_of_queue.simps current_msgqs.simps)
 
 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_died_init_msg tl_set_prop1)
+  dest!:current_has_sec' hd_set_prop1 dest:tl_set_prop1)
 done 
 
 lemma current_has_smsg':
@@ -251,8 +250,7 @@
 apply (frule cqm2sms_other, simp+)
 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_died_init_msg) 
+           split:t_object.splits option.splits if_splits)
 done
 
 lemma cq2smsg_createmsgq:
@@ -283,7 +281,8 @@
 
 lemma current_has_smsgq:
   "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sq. cq2smsgq s q = Some sq"
-by (auto simp:cq2smsgq_def split:option.splits dest!:current_has_sec' current_has_sms')
+by (auto simp:cq2smsgq_def split:option.splits 
+  dest!:current_has_sec' current_has_sms' dest:current_has_sec)
 
 lemma current_has_smsgq':
   "\<lbrakk>cq2smsgq s q = None; valid s\<rbrakk> \<Longrightarrow> q \<notin> current_msgqs s"
@@ -311,6 +310,7 @@
 
 lemmas cq2smsgq_simps = cq2smsgq_other cq2smsg_sendmsg cq2smsg_recvmsg cq2smsg_removemsgq
 
+(*
 lemma sm_in_sqsms_init_aux:
   "\<lbrakk>m \<in> set ms; init_cm2smsg q m = Some sm; q \<in> init_msgqs; 
     init_cqm2sms q ms = Some sms\<rbrakk> \<Longrightarrow> sm \<in> set sms"
@@ -321,6 +321,7 @@
   "\<lbrakk>m \<in> set (init_msgs_of_queue q); init_cm2smsg q m = Some sm; q \<in> init_msgqs; 
     init_cqm2sms q (init_msgs_of_queue q) = Some sms\<rbrakk> \<Longrightarrow> sm \<in> set sms"
 by (simp add:sm_in_sqsms_init_aux)
+*)
 
 lemma cqm2sms_prop0:
   "\<lbrakk>m \<in> set ms; cm2smsg s q m = Some sm; cqm2sms s q ms = Some sms\<rbrakk> \<Longrightarrow> sm \<in> set sms"
@@ -334,8 +335,7 @@
 proof (induct s arbitrary:m q qi qsec sms sm)
   case Nil
   thus ?case 
-    by (simp add:cq2smsga_nil_prop cm2smsg_nil_prop init_cq2smsgq_def sm_in_sqsms_init 
-           split:option.splits)
+    by (simp split:option.splits)
 next
   case (Cons e s)
   hence p1:"\<And> m q qi qsec sms sm. \<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s; 

--- a/no_shm_selinux/Current_prop.thy	Tue Dec 31 14:57:13 2013 +0800
+++ b/no_shm_selinux/Current_prop.thy	Wed Jan 01 23:00:24 2014 +0800
@@ -94,6 +94,7 @@
 apply (simp add:file_of_pfd_is_file, simp+)
 done
 
+(*
 lemma tobj_in_init_alive:
   "tobj_in_init obj \<Longrightarrow> init_alive obj"
 by (case_tac obj, auto)
@@ -101,6 +102,7 @@
 lemma tobj_in_alive:
   "tobj_in_init obj \<Longrightarrow> alive [] obj"
 by (case_tac obj, auto simp:is_file_nil)
+*)
 
 end
 

--- a/no_shm_selinux/Delete_prop.thy	Tue Dec 31 14:57:13 2013 +0800
+++ b/no_shm_selinux/Delete_prop.thy	Wed Jan 01 23:00:24 2014 +0800
@@ -112,19 +112,21 @@
 by (case_tac a, auto)
 *)
 
+(*
 lemma not_died_init_msgq:
   "\<lbrakk>\<not> died (O_msgq q) s; q \<in> init_msgqs\<rbrakk> \<Longrightarrow> q \<in> current_msgqs s"
 apply (induct s, simp)
 by (case_tac a, auto)
+*)
 
 lemma current_msg_imp_current_msgq:
   "\<lbrakk>m \<in> set (msgs_of_queue s q); valid s\<rbrakk> \<Longrightarrow> q \<in> current_msgqs s"
-apply (induct s)
-apply (simp add:init_msgs_valid)
+apply (induct s, simp)
 apply (frule vd_cons, drule vt_grant_os)
 apply (case_tac a, auto split:if_splits)
 done
 
+(*
 lemma not_died_init_msg:
   "\<lbrakk>\<not> died (O_msg q m) s; valid s; m \<in> set (init_msgs_of_queue q)\<rbrakk> \<Longrightarrow> m \<in> set (msgs_of_queue s q)"
 apply (induct s, simp)
@@ -132,13 +134,14 @@
 apply (case_tac a, auto dest:current_msg_imp_current_msgq)
 apply (case_tac "msgs_of_queue s q", simp+)
 done
+*)
 
 lemma not_died_imp_alive: (* init_alive obj;  *)
   "\<lbrakk>\<not> died obj s;  valid s; init_alive obj\<rbrakk> \<Longrightarrow> alive s obj"
 apply (case_tac obj)
 apply (auto dest!: not_died_init_file not_died_init_dir not_died_init_proc
-  not_died_init_msg not_died_init_fd1 not_died_init_tcp1 not_died_init_udp1 (* not_died_init_shm *)
-  not_died_init_msgq 
+   not_died_init_fd1 not_died_init_tcp1 not_died_init_udp1 
+  (* not_died_init_shm not_died_init_msg not_died_init_msgq*) 
            intro:is_file_in_current is_dir_in_current is_tcp_in_current is_udp_in_current
   current_msg_imp_current_msgq)
 done

--- a/no_shm_selinux/Enrich.thy	Tue Dec 31 14:57:13 2013 +0800
+++ b/no_shm_selinux/Enrich.thy	Wed Jan 01 23:00:24 2014 +0800
@@ -54,13 +54,13 @@
 
 fun all_msgqs:: "t_state \<Rightarrow> t_msgq set"
 where
-  "all_msgqs [] = init_msgqs"
+  "all_msgqs [] = {}"
 | "all_msgqs (CreateMsgq p q # s) = all_msgqs s \<union> {q}"
 | "all_msgqs (e # s) = all_msgqs s"
 
 fun all_msgs:: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg set"
 where
-  "all_msgs [] q = set (init_msgs_of_queue q)"
+  "all_msgs [] q = {}"
 | "all_msgs (CreateMsgq p q # s) q' = (if q' = q then {} else all_msgs s q')"
 | "all_msgs (SendMsg p q m # s) q' = (if q' = q then all_msgs s q \<union> {m} else all_msgs s q')"
 | "all_msgs (_ # s) q' = all_msgs s q'"
@@ -114,11 +114,6 @@
 apply (case_tac a, auto)
 done
 
-lemma not_all_msgqs_prop2:
-  "p' \<notin> all_msgqs s \<Longrightarrow> p' \<notin> init_msgqs"
-apply (induct s, simp)
-by (case_tac a, auto)
-
 lemma not_all_msgqs_prop3:
   "p' \<notin> all_msgqs s \<Longrightarrow> p' \<notin> current_msgqs s"
 apply (induct s, simp)
@@ -1071,7 +1066,7 @@
       apply (erule_tac x = "E_msg q m" in allE)
       apply (case_tac obj', auto dest:not_all_msgqs_prop3)
       done
-    have "os_grant s' e" using p_in q_in m_not_in
+    have "os_grant s' e" using p_in q_in m_not_in sms_remain os
       by (simp add:SendMsg)
     moreover have "grant s' e" 
     proof-
@@ -1133,9 +1128,6 @@
         apply (case_tac "msgs_of_queue s q", simp)
         apply (simp add:cqm2sms.simps split:option.splits)
         apply (auto simp add:cm2smsg_def split:option.splits if_splits)[1]
-        apply (case_tac "msgs_of_queue s q", simp)
-        apply (simp add:cqm2sms.simps split:option.splits)
-        apply (auto simp add:cm2smsg_def split:option.splits if_splits)[1]
         done
       show ?thesis using p1' p2' p3' grant p1 p2 p3
         by (simp add:RecvMsg)

--- a/no_shm_selinux/Enrich2.thy	Tue Dec 31 14:57:13 2013 +0800
+++ b/no_shm_selinux/Enrich2.thy	Wed Jan 01 23:00:24 2014 +0800
@@ -1,11 +1,10 @@
-theory Enrich
+theory Enrich2
 imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop S2ss_prop S2ss_prop2
  Temp Enrich Proc_fd_of_file_prop
 begin
 
 context tainting_s begin
 
-
 fun enrich_msgq :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msgq \<Rightarrow> t_state"
 where
   "enrich_msgq [] tq dq = []"
@@ -23,7 +22,186 @@
      else RecvMsg p q m # (enrich_msgq s tq dq))"
 | "enrich_msgq (e # s) tq dq = e # (enrich_msgq s tq dq)"
 
+lemma enrich_msgq_duq_in:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> q' \<in> current_msgqs (enrich_msgq s q q')"
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons, case_tac a)
+apply auto
+done
 
+lemma enrich_msgq_duq_sms:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> msgs_of_queue (enrich_msgq s q q') q' = msgs_of_queue s q"
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons, case_tac a)
+apply auto
+done
+
+lemma enrich_msgq_cur_inof:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> inum_of_file (enrich_msgq s q q') f = inum_of_file s f"
+apply (induct s arbitrary:f, simp)
+apply (frule vt_grant_os, frule vd_cons, case_tac a)
+apply (auto split:option.splits)
+done
+
+lemma enrich_msgq_cur_inos:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> inum_of_socket (enrich_msgq s q q') = inum_of_socket s"
+apply (rule ext)
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons, case_tac a)
+apply (auto split:option.splits)
+done
+
+lemma enrich_msgq_cur_inos':
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> inum_of_socket (enrich_msgq s q q') sock = inum_of_socket s sock"
+apply (simp add:enrich_msgq_cur_inos)
+done
+
+lemma enrich_msgq_cur_inums:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> current_inode_nums (enrich_msgq s q q') = current_inode_nums s"
+apply (auto simp:current_inode_nums_def current_file_inums_def 
+  current_sock_inums_def enrich_msgq_cur_inof enrich_msgq_cur_inos)
+done
+
+lemma enrich_msgq_cur_itag:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> itag_of_inum (enrich_msgq s q q') = itag_of_inum s"
+apply (rule ext)
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons, case_tac a)
+apply (auto split:option.splits t_socket_type.splits)
+done
+
+lemma enrich_msgq_cur_tcps:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> is_tcp_sock (enrich_msgq s q q') = is_tcp_sock s"
+apply (rule ext)
+apply (auto simp:is_tcp_sock_def enrich_msgq_cur_itag enrich_msgq_cur_inos
+  split:option.splits t_inode_tag.splits)
+done
+
+lemma enrich_msgq_cur_udps:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> is_udp_sock (enrich_msgq s q q') = is_udp_sock s"
+apply (rule ext)
+apply (auto simp:is_udp_sock_def enrich_msgq_cur_itag enrich_msgq_cur_inos
+  split:option.splits t_inode_tag.splits)
+done
+
+lemma enrich_msgq_cur_msgqs:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> current_msgqs (enrich_msgq s q q') = current_msgqs s \<union> {q'}"
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto)
+done
+
+lemma enrich_msgq_cur_msgs:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> msgs_of_queue (enrich_msgq s q q') =  (msgs_of_queue s) (q' := msgs_of_queue s q)"
+apply (rule ext, simp, rule conjI, rule impI)
+apply (simp add:enrich_msgq_duq_sms)
+apply (rule impI)
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto)
+done
+
+lemma enrich_msgq_cur_procs:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> current_procs (enrich_msgq s q q') = current_procs s"
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto)
+done
+  
+lemma enrich_msgq_cur_files:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> current_files (enrich_msgq s q q') = current_files s"
+apply (auto simp:current_files_def)
+apply (simp add:enrich_msgq_cur_inof)+
+done
+
+lemma enrich_msgq_cur_fds:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> current_proc_fds (enrich_msgq s q q') = current_proc_fds s"
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons, case_tac a)
+apply auto
+done
+
+lemma enrich_msgq_filefd:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> file_of_proc_fd (enrich_msgq s q q') = file_of_proc_fd s"
+apply (rule ext, rule ext)
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons, case_tac a)
+apply auto
+done
+
+lemma enrich_msgq_flagfd:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> flags_of_proc_fd (enrich_msgq s q q') = flags_of_proc_fd s"
+apply (rule ext, rule ext)
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons, case_tac a)
+apply auto
+done
+
+lemma enrich_msgq_proc_fds:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> proc_file_fds (enrich_msgq s q q') = proc_file_fds s"
+apply (auto simp:proc_file_fds_def enrich_msgq_filefd)
+done
+
+lemma enrich_msgq_hungs:
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> files_hung_by_del (enrich_msgq s q q') = files_hung_by_del s"
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons, case_tac a)
+apply (auto simp:files_hung_by_del.simps)
+done
+  
+lemma enrich_msgq_is_file:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> is_file (enrich_msgq s q q') = is_file s"
+apply (rule ext)
+apply (auto simp add:is_file_def enrich_msgq_cur_itag enrich_msgq_cur_inof
+  split:option.splits t_inode_tag.splits)
+done
+
+lemma enrich_msgq_is_dir:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> is_dir (enrich_msgq s q q') = is_dir s"
+apply (rule ext)
+apply (auto simp add:is_dir_def enrich_msgq_cur_itag enrich_msgq_cur_inof
+  split:option.splits t_inode_tag.splits)
+done
+
+lemma enrich_msgq_alive:
+  "\<lbrakk>alive s obj; valid s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s\<rbrakk>
+   \<Longrightarrow> alive (enrich_msgq s q q') obj"
+apply (case_tac obj)
+apply (simp_all add:enrich_msgq_is_file enrich_msgq_is_dir enrich_msgq_cur_msgqs 
+  enrich_msgq_cur_msgs enrich_msgq_cur_procs enrich_msgq_cur_fds
+  enrich_msgq_cur_tcps enrich_msgq_cur_udps)
+apply (rule impI, simp)
+done
+
+lemma enrich_msgq_alive':
+  "\<lbrakk>alive (enrich_msgq s q q') obj; valid s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s\<rbrakk>
+   \<Longrightarrow> alive s obj \<or> obj = O_msgq q' \<or> (\<exists> m. obj = O_msg q' m \<and> alive s (O_msg q m))"
+apply (case_tac obj)
+apply (simp_all add:enrich_msgq_is_file enrich_msgq_is_dir enrich_msgq_cur_msgqs 
+  enrich_msgq_cur_msgs enrich_msgq_cur_procs enrich_msgq_cur_fds
+  enrich_msgq_cur_tcps enrich_msgq_cur_udps)
+apply (auto split:if_splits)
+done
 
 (* enrich s target_proc duplicated_pro *)
 fun enrich_proc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> t_state"
@@ -45,6 +223,11 @@
      if (tp = p) 
      then ReadFile dp fd # ReadFile p fd # (enrich_proc s tp dp)
      else ReadFile p fd # (enrich_proc s tp dp))"
+| "enrich_proc (RecvMsg p q m # s) tp dp = (
+     if (tp = p) 
+     then let dq = new_msgq (enrich_proc s tp dp) in
+          RecvMsg dp dq m # RecvMsg p q m # (enrich_msgq (enrich_proc s tp dp) q dq)
+     else RecvMsg p q m # (enrich_proc s tp dp))"
 (*
 | "enrich_proc (CloseFd p fd # s) tp dp = (
      if (tp = p \<and> fd \<in> proc_file_fds s p)
@@ -1274,6 +1457,8 @@
     by simp
 qed
   
+lemma enrich_proc_s2ss:
+  "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> \<Longrightarrow> s2ss (enrich_proc s p p') = s2ss s"
 
 lemma enrich_proc_valid:
   "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> \<Longrightarrow> valid (enrich_proc s p p')"

--- a/no_shm_selinux/Finite_current.thy	Tue Dec 31 14:57:13 2013 +0800
+++ b/no_shm_selinux/Finite_current.thy	Wed Jan 01 23:00:24 2014 +0800
@@ -94,8 +94,7 @@
 
 lemma maxium_queue:
   "valid s \<Longrightarrow> length (msgs_of_queue s q) \<le> max_queue"
-apply (induct s) 
-apply (simp add:init_msgq_valid)
+apply (induct s, simp) 
 apply (frule vt_grant_os, frule vd_cons, case_tac a, auto)
 done