# HG changeset patch
# User chunhan
# Date 1388473033 -28800
# Node ID 8d18cfc845ddf946b7f8d3ebb190db8b346d413d
# Parent  690636b7b6f1f82212a90ba1a17f4a53a0c9048b
remove init message queue

diff -r 690636b7b6f1 -r 8d18cfc845dd no_shm_selinux/Co2sobj_prop.thy
--- a/no_shm_selinux/Co2sobj_prop.thy	Mon Dec 30 23:41:58 2013 +0800
+++ b/no_shm_selinux/Co2sobj_prop.thy	Tue Dec 31 14:57:13 2013 +0800
@@ -80,9 +80,11 @@
 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 = []"
@@ -262,7 +264,7 @@
 apply (frule vd_cons, frule vt_grant_os)
 apply (frule cqm2sms_createmsgq)
 apply (rule ext, auto simp:cq2smsgq_def sec_createmsgq 
-  split:option.splits if_splits dest:not_died_init_msgq)
+  split:option.splits if_splits)
 done
 
 lemma cq2smsg_sendmsg:
diff -r 690636b7b6f1 -r 8d18cfc845dd no_shm_selinux/Enrich.thy
--- a/no_shm_selinux/Enrich.thy	Mon Dec 30 23:41:58 2013 +0800
+++ b/no_shm_selinux/Enrich.thy	Tue Dec 31 14:57:13 2013 +0800
@@ -141,77 +141,6 @@
 apply (simp add:parentf_is_dir_prop2)
 done
 
-(* enrich s target_proc duplicated_pro *)
-fun enrich_proc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> t_state"
-where 
-  "enrich_proc [] tp dp = []"
-| "enrich_proc (Execve p f fds # s) tp dp = (
-     if (tp = p) 
-     then Execve dp f (fds \<inter> proc_file_fds s p) # Execve p f fds # (enrich_proc s tp dp)
-     else Execve p f fds # (enrich_proc s tp dp))"
-| "enrich_proc (Clone p p' fds # s) tp dp = (
-     if (tp = p') 
-     then Clone p dp (fds \<inter> proc_file_fds s p) # Clone p p' fds # s
-     else Clone p p' fds # (enrich_proc s tp dp))"
-| "enrich_proc (Open p f flags fd opt # s) tp dp = (
-     if (tp = p)
-     then Open dp f (remove_create_flag flags) fd None # Open p f flags fd opt # (enrich_proc s tp dp)
-     else Open p f flags fd opt # (enrich_proc s tp dp))"
-| "enrich_proc (ReadFile p fd # s) tp dp = (
-     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 (CloseFd p fd # s) tp dp = (
-     if (tp = p \<and> fd \<in> proc_file_fds s p)
-     then CloseFd dp fd # CloseFd p fd # (enrich_proc s tp dp)
-     else CloseFd p fd # (enrich_proc s tp dp))"
-*)
-(*
-| "enrich_proc (Attach p h flag # s) tp dp = (
-     if (tp = p)
-     then Attach dp h flag # Attach p h flag # (enrich_proc s tp dp)
-     else Attach p h flag # (enrich_proc s tp dp))"
-| "enrich_proc (Detach p h # s) tp dp = (
-     if (tp = p) 
-     then Detach dp h # Detach p h # (enrich_proc s tp dp)
-     else Detach p h # (enrich_proc s tp dp))"
-*)
-(*
-| "enrich_proc (Kill p p' # s) tp dp = (
-     if (tp = p') then Kill p p' # s
-     else Kill p p' # (enrich_proc s tp dp))"
-| "enrich_proc (Exit p # s) tp dp = (
-     if (tp = p) then Exit p # s
-     else Exit p # (enrich_proc s tp dp))"
-*)
-| "enrich_proc (e # s) tp dp = e # (enrich_proc s tp dp)"
-
-definition is_created_proc:: "t_state \<Rightarrow> t_process \<Rightarrow> bool"
-where
-  "is_created_proc s p \<equiv> p \<in> current_procs s \<and> (p \<in> init_procs \<longrightarrow> died (O_proc p) s)"
-
-definition is_created_proc':: "t_state \<Rightarrow> t_process \<Rightarrow> bool"
-where
-  "is_created_proc' s p \<equiv> p \<in> current_procs s \<and> p \<notin> init_procs"
-
-lemma no_del_died:
-  "\<lbrakk>no_del_event s; died obj s\<rbrakk> \<Longrightarrow> (\<exists> p fd. obj = O_fd p fd \<or> obj = O_tcp_sock (p, fd) \<or> obj = O_udp_sock (p, fd))
-  \<or> (\<exists> q m. obj = O_msg q m) "
-apply (induct s)
-apply simp
-apply (case_tac a)
-apply (auto split:option.splits)
-done
-
-lemma no_del_created_eq:
-  "no_del_event s \<Longrightarrow> is_created_proc s p = is_created_proc' s p"
-apply (induct s)
-apply (simp add:is_created_proc_def is_created_proc'_def)
-apply (case_tac a)
-apply (auto simp add:is_created_proc_def is_created_proc'_def dest:no_del_died)
-done
-
 lemma enrich_search_check:
   assumes grant: "search_check s (up, rp, tp) f"
   and cf2sf: "\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile s' f = cf2sfile s f"
@@ -1248,74 +1177,44 @@
   qed 
 qed
 
-lemma created_proc_clone:
-  "valid (Clone p p' fds # s) \<Longrightarrow> 
-   is_created_proc (Clone p p' fds # s) tp = (if (tp = p') then True else is_created_proc s tp)"
-apply (drule vt_grant_os)
-apply (auto simp:is_created_proc_def dest:not_all_procs_prop2)
-using not_died_init_proc
-by auto
-
-lemma created_proc_exit: 
-  "is_created_proc (Exit p # s) tp = (if (tp = p) then False else is_created_proc s tp)"
-by (simp add:is_created_proc_def)
-
-lemma created_proc_kill:
-  "is_created_proc (Kill p p' # s) tp = (if (tp = p') then False else is_created_proc s tp)"
-by (simp add:is_created_proc_def)
+lemma current_proc_fds_in_curp:
+  "\<lbrakk>fd \<in> current_proc_fds s p; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
+apply (induct s)
+apply (simp add:init_fds_of_proc_prop1)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto split:if_splits option.splits)
+done
 
-lemma created_proc_other:
-  "\<lbrakk>\<And> p p' fds. e \<noteq> Clone p p' fds;
-    \<And> p. e \<noteq> Exit p;
-    \<And> p p'. e \<noteq> Kill p p'\<rbrakk> \<Longrightarrow> is_created_proc (e # s) tp = is_created_proc s tp"
-by (case_tac e, auto simp:is_created_proc_def)
-
-lemmas is_created_proc_simps = created_proc_clone created_proc_exit created_proc_kill created_proc_other
-(*
-
-
-
-
-       (p \<in> current_procs s \<longrightarrow> co2sobj (enrich_proc s p p') (O_proc p') = co2sobj (enrich_proc s p p') (O_proc p)) \<and>
-       (\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p')  obj) \<and> 
-       (\<forall> p'. p' \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') p' = cp2sproc s p) \<and>
-       (\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f) \<and>
-       (Tainted (enrich_proc s p p') = (Tainted s \<union> (if (O_proc p \<in> Tainted s) then {O_proc p'} else {})))"*)
-
-lemma enrich_proc_dup_in:
-  "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
-   \<Longrightarrow> p' \<in> current_procs (enrich_proc s p p')"
-apply (induct s, simp add:is_created_proc_def)
-apply (frule vt_grant_os, frule vd_cons)
-apply (case_tac a, auto simp:is_created_proc_def dest:not_all_procs_prop3)
+lemma get_parentfs_ctxts_prop:
+  "\<lbrakk>get_parentfs_ctxts s (a # f) = Some ctxts; sectxt_of_obj s (O_dir f) = Some ctxt; valid s\<rbrakk>
+   \<Longrightarrow> ctxt \<in> set (ctxts)"
+apply (induct f)
+apply (auto split:option.splits)
 done
 
-lemma enrich_proc_dup_ffd:
-  "\<lbrakk>file_of_proc_fd s p fd = Some f; is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
-   \<Longrightarrow> file_of_proc_fd (enrich_proc s p p') p' fd = Some f"
-apply (induct s, simp add:is_created_proc_def)
-apply (frule vt_grant_os, frule vd_cons)
-apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def
-  dest:not_all_procs_prop3 split:if_splits option.splits)
-done 
+lemma search_check_allp_intro:
+  "\<lbrakk>search_check s sp pf; get_parentfs_ctxts s pf = Some ctxts; valid s; is_dir s pf\<rbrakk>
+   \<Longrightarrow> search_check_allp sp (set ctxts)"
+apply (case_tac pf)
+apply (simp split:option.splits if_splits add:search_check_allp_def)
+apply (rule ballI)
+apply (auto simp:search_check_ctxt_def search_check_dir_def split:if_splits option.splits)
+apply (auto simp:search_check_allp_def search_check_file_def)
+apply (frule is_dir_not_file, simp)
+done
 
-lemma enrich_proc_dup_ffd':
-  "\<lbrakk>file_of_proc_fd (enrich_proc s p p') p' fd = Some f; is_created_proc s p; p' \<notin> all_procs s;
-    no_del_event s; valid s\<rbrakk>
-   \<Longrightarrow> file_of_proc_fd s p fd = Some f"
-apply (induct s, simp add:is_created_proc_def)
-apply (frule vt_grant_os, frule vd_cons)
-apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def
-  dest:not_all_procs_prop3 split:if_splits option.splits)
-done 
+lemma search_check_leveling_f:
+  "\<lbrakk>search_check s sp pf; parent f = Some pf; is_file s f; valid s;
+    sectxt_of_obj s (O_file f) = Some fctxt; search_check_file sp fctxt\<rbrakk>
+   \<Longrightarrow> search_check s sp f"
+apply (case_tac f, simp+)
+apply (auto split:option.splits simp:search_check_ctxt_def)
+apply (frule parentf_is_dir_prop2, simp)
+apply (erule get_pfs_secs_prop, simp)
+apply (erule_tac search_check_allp_intro, simp_all)
+apply (simp add:parentf_is_dir_prop2)
+done
 
-lemma enrich_proc_dup_ffd_eq:
-  "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
-  \<Longrightarrow> file_of_proc_fd (enrich_proc s p p') p' fd = file_of_proc_fd s p fd"
-apply (case_tac "file_of_proc_fd s p fd")
-apply (case_tac[!] "file_of_proc_fd (enrich_proc s p p') p' fd")
-apply (auto dest:enrich_proc_dup_ffd enrich_proc_dup_ffd')
-done
 
 lemma current_fflag_in_fds:
   "\<lbrakk>flags_of_proc_fd s p fd = Some flag; valid s\<rbrakk> \<Longrightarrow> fd \<in> current_proc_fds s p"
@@ -1333,37 +1232,6 @@
 apply (auto split:if_splits option.splits dest:proc_fd_in_fds)
 done
 
-lemma enrich_proc_dup_fflags:
-  "\<lbrakk>flags_of_proc_fd s p fd = Some flag; is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
-   \<Longrightarrow> flags_of_proc_fd (enrich_proc s p p') p' fd = Some (remove_create_flag flag) \<or>
-       flags_of_proc_fd (enrich_proc s p p') p' fd = Some flag"
-apply (induct s arbitrary:p, simp add:is_created_proc_def)
-apply (frule vt_grant_os, frule vd_cons)
-apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def is_creat_flag_def
-  dest:not_all_procs_prop3 split:if_splits option.splits)
-done
-
-lemma enrich_proc_dup_ffds:
-  "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
-   \<Longrightarrow> proc_file_fds (enrich_proc s p p') p' = proc_file_fds s p"
-apply (auto simp:proc_file_fds_def)
-apply (rule_tac x = f in exI) 
-apply (erule enrich_proc_dup_ffd', simp+)
-apply (rule_tac x = f in exI)
-apply (erule enrich_proc_dup_ffd, simp+)
-done
-
-lemma enrich_proc_dup_ffds_eq_fds:
-  "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
-   \<Longrightarrow> current_proc_fds (enrich_proc s p p') p' = proc_file_fds s p"
-apply (induct s arbitrary:p)
-apply (simp add: is_created_proc_def)
-apply (frule not_all_procs_prop3)
-apply (frule vd_cons, frule vt_grant_os, case_tac a)
-apply (auto split:if_splits option.splits dest:proc_fd_in_fds set_mp not_all_procs_prop3 
-  simp:proc_file_fds_def is_created_proc_def)
-done
-
 lemma oflags_check_remove_create: 
   "oflags_check flags sp sf \<Longrightarrow> oflags_check (remove_create_flag flags) sp sf"
 apply (case_tac flags)
diff -r 690636b7b6f1 -r 8d18cfc845dd no_shm_selinux/Enrich2.thy
--- a/no_shm_selinux/Enrich2.thy	Mon Dec 30 23:41:58 2013 +0800
+++ b/no_shm_selinux/Enrich2.thy	Tue Dec 31 14:57:13 2013 +0800
@@ -5,44 +5,147 @@
 
 context tainting_s begin
 
-(* \<And> *)
-lemma current_proc_fds_in_curp:
-  "\<lbrakk>fd \<in> current_proc_fds s p; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
+
+fun enrich_msgq :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msgq \<Rightarrow> t_state"
+where
+  "enrich_msgq [] tq dq = []"
+| "enrich_msgq (CreateMsgq p q # s) tq dq = 
+    (if (tq = q) 
+     then (CreateMsgq p dq # CreateMsgq p q # s)
+     else CreateMsgq p q # (enrich_msgq s tq dq))"
+| "enrich_msgq (SendMsg p q m # s) tq dq = 
+    (if (tq = q) 
+     then (SendMsg p dq m # SendMsg p q m # (enrich_msgq s tq dq))
+     else SendMsg p q m # (enrich_msgq s tq dq))"
+| "enrich_msgq (RecvMsg p q m # s) tq dq = 
+    (if (tq = q) 
+     then (RecvMsg p dq m # RecvMsg p q m # (enrich_msgq s tq dq))
+     else RecvMsg p q m # (enrich_msgq s tq dq))"
+| "enrich_msgq (e # s) tq dq = e # (enrich_msgq s tq dq)"
+
+
+
+(* enrich s target_proc duplicated_pro *)
+fun enrich_proc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> t_state"
+where 
+  "enrich_proc [] tp dp = []"
+| "enrich_proc (Execve p f fds # s) tp dp = (
+     if (tp = p) 
+     then Execve dp f (fds \<inter> proc_file_fds s p) # Execve p f fds # (enrich_proc s tp dp)
+     else Execve p f fds # (enrich_proc s tp dp))"
+| "enrich_proc (Clone p p' fds # s) tp dp = (
+     if (tp = p') 
+     then Clone p dp (fds \<inter> proc_file_fds s p) # Clone p p' fds # s
+     else Clone p p' fds # (enrich_proc s tp dp))"
+| "enrich_proc (Open p f flags fd opt # s) tp dp = (
+     if (tp = p)
+     then Open dp f (remove_create_flag flags) fd None # Open p f flags fd opt # (enrich_proc s tp dp)
+     else Open p f flags fd opt # (enrich_proc s tp dp))"
+| "enrich_proc (ReadFile p fd # s) tp dp = (
+     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 (CloseFd p fd # s) tp dp = (
+     if (tp = p \<and> fd \<in> proc_file_fds s p)
+     then CloseFd dp fd # CloseFd p fd # (enrich_proc s tp dp)
+     else CloseFd p fd # (enrich_proc s tp dp))"
+*)
+(*
+| "enrich_proc (Attach p h flag # s) tp dp = (
+     if (tp = p)
+     then Attach dp h flag # Attach p h flag # (enrich_proc s tp dp)
+     else Attach p h flag # (enrich_proc s tp dp))"
+| "enrich_proc (Detach p h # s) tp dp = (
+     if (tp = p) 
+     then Detach dp h # Detach p h # (enrich_proc s tp dp)
+     else Detach p h # (enrich_proc s tp dp))"
+*)
+(*
+| "enrich_proc (Kill p p' # s) tp dp = (
+     if (tp = p') then Kill p p' # s
+     else Kill p p' # (enrich_proc s tp dp))"
+| "enrich_proc (Exit p # s) tp dp = (
+     if (tp = p) then Exit p # s
+     else Exit p # (enrich_proc s tp dp))"
+*)
+| "enrich_proc (e # s) tp dp = e # (enrich_proc s tp dp)"
+
+definition is_created_proc:: "t_state \<Rightarrow> t_process \<Rightarrow> bool"
+where
+  "is_created_proc s p \<equiv> p \<in> current_procs s \<and> (p \<in> init_procs \<longrightarrow> died (O_proc p) s)"
+
+definition is_created_proc':: "t_state \<Rightarrow> t_process \<Rightarrow> bool"
+where
+  "is_created_proc' s p \<equiv> p \<in> current_procs s \<and> p \<notin> init_procs"
+
+lemma created_proc_clone:
+  "valid (Clone p p' fds # s) \<Longrightarrow> 
+   is_created_proc (Clone p p' fds # s) tp = (if (tp = p') then True else is_created_proc s tp)"
+apply (drule vt_grant_os)
+apply (auto simp:is_created_proc_def dest:not_all_procs_prop2)
+using not_died_init_proc
+by auto
+
+lemma created_proc_exit: 
+  "is_created_proc (Exit p # s) tp = (if (tp = p) then False else is_created_proc s tp)"
+by (simp add:is_created_proc_def)
+
+lemma created_proc_kill:
+  "is_created_proc (Kill p p' # s) tp = (if (tp = p') then False else is_created_proc s tp)"
+by (simp add:is_created_proc_def)
+
+lemma created_proc_other:
+  "\<lbrakk>\<And> p p' fds. e \<noteq> Clone p p' fds;
+    \<And> p. e \<noteq> Exit p;
+    \<And> p p'. e \<noteq> Kill p p'\<rbrakk> \<Longrightarrow> is_created_proc (e # s) tp = is_created_proc s tp"
+by (case_tac e, auto simp:is_created_proc_def)
+
+lemmas is_created_proc_simps = created_proc_clone created_proc_exit created_proc_kill created_proc_other
+
+lemma no_del_died:
+  "\<lbrakk>no_del_event s; died obj s\<rbrakk> \<Longrightarrow> (\<exists> p fd. obj = O_fd p fd \<or> obj = O_tcp_sock (p, fd) \<or> obj = O_udp_sock (p, fd))
+  \<or> (\<exists> q m. obj = O_msg q m) "
 apply (induct s)
-apply (simp add:init_fds_of_proc_prop1)
-apply (frule vt_grant_os, frule vd_cons)
-apply (case_tac a, auto split:if_splits option.splits)
-done
-
-lemma get_parentfs_ctxts_prop:
-  "\<lbrakk>get_parentfs_ctxts s (a # f) = Some ctxts; sectxt_of_obj s (O_dir f) = Some ctxt; valid s\<rbrakk>
-   \<Longrightarrow> ctxt \<in> set (ctxts)"
-apply (induct f)
+apply simp
+apply (case_tac a)
 apply (auto split:option.splits)
 done
 
-lemma search_check_allp_intro:
-  "\<lbrakk>search_check s sp pf; get_parentfs_ctxts s pf = Some ctxts; valid s; is_dir s pf\<rbrakk>
-   \<Longrightarrow> search_check_allp sp (set ctxts)"
-apply (case_tac pf)
-apply (simp split:option.splits if_splits add:search_check_allp_def)
-apply (rule ballI)
-apply (auto simp:search_check_ctxt_def search_check_dir_def split:if_splits option.splits)
-apply (auto simp:search_check_allp_def search_check_file_def)
-apply (frule is_dir_not_file, simp)
+lemma no_del_created_eq:
+  "no_del_event s \<Longrightarrow> is_created_proc s p = is_created_proc' s p"
+apply (induct s)
+apply (simp add:is_created_proc_def is_created_proc'_def)
+apply (case_tac a)
+apply (auto simp add:is_created_proc_def is_created_proc'_def dest:no_del_died)
+done
+
+lemma enrich_proc_dup_in:
+  "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
+   \<Longrightarrow> p' \<in> current_procs (enrich_proc s p p')"
+apply (induct s, simp add:is_created_proc_def)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto simp:is_created_proc_def dest:not_all_procs_prop3)
 done
 
-lemma search_check_leveling_f:
-  "\<lbrakk>search_check s sp pf; parent f = Some pf; is_file s f; valid s;
-    sectxt_of_obj s (O_file f) = Some fctxt; search_check_file sp fctxt\<rbrakk>
-   \<Longrightarrow> search_check s sp f"
-apply (case_tac f, simp+)
-apply (auto split:option.splits simp:search_check_ctxt_def)
-apply (frule parentf_is_dir_prop2, simp)
-apply (erule get_pfs_secs_prop, simp)
-apply (erule_tac search_check_allp_intro, simp_all)
-apply (simp add:parentf_is_dir_prop2)
-done
+lemma enrich_proc_dup_ffd:
+  "\<lbrakk>file_of_proc_fd s p fd = Some f; is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
+   \<Longrightarrow> file_of_proc_fd (enrich_proc s p p') p' fd = Some f"
+apply (induct s, simp add:is_created_proc_def)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def
+  dest:not_all_procs_prop3 split:if_splits option.splits)
+done 
+
+lemma enrich_proc_dup_ffd':
+  "\<lbrakk>file_of_proc_fd (enrich_proc s p p') p' fd = Some f; is_created_proc s p; p' \<notin> all_procs s;
+    no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> file_of_proc_fd s p fd = Some f"
+apply (induct s, simp add:is_created_proc_def)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def
+  dest:not_all_procs_prop3 split:if_splits option.splits)
+done 
 
 lemma enrich_proc_dup_ffds':
   "\<lbrakk>fd \<notin> current_proc_fds (enrich_proc s p p') p'; is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
@@ -51,6 +154,46 @@
 apply (simp add:proc_file_fds_def)
 done
 
+lemma enrich_proc_dup_ffd_eq:
+  "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
+  \<Longrightarrow> file_of_proc_fd (enrich_proc s p p') p' fd = file_of_proc_fd s p fd"
+apply (case_tac "file_of_proc_fd s p fd")
+apply (case_tac[!] "file_of_proc_fd (enrich_proc s p p') p' fd")
+apply (auto dest:enrich_proc_dup_ffd enrich_proc_dup_ffd')
+done
+
+
+lemma enrich_proc_dup_fflags:
+  "\<lbrakk>flags_of_proc_fd s p fd = Some flag; is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
+   \<Longrightarrow> flags_of_proc_fd (enrich_proc s p p') p' fd = Some (remove_create_flag flag) \<or>
+       flags_of_proc_fd (enrich_proc s p p') p' fd = Some flag"
+apply (induct s arbitrary:p, simp add:is_created_proc_def)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def is_creat_flag_def
+  dest:not_all_procs_prop3 split:if_splits option.splits)
+done
+
+lemma enrich_proc_dup_ffds:
+  "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> proc_file_fds (enrich_proc s p p') p' = proc_file_fds s p"
+apply (auto simp:proc_file_fds_def)
+apply (rule_tac x = f in exI) 
+apply (erule enrich_proc_dup_ffd', simp+)
+apply (rule_tac x = f in exI)
+apply (erule enrich_proc_dup_ffd, simp+)
+done
+
+lemma enrich_proc_dup_ffds_eq_fds:
+  "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> current_proc_fds (enrich_proc s p p') p' = proc_file_fds s p"
+apply (induct s arbitrary:p)
+apply (simp add: is_created_proc_def)
+apply (frule not_all_procs_prop3)
+apply (frule vd_cons, frule vt_grant_os, case_tac a)
+apply (auto split:if_splits option.splits dest:proc_fd_in_fds set_mp not_all_procs_prop3 
+  simp:proc_file_fds_def is_created_proc_def)
+done
+
 lemma enrich_proc_cur_inof:
   "\<lbrakk>valid s; no_del_event s\<rbrakk> \<Longrightarrow> inum_of_file (enrich_proc s p p') f = inum_of_file s f"
 apply (induct s arbitrary:f)
diff -r 690636b7b6f1 -r 8d18cfc845dd no_shm_selinux/Finite_current.thy
--- a/no_shm_selinux/Finite_current.thy	Mon Dec 30 23:41:58 2013 +0800
+++ b/no_shm_selinux/Finite_current.thy	Tue Dec 31 14:57:13 2013 +0800
@@ -92,6 +92,12 @@
 apply (case_tac a, auto simp: init_finite_sets)
 done
 
+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 (frule vt_grant_os, frule vd_cons, case_tac a, auto)
+done
 
 lemma finite_option: "finite {x. \<exists> y. f x = Some y} \<Longrightarrow> finite {y. \<exists> x. f x = Some y}"
 apply (drule_tac h = f in finite_imageI)
diff -r 690636b7b6f1 -r 8d18cfc845dd no_shm_selinux/Flask.thy
--- a/no_shm_selinux/Flask.thy	Mon Dec 30 23:41:58 2013 +0800
+++ b/no_shm_selinux/Flask.thy	Tue Dec 31 14:57:13 2013 +0800
@@ -135,8 +135,11 @@
 *)
   and init_socket_state ::      "t_socket \<rightharpoonup> t_sock_state"
 
+(*
   and init_msgqs :: "t_msgq set"
   and init_msgs_of_queue:: "t_msgq \<Rightarrow> t_msg list"
+*)
+  and max_queue :: "nat"
 (*
   and init_shms :: "t_shm set"
   and init_procs_of_shm :: "t_shm \<Rightarrow> (t_process \<times> t_shm_attach_flag) set" 
@@ -162,8 +165,12 @@
   and init_procs_has_shm:      "\<And> p h flag. (p,flag) \<in> init_procs_of_shm h \<Longrightarrow> p \<in> init_procs \<and> h \<in> init_shms \<and> init_flag_of_proc_shm p h = Some flag"
   and init_shmflag_has_proc:   "\<And> p h flag. init_flag_of_proc_shm p h = Some flag \<Longrightarrow> (p, flag) \<in> init_procs_of_shm h"
 *)
+
+(*
   and init_msgs_distinct:      "\<And> q. distinct (init_msgs_of_queue q)"
   and init_msgs_valid:         "\<And> m q. m \<in> set (init_msgs_of_queue q) \<Longrightarrow> q \<in> init_msgqs"
+  and init_msgq_valid:         "\<And> q. length (init_msgs_of_queue q) \<le> max_queue"
+*)
 
   and init_socket_has_inode:   "\<And> p fd. (p, fd) \<in> init_sockets \<Longrightarrow> \<exists> im. init_inum_of_socket (p, fd) = Some im \<and> p \<in> init_procs \<and> fd \<in> init_fds_of_proc p \<and> init_file_of_proc_fd p fd = None"
   and inos_has_sock_tag:  "\<And> s im. init_inum_of_socket s = Some im \<Longrightarrow> s \<in> init_sockets \<and> (\<exists> tag. init_itag_of_inum im = Some tag \<and> is_sock_itag tag)"
@@ -174,7 +181,7 @@
   and init_netobj_has_raddr:   "\<And> s. after_conacc (init_netobj_state s) \<Longrightarrow> init_netobj_remoteaddr s \<noteq> None"
 *)
 
-  and init_finite_sets:   "finite init_files \<and> finite init_procs \<and> (\<forall> p. finite (init_fds_of_proc p)) \<and> finite init_shms \<and> finite init_msgqs \<and> finite init_users" 
+  and init_finite_sets:   "finite init_files \<and> finite init_procs \<and> (\<forall> p. finite (init_fds_of_proc p)) \<and> finite init_shms \<and> finite init_users"  (* finite init_msgqs *)
 
 begin 
 
@@ -226,8 +233,8 @@
 (*
 | "init_alive (O_shm  h)     = (h \<in> init_shms)"
 *)
-| "init_alive (O_msgq q)     = (q \<in> init_msgqs)"
-| "init_alive (O_msg q m)    = (m \<in> set (init_msgs_of_queue q) \<and> q \<in> init_msgqs)"
+| "init_alive (O_msgq q)     = False" (* (q \<in> init_msgqs) *)
+| "init_alive (O_msg q m)    = False" (* (m \<in> set (init_msgs_of_queue q) \<and> q \<in> init_msgqs)" *)
 
 
 (************ system listeners, event-related ***********)
@@ -512,14 +519,14 @@
 
 fun current_msgqs :: "t_state \<Rightarrow> t_msgq set"
 where
-  "current_msgqs [] = init_msgqs"
+  "current_msgqs [] = {}" (* init_msgqs *)
 | "current_msgqs (CreateMsgq p q # \<tau>) = insert q (current_msgqs \<tau>)"
 | "current_msgqs (RemoveMsgq p q # \<tau>) = (current_msgqs \<tau>) - {q}"
 | "current_msgqs (_ # \<tau>) = current_msgqs \<tau>"
 
 fun msgs_of_queue :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg list"
 where
-  "msgs_of_queue [] = init_msgs_of_queue"
+  "msgs_of_queue [] = (\<lambda> x. [])" (* init_msgs_of_queue*)
 | "msgs_of_queue (CreateMsgq p q # \<tau>) = (msgs_of_queue \<tau>)(q := [])"
 | "msgs_of_queue (SendMsg p q m  # \<tau>) = (msgs_of_queue \<tau>)(q := msgs_of_queue \<tau> q @ [m])"
 | "msgs_of_queue (RecvMsg p q m  # \<tau>) = (msgs_of_queue \<tau>)(q := tl (msgs_of_queue \<tau> q))"
@@ -720,7 +727,8 @@
 | "os_grant \<tau> (CreateMsgq p q)                = 
     (p \<in> current_procs \<tau> \<and> q \<notin> (current_msgqs \<tau>))"
 | "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)))"
+    (p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau> \<and> m \<notin> (set (msgs_of_queue \<tau> q)) \<and> 
+     length (msgs_of_queue \<tau> q) < max_queue)"
 | "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) \<and> msgs_of_queue \<tau> q \<noteq> [])"
 | "os_grant \<tau> (RemoveMsgq p q)                = 
@@ -1477,7 +1485,8 @@
   "valid []"
 | "\<lbrakk>valid s; os_grant s e; grant s e\<rbrakk> \<Longrightarrow> valid (e # s)"
 
-(* tobj: object that can be tainted *)
+
+(* tobj: object that can be tainted 
 fun tobj_in_init :: "t_object \<Rightarrow> bool"
 where
   "tobj_in_init (O_proc p) = (p \<in> init_procs)"
@@ -1489,6 +1498,8 @@
 | "tobj_in_init (O_msg q m) = (m \<in> set (init_msgs_of_queue q) \<and> q \<in> init_msgqs)"
 *)
 | "tobj_in_init _ = False" (* other kind of obj cannot be tainted *)
+*)
+
 
 (* no use
 fun no_del_event:: "t_event list \<Rightarrow> bool"
diff -r 690636b7b6f1 -r 8d18cfc845dd no_shm_selinux/Init_prop.thy
--- a/no_shm_selinux/Init_prop.thy	Mon Dec 30 23:41:58 2013 +0800
+++ b/no_shm_selinux/Init_prop.thy	Tue Dec 31 14:57:13 2013 +0800
@@ -334,13 +334,13 @@
 lemma init_alive_node: "n \<in> init_nodes \<Longrightarrow> init_alive (O_node n)" by simp
 (*
 lemma init_alive_shm: "h \<in> init_shms \<Longrightarrow> init_alive (O_shm h)" by simp
-*)
 lemma init_alive_msgq: "q \<in> init_msgqs \<Longrightarrow> init_alive (O_msgq q)" by simp
 lemma init_alive_msg: "\<lbrakk>m \<in> set (init_msgs_of_queue q); q \<in> init_msgqs\<rbrakk>
   \<Longrightarrow> init_alive (O_msg q m)" by simp
+*)
 
 lemmas init_alive_intros = init_alive_proc init_alive_file init_alive_dir init_alive_fd 
-  init_alive_tcp init_alive_udp init_alive_node  init_alive_msgq init_alive_msg (*init_alive_shm*)
+  init_alive_tcp init_alive_udp init_alive_node (*init_alive_msgq init_alive_msg*) (*init_alive_shm*)
 
 
 lemma init_file_type_prop1: "is_init_file f \<Longrightarrow> \<exists> t. init_type_of_obj (O_file f) = Some t"
@@ -541,6 +541,7 @@
 by (rule notI, drule init_shm_has_ctxt, simp)
 *)
 
+(*
 lemma init_msgq_has_ctxt:
   "q \<in> init_msgqs \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_msgq q) = Some sec"
 apply (simp add:init_sectxt_of_obj_def split:option.splits)
@@ -560,6 +561,7 @@
 lemma init_msg_has_ctxt':
   "init_sectxt_of_obj (O_msg q m) = None \<Longrightarrow> m \<notin> set (init_msgs_of_queue q) \<or> q \<notin> init_msgqs"
 by (auto dest:init_msg_has_ctxt)
+*)
 
 lemma init_rootf_has_ctxt:
   "\<exists> sec. init_sectxt_of_obj (O_dir []) = Some sec"
@@ -571,12 +573,12 @@
 using init_rootf_has_ctxt by auto
 
 lemmas init_has_ctxt = init_file_has_ctxt init_dir_has_ctxt init_proc_has_ctxt init_fd_has_ctxt
-  init_node_has_ctxt init_tcp_has_ctxt init_udp_has_ctxt (* init_shm_has_ctxt *) init_msgq_has_ctxt
-  init_msg_has_ctxt init_rootf_has_ctxt
+  init_node_has_ctxt init_tcp_has_ctxt init_udp_has_ctxt (* init_shm_has_ctxt *) (* init_msgq_has_ctxt
+  init_msg_has_ctxt*) init_rootf_has_ctxt
 
 lemmas init_has_ctxt' = init_file_has_ctxt' init_dir_has_ctxt' init_proc_has_ctxt' init_fd_has_ctxt'
-  init_node_has_ctxt' init_tcp_has_ctxt' init_udp_has_ctxt' (* init_shm_has_ctxt' *) init_msgq_has_ctxt'
-  init_msg_has_ctxt' init_rootf_has_ctxt'
+  init_node_has_ctxt' init_tcp_has_ctxt' init_udp_has_ctxt' (* init_shm_has_ctxt' *) (*init_msgq_has_ctxt'
+  init_msg_has_ctxt'*) init_rootf_has_ctxt'
 
 lemma sec_of_root_valid:
   "init_sectxt_of_obj (O_dir []) = Some sec_of_root"
@@ -668,6 +670,7 @@
 apply (simp add:init_cp2sproc_def)
 by (case_tac sec, simp+)
 
+(*
 lemma init_cqm2sms_has_sms_aux:
   "\<forall> m \<in> set ms. init_sectxt_of_obj (O_msg q m) \<noteq> None \<Longrightarrow> (\<exists> sms. init_cqm2sms q ms = Some sms)"
 by (induct ms, auto split:option.splits simp:init_cm2smsg_def)
@@ -682,6 +685,7 @@
 apply (frule init_msgq_has_ctxt, erule exE, drule init_cqm2sms_has_sms, erule exE)
 apply (simp add:init_cq2smsgq_def)
 by (case_tac sec, simp+)
+*)
 
 lemma cf2sfile_nil_prop:
   "f \<in> init_files \<Longrightarrow> cf2sfile [] f = init_cf2sfile f"
@@ -758,6 +762,7 @@
 by (auto simp add:init_cp2sproc_def cp2sproc_def init_sectxt_prop cpfd2sfds_nil_prop (*cph2spshs_nil_prop*)
          split:option.splits)
 
+(*
 lemma msg_has_sec_imp_init: 
   "init_sectxt_of_obj (O_msg q m) = Some sec \<Longrightarrow> q \<in> init_msgqs \<and> m \<in> set (init_msgs_of_queue q)"
 apply (simp add:init_sectxt_of_obj_def split:option.splits)
@@ -783,14 +788,15 @@
   "cq2smsgq [] q = init_cq2smsgq q"
 by (auto simp add:cq2smsgq_def init_cq2smsgq_def init_sectxt_prop cqm2sms_nil_prop
             intro:msgq_has_sec_imp_init split:option.splits)
+*)
 
 lemma co2sobj_nil_prop:
   "init_alive obj \<Longrightarrow> co2sobj [] obj = init_obj2sobj obj"
 apply (case_tac obj)
-apply (auto simp add:cf2sfile_nil_prop cq2smsga_nil_prop cqm2sms_nil_prop tainted_nil_prop 
+apply (auto simp add:cf2sfile_nil_prop (*cq2smsga_nil_prop cqm2sms_nil_prop*) tainted_nil_prop 
                      cp2sproc_nil_prop cfs2sfiles_nil_prop is_init_dir_prop1 is_init_file_prop1
                      is_init_udp_sock_prop1 is_init_tcp_sock_prop1 (* ch2sshm_nil_prop *)
-                     same_inode_nil_prop  cm2smsg_nil_prop 
+                     same_inode_nil_prop  (*cm2smsg_nil_prop *)
             dest:init_same_inode_prop1 
                split:option.splits)
 apply (rule_tac x = list in exI, simp add:init_same_inode_files_def)
diff -r 690636b7b6f1 -r 8d18cfc845dd no_shm_selinux/ROOT
--- a/no_shm_selinux/ROOT	Mon Dec 30 23:41:58 2013 +0800
+++ b/no_shm_selinux/ROOT	Tue Dec 31 14:57:13 2013 +0800
@@ -35,4 +35,10 @@
   options [document = false]
   theories
     S2ss_prop
-    S2ss_prop2
\ No newline at end of file
+    S2ss_prop2
+
+session "enrich" = "s2ss" + 
+  options [document = false]
+  theories
+    Enrich
+    Enrich1
\ No newline at end of file
diff -r 690636b7b6f1 -r 8d18cfc845dd no_shm_selinux/Static.thy
--- a/no_shm_selinux/Static.thy	Mon Dec 30 23:41:58 2013 +0800
+++ b/no_shm_selinux/Static.thy	Tue Dec 31 14:57:13 2013 +0800
@@ -77,6 +77,7 @@
 where
   "init_o2s_afs f \<equiv> {sec. \<exists> f'. f' \<preceq> f \<and> init_sectxt_of_obj (O_dir f') = Some sec}" *)
 
+(*
 definition init_cm2smsg :: "t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsg option"
 where
   "init_cm2smsg q m \<equiv> (case (init_sectxt_of_obj (O_msg q m)) of 
@@ -96,6 +97,7 @@
   "init_cq2smsgq q \<equiv> (case (init_sectxt_of_obj (O_msgq q), init_cqm2sms q (init_msgs_of_queue q)) of 
        (Some sec, Some sms) \<Rightarrow> Some (Init q, sec, sms)
      | _ \<Rightarrow> None)"
+*)
 
 fun init_obj2sobj :: "t_object \<Rightarrow> t_sobject option"
 where
@@ -110,11 +112,13 @@
      (case (init_cf2sfile f) of
            Some sf \<Rightarrow> Some (S_dir sf) 
          | _ \<Rightarrow> None)"
-| "init_obj2sobj (O_msgq q) = 
+| "init_obj2sobj (O_msgq q) = None"
+
+(*
      (case (init_cq2smsgq q) of
        Some sq \<Rightarrow> Some (S_msgq sq)
      | _ \<Rightarrow> None)"
-(*
+
 | "init_obj2sobj (O_shm h) = 
      (case (init_ch2sshm h) of 
        Some sh \<Rightarrow> Some (S_shm sh)
@@ -184,6 +188,7 @@
        cpfd2sfds s p)
                    | _ \<Rightarrow> None)"
 
+(*
 definition cm2smsg :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsg option"
 where
   "cm2smsg s q m \<equiv> (case (sectxt_of_obj s (O_msg q m)) of 
@@ -191,6 +196,13 @@
  Some (if (\<not> died (O_msg q m) s \<and> m \<in> set (init_msgs_of_queue q)) then Init m else Created,
        sec, O_msg q m \<in> tainted s)
                     | _ \<Rightarrow> None)"
+*)
+
+definition cm2smsg :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsg option"
+where
+  "cm2smsg s q m \<equiv> (case (sectxt_of_obj s (O_msg q m)) of 
+                      Some sec \<Rightarrow> Some (Created, sec, O_msg q m \<in> tainted s)
+                    | _ \<Rightarrow> None)"
 
 fun cqm2sms:: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg list \<Rightarrow> (t_smsg list) option"
 where 
@@ -199,7 +211,7 @@
      (case (cqm2sms s q ms, cm2smsg s q m) of 
        (Some sms, Some sm) \<Rightarrow> Some (sm#sms) 
      | _ \<Rightarrow> None)"
-
+(*
 definition cq2smsgq :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_smsgq option"
 where
   "cq2smsgq s q \<equiv> (case (sectxt_of_obj s (O_msgq q), cqm2sms s q (msgs_of_queue s q)) of 
@@ -207,6 +219,13 @@
  Some (if (\<not> died (O_msgq q) s \<and> q \<in> init_msgqs) then Init q else Created,
        sec, sms)
                    | _ \<Rightarrow> None)"
+*)
+
+definition cq2smsgq :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_smsgq option"
+where
+  "cq2smsgq s q \<equiv> (case (sectxt_of_obj s (O_msgq q), cqm2sms s q (msgs_of_queue s q)) of 
+                     (Some sec, Some sms) \<Rightarrow> Some (Created, sec, sms)
+                   | _ \<Rightarrow> None)"
 
 fun co2sobj :: "t_state \<Rightarrow> t_object \<Rightarrow> t_sobject option"
 where
@@ -266,22 +285,24 @@
   "is_many_sproc (Created, sec,fds) = True"
 | "is_many_sproc _                       = False"
 
+(*
 fun is_many_smsg :: "t_smsg \<Rightarrow> bool"
 where
   "is_many_smsg (Created,sec,tag) = True"
 | "is_many_smsg _                 = False"
-
+*)
 (* wrong def 
 fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool"
 where
   "is_many_smsgq (Created,sec,sms) = (True \<and> (\<forall> sm \<in> (set sms). is_many_smsg sm))"
 | "is_many_smsgq _                 = False"
 *)
-
+(*
 fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool"
 where
   "is_many_smsgq (Created,sec,sms) = True"
 | "is_many_smsgq _                 = False"
+*)
 (*
 fun is_many_sshm :: "t_sshm \<Rightarrow> bool"
 where
@@ -293,16 +314,17 @@
   "is_many (S_proc sp   tag) = is_many_sproc sp"
 | "is_many (S_file sfs  tag) = (\<forall> sf \<in> sfs. is_many_sfile sf)"
 | "is_many (S_dir  sf      ) = is_many_sfile sf"
-| "is_many (S_msgq sq      ) = is_many_smsgq sq"
+| "is_many (S_msgq sq      ) = True"
 (*
 | "is_many (S_shm  sh      ) = is_many_sshm  sh"
 *)
 
+(*
 fun is_init_smsgq :: "t_smsgq \<Rightarrow> bool"
 where
   "is_init_smsgq (Init q,sec,sms) = True"
 | "is_init_smsgq _                = False"
-
+*)
 (*
 fun is_init_sshm :: "t_sshm \<Rightarrow> bool"
 where
@@ -314,7 +336,7 @@
   "is_init_sobj (S_proc sp tag ) = is_init_sproc sp"
 | "is_init_sobj (S_file sfs tag) = (\<exists> sf \<in> sfs. is_init_sfile sf)"
 | "is_init_sobj (S_dir  sf     ) = is_init_sfile sf"
-| "is_init_sobj (S_msgq sq     ) = is_init_smsgq sq"
+| "is_init_sobj (S_msgq sq     ) = False"
 (*
 | "is_init_sobj (S_shm  sh     ) = is_init_sshm sh"
 *)
diff -r 690636b7b6f1 -r 8d18cfc845dd no_shm_selinux/Temp.thy
--- a/no_shm_selinux/Temp.thy	Mon Dec 30 23:41:58 2013 +0800
+++ b/no_shm_selinux/Temp.thy	Tue Dec 31 14:57:13 2013 +0800
@@ -124,7 +124,7 @@
 | s_sendmsg: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds) tagp \<in> ss; S_msgq (qi,qctxt,sms) \<in> ss;
                permission_check pctxt qctxt C_msgq P_enqueue;
                permission_check pctxt qctxt C_msgq P_write; 
-               permission_check pctxt pctxt C_msg  P_create\<rbrakk>
+               permission_check pctxt pctxt C_msg  P_create; length sms < max_queue\<rbrakk>
   \<Longrightarrow> (update_ss ss (S_msgq (qi,qctxt,sms)) 
                     (S_msgq (qi,qctxt,sms @ [(Created, pctxt, tagp)]))) \<in> static"
 | s_recvmsg: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds) tagp \<in> ss;