theory tainted_vs_tainted_s

imports Main rc_theory os_rc deleted_prop tainted obj2sobj_prop source_prop all_sobj_prop 

begin

context tainting_s_complete begin

lemma t2ts[rule_format]: 

  "obj \<in> tainted s \<Longrightarrow> obj2sobj s obj \<in> tainted_s "  

proof (induct rule:tainted.induct)

  case (t_init obj) 

  assume seed: "obj \<in> seeds" 

  hence"exists [] obj" by (drule_tac seeds_in_init, case_tac obj, auto)

  thus ?case using seed by (simp add:ts_init obj2sobj_nil_init)

next

  case (t_clone p s p') 

  assume p1: "Proc p \<in> tainted s" 

  and p2: "obj2sobj s (Proc p) \<in> tainted_s"

  and p3: "valid (Clone p p' # s)"

  from p3 have os: "os_grant s (Clone p p')" and rc: "rc_grant s (Clone p p')"

    and vs: "valid s" by (auto dest:valid_cons valid_os valid_rc)

  from os have exp: "exists s (Proc p)" by (simp add:os_grant.simps)

  from exp obtain r fr pt u sp where sproc: "cp2sproc s p = Some (r,fr,pt,u)"

    and srp: "source_proc s p = Some sp" using vs

    apply (simp del:cp2sproc.simps)

    by (frule current_proc_has_sproc, simp, frule current_proc_has_srp, simp, blast)

  with exp all_sobjs_I[where obj = "Proc p" and s = s] vs

  have "obj2sobj (Clone p p' # s) (Proc p') = SProc (r,fr,clone_type_aux r pt, u) (Some sp)"

    using sproc srp p3

    by (simp add:obj2sobj.simps cp2sproc_clone del:cp2sproc.simps)

  moreover have "(r, Proc_type pt, CREATE) \<in> compatible" using rc sproc

    by (auto split:option.splits)

  moreover have "SProc (r, fr, pt, u) (Some sp) \<in> tainted_s" using p2 sproc srp

    by simp

  ultimately show ?case by (auto intro:ts_clone) 

next

  case (t_exec f s p)

  assume p1: "File f \<in> tainted s"

  and p2: "obj2sobj s (File f) \<in> tainted_s"

  and p3: "valid (Execute p f # s)"

  from p3 have os: "os_grant s (Execute p f)" and rc: "rc_grant s (Execute p f)"

    and vs: "valid s" by (auto dest:valid_cons valid_os valid_rc)

  from os have exp: "exists s (Proc p)" and exf: "exists s (File f)" by auto 

  from exp obtain r fr pt u where sproc: "cp2sproc s p = Some (r,fr,pt,u)"

    using vs by (auto simp del:cp2sproc.simps dest!:current_proc_has_sproc)

  with exp all_sobjs_I[where obj = "Proc p" and s = s] vs

  have SP: "SProc (r,fr,pt,u) (source_proc s p) \<in> all_sobjs"

    by (auto simp:obj2sobj.simps)

  from exf obtain ft sd where etype: "etype_of_file s f = Some ft"

    and srdir: "source_dir s f = Some sd" using vs

    by (simp, drule_tac current_file_has_sd, auto dest:current_file_has_etype)

  with p2 obtain srf where TF: "SFile (ft, sd) srf \<in> tainted_s" 

    by (auto simp:obj2sobj.simps split:if_splits)

  from sproc srdir have "u \<in> init_users" and "sd \<in> init_files" using vs

    by (auto simp:obj2sobj.simps cp2sproc.simps 

            intro:source_dir_in_init owner_in_users 

            split:option.splits)

  then obtain nr nfr where nrole: "exec_role_aux r sd u = Some nr" 

    and nfrole: "erole_functor init_file_forcedrole InheritUpMixed sd = Some nfr"

    by (frule_tac r = r in exec_role_some, simp, frule_tac efffrole_sdir_some, auto)

  hence "cp2sproc (Execute p f # s) p = Some (nr, nfr, exec_type_aux r pt, u)" 

    using p3 srdir sproc by (simp add:cp2sproc_exec)

  with nrole nfrole TF SP rc sproc etype

  show ?case 

    by (auto simp:obj2sobj.simps cp2sproc.simps intro!:ts_exec1 split:option.splits)

next

  case (t_cfile p s f)

  assume p1: "Proc p \<in> tainted s" and p2: "obj2sobj s (Proc p) \<in> tainted_s"

    and p3: "valid (CreateFile p f # s)"

  from p3 have os: "os_grant s (CreateFile p f)" and rc: "rc_grant s (CreateFile p f)"

    and vs: "valid s" by (auto dest:valid_cons valid_os valid_rc)

  from os obtain pf where parent: "parent f = Some pf" and exp: "exists s (Proc p)"

    and expf: "exists s (File pf)" by auto

  from exp obtain r fr pt u where sproc: "cp2sproc s p = Some (r,fr,pt,u)"

    using vs by (auto simp del:cp2sproc.simps dest!:current_proc_has_sproc)

  with p2 have TP: "SProc (r,fr,pt,u) (source_proc s p) \<in> tainted_s"

    by (auto simp:obj2sobj.simps cp2sproc.simps)

  from expf obtain pft sd where etype: "etype_of_file s pf = Some pft"

    and srdir: "source_dir s pf = Some sd" using vs

    by (simp, drule_tac current_file_has_sd, auto dest:current_file_has_etype)

  with expf all_sobjs_I[where obj = "File pf" and s = s] vs

  obtain srpf where SF: "SFile (pft, sd) srpf \<in> all_sobjs"

    by (auto simp:obj2sobj.simps cp2sproc.simps split:if_splits)

  show ?case using etype srdir p3 parent os

    apply (auto simp:source_dir_simps init_notin_curf_deleted obj2sobj.simps split:option.splits

               dest!:current_file_has_etype')

    apply (case_tac "default_fd_create_type r")

    using SF TP rc sproc

    apply (rule_tac sf = srpf in ts_cfd',

           auto simp:etype_of_file_def etype_aux_prop3 obj2sobj.simps cp2sproc.simps

               split:option.splits) [1]

    using SF TP rc sproc

    apply (rule_tac sf = srpf in ts_cfd)

    apply (auto simp:etype_of_file_def etype_aux_prop4 cp2sproc.simps split:option.splits)

    done

next

  case (t_cipc p s i)

  assume p1: "Proc p \<in> tainted s" and p2: "obj2sobj s (Proc p) \<in> tainted_s"

    and p3: "valid (CreateIPC p i # s)"

  from p3 have os: "os_grant s (CreateIPC p i)" and rc: "rc_grant s (CreateIPC p i)"

    and vs: "valid s" by (auto dest:valid_cons valid_os valid_rc)

  from os have exp: "exists s (Proc p)" by simp

  from exp obtain r fr pt u where sproc: "cp2sproc s p = Some (r,fr,pt,u)"

    using vs by (auto simp del:cp2sproc.simps dest!:current_proc_has_sproc)

  with p2 have TP: "SProc (r,fr,pt,u) (source_proc s p) \<in> tainted_s"

    by (auto simp:obj2sobj.simps cp2sproc.simps)

  show ?case using p3 sproc os rc TP 

    by (auto simp:ni_init_deled obj2sobj.simps cp2sproc.simps 

            split:option.splits intro!:ts_cipc)

next

  case (t_read f s p)

  assume p1: "File f \<in> tainted s" and p2: "obj2sobj s (File f) \<in> tainted_s"

    and p3: "valid (ReadFile p f # s)"

  from p3 have os: "os_grant s (ReadFile p f)" and rc: "rc_grant s (ReadFile p f)"

    and vs: "valid s" by (auto dest:valid_cons valid_os valid_rc)

  from os have exp: "exists s (Proc p)" and exf: "exists s (File f)" by auto 

  from exp obtain r fr pt u where sproc: "cp2sproc s p = Some (r,fr,pt,u)"

    using vs by (auto simp del:cp2sproc.simps dest!:current_proc_has_sproc)

  with exp all_sobjs_I[where obj = "Proc p" and s = s] vs

  have SP: "SProc (r,fr,pt,u) (source_proc s p) \<in> all_sobjs"

    by (auto simp:obj2sobj.simps)

  from exf obtain ft sd where etype: "etype_of_file s f = Some ft"

    and srdir: "source_dir s f = Some sd" using vs

    by (simp, drule_tac current_file_has_sd, auto dest:current_file_has_etype)

  with p2 obtain srf where TF: "SFile (ft, sd) srf \<in> tainted_s"

    by (auto simp:obj2sobj.simps cp2sproc.simps split:if_splits)

  show ?case using sproc SP TF rc etype 

    by (auto simp:obj2sobj.simps cp2sproc.simps 

            split:option.splits intro!:ts_read) 

next

  case (t_write p s f)

  assume p1: "Proc p \<in> tainted s" and p2: "obj2sobj s (Proc p) \<in> tainted_s"

    and p3: "valid (WriteFile p f # s)"

  from p3 have os: "os_grant s (WriteFile p f)" and rc: "rc_grant s (WriteFile p f)"

    and vs: "valid s" by (auto dest:valid_cons valid_os valid_rc)

  from os have exp: "exists s (Proc p)" and exf: "exists s (File f)" by auto 

  from exf obtain ft sd where etype: "etype_of_file s f = Some ft"

    and srdir: "source_dir s f = Some sd" using vs

    by (simp, drule_tac current_file_has_sd, auto dest:current_file_has_etype)

  from exp obtain r fr pt u where sproc: "cp2sproc s p = Some (r,fr,pt,u)"

    using vs by (auto simp del:cp2sproc.simps dest!:current_proc_has_sproc)

  with exp p2 have TP: "SProc (r,fr,pt,u) (source_proc s p) \<in> tainted_s"

    by (auto simp:obj2sobj.simps)

  from etype p3 have etype':"etype_of_file (WriteFile p f # s) f = Some ft"

    by (case_tac f, auto simp:etype_of_file_def)

  have SF: "obj2sobj s (File f) \<in> all_sobjs" using exf vs 

    by (rule_tac all_sobjs_I, simp+) 

  show ?case using sproc TP rc etype p3 srdir etype' SF

    by (auto simp:source_dir_simps obj2sobj.simps cp2sproc.simps

            split:option.splits intro!:ts_write) 

next

  case (t_send p s i)

  assume p1: "Proc p \<in> tainted s" and p2: "obj2sobj s (Proc p) \<in> tainted_s"

    and p3: "valid (Send p i # s)"

  from p3 have os: "os_grant s (Send p i)" and rc: "rc_grant s (Send p i)"

    and vs: "valid s" by (auto dest:valid_cons valid_os valid_rc)

  from os have exp: "exists s (Proc p)" and exi: "exists s (IPC i)" by auto 

  from exi obtain t where etype: "type_of_ipc s i = Some t" using vs

    by (simp, drule_tac current_ipc_has_type, auto)

  from exp obtain r fr pt u where sproc: "cp2sproc s p = Some (r,fr,pt,u)"

    using vs by (auto simp del:cp2sproc.simps dest!:current_proc_has_sproc)

  with exp p2 have TP: "SProc (r,fr,pt,u) (source_proc s p) \<in> tainted_s"

    by (auto simp:obj2sobj.simps cp2sproc.simps)

  have SI: "obj2sobj s (IPC i) \<in> all_sobjs" using exi vs

    by (simp add:all_sobjs_I del:obj2sobj.simps)

  show ?case using sproc TP rc etype p3 vs SI

    by (auto simp:obj2sobj.simps cp2sproc.simps 

            split:option.splits intro!:ts_send)

next

  case (t_recv i s p)

  assume p1: "IPC i \<in> tainted s" and p2: "obj2sobj s (IPC i) \<in> tainted_s"

    and p3: "valid (Recv p i # s)"

  from p3 have os: "os_grant s (Recv p i)" and rc: "rc_grant s (Recv p i)"

    and vs: "valid s" by (auto dest:valid_cons valid_os valid_rc)

  from os have exp: "exists s (Proc p)" and exi: "exists s (IPC i)" by auto 

  from exp obtain r fr pt u where sproc: "cp2sproc s p = Some (r,fr,pt,u)"

    using vs by (auto simp del:cp2sproc.simps dest!:current_proc_has_sproc)

  with exp all_sobjs_I[where obj = "Proc p" and s = s] vs

  have SP: "SProc (r,fr,pt,u) (source_proc s p) \<in> all_sobjs"

    by (auto simp:obj2sobj.simps)

  from exi obtain t where etype: "type_of_ipc s i = Some t"using vs

    by (simp, drule_tac current_ipc_has_type, auto)

  with p2 obtain sri where TI: "SIPC t sri \<in> tainted_s"

    by (auto simp:obj2sobj.simps split:if_splits)

  show ?case using sproc SP TI rc etype 

    by (auto simp:obj2sobj.simps cp2sproc.simps 

            split:option.splits intro!:ts_recv) 

next

  case (t_remain obj s e)

  from t_remain(1) have p5: "exists s obj" by (rule tainted_is_current)

  from t_remain(3) have os: "os_grant s e" and vs: "valid s" and rc: "rc_grant s e"

    by (auto dest:valid_os valid_cons valid_rc)

  show ?case

  proof (cases obj)

    case (File f)

    have "obj2sobj (e # s) (File f) = obj2sobj s (File f)"

    proof-

      have "etype_of_file (e # s) f = etype_of_file s f"

        using p5 os vs File t_remain(3,4)

        apply (case_tac e, auto simp:etype_of_file_def split:option.splits)

        by (auto dest:ancient_file_in_current intro!:etype_aux_prop)

      moreover have "source_dir (e # s) f = source_dir s f"

        using p5 os vs File t_remain(3,4)

        by (case_tac e, auto simp:source_dir_simps dest:source_dir_prop)

      ultimately show ?thesis using vs t_remain(4) File

        apply (auto simp:obj2sobj.simps cp2sproc.simps 

                   split:if_splits option.splits dest:not_deleted_cons_D)

        by (case_tac e, auto)

    qed

    with File t_remain(2) show ?thesis by simp

  next

    case (IPC i) 

    have "obj2sobj (e # s) (IPC i) = obj2sobj s (IPC i)" using p5 t_remain(3,4) os IPC

      by (case_tac e, auto simp:ni_init_deled ni_notin_curi obj2sobj.simps 

                          split:option.splits

                          dest!:current_proc_has_role')

    with IPC t_remain(2) show ?thesis by simp

  next

    case (Proc p) 

    show ?thesis 

    proof-

      have "\<And> f. e = Execute p f \<Longrightarrow> obj2sobj (e # s) (Proc p) \<in> tainted_s"

      proof-

        fix f

        assume ev: "e = Execute p f"

        show "obj2sobj (e # s) (Proc p) \<in> tainted_s"

        proof-

          from os ev have exp: "exists s (Proc p)" and exf: "exists s (File f)" by auto 

          from exp obtain r fr pt u where sproc: "cp2sproc s p = Some (r,fr,pt,u)"

            using vs by (auto simp del:cp2sproc.simps dest!:current_proc_has_sproc)

          with Proc t_remain(2) 

          have TP: "SProc (r,fr,pt,u) (source_proc s p) \<in> tainted_s"

            by (auto simp:obj2sobj.simps cp2sproc.simps)

          from exf obtain ft sd where etype: "etype_of_file s f = Some ft"

            and srdir: "source_dir s f = Some sd" using vs

            by (simp, drule_tac current_file_has_sd, auto dest:current_file_has_etype)

          with exf all_sobjs_I[where obj = "File f" and s = s] vs

          obtain srf where SF: "SFile (ft, sd) srf \<in> all_sobjs"

            by (auto simp:obj2sobj.simps split:if_splits) 

          from sproc srdir have "u \<in> init_users" and "sd \<in> init_files" using vs

            by (auto simp:obj2sobj.simps cp2sproc.simps

                    intro:source_dir_in_init owner_in_users split:option.splits)

          then obtain nr nfr where nrole: "exec_role_aux r sd u = Some nr" 

            and nfrole: "erole_functor init_file_forcedrole InheritUpMixed sd = Some nfr"

            by (frule_tac r = r in exec_role_some, simp, frule_tac efffrole_sdir_some, auto)

          hence "cp2sproc (Execute p f # s) p = Some (nr, nfr, exec_type_aux r pt, u)" 

            using t_remain(3) srdir sproc ev by (simp add:cp2sproc_exec)

          with nrole nfrole SF TP rc sproc etype ev

          show ?thesis

            by (auto simp:obj2sobj.simps cp2sproc.simps 

                   intro!:ts_exec2 split:option.splits)

        qed

      qed  moreover 

      have "\<And> r'. e = ChangeRole p r' \<Longrightarrow> obj2sobj (e # s) (Proc p) \<in> tainted_s"

      proof-

        fix r' 

        assume ev: "e = ChangeRole p r'"

        show "obj2sobj (e # s) (Proc p) \<in> tainted_s"

        proof-

          from os ev have exp: "exists s (Proc p)" by auto 

          from exp obtain r fr pt u where sproc: "cp2sproc s p = Some (r,fr,pt,u)"

            using vs by (auto simp del:cp2sproc.simps dest!:current_proc_has_sproc)

          with Proc t_remain(2)

          have TP: "SProc (r,fr,pt,u) (source_proc s p) \<in> tainted_s"

            by (auto simp:obj2sobj.simps cp2sproc.simps)

          with rc sproc ev show ?thesis 

            apply (simp add:obj2sobj.simps cp2sproc.simps split:option.splits)

            by (rule_tac ts_crole, simp+)

        qed

      qed  moreover 

      have "\<And> u'. e = ChangeOwner p u' \<Longrightarrow> obj2sobj (e # s) (Proc p) \<in> tainted_s"

      proof-

        fix u'

        assume ev: "e = ChangeOwner p u'"

        show "obj2sobj (e # s) (Proc p) \<in> tainted_s"

        proof-        

          from os ev have exp: "exists s (Proc p)" by auto 

          from exp obtain r fr pt u where sproc: "cp2sproc s p = Some (r,fr,pt,u)"

            using vs by (auto simp del:cp2sproc.simps dest!:current_proc_has_sproc)

          with Proc t_remain(2)

          have TP: "SProc (r,fr,pt,u) (source_proc s p) \<in> tainted_s"

            by (auto simp:obj2sobj.simps cp2sproc.simps)

          from os ev have uinit: "u' \<in> init_users" by simp

          then obtain nr where chown: "chown_role_aux r fr u' = Some nr" 

            by (auto dest:chown_role_some)

          hence nsproc:"cp2sproc (e#s) p = Some (nr,fr,chown_type_aux r nr pt, u')" 

            using sproc ev os

            by (auto split:option.splits t_role.splits 

                  simp del:currentrole.simps type_of_process.simps

                  simp add:obj2sobj.simps cp2sproc.simps 

                           chown_role_aux_valid chown_type_aux_valid)

          with rc sproc ev TP uinit chown

          show ?thesis

            by (auto simp:obj2sobj.simps cp2sproc.simps 

                   intro!:ts_chown split:option.splits)

        qed

      qed  moreover 

      have "\<lbrakk>\<forall> f. e \<noteq> Execute p f; \<forall> r. e \<noteq> ChangeRole p r; \<forall> u. e \<noteq> ChangeOwner p u\<rbrakk>

        \<Longrightarrow> obj2sobj (e # s) (Proc p) \<in> tainted_s"

        using t_remain(2,3,4) os p5 Proc

        by (case_tac e, auto simp add:obj2sobj.simps cp2sproc_simps np_notin_curp 

                             simp del:cp2sproc.simps  split:option.splits) 

      ultimately show ?thesis using Proc

        by (case_tac e, auto simp del:obj2sobj.simps) 

    qed

  qed

qed

end

context tainting_s_sound begin

lemma tainted_s'_eq1: "sobj \<in> tainted_s \<Longrightarrow> sobj \<in> tainted_s'"

apply (erule tainted_s.induct)

apply (auto elim:ts'_init ts'_exec1 ts'_exec2 ts'_cfd ts'_cfd' ts'_cipc ts'_read ts'_write ts'_recv ts'_send ts'_crole ts'_chown simp:all_sobjs'_eq)

by (simp add:clone_type_aux_def clone_type_unchange)

lemma tainted_s'_eq2: "sobj \<in> tainted_s' \<Longrightarrow> sobj \<in> tainted_s"

apply (erule tainted_s'.induct)

by (auto intro:ts_init ts_exec1 ts_exec2 ts_cfd ts_cfd' ts_cipc ts_read ts_write ts_recv ts_send ts_crole ts_chown ts_clone simp:all_sobjs'_eq)

lemma tainted_s'_eq: "(sobj \<in> tainted_s) = (sobj \<in> tainted_s')"

by (auto intro:iffI tainted_s'_eq1 tainted_s'_eq2)

(* cause sobj_source_eq_sobj may conflict with initp_intact, so remove it too. *) 

lemma ts2t_intact:

  "sobj \<in> tainted_s' \<Longrightarrow> \<exists> obj s. obj2sobj s obj = sobj \<and> obj \<in> tainted s \<and> 

                                 no_del_event s \<and> initp_intact s"

proof (induct rule:tainted_s'.induct)

  case (ts'_init obj)

  hence ex: "exists [] obj"

    apply (drule_tac seeds_in_init) 

    by (case_tac obj, simp+)

  have "obj2sobj [] obj = init_obj2sobj obj" using ex 

    by (simp add:obj2sobj_nil_init)

  moreover have "obj \<in> tainted []" using ts'_init by (simp add:t_init)

  moreover have "initp_intact []"

    by (auto simp:initp_intact_def obj2sobj.simps cp2sproc.simps split:option.splits)

  ultimately show ?case 

    by (rule_tac x = obj in exI, rule_tac x = "[]" in exI, simp+)

next

  case (ts'_exec1 t sd srf r fr pt u srp r' fr')

  then obtain f s  where TF: "(File f) \<in> tainted s" and vds: "valid s" 

    and "f \<in> current_files s \<and> obj2sobj s (File f) = SFile (t, sd) srf \<and> 

         no_del_event s \<and> initp_intact s" 

    apply (clarsimp, frule_tac obj2sobj_file)

    by (frule tainted_is_valid, frule tainted_is_current, auto)

  with ts'_exec1(3) obtain p s' where vds's: "valid (s' @ s)"

    and etype: "obj2sobj (s'@s) (File f) = SFile (t, sd) srf"

    and nodels': "no_del_event (s'@s)"

    and intacts': "initp_intact (s'@s)" 

    and ISP: "obj2sobj (s'@s) (Proc p) = SProc (r,fr,pt,u) srp"

    and exp: "p \<in> current_procs (s' @ s)"

    and exf: "f \<in> current_files (s' @ s)"

    apply (drule_tac s' =s and obj' = "File f" in all_sobjs_E0, auto)

    apply (frule_tac obj = "File f" in nodel_tainted_exists, simp)

    by (frule obj2sobj_proc, clarsimp)

  obtain ev \<tau> where ev: "ev = Execute (new_proc (s'@s)) f"

    and tau: "\<tau> = Clone p (new_proc (s'@s)) # (s' @ s)" by auto

  hence vs_tau:"valid \<tau>" using exp vds's by (auto intro:clone_event_no_limit)

  have valid: "valid (ev # \<tau>)"

  proof-

    have "os_grant \<tau> ev"

      using ev tau by (simp add:exf exp)

    moreover have "rc_grant \<tau> ev" 

      using ev tau ts'_exec1 ISP etype

      by (auto simp:etype_of_file_def cp2sproc.simps obj2sobj.simps

              split:if_splits option.splits)

    ultimately show ?thesis using vs_tau

      by (erule_tac vs_step, simp+)

  qed  moreover

  have "obj2sobj (ev # \<tau>) (Proc (new_proc (s'@s))) = 

        SProc (r', fr', exec_type_aux r pt, u) srp"

  proof-

    have "obj2sobj (s'@s) (Proc p) = SProc (r,fr,pt,u) srp" using ISP tau vs_tau

      by (auto split:option.splits simp:cp2sproc_simps obj2sobj.simps)

    hence "obj2sobj \<tau> (Proc (new_proc (s'@s))) = SProc (r,fr,pt,u) srp" using tau

      by (auto simp:obj2sobj.simps cp2sproc.simps pct_def clone_type_unchange 

              split:option.splits)

    moreover have "source_dir \<tau> f = Some sd" using vs_tau etype tau 

      by (auto simp:obj2sobj.simps source_dir_simps split:option.splits if_splits)

    ultimately show ?thesis using valid ts'_exec1(5) ts'_exec1(6) ev

      by (auto simp:cp2sproc_exec obj2sobj.simps split:option.splits)

  qed  moreover

  have "Proc (new_proc (s'@s)) \<in> tainted (ev # \<tau>)"

  proof-

    have "(File f) \<in> tainted \<tau>" using TF nodels' tau vs_tau

      by (drule_tac s = "Clone p (new_proc (s' @ s)) # s'" in t_remain_app,auto)

    thus ?thesis using ev valid

      by (drule_tac t_exec, simp+)

  qed  moreover

  have "no_del_event (ev # \<tau>)" using ev tau nodels' by simp 

  moreover have "initp_intact (ev#\<tau>)" using ev tau intacts' valid

    by (simp add:initp_intact_I_exec)

  ultimately show ?case

    apply (rule_tac x = "Proc (new_proc (s'@s))" in exI)

    by (rule_tac x = "ev#\<tau>" in exI, auto)

next

  case (ts'_exec2 r fr pt u srp t sd srf r' fr')

  then obtain p s where TP: "(Proc p) \<in> tainted s" and vds: "valid s" 

    and "p \<in> current_procs s \<and> obj2sobj s (Proc p) = SProc (r, fr, pt, u) srp \<and> 

         no_del_event s \<and> initp_intact s" 

    apply (clarsimp, frule_tac obj2sobj_proc)

    by (frule tainted_is_valid, frule tainted_is_current, auto)

  with ts'_exec2(3) obtain f s' where vds's: "valid (s' @ s)"

    and etype: "obj2sobj (s'@s) (File f) = SFile (t, sd) srf"

    and nodels': "no_del_event (s'@s)"

    and intacts': "initp_intact (s'@s)" 

    and ISP: "obj2sobj (s'@s) (Proc p) = SProc (r,fr,pt,u) srp"

    and exp: "p \<in> current_procs (s' @ s)"

    and exf: "f \<in> current_files (s' @ s)"

    apply (drule_tac s' =s and obj' = "Proc p" in all_sobjs_E0, auto)

    apply (frule_tac obj = "Proc p" in nodel_tainted_exists, simp)

    by (frule obj2sobj_file, clarsimp)

  obtain ev \<tau> where ev: "ev = Execute (new_proc (s'@s)) f"

    and tau: "\<tau> = Clone p (new_proc (s'@s)) # (s' @ s)" by auto

  hence vs_tau:"valid \<tau>" using exp vds's by (auto intro:clone_event_no_limit)

  have valid: "valid (ev # \<tau>)"

  proof-

    have "os_grant \<tau> ev"

      using ev tau by (simp add:exf exp)

    moreover have "rc_grant \<tau> ev" 

      using ev tau ts'_exec2(4) ISP etype

      by (auto simp:etype_of_file_def cp2sproc.simps obj2sobj.simps 

              split:if_splits option.splits)

    ultimately show ?thesis using vs_tau

      by (erule_tac vs_step, simp+)

  qed  moreover

  have "obj2sobj (ev # \<tau>) (Proc (new_proc (s'@s))) = 

        SProc (r', fr', exec_type_aux r pt, u) srp"

  proof-

    have "obj2sobj (s'@s) (Proc p) = SProc (r,fr,pt,u) srp" using ISP tau vs_tau

      by (auto split:option.splits simp:cp2sproc_simps obj2sobj.simps)

    hence "obj2sobj \<tau> (Proc (new_proc (s'@s))) = SProc (r,fr,pt,u) srp" using tau

      by (auto simp:obj2sobj.simps cp2sproc.simps pct_def clone_type_unchange 

              split:option.splits)

    moreover have "source_dir \<tau> f = Some sd" using vs_tau etype tau 

      by (auto simp:source_dir_simps obj2sobj.simps split:option.splits if_splits)

    ultimately show ?thesis using valid ts'_exec2(5) ts'_exec2(6) ev

      by (auto simp:cp2sproc_exec obj2sobj.simps split:option.splits)

  qed  moreover

  have "Proc (new_proc (s'@s)) \<in> tainted (ev # \<tau>)"

  proof-

    have "Proc p \<in> tainted (s' @ s)" using TP vds's nodels'

      by (drule_tac s = s' in t_remain_app, auto)

    hence "Proc (new_proc (s'@s)) \<in> tainted \<tau>" using TP tau vs_tau

      by (auto intro:t_clone)

    thus ?thesis using ev valid

      by (drule_tac t_remain, auto dest:valid_os)

  qed  moreover

  have "no_del_event (ev # \<tau>)" using ev tau nodels' by simp 

  moreover have "initp_intact (ev#\<tau>)" using ev tau intacts' valid

    by (simp add:initp_intact_I_exec)

  ultimately show ?case

    by (rule_tac x = "Proc (new_proc (s'@s))" in exI, rule_tac x = "ev#\<tau>" in exI, auto)

next

  case (ts'_cfd r fr pt u srp t sd srf t')

  then obtain p s where TP: "(Proc p) \<in> tainted s" 

    and "valid s \<and> p \<in> current_procs s \<and> no_del_event s \<and> initp_intact s \<and>

         obj2sobj s (Proc p) = SProc (r,fr,pt,u) srp"

    apply (clarsimp, frule_tac obj2sobj_proc)

    by (frule tainted_is_valid, frule tainted_is_current, auto)

  with ts'_cfd(3) obtain pf s' where vds': "valid (s' @ s)"

    and SF: "obj2sobj (s'@s) (File pf) = SFile (t, sd) srf"

    and nodels': "no_del_event (s'@s)"

    and intacts': "initp_intact (s'@s)"

    and SP: "obj2sobj (s'@s) (Proc p) = SProc (r,fr,pt,u) srp"

    and exp: "p \<in> current_procs (s' @ s)"

    and exf: "pf \<in> current_files (s' @ s)"

    apply (drule_tac s' =s and obj' = "Proc p" in all_sobjs_E0, auto)

    apply (frule_tac obj = "Proc p" in nodel_tainted_exists, simp)

    by (frule obj2sobj_file, clarsimp)

  obtain e \<tau> where ev: "e = CreateFile p (new_childf pf \<tau>)"

    and tau: "\<tau> = (s' @ s)" by auto

  have valid: "valid (e# \<tau>)"

  proof-

    have "os_grant \<tau> e"

      using ev tau exp exf by (simp add:ncf_notin_curf ncf_parent)

    moreover have "rc_grant \<tau> e" 

      using ev tau ts'_cfd(4,5,6) SP SF

      by (auto simp:etype_of_file_def cp2sproc.simps ncf_parent obj2sobj.simps

        split:if_splits option.splits t_rc_file_type.splits)

    ultimately show ?thesis using vds' tau

      by (rule_tac vs_step, simp+)

  qed  moreover

  have nodel: "no_del_event (e#\<tau>)" using nodels' tau ev by simp  moreover

  have "obj2sobj (e#\<tau>) (File (new_childf pf \<tau>)) = SFile (t', sd) None"

  proof-

    have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = Some t'"

      using ev tau SF SP ts'_cfd(4)

      by (auto simp:obj2sobj.simps etype_of_file_def cp2sproc.simps

              split:option.splits if_splits  intro!:etype_aux_prop4)

    moreover have "source_dir (e#\<tau>) (new_childf pf \<tau>) = Some sd"

      using ev tau SF SP valid ncf_parent

      by (auto simp:source_dir_simps obj2sobj.simps cp2sproc.simps

              split:if_splits option.splits)

    ultimately show ?thesis  using nodel ncf_notin_curf[where s = \<tau>]

      nodel_imp_exists[where obj = "File (new_childf pf \<tau>)" and s =\<tau>]

      by (auto simp:obj2sobj.simps dest:no_del_event_cons_D)

  qed  moreover

  have "initp_intact (e#\<tau>)" using ev tau intacts' valid nodels'

    by (auto intro!:initp_intact_I_others)  moreover

  have "File (new_childf pf \<tau>) \<in> tainted (e#\<tau>)" 

  proof- 

    have "Proc p \<in> tainted \<tau>" using nodel vds' TP ev tau

      by (drule_tac s = "s'" and s' = s in t_remain_app, auto)

    thus ?thesis using ev tau valid by (auto intro:t_cfile)

  qed

  ultimately show ?case using tau ev

    apply (rule_tac x = "File (new_childf pf \<tau>)" in exI)

    by (rule_tac x = "e#\<tau>" in exI, auto)

next

  case (ts'_cfd' r fr pt u srp t sd srf)

  then obtain p s where TP: "(Proc p) \<in> tainted s" 

    and "valid s \<and> p \<in> current_procs s \<and> no_del_event s \<and> initp_intact s \<and>

         obj2sobj s (Proc p) = SProc (r,fr,pt,u) srp"

    apply (clarsimp, frule_tac obj2sobj_proc)

    by (frule tainted_is_valid, frule tainted_is_current, auto)

  with ts'_cfd'(3) obtain pf s' where vds': "valid (s' @ s)"

    and SF: "obj2sobj (s'@s) (File pf) = SFile (t, sd) srf"

    and nodels': "no_del_event (s'@s)"

    and intacts': "initp_intact (s'@s)"

    and SP: "obj2sobj (s'@s) (Proc p) = SProc (r,fr,pt,u) srp"

    and exp: "p \<in> current_procs (s' @ s)"