1 theory tainted_vs_tainted_s

     2 imports Main rc_theory os_rc deleted_prop tainted obj2sobj_prop source_prop all_sobj_prop 

     3 begin

     4 

     5 context tainting_s_complete begin

     6 

     7 lemma t2ts[rule_format]: 

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

     9 proof (induct rule:tainted.induct)

    10   case (t_init obj) 

    11   assume seed: "obj \<in> seeds" 

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

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

    14 next

    15   case (t_clone p s p') 

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

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

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

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

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

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

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

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

    24     apply (simp del:cp2sproc.simps)

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

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

    27 

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

    29     using sproc srp p3

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

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

    32     by (auto split:option.splits)

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

    34     by simp

    35   ultimately show ?case by (auto intro:ts_clone) 

    36 next

    37   case (t_exec f s p)

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

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

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

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

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

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

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

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

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

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

    48     by (auto simp:obj2sobj.simps)

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

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

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

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

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

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

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

    56             intro:source_dir_in_init owner_in_users 

    57             split:option.splits)

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

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

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

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

    62     using p3 srdir sproc by (simp add:cp2sproc_exec)

    63   with nrole nfrole TF SP rc sproc etype

    64   show ?case 

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

    66 next

    67   case (t_cfile p s f)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    84   show ?case using etype srdir p3 parent os

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

    86                dest!:current_file_has_etype')

    87     apply (case_tac "default_fd_create_type r")

    88     using SF TP rc sproc

    89     apply (rule_tac sf = srpf in ts_cfd',

    90            auto simp:etype_of_file_def etype_aux_prop3 obj2sobj.simps cp2sproc.simps

    91                split:option.splits) [1]

    92     using SF TP rc sproc

    93     apply (rule_tac sf = srpf in ts_cfd)

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

    95     done

    96 next

    97   case (t_cipc p s i)

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

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

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

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

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

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

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

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

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

   107   show ?case using p3 sproc os rc TP 

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

   109             split:option.splits intro!:ts_cipc)

   110 next

   111   case (t_read f s p)

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

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

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

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

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

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

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

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

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

   121     by (auto simp:obj2sobj.simps)

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

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

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

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

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

   127   show ?case using sproc SP TF rc etype 

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

   129             split:option.splits intro!:ts_read) 

   130 next

   131   case (t_write p s f)

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

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

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

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

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

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

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

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

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

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

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

   143     by (auto simp:obj2sobj.simps)

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

   145     by (case_tac f, auto simp:etype_of_file_def)

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

   147     by (rule_tac all_sobjs_I, simp+) 

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

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

   150             split:option.splits intro!:ts_write) 

   151 next

   152   case (t_send p s i)

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

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

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

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

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

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

   159     by (simp, drule_tac current_ipc_has_type, auto)

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

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

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

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

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

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

   166   show ?case using sproc TP rc etype p3 vs SI

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

   168             split:option.splits intro!:ts_send)

   169 next

   170   case (t_recv i s p)

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

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

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

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

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

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

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

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

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

   180     by (auto simp:obj2sobj.simps)

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

   182     by (simp, drule_tac current_ipc_has_type, auto)

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

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

   185   show ?case using sproc SP TI rc etype 

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

   187             split:option.splits intro!:ts_recv) 

   188 next

   189   case (t_remain obj s e)

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

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

   192     by (auto dest:valid_os valid_cons valid_rc)

   193   show ?case

   194   proof (cases obj)

   195     case (File f)

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

   197     proof-

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

   199         using p5 os vs File t_remain(3,4)

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

   201         by (auto dest:ancient_file_in_current intro!:etype_aux_prop)

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

   203         using p5 os vs File t_remain(3,4)

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

   205       ultimately show ?thesis using vs t_remain(4) File

   206         apply (auto simp:obj2sobj.simps cp2sproc.simps 

   207                    split:if_splits option.splits dest:not_deleted_cons_D)

   208         by (case_tac e, auto)

   209     qed

   210     with File t_remain(2) show ?thesis by simp

   211   next

   212     case (IPC i) 

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

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

   215                           split:option.splits

   216                           dest!:current_proc_has_role')

   217     with IPC t_remain(2) show ?thesis by simp

   218   next

   219     case (Proc p) 

   220     show ?thesis 

   221     proof-

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

   223       proof-

   224         fix f

   225         assume ev: "e = Execute p f"

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

   227         proof-

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

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

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

   231           with Proc t_remain(2) 

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

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

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

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

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

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

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

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

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

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

   242                     intro:source_dir_in_init owner_in_users split:option.splits)

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

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

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

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

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

   248           with nrole nfrole SF TP rc sproc etype ev

   249           show ?thesis

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

   251                    intro!:ts_exec2 split:option.splits)

   252         qed

   253       qed  moreover 

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

   255       proof-

   256         fix r' 

   257         assume ev: "e = ChangeRole p r'"

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

   259         proof-

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

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

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

   263           with Proc t_remain(2)

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

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

   266           with rc sproc ev show ?thesis 

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

   268             by (rule_tac ts_crole, simp+)

   269         qed

   270       qed  moreover 

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

   272       proof-

   273         fix u'

   274         assume ev: "e = ChangeOwner p u'"

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

   276         proof-        

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

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

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

   280           with Proc t_remain(2)

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

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

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

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

   285             by (auto dest:chown_role_some)

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

   287             using sproc ev os

   288             by (auto split:option.splits t_role.splits 

   289                   simp del:currentrole.simps type_of_process.simps

   290                   simp add:obj2sobj.simps cp2sproc.simps 

   291                            chown_role_aux_valid chown_type_aux_valid)

   292           with rc sproc ev TP uinit chown

   293           show ?thesis

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

   295                    intro!:ts_chown split:option.splits)

   296         qed

   297       qed  moreover 

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

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

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

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

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

   303       ultimately show ?thesis using Proc

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

   305     qed

   306   qed

   307 qed

   308 

   309 end

   310 

   311 context tainting_s_sound begin

   312 

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

   314 apply (erule tainted_s.induct)

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

   316 by (simp add:clone_type_aux_def clone_type_unchange)

   317 

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

   319 apply (erule tainted_s'.induct)

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

   321 

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

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

   324 

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

   326 lemma ts2t_intact:

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

   328                                  no_del_event s \<and> initp_intact s"

   329 

   330 proof (induct rule:tainted_s'.induct)

   331   case (ts'_init obj)

   332   hence ex: "exists [] obj"

   333     apply (drule_tac seeds_in_init) 

   334     by (case_tac obj, simp+)

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

   336     by (simp add:obj2sobj_nil_init)

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

   338   moreover have "initp_intact []"

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

   340   ultimately show ?case 

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

   342 next

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

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

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

   346          no_del_event s \<and> initp_intact s" 

   347     apply (clarsimp, frule_tac obj2sobj_file)

   348     by (frule tainted_is_valid, frule tainted_is_current, auto)

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

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

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

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

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

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

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

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

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

   358     by (frule obj2sobj_proc, clarsimp)

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

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

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

   362 

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

   364   proof-

   365     have "os_grant \<tau> ev"

   366       using ev tau by (simp add:exf exp)

   367     moreover have "rc_grant \<tau> ev" 

   368       using ev tau ts'_exec1 ISP etype

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

   370               split:if_splits option.splits)

   371     ultimately show ?thesis using vs_tau

   372       by (erule_tac vs_step, simp+)

   373   qed  moreover

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

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

   376   proof-

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

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

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

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

   381               split:option.splits)

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

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

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

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

   386   qed  moreover

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

   388   proof-

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

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

   391     thus ?thesis using ev valid

   392       by (drule_tac t_exec, simp+)

   393   qed  moreover

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

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

   396     by (simp add:initp_intact_I_exec)

   397   ultimately show ?case

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

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

   400 next

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

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

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

   404          no_del_event s \<and> initp_intact s" 

   405     apply (clarsimp, frule_tac obj2sobj_proc)

   406     by (frule tainted_is_valid, frule tainted_is_current, auto)

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

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

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

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

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

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

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

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

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

   416     by (frule obj2sobj_file, clarsimp)

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

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

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

   420 

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

   422   proof-

   423     have "os_grant \<tau> ev"

   424       using ev tau by (simp add:exf exp)

   425     moreover have "rc_grant \<tau> ev" 

   426       using ev tau ts'_exec2(4) ISP etype

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

   428               split:if_splits option.splits)

   429     ultimately show ?thesis using vs_tau

   430       by (erule_tac vs_step, simp+)

   431   qed  moreover

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

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

   434   proof-

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

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

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

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

   439               split:option.splits)

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

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

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

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

   444   qed  moreover

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

   446   proof-

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

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

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

   450       by (auto intro:t_clone)

   451     thus ?thesis using ev valid

   452       by (drule_tac t_remain, auto dest:valid_os)

   453   qed  moreover

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

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

   456     by (simp add:initp_intact_I_exec)

   457   ultimately show ?case

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

   459 next

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

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

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

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

   464     apply (clarsimp, frule_tac obj2sobj_proc)

   465     by (frule tainted_is_valid, frule tainted_is_current, auto)

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

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

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

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

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

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

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

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

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

   475     by (frule obj2sobj_file, clarsimp)

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

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

   478 

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

   480   proof-

   481     have "os_grant \<tau> e"

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

   483     moreover have "rc_grant \<tau> e" 

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

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

   486         split:if_splits option.splits t_rc_file_type.splits)

   487     ultimately show ?thesis using vds' tau

   488       by (rule_tac vs_step, simp+)

   489   qed  moreover

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

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

   492   proof-

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

   494       using ev tau SF SP ts'_cfd(4)

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

   496               split:option.splits if_splits  intro!:etype_aux_prop4)

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

   498       using ev tau SF SP valid ncf_parent

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

   500               split:if_splits option.splits)

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

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

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

   504   qed  moreover

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

   506     by (auto intro!:initp_intact_I_others)  moreover

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

   508   proof- 

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

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

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

   512   qed

   513   ultimately show ?case using tau ev

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

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

   516 next

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

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

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

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

   521     apply (clarsimp, frule_tac obj2sobj_proc)

   522     by (frule tainted_is_valid, frule tainted_is_current, auto)

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

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

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

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

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

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

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

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

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

   532     by (frule obj2sobj_file, clarsimp)

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

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

   535 

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

   537   proof-

   538     have "os_grant \<tau> e"

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

   540     moreover have "rc_grant \<tau> e" 

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

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

   543         split:if_splits option.splits t_rc_file_type.splits)

   544     ultimately show ?thesis using vds' tau

   545       by (rule_tac vs_step, simp+)

   546   qed  moreover

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

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

   549   proof-

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

   551       proof-

   552         have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = etype_of_file \<tau> pf"

   553           using ev tau SP ts'_cfd'(4)

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

   555             split:option.splits   intro!:etype_aux_prop3)

   556         thus ?thesis using SF tau ev

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

   558       qed

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

   560       using ev tau SF SP valid ncf_parent

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

   562               split:if_splits option.splits)

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

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

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

   566   qed  moreover

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

   568     by (auto intro!:initp_intact_I_others)  moreover

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

   570   proof- 

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

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

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

   574   qed

   575   ultimately show ?case using tau ev

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

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

   578 next

   579   case (ts'_cipc r fr pt u srp)

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

   581     and vds: "valid s" and exp: "p \<in> current_procs s" 

   582     and nodels: "no_del_event s" and intacts: "initp_intact s"

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

   584     apply (clarsimp, frule_tac obj2sobj_proc)

   585     by (frule tainted_is_valid, frule tainted_is_current, auto)

   586   obtain e where ev: "e = CreateIPC p (new_ipc s)" by simp

   587       

   588   have valid: "valid (e # s)" 

   589   proof-

   590     have "os_grant s e"

   591       using ev exp by (simp)

   592     moreover have "rc_grant s e" 

   593       using ev ts'_cipc(3) SP

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

   595     ultimately show ?thesis using vds

   596       by (rule_tac vs_step, simp+)

   597   qed  moreover

   598   have nodel: "no_del_event (e#s)" using nodels ev by simp  moreover

   599   have "initp_intact (e#s)" using ev intacts valid nodels

   600     by (auto intro!:initp_intact_I_others)  moreover

   601   have "IPC (new_ipc s) \<in> tainted (e#s)" using TP ev valid

   602     by (auto intro:t_cipc)  moreover

   603   have "obj2sobj (e#s) (IPC (new_ipc s)) = SIPC (default_ipc_create_type r) None"

   604     using ev SP nodel nodel_imp_exists[where obj = "IPC (new_ipc s)" and s=s]

   605     by (auto simp:obj2sobj.simps ni_notin_curi cp2sproc.simps

   606             split:option.splits dest:no_del_event_cons_D)

   607   ultimately show ?case using ev

   608     apply (rule_tac x = "IPC (new_ipc s)" in exI)

   609     by (rule_tac x = "e # s" in exI, auto)

   610 next

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

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

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

   614          no_del_event s \<and> initp_intact s" 

   615     apply (clarsimp, frule_tac obj2sobj_file)

   616     by (frule tainted_is_valid, frule tainted_is_current, auto)

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

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

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

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

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

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

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

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

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

   626     by (frule obj2sobj_proc, clarsimp)

   627   obtain e \<tau> where ev: "e = ReadFile p f" and tau: "\<tau> = s' @ s" by auto

   628 

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

   630   proof-

   631     have "os_grant \<tau> e"

   632       using ev tau by (simp add:exf exp)

   633     moreover have "rc_grant \<tau> e" 

   634       using ev tau ts'_read(4) SP SF

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

   636               split:if_splits option.splits)

   637     ultimately show ?thesis using vds' tau

   638       by (rule_tac vs_step, simp+)

   639   qed  moreover

   640   have "obj2sobj (e # \<tau>) (Proc p) = SProc (r, fr, pt, u) srp" using valid tau ev SP

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

   642   moreover  have "Proc p \<in> tainted (e # \<tau>)"

   643   proof-

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

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

   646     thus ?thesis using ev valid

   647       by (drule_tac t_read, simp+)

   648   qed  moreover

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

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

   651     by (auto intro!:initp_intact_I_others) 

   652   ultimately show ?case

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

   654 next

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

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

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

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

   659     apply (clarsimp, frule_tac obj2sobj_proc)

   660     by (frule tainted_is_valid, frule tainted_is_current, auto)

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

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

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

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

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

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

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

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

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

   670     by (frule obj2sobj_file, clarsimp)

   671   obtain e \<tau> where ev: "e = WriteFile p f" and tau: "\<tau> = (s' @ s)" by auto

   672 

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

   674   proof-

   675     have "os_grant \<tau> e"

   676       using ev tau exp exf by simp

   677     moreover have "rc_grant \<tau> e" 

   678       using ev tau ts'_write(4) SP SF

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

   680               split:if_splits option.splits)

   681     ultimately show ?thesis using vds' tau

   682       by (rule_tac vs_step, simp+)

   683   qed  moreover

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

   685   have "obj2sobj (e#\<tau>) (File f) = SFile (t, sd) srf"

   686     using tau ev SF valid

   687     by (auto simp:obj2sobj.simps source_dir_simps etype_of_file_def

   688             split:option.splits if_splits)

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

   690     by (auto intro!:initp_intact_I_others)   moreover

   691   have "File f \<in> tainted (e#\<tau>)" 

   692   proof- 

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

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

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

   696   qed

   697   ultimately show ?case using tau ev

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

   699 next 

   700   case (ts'_recv t sri r fr pt u srp)

   701   then obtain i s  where TI: "(IPC i) \<in> tainted s" and vds: "valid s" 

   702     and "i \<in> current_ipcs s \<and> obj2sobj s (IPC i) = SIPC t sri \<and> 

   703          no_del_event s \<and> initp_intact s" 

   704     apply (clarsimp, frule_tac obj2sobj_ipc)

   705     by (frule tainted_is_valid, frule tainted_is_current, auto)

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

   707     and SI: "obj2sobj (s'@s) (IPC i) = SIPC t sri"

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

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

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

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

   712     and exi: "i \<in> current_ipcs (s' @ s)"

   713     apply (drule_tac s' =s and obj' = "IPC i" in all_sobjs_E0, auto)

   714     apply (frule_tac obj = "IPC i" in nodel_tainted_exists, simp)

   715     by (frule obj2sobj_proc, clarsimp)

   716   obtain e \<tau> where ev: "e = Recv p i" and tau: "\<tau> = s' @ s" by auto

   717 

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

   719   proof-

   720     have "os_grant \<tau> e"

   721       using ev tau by (simp add:exi exp)

   722     moreover have "rc_grant \<tau> e" 

   723       using ev tau ts'_recv(4) SP SI

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

   725               split:if_splits option.splits)

   726     ultimately show ?thesis using vds' tau

   727       by (rule_tac vs_step, simp+)

   728   qed  moreover

   729   have "obj2sobj (e # \<tau>) (Proc p) = SProc (r, fr, pt, u) srp" using valid tau ev SP

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

   731   moreover  have "Proc p \<in> tainted (e # \<tau>)"

   732   proof-

   733     have "(IPC i) \<in> tainted \<tau>" using TI nodels' tau vds'

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

   735     thus ?thesis using ev valid

   736       by (drule_tac t_recv, simp+)

   737   qed  moreover

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

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

   740     by (auto intro!:initp_intact_I_others)   

   741   ultimately show ?case

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

   743 next

   744   case (ts'_send r fr pt u srp t sri)

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

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

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

   748     apply (clarsimp, frule_tac obj2sobj_proc)

   749     by (frule tainted_is_valid, frule tainted_is_current, auto)

   750   with ts'_send(3) obtain i s' where vds': "valid (s' @ s)"

   751     and SI: "obj2sobj (s'@s) (IPC i) = SIPC t sri"

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

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

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

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

   756     and exi: "i \<in> current_ipcs (s' @ s)"

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

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

   759     by (frule obj2sobj_ipc, clarsimp)

   760   obtain e \<tau> where ev: "e = Send p i" and tau: "\<tau> = (s' @ s)" by auto

   761 

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

   763   proof-

   764     have "os_grant \<tau> e"

   765       using ev tau exp exi by simp

   766     moreover have "rc_grant \<tau> e" 

   767       using ev tau ts'_send(4) SP SI

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

   769               split:if_splits option.splits)

   770     ultimately show ?thesis using vds' tau

   771       by (rule_tac vs_step, simp+)

   772   qed  moreover

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

   774   have "obj2sobj (e#\<tau>) (IPC i) = SIPC t sri"

   775     using tau ev SI valid

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

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

   778     by (auto intro!:initp_intact_I_others)  moreover

   779   have "IPC i \<in> tainted (e#\<tau>)" 

   780   proof- 

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

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

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

   784   qed

   785   ultimately show ?case using tau ev 

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

   787 next

   788   case (ts'_crole r fr pt u srp r')

   789   then obtain p s where exp: "p \<in> current_procs s"

   790     and TP: "(Proc p) \<in> tainted s" and vds: "valid s" and nodels: "no_del_event s"

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

   792     and intacts: "initp_intact s" 

   793     apply (clarsimp, frule_tac obj2sobj_proc)

   794     by (frule tainted_is_valid, frule tainted_is_current, auto)

   795   obtain e \<tau> where ev: "e = ChangeRole (new_proc s) r'"

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

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

   798 

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

   800   proof-

   801     have "os_grant \<tau> e"

   802       using ev tau exp by simp

   803     moreover have "rc_grant \<tau> e" 

   804       using ev tau ts'_crole(3) SP

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

   806     ultimately show ?thesis using vs_tau

   807       by (erule_tac vs_step, simp+)

   808   qed  moreover

   809   have "obj2sobj (e # \<tau>) (Proc (new_proc s)) = SProc (r',fr,pt,u) srp"

   810   proof-

   811     have "obj2sobj \<tau> (Proc (new_proc s)) = SProc (r,fr,pt,u) srp" using SP tau vs_tau

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

   813     thus ?thesis using valid ev

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

   815   qed  moreover

   816   have "Proc (new_proc s) \<in> tainted (e # \<tau>)"

   817   proof-

   818     have "(Proc (new_proc s)) \<in> tainted \<tau>" using TP tau vs_tau

   819       by (auto intro!:t_clone)

   820     thus ?thesis using ev valid

   821       by (drule_tac t_remain, auto dest:valid_os)

   822   qed  moreover

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

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

   825     by (simp add:initp_intact_I_crole)  

   826   ultimately show ?case

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

   828 next

   829   case (ts'_chown r fr pt u srp u' nr)

   830   then obtain p s where exp: "p \<in> current_procs s"

   831     and TP: "(Proc p) \<in> tainted s" and vds: "valid s" and nodels: "no_del_event s"

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

   833     and intacts: "initp_intact s" 

   834     apply (clarsimp, frule_tac obj2sobj_proc)

   835     by (frule tainted_is_valid, frule tainted_is_current, auto)

   836   obtain e \<tau> where ev: "e = ChangeOwner (new_proc s) u'"

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

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

   839 

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

   841   proof-

   842     have "os_grant \<tau> e"

   843       using ev tau exp ts'_chown(3) by simp

   844     moreover have "rc_grant \<tau> e" 

   845       using ev tau ts'_chown(5) SP

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

   847               split:option.splits t_rc_proc_type.splits)

   848         (* here is another place of no_limit of clone event assumption *)

   849     ultimately show ?thesis using vs_tau

   850       by (erule_tac vs_step, simp+)

   851   qed  moreover

   852   have "obj2sobj (e # \<tau>) (Proc (new_proc s)) = SProc (nr, fr, chown_type_aux r nr pt, u') srp"

   853   proof-

   854     have "obj2sobj \<tau> (Proc (new_proc s)) = SProc (r,fr,pt,u) srp" using SP tau vs_tau

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

   856     thus ?thesis using valid ev ts'_chown(4)

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

   858   qed  moreover

   859   have "Proc (new_proc s) \<in> tainted (e # \<tau>)"

   860   proof-

   861     have "Proc (new_proc s) \<in> tainted \<tau>" using TP tau vs_tau exp

   862       by (auto intro!:t_clone)

   863     thus ?thesis using ev valid

   864       by (drule_tac t_remain, auto dest:valid_os)

   865   qed  moreover

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

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

   868     by (simp add:initp_intact_I_chown)

   869   ultimately show ?case

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

   871 qed

   872 

   873 lemma ts2t:

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

   875                                  sobj_source_eq_obj sobj obj \<and> no_del_event s \<and> 

   876                                  initp_intact_but s sobj"

   877 proof (induct rule:tainted_s'.induct)

   878   case (ts'_init obj)

   879   hence ex: "exists [] obj"

   880     apply (drule_tac seeds_in_init) 

   881     by (case_tac obj, simp+)

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

   883     by (simp add:obj2sobj_nil_init)

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

   885   moreover have "sobj_source_eq_obj (init_obj2sobj obj) obj" using ex

   886     apply (frule_tac init_obj_has_sobj)

   887     apply (case_tac "init_obj2sobj obj", case_tac[!] obj)

   888     by (auto split:option.splits)

   889   ultimately show ?case 

   890     apply (rule_tac x = obj in exI, rule_tac x = "[]" in exI)

   891     by (auto simp:initp_intact_but_nil)

   892 next

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

   894   then obtain f s  where "sobj_source_eq_obj (SFile (t, sd) srf) (File f)"

   895     and TF: "(File f) \<in> tainted s" and vds: "valid s" and "f \<in> current_files s"

   896     and "obj2sobj s (File f) = SFile (t, sd) srf \<and> no_del_event s \<and> initp_intact s" 

   897     apply (clarsimp, frule_tac obj2sobj_file)

   898     by (frule tainted_is_valid, frule tainted_is_current, auto)

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

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

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

   902     and intacts': "initp_intact_but (s'@s) (SProc (r,fr,pt,u) srp)" 

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

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

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

   906     and sreq: "sobj_source_eq_obj (SProc (r,fr,pt,u) srp) (Proc p)"

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

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

   909     by (frule obj2sobj_proc, clarsimp)

   910   from vds's ISP sreq exp have srpeq: "srp = Some p" by (simp add:proc_source_eq_prop)

   911   with exp vds's ISP have initp: "p \<in> init_processes" 

   912     by (auto simp:obj2sobj.simps dest:source_proc_in_init split:option.splits)

   913   obtain ev \<tau> where ev: "ev = Execute p f"

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

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

   916 

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

   918   proof-

   919     have "os_grant \<tau> ev"

   920       using ev tau by (simp add:exf exp)

   921     moreover have "rc_grant \<tau> ev" 

   922       using ev tau ts'_exec1 ISP etype

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

   924               split:if_splits option.splits)

   925     ultimately show ?thesis using vs_tau

   926       by (erule_tac vs_step, simp+)

   927   qed  moreover

   928   have "obj2sobj (ev # \<tau>) (Proc p) = SProc (r', fr', exec_type_aux r pt, u) srp"

   929   proof-

   930     have "obj2sobj \<tau> (Proc p) = SProc (r,fr,pt,u) srp" using ISP tau vs_tau

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

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

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

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

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

   936   qed  moreover

   937   have "Proc p \<in> tainted (ev # \<tau>)"

   938   proof-

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

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

   941     thus ?thesis using ev valid

   942       by (drule_tac t_exec, simp+)

   943   qed  moreover

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

   945   moreover have "initp_intact_but (ev#\<tau>) (SProc (r', fr', exec_type_aux r pt, u) srp)"

   946     using ev tau nodels' intacts' srpeq valid initp

   947     by (simp, rule_tac initp_intact_butp_I_exec, simp_all)

   948   moreover have "sobj_source_eq_obj (SProc (r', fr', exec_type_aux r pt, u) srp) (Proc p)"

   949     using sreq by (case_tac srp, simp+)

   950   ultimately show ?case

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

   952 next

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

   954   then obtain p s  where sreq:"sobj_source_eq_obj (SProc (r, fr, pt, u) srp) (Proc p)"

   955     and TP: "(Proc p) \<in> tainted s" and vds: "valid s" and "p \<in> current_procs s"

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

   957          initp_intact_but s (SProc (r, fr, pt, u) srp)" 

   958     apply (clarsimp, frule_tac obj2sobj_proc)

   959     by (frule tainted_is_valid, frule tainted_is_current, auto)

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

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

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

   963     and intacts': "initp_intact_but (s'@s) (SProc (r,fr,pt,u) srp)" 

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

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

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

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

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

   969     by (frule obj2sobj_file, clarsimp)

   970   from vds's ISP sreq exp have srpeq: "srp = Some p" by (simp add:proc_source_eq_prop)

   971   with exp vds's ISP have initp: "p \<in> init_processes" 

   972     by (auto simp:obj2sobj.simps dest:source_proc_in_init split:option.splits)

   973   obtain ev \<tau> where ev: "ev = Execute p f"

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

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

   976 

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

   978   proof-

   979     have "os_grant \<tau> ev"

   980       using ev tau by (simp add:exf exp)

   981     moreover have "rc_grant \<tau> ev" 

   982       using ev tau ts'_exec2 ISP etype

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

   984               split:if_splits option.splits)

   985     ultimately show ?thesis using vs_tau

   986       by (erule_tac vs_step, simp+)

   987   qed  moreover

   988   have "obj2sobj (ev # \<tau>) (Proc p) = SProc (r', fr', exec_type_aux r pt, u) srp"

   989   proof-

   990     have "obj2sobj \<tau> (Proc p) = SProc (r,fr,pt,u) srp" using ISP tau vs_tau

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

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

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

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

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

   996   qed  moreover

   997   have "Proc p \<in> tainted (ev # \<tau>)"

   998   proof-

   999     have "(Proc p) \<in> tainted \<tau>" using TP nodels' tau vs_tau

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

  1001     thus ?thesis using ev valid

  1002       by (drule_tac t_remain, auto dest:valid_os)

  1003   qed  moreover

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

  1005   moreover have "initp_intact_but (ev#\<tau>) (SProc (r', fr', exec_type_aux r pt, u) srp)"

  1006     using ev tau nodels' intacts' srpeq valid initp

  1007     by (simp, rule_tac initp_intact_butp_I_exec, simp_all)

  1008   moreover have "sobj_source_eq_obj (SProc (r', fr', exec_type_aux r pt, u) srp) (Proc p)"

  1009     using sreq by (case_tac srp, simp+)

  1010   ultimately show ?case

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

  1012 next

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

  1014   from ts'_cfd(1) obtain p s where TP: "(Proc p) \<in> tainted s" 

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

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

  1017     apply (drule_tac ts2t_intact, clarsimp, frule_tac obj2sobj_proc)

  1018     by (frule tainted_is_valid, frule tainted_is_current, auto)

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

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

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

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

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

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

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

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

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

  1028     by (frule obj2sobj_file, clarsimp)

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

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

  1031 

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

  1033   proof-

  1034     have "os_grant \<tau> e"

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

  1036     moreover have "rc_grant \<tau> e" 

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

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

  1039         split:if_splits option.splits t_rc_file_type.splits)

  1040     ultimately show ?thesis using vds' tau

  1041       by (rule_tac vs_step, simp+)

  1042   qed  moreover

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

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

  1045   proof-

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

  1047       using ev tau SF SP ts'_cfd(4)

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

  1049               split:option.splits if_splits  intro!:etype_aux_prop4)

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

  1051       using ev tau SF SP valid ncf_parent

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

  1053               split:if_splits option.splits)

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

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

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

  1057   qed  moreover

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

  1059     by (auto intro!:initp_intact_I_others)  moreover

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

  1061   proof- 

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

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

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

  1065   qed

  1066   ultimately show ?case using tau ev

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

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

  1069 next

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

  1071   from ts'_cfd'(1) obtain p s where TP: "(Proc p) \<in> tainted s" 

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

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

  1074     apply (drule_tac ts2t_intact, clarsimp, frule_tac obj2sobj_proc)

  1075     by (frule tainted_is_valid, frule tainted_is_current, auto)

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

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

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

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

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

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

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

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

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

  1085     by (frule obj2sobj_file, clarsimp)

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

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

  1088 

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

  1090   proof-

  1091     have "os_grant \<tau> e"

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

  1093     moreover have "rc_grant \<tau> e" 

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

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

  1096         split:if_splits option.splits t_rc_file_type.splits)

  1097     ultimately show ?thesis using vds' tau

  1098       by (rule_tac vs_step, simp+)

  1099   qed  moreover

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

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

  1102   proof-

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

  1104       proof-

  1105         have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = etype_of_file \<tau> pf"

  1106           using ev tau SP ts'_cfd'(4)

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

  1108             split:option.splits   intro!:etype_aux_prop3)

  1109         thus ?thesis using SF tau ev

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

  1111       qed

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

  1113       using ev tau SF SP valid ncf_parent

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

  1115               split:if_splits option.splits)

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

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

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

  1119   qed  moreover

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

  1121     by (auto intro!:initp_intact_I_others)  moreover

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

  1123   proof- 

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

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

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

  1127   qed

  1128   ultimately show ?case using tau ev

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

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

  1131 next

  1132   case (ts'_cipc r fr pt u srp)

  1133   from ts'_cipc(1) obtain p s where TP: "(Proc p) \<in> tainted s" 

  1134     and vds: "valid s" and exp: "p \<in> current_procs s" 

  1135     and nodels: "no_del_event s" and intacts: "initp_intact s"