Theory After_Execution

section ‹After-execution security› 

theory After_Execution
imports During_Execution
begin 


(* Note: For the paper, I will need the theorems as they are stated. *)

context PL_Indis
begin

subsection‹Setup for bisimilarities›

(* Sbis: *)
lemma Sbis_transC[consumes 3, case_names Match]: 
assumes 0: "c ≈s d" and "s ≈ t" and "(c,s) →c (c',s')"
obtains d' t' where 
"(d,t) →c (d',t')" and "s' ≈ t'" and "c' ≈s d'"
using assms Sbis_matchC_C[OF 0] 
unfolding matchC_C_def by blast

lemma Sbis_transT[consumes 3, case_names Match]: 
assumes 0: "c ≈s d" and "s ≈ t" and "(c,s) →t s'"
obtains t' where "(d,t) →t t'" and "s' ≈ t'"
using assms Sbis_matchT_T[OF 0] 
unfolding matchT_T_def by blast

lemma Sbis_transC2[consumes 3, case_names Match]: 
assumes 0: "c ≈s d" and "s ≈ t" and "(d,t) →c (d',t')"
obtains c' s' where 
"(c,s) →c (c',s')" and "s' ≈ t'" and "c' ≈s d'"
using assms Sbis_matchC_C_rev[OF 0] Sbis_Sym
unfolding matchC_C_def2 by blast

lemma Sbis_transT2[consumes 3, case_names Match]: 
assumes 0: "c ≈s d" and "s ≈ t" and "(d,t) →t t'"
obtains s' where "(c,s) →t s'" and "s' ≈ t'"
using assms Sbis_matchT_T_rev[OF 0] Sbis_Sym
unfolding matchT_T_def2 by blast

(* ZObisT: *)
lemma ZObisT_transC[consumes 3, case_names Match MatchS]: 
assumes 0: "c ≈01T d" and "s ≈ t" and "(c,s) →c (c',s')"
and "⋀ d' t'. ⟦(d,t) →c (d',t'); s' ≈ t'; c' ≈01T d'⟧ ⟹ thesis"
and "⟦s' ≈ t; c' ≈01T d⟧ ⟹ thesis"
shows thesis
using assms ZObisT_matchC_ZOC[OF 0]
unfolding matchC_ZOC_def by blast

lemma ZObisT_transT[consumes 3, case_names Match]: 
assumes 0: "c ≈01T d" and "s ≈ t" and "(c,s) →t s'"
obtains t' where "(d,t) →t t'" and "s' ≈ t'"
using assms ZObisT_matchT_T[OF 0] 
unfolding matchT_T_def by blast

lemma ZObisT_transC2[consumes 3, case_names Match MatchS]: 
assumes 0: "c ≈01T d" and 2: "s ≈ t" and 3: "(d,t) →c (d',t')"
and 4: "⋀ c' s'. ⟦(c,s) →c (c',s'); s' ≈ t'; c' ≈01T d'⟧ ⟹ thesis"
and 5: "⟦s ≈ t'; c ≈01T d'⟧ ⟹ thesis"
shows thesis 
using assms ZObisT_matchC_ZOC_rev[OF 0] ZObisT_Sym
unfolding matchC_ZOC_def2 by blast

lemma ZObisT_transT2[consumes 3, case_names Match]: 
assumes 0: "c ≈01T d" and "s ≈ t" and "(d,t) →t t'"
obtains s' where "(c,s) →t s'" and "s' ≈ t'"
using assms ZObisT_matchT_T_rev[OF 0] ZObisT_Sym
unfolding matchT_T_def2 by blast

(* WbisT: *)
lemma WbisT_transC[consumes 3, case_names Match]: 
assumes 0: "c ≈wT d" and "s ≈ t" and "(c,s) →c (c',s')"
obtains d' t' where 
"(d,t) →*c (d',t')" and "s' ≈ t'" and "c' ≈wT d'"
using assms WbisT_matchC_MC[OF 0] 
unfolding matchC_MC_def by blast

lemma WbisT_transT[consumes 3, case_names Match]: 
assumes 0: "c ≈wT d" and "s ≈ t" and "(c,s) →t s'"
obtains t' where "(d,t) →*t t'" and "s' ≈ t'"
using assms WbisT_matchT_MT[OF 0] 
unfolding matchT_MT_def by blast

lemma WbisT_transC2[consumes 3, case_names Match]: 
assumes 0: "c ≈wT d" and "s ≈ t" and "(d,t) →c (d',t')"
obtains c' s' where 
"(c,s) →*c (c',s')" and "s' ≈ t'" and "c' ≈wT d'"
using assms WbisT_matchC_MC_rev[OF 0] WbisT_Sym
unfolding matchC_MC_def2 by blast

lemma WbisT_transT2[consumes 3, case_names Match]: 
assumes 0: "c ≈wT d" and "s ≈ t" and "(d,t) →t t'"
obtains s' where "(c,s) →*t s'" and "s' ≈ t'"
using assms WbisT_matchT_MT_rev[OF 0] WbisT_Sym
unfolding matchT_MT_def2 by blast

(*  *)
lemma WbisT_MtransC[consumes 3, case_names Match]: 
assumes 1: "c ≈wT d" and 2: "s ≈ t" and 3: "(c,s) →*c (c',s')"
obtains d' t' where 
"(d,t) →*c (d',t')" and "s' ≈ t'" and "c' ≈wT d'"
proof-
  have "(c,s) →*c (c',s') ⟹ 
        c ≈wT d ⟹ s ≈ t ⟹ 
        (∃ d' t'. (d,t) →*c (d',t') ∧ s' ≈ t' ∧ c' ≈wT d')"
  proof (induct rule: MtransC_induct2)
    case (Trans c s c' s' c'' s'')
    then obtain d' t' where d: "(d, t) →*c (d', t')" 
    and "s' ≈ t'" and "c' ≈wT d'"
    and "(c', s') →c (c'', s'')" by auto
    then obtain d'' t'' where "s'' ≈ t''" and "c'' ≈wT d''" 
    and "(d', t') →*c (d'', t'')" by (metis WbisT_transC)
    thus ?case using d by (metis MtransC_Trans) 
  qed (metis MtransC_Refl)
  thus thesis using that assms by auto
qed

lemma WbisT_MtransT[consumes 3, case_names Match]: 
assumes 1: "c ≈wT d" and 2: "s ≈ t" and 3: "(c,s) →*t s'"
obtains t' where "(d,t) →*t t'" and "s' ≈ t'"
proof-
  obtain c'' s'' where 4: "(c,s) →*c (c'',s'')" 
  and 5: "(c'',s'') →t s'" using 3 by (metis MtransT_invert2)
  then obtain d'' t'' where d: "(d,t) →*c (d'',t'')" 
  and "s'' ≈ t''" and "c'' ≈wT d''" using 1 2 4 WbisT_MtransC by blast
  then obtain t' where "s' ≈ t'" and "(d'',t'') →*t t'"
  by (metis 5 WbisT_transT) 
  thus thesis using d that by (metis MtransC_MtransT)
qed

lemma WbisT_MtransC2[consumes 3, case_names Match]: 
assumes "c ≈wT d" and "s ≈ t" and 1: "(d,t) →*c (d',t')"
obtains c' s' where 
"(c,s) →*c (c',s')" and "s' ≈ t'" and "c' ≈wT d'"
proof-
  have "d ≈wT c" and "t ≈ s" 
  using assms by (metis WbisT_Sym indis_sym)+
  then obtain c' s' where 
  "(c,s) →*c (c',s')" and "t' ≈ s'" and "d' ≈wT c'"
  by (metis 1 WbisT_MtransC)
  thus ?thesis using that by (metis WbisT_Sym indis_sym)
qed

lemma WbisT_MtransT2[consumes 3, case_names Match]: 
assumes "c ≈wT d" and "s ≈ t" and "(d,t) →*t t'"
obtains s' where "(c,s) →*t s'" and "s' ≈ t'"
by (metis WbisT_MtransT WbisT_Sym assms indis_sym)

(* ZObis: *)
lemma ZObis_transC[consumes 3, case_names Match MatchO MatchS]: 
assumes 0: "c ≈01 d" and "s ≈ t" and "(c,s) →c (c',s')"
and "⋀ d' t'. ⟦(d,t) →c (d',t'); s' ≈ t'; c' ≈01 d'⟧ ⟹ thesis" 
and "⋀ t'. ⟦(d,t) →t t'; s' ≈ t'; discr c'⟧ ⟹ thesis"
and "⟦s' ≈ t; c' ≈01 d⟧ ⟹ thesis"
shows thesis
using assms ZObis_matchC_ZO[OF 0] 
unfolding matchC_ZO_def by blast

lemma ZObis_transT[consumes 3, case_names Match MatchO MatchS]: 
assumes 0: "c ≈01 d" and "s ≈ t" and "(c,s) →t s'"
and "⋀ t'. ⟦(d,t) →t t'; s' ≈ t'⟧ ⟹ thesis"
and "⋀ d' t'. ⟦(d,t) →c (d',t'); s' ≈ t'; discr d'⟧ ⟹ thesis"
and "⟦s' ≈ t; discr d⟧ ⟹ thesis"
shows thesis
using assms ZObis_matchT_ZO[OF 0] 
unfolding matchT_ZO_def by blast

lemma ZObis_transC2[consumes 3, case_names Match MatchO MatchS]: 
assumes 0: "c ≈01 d" and "s ≈ t" and "(d,t) →c (d',t')"
and "⋀ c' s'. ⟦(c,s) →c (c',s'); s' ≈ t'; c' ≈01 d'⟧ ⟹ thesis"
and "⋀ s'. ⟦(c,s) →t s'; s' ≈ t'; discr d'⟧ ⟹ thesis"
and "⟦s ≈ t'; c ≈01 d'⟧ ⟹ thesis"
shows thesis 
using assms ZObis_matchC_ZO_rev[OF 0] ZObis_Sym
unfolding matchC_ZO_def2 by blast

lemma ZObis_transT2[consumes 3, case_names Match MatchO MatchS]: 
assumes 0: "c ≈01 d" and "s ≈ t" and "(d,t) →t t'"
and "⋀ s'. ⟦(c,s) →t s'; s' ≈ t'⟧ ⟹ thesis"
and "⋀ c' s'. ⟦(c,s) →c (c',s'); s' ≈ t'; discr c'⟧ ⟹ thesis"
and "⟦s ≈ t'; discr c⟧ ⟹ thesis"
shows thesis
using assms ZObis_matchT_ZO_rev[OF 0] ZObis_Sym
unfolding matchT_ZO_def2 by blast

(* Wbis: *)
lemma Wbis_transC[consumes 3, case_names Match MatchO]: 
assumes 0: "c ≈w d" and "s ≈ t" and "(c,s) →c (c',s')"
and "⋀ d' t'. ⟦(d,t) →*c (d',t'); s' ≈ t'; c' ≈w d'⟧ ⟹ thesis" 
and "⋀ t'. ⟦(d,t) →*t t'; s' ≈ t'; discr c'⟧ ⟹ thesis"
shows thesis
using assms Wbis_matchC_M[OF 0] 
unfolding matchC_M_def by blast

lemma Wbis_transT[consumes 3, case_names Match MatchO]: 
assumes 0: "c ≈w d" and "s ≈ t" and "(c,s) →t s'"
and "⋀ t'. ⟦(d,t) →*t t'; s' ≈ t'⟧ ⟹ thesis"
and "⋀ d' t'. ⟦(d,t) →*c (d',t'); s' ≈ t'; discr d'⟧ ⟹ thesis"
shows thesis
using assms Wbis_matchT_M[OF 0] 
unfolding matchT_M_def by blast

lemma Wbis_transC2[consumes 3, case_names Match MatchO]: 
assumes 0: "c ≈w d" and "s ≈ t" and "(d,t) →c (d',t')"
and "⋀ c' s'. ⟦(c,s) →*c (c',s'); s' ≈ t'; c' ≈w d'⟧ ⟹ thesis"
and "⋀ s'. ⟦(c,s) →*t s'; s' ≈ t'; discr d'⟧ ⟹ thesis"
shows thesis 
using assms Wbis_matchC_M_rev[OF 0] Wbis_Sym
unfolding matchC_M_def2 by blast

lemma Wbis_transT2[consumes 3, case_names Match MatchO]: 
assumes 0: "c ≈w d" and "s ≈ t" and "(d,t) →t t'"
and "⋀ s'. ⟦(c,s) →*t s'; s' ≈ t'⟧ ⟹ thesis"
and "⋀ c' s'. ⟦(c,s) →*c (c',s'); s' ≈ t'; discr c'⟧ ⟹ thesis"
shows thesis
using assms Wbis_matchT_M_rev[OF 0] Wbis_Sym
unfolding matchT_M_def2 by blast

(*  *)
lemma Wbis_MtransC[consumes 3, case_names Match MatchO]: 
assumes "c ≈w d" and "s ≈ t" and "(c,s) →*c (c',s')"
and "⋀ d' t'. ⟦(d,t) →*c (d',t'); s' ≈ t'; c' ≈w d'⟧ ⟹ thesis"
and "⋀ t'. ⟦(d,t) →*t t'; s' ≈ t'; discr c'⟧ ⟹ thesis"
shows thesis
proof- 
  have "(c,s) →*c (c',s') ⟹ 
        c ≈w d ⟹ s ≈ t ⟹ 
        (∃ d' t'. (d,t) →*c (d',t') ∧ s' ≈ t' ∧ c' ≈w d') ∨ 
        (∃ t'. (d,t) →*t t' ∧ s' ≈ t' ∧ discr c')"
  proof (induct rule: MtransC_induct2)
    case (Trans c s c' s' c'' s'')
    hence c's': "(c', s') →c (c'', s'')"
    and  
    "(∃d' t'. (d, t) →*c (d', t') ∧ s' ≈ t' ∧ c' ≈w d') ∨
     (∃t'. (d, t) →*t t' ∧ s' ≈ t' ∧ discr c')" by auto
    thus ?case (is "?A ∨ ?B")
    proof(elim disjE exE conjE)
      fix d' t'
      assume c'd': "c' ≈w d'" and s't': "s' ≈ t'"
      and dt: "(d, t) →*c (d', t')" 
      from c'd' s't' c's' show ?case
      apply (cases rule: Wbis_transC) 
      by (metis dt MtransC_Trans MtransC_MtransT)+
    next
      fix t'
      assume s't': "s' ≈ t'" and c': "discr c'" 
      and dt: "(d, t) →*t t'" 
      from c' s't' c's' show ?case
      by (metis discr.simps dt indis_sym indis_trans)
    qed
  qed auto
  thus thesis using assms by auto
qed

lemma Wbis_MtransT[consumes 3, case_names Match MatchO]: 
assumes c_d: "c ≈w d" and st: "s ≈ t" and cs: "(c,s) →*t s'" 
and 1: "⋀ t'. ⟦(d,t) →*t t'; s' ≈ t'⟧ ⟹ thesis"
and 2: "⋀ d' t'. ⟦(d,t) →*c (d',t'); s' ≈ t'; discr d'⟧ ⟹ thesis"
shows thesis
using cs proof(elim MtransT_invert2)
  fix c'' s'' assume cs: "(c,s) →*c (c'',s'')" 
  and c''s'': "(c'',s'') →t s'" 
  from c_d st cs show thesis
  proof (cases rule: Wbis_MtransC)
    fix d'' t'' 
    assume dt: "(d, t) →*c (d'', t'')"
    and s''t'': "s'' ≈ t''" and c''d'': "c'' ≈w d''"
    from c''d'' s''t'' c''s'' show thesis
    apply (cases rule: Wbis_transT)
    by (metis 1 2 dt MtransC_MtransT MtransC_Trans)+
  next
    case (MatchO t')
    thus ?thesis using 1 c''s''
    by (metis discr_MtransT indis_sym indis_trans transT_MtransT)
  qed
qed

lemma Wbis_MtransC2[consumes 3, case_names Match MatchO]: 
assumes "c ≈w d" and "s ≈ t" and dt: "(d,t) →*c (d',t')"
and 1: "⋀ c' s'. ⟦(c,s) →*c (c',s'); s' ≈ t'; c' ≈w d'⟧ ⟹ thesis"
and 2: "⋀ s'. ⟦(c,s) →*t s'; s' ≈ t'; discr d'⟧ ⟹ thesis"
shows thesis
proof-
  have dc: "d ≈w c" and ts: "t ≈ s"
  by (metis assms Wbis_Sym indis_sym)+
  from dc ts dt show thesis
  apply(cases rule: Wbis_MtransC)
  by (metis 1 2 Wbis_Sym indis_sym)+
qed

lemma Wbis_MtransT2[consumes 3, case_names Match MatchO]: 
assumes "c ≈w d" and "s ≈ t" and dt: "(d,t) →*t t'"
and 1: "⋀ s'. ⟦(c,s) →*t s'; s' ≈ t'⟧ ⟹ thesis"
and 2: "⋀ c' s'. ⟦(c,s) →*c (c',s'); s' ≈ t'; discr c'⟧ ⟹ thesis"
shows thesis
proof-
  have dc: "d ≈w c" and ts: "t ≈ s"
  by (metis assms Wbis_Sym indis_sym)+
  from dc ts dt show thesis
  apply(cases rule: Wbis_MtransT)
  by (metis 1 2 Wbis_Sym indis_sym)+
qed

(* BisT: *)
lemma BisT_transC[consumes 5, case_names Match]: 
assumes 0: "c ≈T d" 
and "mustT c s" and "mustT d t"
and "s ≈ t" and "(c,s) →c (c',s')"
obtains d' t' where 
"(d,t) →*c (d',t')" and "s' ≈ t'" and "c' ≈T d'"
using assms BisT_matchC_TMC[OF 0] 
unfolding matchC_TMC_def by blast

lemma BisT_transT[consumes 5, case_names Match]: 
assumes 0: "c ≈T d" 
and "mustT c s" and "mustT d t"
and "s ≈ t" and "(c,s) →t s'"
obtains t' where "(d,t) →*t t'" and "s' ≈ t'"
using assms BisT_matchT_TMT[OF 0] 
unfolding matchT_TMT_def by blast

lemma BisT_transC2[consumes 5, case_names Match]: 
assumes 0: "c ≈T d" 
and "mustT c s" and "mustT d t"
and "s ≈ t" and "(d,t) →c (d',t')"
obtains c' s' where 
"(c,s) →*c (c',s')" and "s' ≈ t'" and "c' ≈T d'"
using assms BisT_matchC_TMC_rev[OF 0] BisT_Sym
unfolding matchC_TMC_def2 by blast

lemma BisT_transT2[consumes 5, case_names Match]: 
assumes 0: "c ≈T d" 
and "mustT c s" and "mustT d t"
and "s ≈ t" and "(d,t) →t t'"
obtains s' where "(c,s) →*t s'" and "s' ≈ t'"
using assms BisT_matchT_TMT_rev[OF 0] BisT_Sym
unfolding matchT_TMT_def2 by blast

(*  *)
lemma BisT_MtransC[consumes 5, case_names Match]: 
assumes "c ≈T d" 
and "mustT c s" "mustT d t"
and "s ≈ t" and "(c,s) →*c (c',s')"
obtains d' t' where 
"(d,t) →*c (d',t')" and "s' ≈ t'" and "c' ≈T d'"
proof-
  have "(c,s) →*c (c',s') ⟹ 
        mustT c s ⟹ mustT d t ⟹ 
        c ≈T d ⟹ s ≈ t ⟹ 
        (∃ d' t'. (d,t) →*c (d',t') ∧ s' ≈ t' ∧ c' ≈T d')"
  proof (induct rule: MtransC_induct2)
    case (Trans c s c' s' c'' s'')
    then obtain d' t' where d: "(d, t) →*c (d', t')" 
    and "s' ≈ t'" and "c' ≈T d'"
    and c's': "(c', s') →c (c'', s'')" by auto
    moreover have "mustT c' s'" "mustT d' t'"
    by (metis Trans mustT_MtransC d)+
    ultimately obtain d'' t'' where "s'' ≈ t''" and "c'' ≈T d''" 
    and "(d', t') →*c (d'', t'')" by (metis BisT_transC)
    thus ?case using d by (metis MtransC_Trans) 
  qed (metis MtransC_Refl)
  thus thesis using that assms by auto
qed

lemma BisT_MtransT[consumes 5, case_names Match]: 
assumes 1: "c ≈T d" 
and ter: "mustT c s" "mustT d t"
and 2: "s ≈ t" and 3: "(c,s) →*t s'"
obtains t' where "(d,t) →*t t'" and "s' ≈ t'"
proof-
  obtain c'' s'' where 4: "(c,s) →*c (c'',s'')" 
  and 5: "(c'',s'') →t s'" using 3 by (metis MtransT_invert2)
  then obtain d'' t'' where d: "(d,t) →*c (d'',t'')" 
  and "s'' ≈ t''" and "c'' ≈T d''" using 1 2 ter 4 BisT_MtransC by blast
  moreover have "mustT c'' s''" "mustT d'' t''"
  by (metis d 4 assms mustT_MtransC)+
  ultimately obtain t' where "s' ≈ t'" and "(d'',t'') →*t t'"
  by (metis 5 ter BisT_transT) 
  thus thesis using d that by (metis MtransC_MtransT)
qed

lemma BisT_MtransC2[consumes 3, case_names Match]: 
assumes "c ≈T d" 
and ter: "mustT c s" "mustT d t"
and "s ≈ t" and 1: "(d,t) →*c (d',t')"
obtains c' s' where 
"(c,s) →*c (c',s')" and "s' ≈ t'" and "c' ≈T d'"
proof-
  have "d ≈T c" and "t ≈ s" 
  using assms by (metis BisT_Sym indis_sym)+
  then obtain c' s' where 
  "(c,s) →*c (c',s')" and "t' ≈ s'" and "d' ≈T c'"
  by (metis 1 ter BisT_MtransC)
  thus ?thesis using that by (metis BisT_Sym indis_sym)
qed

lemma BisT_MtransT02[consumes 3, case_names Match]: 
assumes "c ≈T d" 
and ter: "mustT c s" "mustT d t"
and "s ≈ t" and "(d,t) →*t t'"
obtains s' where "(c,s) →*t s'" and "s' ≈ t'"
by (metis BisT_MtransT BisT_Sym assms indis_sym)


subsection ‹Execution traces›

(* Partial traces, modeled as lists of configurations *) 
primrec parTrace where
"parTrace [] ⟷ False" |
"parTrace (cf#cfl) ⟷ (cfl ≠ [] ⟶ parTrace cfl ∧ cf →c hd cfl)"

lemma trans_Step2:
  "cf →*c cf' ⟹ cf' →c cf'' ⟹ cf →*c cf''"
  using trans_Step[of "fst cf" "snd cf" "fst cf'" "snd cf'" "fst cf''" "snd cf''"]
  by simp

lemma parTrace_not_empty[simp]: "parTrace cfl ⟹ cfl ≠ []"
  by (cases "cfl = []") simp

lemma parTrace_snoc[simp]:
  "parTrace (cfl@[cf]) ⟷ (cfl ≠ [] ⟶ parTrace cfl ∧ last cfl →c cf)"
  by (induct cfl) auto

lemma MtransC_Ex_parTrace:
  assumes "cf →*c cf'" shows "∃cfl. parTrace cfl ∧ hd cfl = cf ∧ last cfl = cf'"
using assms
proof (induct rule: MtransC_induct)
  case (Refl cf) then show ?case
    by (auto intro!: exI[of _ "[cf]"])
next
  case (Trans cf cf' cf'')
  then obtain cfl where "parTrace cfl" "hd cfl = cf" "last cfl = cf'" by auto
  with ‹cf' →c cf''› show ?case
    by (auto intro!: exI[of _ "cfl @ [cf'']"])
qed

lemma parTrace_imp_MtransC:
  assumes pT: "parTrace cfl"
  shows "(hd cfl) →*c (last cfl)"
using pT proof (induct cfl rule: rev_induct)
  case (snoc cf cfl)
  with trans_Step2[of "hd cfl" "last cfl" cf]
  show ?case
    by auto
qed simp

(* Finite traces, modeled as pairs (partial trace, state): *)
fun finTrace where
"finTrace (cfl,s) ⟷  
 parTrace cfl ∧ last cfl →t s"

declare finTrace.simps[simp del]

(* The length of a finite trace *)
definition "lengthFT tr ≡ Suc (length (fst tr))"

(* The final state of a finite trace *)
definition "fstate tr ≡ snd tr"

(* The initial configuration of a finite trace *)
definition "iconfig tr ≡ hd (fst tr)"

lemma MtransT_Ex_finTrace:
  assumes "cf →*t s" shows "∃tr. finTrace tr ∧ iconfig tr = cf ∧ fstate tr = s"
proof -
  from ‹cf →*t s› obtain cf' cfl where "parTrace cfl" "hd cfl = cf" "last cfl →t s"
    by (auto simp: MtransT.simps dest!: MtransC_Ex_parTrace)
  then show ?thesis
    by (auto simp: finTrace.simps iconfig_def fstate_def
             intro!: exI[of _ "cfl"] exI[of _ s])
qed

lemma finTrace_imp_MtransT:
  "finTrace tr ⟹ iconfig tr →*t fstate tr"
  using parTrace_imp_MtransC[of "fst tr"]
  by (cases tr)
     (auto simp add: iconfig_def fstate_def finTrace.simps MtransT.simps
           simp del: split_paired_Ex)

subsection
‹Relationship between during-execution and after-execution security›

(* For the termination-sensitive versions: *)

lemma WbisT_trace2:
  assumes bis: "c ≈wT d" "s ≈ t" 
  and tr: "finTrace tr" "iconfig tr = (c,s)"
  shows "∃tr'. finTrace tr' ∧ iconfig tr' = (d,t) ∧ fstate tr ≈ fstate tr'"
proof -
  from tr finTrace_imp_MtransT[of tr]
  have "(c, s) →*t fstate tr"
    by auto
  from WbisT_MtransT[OF bis this]
  obtain t' where "(d, t) →*t t'" "fstate tr ≈ t'"
    by auto
  from MtransT_Ex_finTrace[OF this(1)] this(2)
  show ?thesis by auto
qed

theorem WbisT_trace:
  assumes "c ≈wT c" and "s ≈ t" 
  and "finTrace tr" and "iconfig tr = (c,s)"
  shows "∃tr'. finTrace tr' ∧ iconfig tr' = (c,t) ∧ fstate tr ≈ fstate tr'"
using WbisT_trace2[OF assms] .

theorem ZObisT_trace2:
  assumes bis: "c ≈01T d" "s ≈ t" 
  and tr: "finTrace tr" "iconfig tr = (c,s)"
  shows "∃tr'. finTrace tr' ∧ iconfig tr' = (d,t) ∧
               fstate tr ≈ fstate tr' ∧ lengthFT tr' ≤ lengthFT tr"
proof -
  obtain s' cfl where tr_eq: "tr = (cfl, s')" by (cases tr) auto
  with tr have cfl: "cfl ≠ []" "parTrace cfl" "last cfl →t s'" "hd cfl = (c,s)"
    by (auto simp add: finTrace.simps iconfig_def)
  from this bis
  show ?thesis unfolding tr_eq fstate_def snd_conv
  proof (induct cfl arbitrary: c d s t rule: list_nonempty_induct)
    case (single cf)
    with ZObisT_transT[of c d s t s']
    obtain t' where "(d,t) →t t'" "s' ≈ t'" "cf = (c,s)"
      by auto
    then show ?case
      by (intro exI[of _ "([(d,t)], t')"])
         (simp add: finTrace.simps parTrace_def iconfig_def fstate_def lengthFT_def)
  next
    case (cons cf cfl)
    then have cfl: "parTrace cfl" "last cfl →t s'"
      by auto

    from cons have "(c,s) →c (fst (hd cfl), snd (hd cfl))"
      unfolding parTrace_def by (auto simp add: hd_conv_nth)
    with ‹c ≈01T d› ‹s ≈ t› show ?case
    proof (cases rule: ZObisT_transC)
      case MatchS
      from cons(2)[OF cfl _ this(2,1)]
      show ?thesis
        by (auto simp: lengthFT_def le_Suc_eq)
    next
      case (Match d' t')
      from cons(2)[OF cfl _ Match(3,2)]
      obtain cfl' s where "finTrace (cfl', s)" "hd cfl' = (d', t')" "s' ≈ s" "length cfl' ≤ length cfl"
        by (auto simp: iconfig_def lengthFT_def)
      with Match(1) show ?thesis
        by (intro exI[of _ "((d,t)#cfl', s)"])
           (auto simp: iconfig_def lengthFT_def finTrace.simps)
    qed
  qed
qed

theorem ZObisT_trace:
  assumes "c ≈01T c" "s ≈ t"
  and "finTrace tr" "iconfig tr = (c,s)"
  shows "∃tr'. finTrace tr' ∧ iconfig tr' = (c,t) ∧
               fstate tr ≈ fstate tr' ∧ lengthFT tr' ≤ lengthFT tr"
  using ZObisT_trace2[OF assms] .

theorem Sbis_trace:
  assumes bis: "c ≈s d" "s ≈ t"
  and tr: "finTrace tr" "iconfig tr = (c,s)"
  shows "∃tr'. finTrace tr' ∧ iconfig tr' = (d,t) ∧ fstate tr ≈ fstate tr' ∧
               lengthFT tr' = lengthFT tr"
proof -
  obtain s' cfl where tr_eq: "tr = (cfl, s')" by (cases tr) auto
  with tr have cfl: "cfl ≠ []" "parTrace cfl" "last cfl →t s'" "hd cfl = (c,s)"
    by (auto simp add: finTrace.simps iconfig_def)
  from this bis
  show ?thesis unfolding tr_eq fstate_def snd_conv
  proof (induct cfl arbitrary: c d s t rule: list_nonempty_induct)
    case (single cf)
    with Sbis_transT[of c d s t s']
    obtain t' where "(d,t) →t t'" "s' ≈ t'" "cf = (c,s)"
      by auto
    with single show ?case
      by (intro exI[of _ "([(d,t)], t')"])
         (simp add: lengthFT_def iconfig_def indis_refl finTrace.simps)
  next
    case (cons cf cfl)
    with Sbis_transC[of c d s t "fst (hd cfl)" "snd (hd cfl)"]
    obtain d' t' where *: "(d,t) →c (d',t')" "snd (hd cfl) ≈ t'" "fst (hd cfl) ≈s d'"
      by auto
    moreover
    with cons(2)[of "fst (hd cfl)" "snd (hd cfl)" d' t'] cons(1,3,4)
    obtain cfl' s where "finTrace (cfl', s)" "hd cfl' = (d', t')" "s' ≈ s" "length cfl' = length cfl"
      by (auto simp: iconfig_def lengthFT_def)
    ultimately show ?case
      by (intro exI[of _ "((d,t)#cfl', s)"])
         (auto simp: finTrace.simps lengthFT_def iconfig_def)
  qed
qed

corollary siso_trace:
assumes "siso c" and "s ≈ t" 
and "finTrace tr" and "iconfig tr = (c,s)"
shows 
"∃ tr'. finTrace tr' ∧ iconfig tr' = (c,t) ∧ fstate tr ≈ fstate tr'
        ∧ lengthFT tr' = lengthFT tr"
apply(rule Sbis_trace)
using assms by auto

(* For the termination-insensitive versions: *)
theorem Wbis_trace:
  assumes T: "⋀s. mustT c s"
  and bis: "c ≈w c" "s ≈ t"
  and tr: "finTrace tr" "iconfig tr = (c,s)"
  shows "∃tr'. finTrace tr' ∧ iconfig tr' = (c,t) ∧ fstate tr ≈ fstate tr'"
proof -
  from tr finTrace_imp_MtransT[of tr]
  have "(c, s) →*t fstate tr"
    by auto
  from bis this
  show ?thesis
  proof (cases rule: Wbis_MtransT)
    case (Match t')
    from MtransT_Ex_finTrace[OF this(1)] this(2)
    show ?thesis by auto
  next
    case (MatchO d' t')
    from T[THEN mustT_MtransC, OF MatchO(1)] have "mustT d' t'" .
    from this[THEN mustT_MtransT] obtain s' where "(d', t') →*t s'" ..
    from MatchO(1) ‹(d', t') →*t s'› have "(c, t) →*t s'" by (rule MtransC_MtransT)
    note MtransT_Ex_finTrace[OF this]
    moreover
    from ‹discr d'› ‹(d', t') →*t s'› have "t' ≈ s'" by (rule discr_MtransT)
    with ‹fstate tr ≈ t'›have "fstate tr ≈ s'" by (rule indis_trans)
    ultimately show ?thesis
      by auto
  qed
qed

corollary ZObis_trace:
  assumes T: "⋀s. mustT c s"
  and ZObis: "c ≈01 c" and indis: "s ≈ t"
  and tr: "finTrace tr" "iconfig tr = (c,s)"
  shows "∃tr'. finTrace tr' ∧ iconfig tr' = (c,t) ∧ fstate tr ≈ fstate tr'"
  by (rule Wbis_trace[OF T bis_imp(4)[OF ZObis] indis tr])

(* For the mustT-interactive notion: *)

theorem BisT_trace:
  assumes bis: "c ≈T c" "s ≈ t"
  and T: "mustT c s" "mustT c t"
  and tr: "finTrace tr" "iconfig tr = (c,s)"
  shows "∃tr'. finTrace tr' ∧ iconfig tr' = (c,t) ∧ fstate tr ≈ fstate tr'"
proof -
  from tr finTrace_imp_MtransT[of tr]
  have "(c, s) →*t fstate tr"
    by auto
  from BisT_MtransT[OF bis(1) T bis(2) this]
  obtain t' where "(c,t) →*t t'" "fstate tr ≈ t'" .
  from MtransT_Ex_finTrace[OF this(1)] this(2)
  show ?thesis
    by auto
qed

end 
(* context PL_Indis  *)


end