theory Info_flow_shm_propimports Main Flask_type Flask My_list_prefix Init_prop Valid_prop Delete_prop Current_propbegincontext flask begin(*********** simpset for one_flow_shm **************)lemma one_flow_not_self: "one_flow_shm s h p p \<Longrightarrow> False"by (simp add:one_flow_shm_def)lemma one_flow_shm_attach: "valid (Attach p h flag # s) \<Longrightarrow> one_flow_shm (Attach p h flag # s) = (\<lambda> h' pa pb. if (h' = h) then (pa = p \<and> pb \<noteq> p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pb, flagb) \<in> procs_of_shm s h)) \<or> (pb = p \<and> pa \<noteq> p \<and> (pa, SHM_RDWR) \<in> procs_of_shm s h) \<or> (one_flow_shm s h pa pb) else one_flow_shm s h' pa pb )"apply (rule ext, rule ext, rule ext, frule vd_cons, frule vt_grant_os)by (auto simp add: one_flow_shm_def)lemma one_flow_shm_detach: "valid (Detach p h # s) \<Longrightarrow> one_flow_shm (Detach p h # s) = (\<lambda> h' pa pb. if (h' = h) then (pa \<noteq> p \<and> pb \<noteq> p \<and> one_flow_shm s h' pa pb) else one_flow_shm s h' pa pb)"apply (rule ext, rule ext, rule ext, frule vt_grant_os)by (auto simp:one_flow_shm_def)lemma one_flow_shm_deleteshm: "valid (DeleteShM p h # s) \<Longrightarrow> one_flow_shm (DeleteShM p h # s) = (\<lambda> h' pa pb. if (h' = h) then False else one_flow_shm s h' pa pb)"apply (rule ext, rule ext, rule ext, frule vt_grant_os)by (auto simp: one_flow_shm_def)lemma one_flow_shm_clone: "valid (Clone p p' fds shms # s) \<Longrightarrow> one_flow_shm (Clone p p' fds shms # s) = (\<lambda> h pa pb. if (pa = p' \<and> pb \<noteq> p' \<and> h \<in> shms) then (if (pb = p) then (flag_of_proc_shm s p h = Some SHM_RDWR) else one_flow_shm s h p pb) else if (pb = p' \<and> pa \<noteq> p' \<and> h \<in> shms) then (if (pa = p) then (flag_of_proc_shm s p h = Some SHM_RDWR) else one_flow_shm s h pa p) else one_flow_shm s h pa pb)"apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons, clarsimp)apply (frule_tac p = p' in procs_of_shm_prop2', simp)apply (auto simp:one_flow_shm_def intro:procs_of_shm_prop4 flag_of_proc_shm_prop1)donelemma one_flow_shm_execve: "valid (Execve p f fds # s) \<Longrightarrow> one_flow_shm (Execve p f fds # s) = (\<lambda> h pa pb. pa \<noteq> p \<and> pb \<noteq> p \<and> one_flow_shm s h pa pb )"apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)by (auto simp:one_flow_shm_def)lemma one_flow_shm_kill: "valid (Kill p p' # s) \<Longrightarrow> one_flow_shm (Kill p p' # s) = (\<lambda> h pa pb. pa \<noteq> p' \<and> pb \<noteq> p' \<and> one_flow_shm s h pa pb )"apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)by (auto simp:one_flow_shm_def)lemma one_flow_shm_exit: "valid (Exit p # s) \<Longrightarrow> one_flow_shm (Exit p # s) = (\<lambda> h pa pb. pa \<noteq> p \<and> pb \<noteq> p \<and> one_flow_shm s h pa pb )"apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)by (auto simp:one_flow_shm_def)lemma one_flow_shm_other: "\<lbrakk>valid (e # s); \<forall> p h flag. e \<noteq> Attach p h flag; \<forall> p h. e \<noteq> Detach p h; \<forall> p h. e \<noteq> DeleteShM p h; \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms; \<forall> p f fds. e \<noteq> Execve p f fds; \<forall> p p'. e \<noteq> Kill p p'; \<forall> p. e \<noteq> Exit p \<rbrakk> \<Longrightarrow> one_flow_shm (e # s) = one_flow_shm s"apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)apply (case_tac e, auto simp:one_flow_shm_def dest:procs_of_shm_prop2)apply (drule procs_of_shm_prop1, auto)donelemmas one_flow_shm_simps = one_flow_shm_other one_flow_shm_attach one_flow_shm_detach one_flow_shm_deleteshm one_flow_shm_clone one_flow_shm_execve one_flow_shm_kill one_flow_shm_exittype_synonym t_edge_shm = "t_process \<times> t_shm \<times> t_process"fun Fst:: "t_edge_shm \<Rightarrow> t_process" where "Fst (a, b, c) = a"fun Snd:: "t_edge_shm \<Rightarrow> t_shm" where "Snd (a, b, c) = b"fun Trd:: "t_edge_shm \<Rightarrow> t_process" where "Trd (a, b, c) = c"fun edge_related:: "t_edge_shm list \<Rightarrow> t_process \<Rightarrow> t_shm \<Rightarrow> bool"where "edge_related [] p h = False"| "edge_related ((from, shm, to) # path) p h = (if (((p = from) \<or> (p = to)) \<and> (h = shm)) then True else edge_related path p h)"inductive path_by_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_edge_shm list \<Rightarrow> t_process \<Rightarrow> bool"where pbs1: "p \<in> current_procs s \<Longrightarrow> path_by_shm s p [] p"| pbs2: "\<lbrakk>path_by_shm s p path p'; one_flow_shm s h p' p''; p'' \<notin> set (map Fst path)\<rbrakk> \<Longrightarrow> path_by_shm s p ((p', h, p'')# path) p''"lemma one_step_path: "\<lbrakk>one_flow_shm s h p p'; valid s\<rbrakk> \<Longrightarrow> path_by_shm s p [(p, h, p')] p'"apply (rule_tac path = "[]" and p = p in path_by_shm.intros(2))apply (rule path_by_shm.intros(1))apply (auto intro:procs_of_shm_prop2 simp:one_flow_shm_def)donelemma pbs_prop1: "path_by_shm s p path p' \<Longrightarrow> ((path = []) = (p = p')) \<and> (path \<noteq> [] \<longrightarrow> p \<in> set (map Fst path))"apply (erule path_by_shm.induct, simp)apply (auto simp:one_flow_shm_def)donelemma pbs_prop2: "path_by_shm s p path p' \<Longrightarrow> (path = []) = (p = p')"by (simp add:pbs_prop1)lemma pbs_prop2': "path_by_shm s p path p \<Longrightarrow> path = []"by (simp add:pbs_prop2)lemma pbs_prop3: "\<lbrakk>path_by_shm s p path p'; path \<noteq> []\<rbrakk> \<Longrightarrow> p \<in> set (map Fst path)"by (drule pbs_prop1, auto)lemma pbs_prop4[rule_format]: "path_by_shm s p path p'\<Longrightarrow> path \<noteq> [] \<longrightarrow> p' \<in> set (map Trd path)"by (erule path_by_shm.induct, auto)lemma pbs_prop5[rule_format]: "path_by_shm s p path p' \<Longrightarrow> path \<noteq> [] \<longrightarrow> p' \<notin> set (map Fst path)"by (erule path_by_shm.induct, auto simp:one_flow_shm_def)lemma pbs_prop6_aux: "path_by_shm s pa pathac pc \<Longrightarrow> valid s \<longrightarrow> (\<forall> pb \<in> set (map Fst pathac). \<exists> pathab pathbc. path_by_shm s pa pathab pb \<and> path_by_shm s pb pathbc pc \<and> pathac = pathbc @ pathab)"apply (erule path_by_shm.induct)apply simpapply clarifyapply (case_tac "pb = p'", simp)apply (rule_tac x = path in exI, simp)apply (erule one_step_path, simp)apply (erule_tac x = pb in ballE, simp_all, clarsimp)apply (rule_tac x = pathab in exI, simp)apply (erule pbs2, auto)donelemma pbs_prop6: "\<lbrakk>path_by_shm s pa pathac pc; pb \<in> set (map Fst pathac); valid s\<rbrakk> \<Longrightarrow> \<exists> pathab pathbc. path_by_shm s pa pathab pb \<and> path_by_shm s pb pathbc pc \<and> pathac = pathbc @ pathab"by (drule pbs_prop6_aux, auto)lemma pbs_prop7_aux: "path_by_shm s pa pathac pc \<Longrightarrow> valid s \<longrightarrow> (\<forall> pb \<in> set (map Trd pathac). \<exists> pathab pathbc. path_by_shm s pa pathab pb \<and> path_by_shm s pb pathbc pc \<and> pathac = pathbc @ pathab)"apply (erule path_by_shm.induct)apply simpapply clarifyapply (case_tac "pb = p''", simp)apply (rule_tac x = "(p',h,p'') # path" in exI, simp)apply (rule conjI, erule pbs2, simp+)apply (rule pbs1, clarsimp simp:one_flow_shm_def procs_of_shm_prop2)apply (erule_tac x = pb in ballE, simp_all, clarsimp)apply (rule_tac x = pathab in exI, simp)apply (erule pbs2, auto)donelemma pbs_prop7: "\<lbrakk>path_by_shm s pa pathac pc; pb \<in> set (map Trd pathac); valid s\<rbrakk> \<Longrightarrow> \<exists> pathab pathbc. path_by_shm s pa pathab pb \<and> path_by_shm s pb pathbc pc \<and> pathac = pathbc @ pathab"by (drule pbs_prop7_aux, drule mp, simp, erule_tac x = pb in ballE, auto)lemma pbs_prop8: "path_by_shm s p path p' \<Longrightarrow> (set (map Fst path) - {p}) = (set (map Trd path) - {p'})"proof (induct rule:path_by_shm.induct) case (pbs1 p s) thus ?case by simpnext case (pbs2 s p path p' h p'') assume p1:"path_by_shm s p path p'" and p2: "set (map Fst path) - {p} = set (map Trd path) - {p'}" and p3: "one_flow_shm s h p' p''" and p4: "p'' \<notin> set (map Fst path)" show "set (map Fst ((p', h, p'') # path)) - {p} = set (map Trd ((p', h, p'') # path)) - {p''}" (is "?left = ?right") proof (cases "path = []") case True with p1 have "p = p'" by (drule_tac pbs_prop2, simp) thus ?thesis using True using p2 by (simp) next case False with p1 have a1: "p \<noteq> p'" by (drule_tac pbs_prop2, simp) from p3 have a2: "p' \<noteq> p''" by (simp add:one_flow_shm_def) from p1 False have a3: "p' \<in> set (map Trd path)" by (drule_tac pbs_prop4, simp+) from p4 p1 False have a4: "p \<noteq> p''" by (drule_tac pbs_prop3, auto) with p2 a2 p4 have a5: "p'' \<notin> set (map Trd path)" by auto have "?left = (set (map Fst path) - {p}) \<union> {p'}" using a1 by auto moreover have "... = (set (map Trd path) - {p'}) \<union> {p'}" using p2 by auto moreover have "... = set (map Trd path)" using a3 by auto moreover have "... = set (map Trd path) - {p''}" using a5 by simp moreover have "... = ?right" by simp ultimately show ?thesis by simp qedqedlemma pbs_prop9_aux[rule_format]: "path_by_shm s p path p' \<Longrightarrow> h \<in> set (map Snd path) \<and> valid s \<longrightarrow> (\<exists> pa pb patha pathb. path_by_shm s p patha pa \<and> path_by_shm s pb pathb p' \<and> one_flow_shm s h pa pb \<and> path = pathb @ [(pa, h, pb)] @ patha \<and> h \<notin> set (map Snd patha))"apply (erule path_by_shm.induct, simp)apply (rule impI, case_tac "h \<in> set (map Snd path)", simp_all)apply (erule exE|erule conjE)+apply (rule_tac x = pa in exI, rule_tac x = pb in exI, rule_tac x = patha in exI, simp)apply (rule pbs2, auto)apply (rule_tac x = p' in exI, rule_tac x = p'' in exI, rule_tac x = path in exI, simp)apply (rule pbs1, clarsimp simp:one_flow_shm_def procs_of_shm_prop2)donelemma pbs_prop9: "\<lbrakk>h \<in> set (map Snd path); path_by_shm s p path p'; valid s\<rbrakk> \<Longrightarrow> \<exists> pa pb patha pathb. path_by_shm s p patha pa \<and> path_by_shm s pb pathb p' \<and> one_flow_shm s h pa pb \<and> path = pathb @ [(pa, h, pb)] @ patha \<and> h \<notin> set (map Snd patha)"by (rule pbs_prop9_aux, auto)lemma path_by_shm_trans_aux[rule_format]: "path_by_shm s p' path' p'' \<Longrightarrow> valid s \<longrightarrow> (\<forall> p path. path_by_shm s p path p' \<longrightarrow> (\<exists> path''. path_by_shm s p path'' p''))"proof (induct rule:path_by_shm.induct) case (pbs1 p s) thus ?case by (clarify, rule_tac x = path in exI, simp)next case (pbs2 s p path p' h p'') hence p1: "path_by_shm s p path p'" and p2: "one_flow_shm s h p' p''" and p3: "valid s \<longrightarrow> (\<forall>pa path. path_by_shm s pa path p \<longrightarrow> (\<exists>path''. path_by_shm s pa path'' p'))" and p4: "p'' \<notin> set (map Fst path)" by auto show ?case proof clarify fix pa path' assume p5: "path_by_shm s pa path' p" and p6: "valid s" with p3 obtain path'' where a1: "path_by_shm s pa path'' p'" by auto have p3': "\<forall>pa path. path_by_shm s pa path p \<longrightarrow> (\<exists>path''. path_by_shm s pa path'' p')" using p3 p6 by simp show "\<exists>path''. path_by_shm s pa path'' p''" proof (cases "p'' \<in> set (map Fst path'')") case True then obtain res where "path_by_shm s pa res p''" using a1 pbs_prop6 p6 by blast thus ?thesis by auto next case False with p2 a1 show ?thesis apply (rule_tac x = "(p', h, p'') # path''" in exI) apply (rule path_by_shm.intros(2), auto) done qed qedqedlemma path_by_shm_trans: "\<lbrakk>path_by_shm s p path p'; path_by_shm s p' path' p''; valid s\<rbrakk> \<Longrightarrow> \<exists> path''. path_by_shm s p path'' p''"by (drule_tac p' = p' and p'' = p'' in path_by_shm_trans_aux, auto)lemma path_by_shm_intro1_prop: "\<not> path_by_shm s p [] p \<Longrightarrow> p \<notin> current_procs s"by (auto dest:path_by_shm.intros(1))lemma path_by_shm_intro3: "\<lbrakk>path_by_shm s p path from; (from, SHM_RDWR) \<in> procs_of_shm s h; (to, flag) \<in> procs_of_shm s h; to \<notin> set (map Fst path); from \<noteq> to\<rbrakk> \<Longrightarrow> path_by_shm s p ((from, h, to)#path) to"apply (rule path_by_shm.intros(2), simp_all)by (auto simp:one_flow_shm_def)lemma path_by_shm_intro4: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> path_by_shm s p [] p"by (drule procs_of_shm_prop2, simp, simp add:path_by_shm.intros(1))lemma path_by_shm_intro5: "\<lbrakk>(from, SHM_RDWR) \<in> procs_of_shm s h; (to,flag) \<in> procs_of_shm s h; valid s; from \<noteq> to\<rbrakk> \<Longrightarrow> path_by_shm s from [(from, h, to)] to"apply (rule_tac p' = "from" and h = h in path_by_shm.intros(2))apply (rule path_by_shm.intros(1), simp add:procs_of_shm_prop2)apply (simp add:one_flow_shm_def, rule_tac x = flag in exI, auto)done(* p'' \<notin> set (map Fst path): not duplicated target process; * p1 - ha \<rightarrow> p2; p2 - hb \<rightarrow> p3; p3 - ha \<rightarrow> p4; so path_by_shm p1 [(p3,ha,p4), (p2,hb,p3),(p1,ha,p2)] p4, * but this could be also path_by_shm p1 [(p1,ha,p4)] p4, so the former one is redundant! *)inductive path_by_shm':: "t_state \<Rightarrow> t_process \<Rightarrow> t_edge_shm list \<Rightarrow> t_process \<Rightarrow> bool"where pbs1': "p \<in> current_procs s \<Longrightarrow> path_by_shm' s p [] p"| pbs2': "\<lbrakk>path_by_shm' s p path p'; one_flow_shm s h p' p''; p'' \<notin> set (map Fst path); h \<notin> set (map Snd path)\<rbrakk> \<Longrightarrow> path_by_shm' s p ((p', h, p'')# path) p''"lemma pbs_prop10: "\<lbrakk>path_by_shm s p path p'; one_flow_shm s h p' p''; valid s\<rbrakk> \<Longrightarrow> \<exists>path'. path_by_shm s p path' p''"apply (case_tac "p'' \<in> set (map Fst path)")apply (drule_tac pb = p'' in pbs_prop6, simp+)apply ((erule exE|erule conjE)+, rule_tac x = pathab in exI, simp)apply (rule_tac x = "(p', h, p'') # path" in exI)apply (erule pbs2, simp+)donelemma pbs'_imp_pbs[rule_format]: "path_by_shm' s p path p' \<Longrightarrow> valid s \<longrightarrow> (\<exists> path'. path_by_shm s p path' p')"apply (erule path_by_shm'.induct)apply (rule impI, rule_tac x = "[]" in exI, simp add:pbs1)apply (rule impI, clarsimp)apply (erule pbs_prop10, simp+)donelemma pbs_imp_pbs'[rule_format]: "path_by_shm s p path p' \<Longrightarrow> valid s \<longrightarrow> (\<exists> path'. path_by_shm' s p path' p')"apply (erule path_by_shm.induct)apply (rule impI, rule_tac x = "[]" in exI, erule pbs1')apply (rule impI, simp, erule exE) (*apply ( erule exE, case_tac "h \<in> set (map Snd path)")apply (drule_tac s = s and p = p and p' = p' in pbs_prop9, simp+) deferapply (rule_tac x = "(p', h, p'') # path'" in exI)apply (erule pbs2', simp+) apply ((erule exE|erule conjE)+)apply (rule_tac x = "(pa, h, p'') # patha" in exI)apply (erule pbs2', auto simp:one_flow_shm_def)done*)sorrylemma pbs'_eq_pbs: "valid s \<Longrightarrow> (\<exists> path'. path_by_shm' s p path' p') = (\<exists> path. path_by_shm s p path p')"by (rule iffI, auto intro:pbs_imp_pbs' pbs'_imp_pbs)definition flow_by_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"where "flow_by_shm s p p' \<equiv> \<exists> path. path_by_shm s p path p'"lemma flow_by_shm_intro': "valid s \<Longrightarrow> flow_by_shm s p p' = (\<exists> path. path_by_shm' s p path p')"by (auto simp:flow_by_shm_def pbs'_eq_pbs)lemma one_step_flows: "\<lbrakk>one_flow_shm s h p p'; valid s\<rbrakk> \<Longrightarrow> flow_by_shm s p p'"by (drule one_step_path, auto simp:flow_by_shm_def)lemma flow_by_shm_trans: "\<lbrakk>flow_by_shm s p p'; flow_by_shm s p' p''; valid s\<rbrakk> \<Longrightarrow> flow_by_shm s p p''"by (auto simp:flow_by_shm_def intro!:path_by_shm_trans)lemma flow_by_shm_intro1_prop: "\<not> flow_by_shm s p p \<Longrightarrow> p \<notin> current_procs s"by (auto dest:path_by_shm.intros(1) simp:flow_by_shm_def)lemma flow_by_shm_intro1: "p \<in> current_procs s \<Longrightarrow> flow_by_shm s p p"by (auto dest:path_by_shm.intros(1) simp:flow_by_shm_def)lemma flow_by_shm_intro2: "\<lbrakk>flow_by_shm s p p'; one_flow_shm s h p' p''; valid s\<rbrakk> \<Longrightarrow> flow_by_shm s p p''"by (auto intro:flow_by_shm_trans dest:one_step_flows)lemma flow_by_shm_intro3: "\<lbrakk>flow_by_shm s p from; (from, SHM_RDWR) \<in> procs_of_shm s h; (to, flag) \<in> procs_of_shm s h; from \<noteq> to; valid s\<rbrakk> \<Longrightarrow> flow_by_shm s p to"apply (rule flow_by_shm_intro2)by (auto simp:one_flow_shm_def)lemma flow_by_shm_intro4: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> flow_by_shm s p p"by (drule procs_of_shm_prop2, simp, simp add:flow_by_shm_intro1)lemma flow_by_shm_intro5: "\<lbrakk>(from, SHM_RDWR) \<in> procs_of_shm s h; (to,flag) \<in> procs_of_shm s h; valid s; from \<noteq> to\<rbrakk> \<Longrightarrow> flow_by_shm s from to"apply (rule_tac p' = "from" and h = h in flow_by_shm_intro2)apply (rule flow_by_shm_intro1, simp add:procs_of_shm_prop2)apply (simp add:one_flow_shm_def, rule_tac x = flag in exI, auto)donelemma flow_by_shm_intro6: "path_by_shm s p path p' \<Longrightarrow> flow_by_shm s p p'"by (auto simp:flow_by_shm_def)(********* simpset for inductive Info_flow_shm **********)lemma path_by_shm_detach1_aux: "path_by_shm s' pa path pb \<Longrightarrow> valid (Detach p h # s) \<and> (s' = Detach p h # s) \<longrightarrow> \<not> edge_related path p h \<and> path_by_shm s pa path pb"apply (erule path_by_shm.induct, simp)apply (rule impI, rule path_by_shm.intros(1), simp+)by (auto simp:one_flow_shm_def split:if_splits intro:path_by_shm_intro3)lemma path_by_shm_detach1: "\<lbrakk>path_by_shm (Detach p h # s) pa path pb; valid (Detach p h # s)\<rbrakk> \<Longrightarrow> \<not> edge_related path p h \<and> path_by_shm s pa path pb"by (auto dest:path_by_shm_detach1_aux)lemma path_by_shm_detach2_aux[rule_format]: "path_by_shm s pa path pb \<Longrightarrow> valid (Detach p h # s) \<and> \<not> edge_related path p h \<longrightarrow> path_by_shm (Detach p h # s) pa path pb"apply (induct rule:path_by_shm.induct)apply (rule impI, rule path_by_shm.intros(1), simp)apply (rule impI, erule conjE, simp split:if_splits)apply (rule path_by_shm.intros(2), simp)apply (simp add:one_flow_shm_detach)apply (rule impI, simp+)donelemma path_by_shm_detach2: "\<lbrakk>valid (Detach p h # s); \<not> edge_related path p h; path_by_shm s pa path pb\<rbrakk> \<Longrightarrow> path_by_shm (Detach p h # s) pa path pb"by (auto intro!:path_by_shm_detach2_aux)lemma path_by_shm_detach: "valid (Detach p h # s) \<Longrightarrow> path_by_shm (Detach p h # s) pa path pb = (\<not> edge_related path p h \<and> path_by_shm s pa path pb)"by (auto dest:path_by_shm_detach1 path_by_shm_detach2)lemma flow_by_shm_detach: "valid (Detach p h # s) \<Longrightarrow> flow_by_shm (Detach p h # s) pa pb = (\<exists> path. \<not> edge_related path p h \<and> path_by_shm s pa path pb)"by (auto dest:path_by_shm_detach simp:flow_by_shm_def)lemma path_by_shm'_attach1_aux: "path_by_shm' s' pa path pb \<Longrightarrow> valid s' \<and> (s' = Attach p h flag # s) \<longrightarrow> (path_by_shm' s pa path pb) \<or> (\<exists> path1 path2 p'. path_by_shm' s pa path1 p' \<and> path_by_shm' s p path2 pb \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path = path2 @ [(p', h, p)] @ path1 ) \<or> (\<exists> path1 path2 p' flag'. path_by_shm' s pa path1 p \<and> path_by_shm' s p' path2 pb \<and> (p', flag') \<in> procs_of_shm s h \<and> path = path2 @ [(p, h, p')] @ path1 \<and> flag = SHM_RDWR)"apply (erule path_by_shm'.induct)apply (simp, rule impI, rule pbs1', simp)apply (rule impI, erule impE, clarsimp)apply (erule disjE)apply (clarsimp simp:one_flow_shm_attach split:if_splits)apply (erule disjE, clarsimp)apply (erule_tac x = path in allE, clarsimp)apply (erule impE, rule pbs1', erule procs_of_shm_prop2, erule vd_cons, simp)apply (erule disjE, clarsimp)apply (rule_tac x = path in exI, rule_tac x = "[]" in exI, rule_tac x = p' in exI, simp)apply (rule pbs1', drule vt_grant_os, clarsimp)apply (drule_tac p = pa and p' = p' and p'' = p'' in pbs2', simp+)apply (drule_tac p = pa and p' = p' and p'' = p'' in pbs2', simp+)apply (erule disjE)apply ((erule exE|erule conjE)+, clarsimp split:if_splits simp:one_flow_shm_attach)apply (clarsimp simp:one_flow_shm_attach split:if_splits)apply (erule disjE, clarsimp)apply (clarsimp)apply (erule conjE)+apply (erule conjE, clarsimp simp only:one_flow_shm_attach split:if_splits)apply simplemma path_by_shm_attach1_aux: "path_by_shm s' pa path pb \<Longrightarrow> valid s' \<and> (s' = Attach p h flag # s) \<longrightarrow> path_by_shm s pa path pb \<or> (if (pa = p \<and> flag = SHM_RDWR) then \<exists> p' flagb path'. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' path' pb \<and> path = path' @ [(p, h, p')] else if (pb = p) then \<exists> p' path'. path_by_shm s pa path' p' \<and> path = (p', h, p) # path' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h else (\<exists> p' flag' patha pathb. path_by_shm s pa patha p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> path_by_shm s p' pathb pb \<and> path = pathb @ [(p, h, p')] @ patha) \<or> (\<exists> p' patha pathb. path_by_shm s pa patha p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s p pathb pb \<and> path = pathb @ [(p', h, p)] @ patha))"proof (induct rule:path_by_shm.induct) case (pbs1 proc \<tau>) show ?case proof (rule impI) assume pre: "valid \<tau> \<and> \<tau> = Attach p h flag # s" from pbs1 pre have "proc \<in> current_procs s" by simp thus "path_by_shm s proc [] proc \<or> (if proc = p \<and> flag = SHM_RDWR then \<exists>p' flagb path'. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' path' proc \<and> [] = path' @ [(p, h, p')] else if proc = p then \<exists>p' path'. path_by_shm s proc path' p' \<and> [] = (p', h, p) # path' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h else (\<exists>p' flag' patha pathb. path_by_shm s proc patha p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> path_by_shm s p' pathb proc \<and> [] = pathb @ [(p, h, p')] @ patha) \<or> (\<exists>p' patha pathb. path_by_shm s proc patha p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s p pathb proc \<and> [] = pathb @ [(p', h, p)] @ patha))" by (auto intro:path_by_shm.intros) qednext case (pbs2 \<tau> pa path pb h' pc) thus ?case proof (rule_tac impI) assume p1:"path_by_shm \<tau> pa path pb" and p2: "valid \<tau> \<and> \<tau> = Attach p h flag # s \<longrightarrow> path_by_shm s pa path pb \<or> (if pa = p \<and> flag = SHM_RDWR then \<exists>p' flagb path'. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' path' pb \<and> path = path' @ [(p, h, p')] else if pb = p then \<exists>p' path'. path_by_shm s pa path' p' \<and> path = (p', h, p) # path' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h else (\<exists>p' flag' pathaa pathb. path_by_shm s pa pathaa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> path_by_shm s p' pathb pb \<and> path = pathb @ [(p, h, p')] @ pathaa) \<or> (\<exists>p' pathaa pathb. path_by_shm s pa pathaa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s p pathb pb \<and> path = pathb @ [(p', h, p)] @ pathaa))" and p3: "one_flow_shm \<tau> h' pb pc" and p4: "valid \<tau> \<and> \<tau> = Attach p h flag # s" from p2 and p4 have p2': " path_by_shm s pa path pb \<or> (if pa = p \<and> flag = SHM_RDWR then \<exists>p' flagb path'. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' path' pb \<and> path = path' @ [(p, h, p')] else if pb = p then \<exists>p' path'. path_by_shm s pa path' p' \<and> path = (p', h, p) # path' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h else (\<exists>p' flag' pathaa pathb. path_by_shm s pa pathaa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> path_by_shm s p' pathb pb \<and> path = pathb @ [(p, h, p')] @ pathaa) \<or> (\<exists>p' pathaa pathb. path_by_shm s pa pathaa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s p pathb pb \<and> path = pathb @ [(p', h, p)] @ pathaa))" by (erule_tac impE, simp) from p4 have p5: "valid s" and p6: "os_grant s (Attach p h flag)" by (auto intro:vd_cons dest:vt_grant_os) from p6 have "p \<in> current_procs s" by simp hence p7:"path_by_shm s p [] p" by (erule_tac path_by_shm.intros) from p3 p4 have p8: "if (h' = h) then (pb = p \<and> pc \<noteq> p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pc, flagb) \<in> procs_of_shm s h)) \<or> (pc = p \<and> pb \<noteq> p \<and> (pb, SHM_RDWR) \<in> procs_of_shm s h) \<or> (one_flow_shm s h pb pc) else one_flow_shm s h' pb pc" by (auto simp add:one_flow_shm_attach) (* have "\<And> flagb. (pc, flagb) \<in> procs_of_shm s h \<Longrightarrow> \<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' [] pc" apply (rule_tac x= pc in exI, rule_tac x = flagb in exI, frule procs_of_shm_prop2) by (simp add:p5, simp add:path_by_shm.intros(1)) hence p10: "\<not> path_by_shm s p path pc \<Longrightarrow> (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' pc) \<or> path_by_shm s pa pc" using p2' p7 p8 p5 by (auto split:if_splits dest:path_by_shm.intros(2)) (* apply (rule_tac x = pb in exI, simp add:one_flow_flows, rule_tac x = flagb in exI, simp)+ *) *) from p1 have a0: "(path = []) = (pa = pb)" using pbs_prop2 by simp have a1:"\<lbrakk>pa = p; flag = SHM_RDWR; \<not> path_by_shm s pa path pb\<rbrakk> \<Longrightarrow> \<exists>p' flagb path'. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' path' pb \<and> path = path' @ [(p, h, p')]" using p2' by auto have b1: "\<lbrakk>pa = p; flag = SHM_RDWR; \<not> path_by_shm s pa path pc\<rbrakk> \<Longrightarrow> \<exists>p' flagb path'. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' path' pc \<and> (pb, h', pc) # path = path' @ [(p, h, p')]" using p8 a1 p7 p5 a0 apply (auto split:if_splits elim:path_by_shm_intro4) apply (rule_tac x = pb in exI, rule conjI, rule_tac x = SHM_RDWR in exI, simp) apply (rule_tac x = pc in exI, rule conjI, rule_tac x = flagb in exI, simp) apply (rule_tac x = "[]" in exI, rule conjI)apply (erule path_by_shm_intro4, simp) apply (case_tac "path_by_shm s pa path pb", simp) defer apply (drule a1, simp+, clarsimp) apply (rule conjI, rule_tac x = flagb in exI, simp) apply (rule path_by_shm_ using p2' p8 p5 apply (auto split:if_splits dest!:pbs_prop2' simp:path_by_shm_intro4) apply (drule pbs_prop2', simp) apply (erule_tac x = pc in allE, simp add:path_by_shm_intro4) apply (drule_tac x = "pc" in allE) apply simp sorry moreover have "pc = p \<Longrightarrow> (\<exists>p' path'. path_by_shm s pa path' p' \<and> (pb, h', pc) # path = path' @ [(p', h, p)] \<and> (p', SHM_RDWR) \<in> procs_of_shm s h) \<or> (path_by_shm s pa path pc \<and> \<not> edge_related path p h)" using p2' p7 p8 p5 sorry (* apply (auto split:if_splits intro:path_by_shm_intro3 simp:one_flow_shm_def) *) moreover have "\<lbrakk>pc \<noteq> p; pa \<noteq> p \<or> flag \<noteq> SHM_RDWR\<rbrakk> \<Longrightarrow> (\<exists>p' flag' pathaa pathb. path_by_shm s pa pathaa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> path_by_shm s p' pathb pc \<and> (pb, h', pc) # path = pathaa @ [(p, h, p')] @ pathb) \<or> (\<exists>p' pathaa pathb. path_by_shm s pa pathaa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s p pathb pc \<and> (pb, h', pc) # path = pathaa @ [(p', h, p)] @ pathb) \<or> (path_by_shm s pa path pc \<and> \<not> edge_related path p h)" using p2' p7 p8 p5 (* apply (auto split:if_splits intro:path_by_shm_intro3 simp:one_flow_shm_def) apply (rule_tac x = pc in exI, simp add:path_by_shm_intro4) apply (rule_tac x = flagb in exI, simp) done *) sorry ultimately show "if (pb, h', pc) # path = [] then pa = pc \<and> pa \<in> current_procs s else path_by_shm s pa ((pb, h', pc) # path) pc \<and> \<not> edge_related ((pb, h', pc) # path) p h \<or> (if pa = p \<and> flag = SHM_RDWR then \<exists>p' flagb path'. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' path' pc \<and> (pb, h', pc) # path = path' @ [(p, h, p')] else if pc = p then \<exists>p' path'. path_by_shm s pa path' p' \<and> (pb, h', pc) # path = (p', h, p) # path' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h else (\<exists>p' flag' pathaa pathb. path_by_shm s pa pathaa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> path_by_shm s p' pathb pc \<and> (pb, h', pc) # path = pathb @ [(p, h, p')] @ pathaa) \<or> (\<exists>p' pathaa pathb. path_by_shm s pa pathaa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s p pathb pc \<and> (pb, h', pc) # path = pathb @ [(p', h, p)] @ pathaa))" apply (auto split:if_splits) using p7 by auto qedqedlemma path_by_shm_attach1: "\<lbrakk>valid (Attach p h flag # s); path_by_shm (Attach p h flag # s) pa pb\<rbrakk> \<Longrightarrow> (if path_by_shm s pa pb then True else (if (pa = p \<and> flag = SHM_RDWR) then (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' pb) else if (pb = p) then (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s pa p') else (\<exists> p' flag'. path_by_shm s pa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> path_by_shm s p' pb) \<or> (\<exists> p'. path_by_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s p pb) ) )"apply (drule_tac p = p and h = h and flag = flag in path_by_shm_attach1_aux)by autolemma path_by_shm_attach_aux[rule_format]: "path_by_shm s pa pb \<Longrightarrow> valid (Attach p h flag # s) \<longrightarrow> path_by_shm (Attach p h flag # s) pa pb"apply (erule path_by_shm.induct)apply (rule impI, rule path_by_shm.intros(1), simp)apply (rule impI, simp, rule_tac h = ha in path_by_shm.intros(2), simp)apply (auto simp add:one_flow_shm_simps)donelemma path_by_shm_attach2: "\<lbrakk>valid (Attach p h flag # s); if path_by_shm s pa pb then True else (if (pa = p \<and> flag = SHM_RDWR) then (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' pb) else if (pb = p) then (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s pa p') else (\<exists> p' flag'. path_by_shm s pa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> path_by_shm s p' pb) \<or> (\<exists> p'. path_by_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s p pb))\<rbrakk> \<Longrightarrow> path_by_shm (Attach p h flag # s) pa pb"apply (frule vt_grant_os, frule vd_cons)apply (auto split:if_splits intro:path_by_shm_intro3 simp:one_flow_shm_def intro:path_by_shm_attach_aux)apply (rule_tac p' = p' in Info_flow_trans)apply (rule_tac p' = p and h = h in path_by_shm.intros(2))apply (rule path_by_shm.intros(1), simp)apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def)apply (rule conjI, rule notI, simp, rule_tac x = flagb in exI, simp)apply (simp add:path_by_shm_attach_aux)apply (rule_tac p' = p' in Info_flow_trans)apply (rule_tac p' = p in Info_flow_trans)apply (simp add:path_by_shm_attach_aux)apply (rule_tac p' = p and h = h in path_by_shm.intros(2))apply (rule path_by_shm.intros(1), simp)apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def)apply (rule conjI, rule notI, simp, rule_tac x = flag' in exI, simp)apply (simp add:path_by_shm_attach_aux)apply (rule_tac p' = p in Info_flow_trans)apply (rule_tac p' = p' in Info_flow_trans)apply (simp add:path_by_shm_attach_aux)apply (rule_tac p' = p' and h = h in path_by_shm.intros(2))apply (rule path_by_shm.intros(1), simp add:procs_of_shm_prop2)apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def)apply (rule notI, simp)apply (simp add:path_by_shm_attach_aux)apply (rule_tac p' = p in Info_flow_trans)apply (rule_tac p' = p' in Info_flow_trans)apply (simp add:path_by_shm_attach_aux)apply (rule_tac p' = p' and h = h in path_by_shm.intros(2))apply (rule path_by_shm.intros(1), simp add:procs_of_shm_prop2)apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def)apply (rule notI, simp)apply (simp add:path_by_shm_attach_aux)donelemma path_by_shm_attach: "valid (Attach p h flag # s) \<Longrightarrow> path_by_shm (Attach p h flag # s) = (\<lambda> pa pb. path_by_shm s pa pb \<or> (if (pa = p \<and> flag = SHM_RDWR) then (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' pb) else if (pb = p) then (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s pa p') else (\<exists> p' flag'. path_by_shm s pa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> path_by_shm s p' pb) \<or> (\<exists> p'. path_by_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s p pb) ) )"apply (rule ext, rule ext, rule iffI)apply (drule_tac pa = pa and pb = pb in path_by_shm_attach1, simp)apply (auto split:if_splits)[1]apply (drule_tac pa = pa and pb = pb in path_by_shm_attach2)apply (auto split:if_splits)donelemma info_flow_shm_detach: "valid (Detach p h # s) \<Longrightarrow> info_flow_shm (Detach p h # s) = (\<lambda> pa pb. self_shm s pa pb \<or> ((p = pa \<or> p = pb) \<and> (\<exists> h'. h' \<noteq> h \<and> one_flow_shm s h' pa pb)) \<or> (pa \<noteq> p \<and> pb \<noteq> p \<and> info_flow_shm s pa pb) )"apply (rule ext, rule ext, frule vt_grant_os)by (auto simp:info_flow_shm_def one_flow_shm_def)lemma info_flow_shm_deleteshm: "valid (DeleteShM p h # s) \<Longrightarrow> info_flow_shm (DeleteShM p h # s) = (\<lambda> pa pb. self_shm s pa pb \<or> (\<exists> h'. h' \<noteq> h \<and> one_flow_shm s h' pa pb) )"apply (rule ext, rule ext, frule vt_grant_os)by (auto simp:info_flow_shm_def one_flow_shm_def)lemma info_flow_shm_clone: "valid (Clone p p' fds shms # s) \<Longrightarrow> info_flow_shm (Clone p p' fds shms # s) = (\<lambda> pa pb. (pa = p' \<and> pb = p') \<or> (pa = p' \<and> pb \<noteq> p' \<and> (\<exists> h \<in> shms. one_flow_shm s h p pb)) \<or> (pb = p' \<and> pa \<noteq> p' \<and> (\<exists> h \<in> shms. one_flow_shm s h pa p)) \<or> (pa \<noteq> p' \<and> pb \<noteq> p' \<and> info_flow_shm s pa pb))"apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons, clarsimp)apply (frule_tac p = p' in procs_of_shm_prop2', simp)sorry (*apply (auto simp:info_flow_shm_def one_flow_shm_def)done *)lemma info_flow_shm_execve: "valid (Execve p f fds # s) \<Longrightarrow> info_flow_shm (Execve p f fds # s) = (\<lambda> pa pb. (pa = p \<and> pb = p) \<or> (pa \<noteq> p \<and> pb \<noteq> p \<and> info_flow_shm s pa pb) )"apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons)by (auto simp:info_flow_shm_def one_flow_shm_def)lemma info_flow_shm_kill: "valid (Kill p p' # s) \<Longrightarrow> info_flow_shm (Kill p p' # s) = (\<lambda> pa pb. pa \<noteq> p' \<and> pb \<noteq> p' \<and> info_flow_shm s pa pb )"apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons)by (auto simp:info_flow_shm_def one_flow_shm_def)lemma info_flow_shm_exit: "valid (Exit p # s) \<Longrightarrow> info_flow_shm (Exit p # s) = (\<lambda> pa pb. pa \<noteq> p \<and> pb \<noteq> p \<and> info_flow_shm s pa pb )"apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons)by (auto simp:info_flow_shm_def one_flow_shm_def)lemma info_flow_shm_other: "\<lbrakk>valid (e # s); \<forall> p h flag. e \<noteq> Attach p h flag; \<forall> p h. e \<noteq> Detach p h; \<forall> p h. e \<noteq> DeleteShM p h; \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms; \<forall> p f fds. e \<noteq> Execve p f fds; \<forall> p p'. e \<noteq> Kill p p'; \<forall> p. e \<noteq> Exit p \<rbrakk> \<Longrightarrow> info_flow_shm (e # s) = info_flow_shm s"apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons)apply (case_tac e, auto simp:info_flow_shm_def one_flow_shm_def dest:procs_of_shm_prop2)apply (erule_tac x = h in allE, simp)apply (drule procs_of_shm_prop1, auto)done(*lemma info_flow_shm_prop1: "\<lbrakk>info_flow_shm s p p'; p \<noteq> p'; valid s\<rbrakk> \<Longrightarrow> \<exists> h h' flag. (p, SHM_RDWR) \<in> procs_of_shm s h \<and> (p', flag) \<in> procs_of_shm s h'"by (induct rule: info_flow_shm.induct, auto)lemma info_flow_shm_cases: "\<lbrakk>info_flow_shm \<tau> pa pb; \<And>p s. \<lbrakk>s = \<tau> ; pa = p; pb = p; p \<in> current_procs s\<rbrakk> \<Longrightarrow> P; \<And>s p p' h p'' flag. \<lbrakk>s = \<tau>; pa = p; pb = p''; info_flow_shm s p p'; (p', SHM_RDWR) \<in> procs_of_shm s h; (p'', flag) \<in> procs_of_shm s h\<rbrakk>\<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"by (erule info_flow_shm.cases, auto)definition one_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"where "one_flow_shm s p p' \<equiv> p \<noteq> p' \<and> (\<exists> h flag. (p, SHM_RDWR) \<in> procs_of_shm s h \<and> (p', flag) \<in> procs_of_shm s h)"inductive flows_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"where "p \<in> current_procs s \<Longrightarrow> flows_shm s p p"| "\<lbrakk>flows_shm s p p'; one_flow_shm s p' p''\<rbrakk> \<Longrightarrow> flows_shm s p p''"definition attached_procs :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_process set"where "attached_procs s h \<equiv> {p. \<exists> flag. (p, flag) \<in> procs_of_shm s h}"definition flowed_procs:: "t_state \<Rightarrow> t_shm \<Rightarrow> t_process set"where "flowed_procs s h \<equiv> {p'. \<exists> p \<in> attached_procs s h. flows_shm s p p'}"inductive flowed_shm:: "t_state \<Rightarrow> t_process \<Rightarrow> t_shm set"fun Info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process set"where "Info_flow_shm [] = (\<lambda> p. {p'. flows_shm [] p p'})"| "Info_flow_shm (Attach p h flag # s) = (\<lambda> p'. if (p' = p) then flowed_procs s h else if () "lemma info_flow_shm_attach: "valid (Attach p h flag # s) \<Longrightarrow> info_flow_shm (Attach p h flag # s) = (\<lambda> pa pb. (info_flow_shm s pa pb) \<or> (if (pa = p) then (if (flag = SHM_RDWR) then (\<exists> flag. (pb, flag) \<in> procs_of_shm s h) else (pb = p)) else (if (pb = p) then (pa, SHM_RDWR) \<in> procs_of_shm s h else info_flow_shm s pa pb)) )"apply (frule vd_cons, frule vt_grant_os, rule ext, rule ext)apply (case_tac "info_flow_shm s pa pb", simp)thm info_flow_shm.casesapply (auto split:if_splits intro:info_flow_shm.intros elim:info_flow_shm_cases)apply (erule info_flow_shm_cases, simp, simp split:if_splits)apply (rule_tac p = pa and p' = p' in info_flow_shm.intros(2), simp+)apply (rule notI, erule info_flow_shm.cases, simp+)pr 5*)lemmas info_flow_shm_simps = info_flow_shm_other (* info_flow_shm_attach *) info_flow_shm_detach info_flow_shm_deleteshm info_flow_shm_clone info_flow_shm_execve info_flow_shm_kill info_flow_shm_exitendend