Theory BD_Security_Unwinding

(*<*)
theory BD_Security_Unwinding
  imports BD_Security_IO
begin
(*>*)

section ‹Unwinding proof method›

text ‹This section formalizes the unwinding proof method for BD Security discussed in
\<^cite>‹‹Section 5.1› in "cocon-CAV2014"››

context BD_Security_IO
begin

definition consume :: "('state,'act,'out) trans ⇒ 'value list ⇒ 'value list ⇒ bool" where
"consume trn vl vl' ≡
 if φ trn then vl ≠ [] ∧ f trn = hd vl ∧ vl' = tl vl
 else vl' = vl"

definition consumeList :: "('state,'act,'out) trans trace ⇒ 'value list ⇒ 'value list ⇒ bool" where
"consumeList tr vl vl' ≡ vl = (V tr) @ vl'"

lemma length_consume[simp]:
"consume trn vl vl' ⟹ length vl' < Suc (length vl)"
unfolding consume_def by (auto split: if_splits)

lemma ex_consume_φ:
assumes "¬ φ trn"
obtains vl' where "consume trn vl vl'"
using assms unfolding consume_def by auto

lemma ex_consume_NO:
assumes "vl ≠ []" and "f trn = hd vl"
obtains vl' where "consume trn vl vl'"
using assms unfolding consume_def by (cases "φ trn") auto

(* independent action: *)
definition iaction where
"iaction Δ s vl s1 vl1 ≡
 ∃ al1 vl1'.
   let tr1 = traceOf s1 al1; s1' = tgtOf (last tr1) in
   list_ex φ tr1 ∧ consumeList tr1 vl1 vl1' ∧
   never γ tr1
   ∧
   Δ s vl s1' vl1'"

(* Multi-step intro, reflecting the improved def: *)
lemma iactionI_ms[intro?]:
assumes s: "sstep s1 al1 = (oul1, s1')"
and l: "list_ex φ (traceOf s1 al1)"
and "consumeList (traceOf s1 al1) vl1 vl1'"
and "never γ (traceOf s1 al1)" and "Δ s vl s1' vl1'"
shows "iaction Δ s vl s1 vl1"
proof-
  have "al1 ≠ []" using l by auto
  from sstep_tgtOf_traceOf[OF this s] assms
  show ?thesis unfolding iaction_def by auto
qed

lemma sstep_eq_singleiff[simp]: "sstep s1 [a1] = ([ou1], s1') ⟷ step s1 a1 = (ou1, s1')"
using sstep_Cons by auto

(* The less expressive, single-step intro: *)
lemma iactionI[intro?]:
assumes "step s1 a1 = (ou1, s1')" and "φ (Trans s1 a1 ou1 s1')"
and "consume (Trans s1 a1 ou1 s1') vl1 vl1'"
and "¬ γ (Trans s1 a1 ou1 s1')" and "Δ s vl s1' vl1'"
shows "iaction Δ s vl s1 vl1"
using assms
by (intro iactionI_ms[of _ "[a1]" "[ou1]"]) (auto simp: consume_def consumeList_def)

definition match where
"match Δ s s1 vl1 a ou s' vl' ≡
 ∃ al1 vl1'.
    let trn = Trans s a ou s'; tr1 = traceOf s1 al1; s1' = tgtOf (last tr1) in
    al1 ≠ [] ∧ consumeList tr1 vl1 vl1' ∧
    O tr1 = O [trn] ∧
    Δ s' vl' s1' vl1'"

lemma matchI_ms[intro?]:
assumes s: "sstep s1 al1 = (oul1, s1')"
and l: "al1 ≠ []"
and "consumeList (traceOf s1 al1) vl1 vl1'"
and "O (traceOf s1 al1) = O [Trans s a ou s']"
and "Δ s' vl' s1' vl1'"
shows "match Δ s s1 vl1 a ou s' vl'"
proof-
  from sstep_tgtOf_traceOf[OF l s] assms
  show ?thesis unfolding match_def by (intro exI[of _ al1]) auto
qed

lemma matchI[intro?]:
assumes "validTrans (Trans s1 a1 ou1 s1')"
and "consume (Trans s1 a1 ou1 s1') vl1 vl1'" and "γ (Trans s a ou s') = γ (Trans s1 a1 ou1 s1')"
and "γ (Trans s a ou s') ⟹ g (Trans s a ou s') = g (Trans s1 a1 ou1 s1')"
and "Δ s' vl' s1' vl1'"
shows "match Δ s s1 vl1 a ou s' vl'"
using assms by (intro matchI_ms[of s1 "[a1]" "[ou1]" s1'])
               (auto simp: consume_def consumeList_def split: if_splits)

definition ignore where
"ignore Δ s s1 vl1 a ou s' vl' ≡
 ¬ γ (Trans s a ou s') ∧
 Δ s' vl' s1 vl1"

lemma ignoreI[intro?]:
assumes "¬ γ (Trans s a ou s')" and "Δ s' vl' s1 vl1"
shows "ignore Δ s s1 vl1 a ou s' vl'"
unfolding ignore_def using assms by auto

(* reaction: *)
definition reaction where
"reaction Δ s vl s1 vl1 ≡
 ∀ a ou s' vl'.
   let trn = Trans s a ou s' in
   validTrans trn ∧ ¬ T trn ∧
   consume trn vl vl'
   ⟶
   match Δ s s1 vl1 a ou s' vl'
   ∨
   ignore Δ s s1 vl1 a ou s' vl'"

lemma reactionI[intro?]:
assumes
"⋀a ou s' vl'.
   ⟦step s a = (ou, s'); ¬ T (Trans s a ou s');
    consume (Trans s a ou s') vl vl'⟧
   ⟹
   match Δ s s1 vl1 a ou s' vl' ∨ ignore Δ s s1 vl1 a ou s' vl'"
shows "reaction Δ s vl s1 vl1"
using assms unfolding reaction_def by auto

definition "exit" :: "'state ⇒ 'value ⇒ bool" where
"exit s v ≡ ∀ tr trn. validFrom s (tr ## trn) ∧ never T (tr ## trn) ∧ φ trn ⟶ f trn ≠ v"

lemma exit_coind:
assumes K: "K s"
and I: "⋀ trn. ⟦K (srcOf trn); validTrans trn; ¬ T trn⟧
        ⟹ (φ trn ⟶ f trn ≠ v) ∧ K (tgtOf trn)"
shows "exit s v"
using K unfolding exit_def proof(intro allI conjI impI)
  fix tr trn assume "K s" and "validFrom s (tr ## trn) ∧ never T (tr ## trn) ∧ φ trn"
  thus "f trn ≠ v"
  using I unfolding validFrom_def by (induction tr arbitrary: s trn)
  (auto, metis neq_Nil_conv rotate1.simps(2) rotate1_is_Nil_conv valid_ConsE)
qed

definition noVal where
"noVal K v ≡
 ∀ s a ou s'. reachNT s ∧ K s ∧ step s a = (ou,s') ∧ φ (Trans s a ou s') ⟶ f (Trans s a ou s') ≠ v"

lemma noVal_disj:
assumes "noVal Inv1 v" and "noVal Inv2 v"
shows "noVal (λ s. Inv1 s ∨ Inv2 s) v"
using assms unfolding noVal_def by metis

lemma noVal_conj:
assumes "noVal Inv1 v" and "noVal Inv2 v"
shows "noVal (λ s. Inv1 s ∧ Inv2 s) v"
using assms unfolding noVal_def by blast

(* Often encountered sufficient criterion for noVal: *)
definition noφ where
"noφ K ≡ ∀ s a ou s'. reachNT s ∧ K s ∧ step s a = (ou,s') ⟶ ¬ φ (Trans s a ou s')"

lemma noφ_noVal: "noφ K ⟹ noVal K v"
unfolding noφ_def noVal_def by auto

(* intro rule for quick inline checks: *)
lemma exitI[consumes 2, induct pred: "exit"]:
assumes rs: "reachNT s" and K: "K s"
and I:
"⋀ s a ou s'.
   ⟦reach s; reachNT s; step s a = (ou,s'); K s⟧
   ⟹ (φ (Trans s a ou s') ⟶ f (Trans s a ou s') ≠ v) ∧ K s'"
shows "exit s v"
proof-
  let ?K = "λ s. reachNT s ∧ K s"
  show ?thesis using assms by (intro exit_coind[of ?K])
  (metis reachNT_reach IO_Automaton.validTrans reachNT.Step trans.exhaust_sel)+
qed

(* intro rule for more elaborate checks: *)
lemma exitI2:
assumes rs: "reachNT s" and K: "K s"
and "invarNT K" and "noVal K v"
shows "exit s v"
proof-
  let ?K = "λ s. reachNT s ∧ K s"
  show ?thesis using assms unfolding invarNT_def noVal_def apply(intro exit_coind[of ?K])
  by metis (metis IO_Automaton.validTrans reachNT.Step trans.exhaust_sel)
qed

(* Binary version of the invariant: *)
definition noVal2 where
"noVal2 K v ≡
 ∀ s a ou s'. reachNT s ∧ K s v ∧ step s a = (ou,s') ∧ φ (Trans s a ou s') ⟶ f (Trans s a ou s') ≠ v"

lemma noVal2_disj:
assumes "noVal2 Inv1 v" and "noVal2 Inv2 v"
shows "noVal2 (λ s v. Inv1 s v ∨ Inv2 s v) v"
using assms unfolding noVal2_def by metis

lemma noVal2_conj:
assumes "noVal2 Inv1 v" and "noVal2 Inv2 v"
shows "noVal2 (λ s v. Inv1 s v ∧ Inv2 s v) v"
using assms unfolding noVal2_def by blast

lemma noVal_noVal2: "noVal K v ⟹ noVal2 (λ s v. K s) v"
unfolding noVal_def noVal2_def by auto

lemma exitI_noVal2[consumes 2, induct pred: "exit"]:
assumes rs: "reachNT s" and K: "K s v"
and I:
"⋀ s a ou s'.
   ⟦reach s; reachNT s; step s a = (ou,s'); K s v⟧
   ⟹ (φ (Trans s a ou s') ⟶ f (Trans s a ou s') ≠ v) ∧ K s' v"
shows "exit s v"
proof-
  let ?K = "λ s. reachNT s ∧ K s v"
  show ?thesis using assms by (intro exit_coind[of ?K])
  (metis reachNT_reach IO_Automaton.validTrans reachNT.Step trans.exhaust_sel)+
qed

lemma exitI2_noVal2:
assumes rs: "reachNT s" and K: "K s v"
and "invarNT (λ s. K s v)" and "noVal2 K v"
shows "exit s v"
proof-
  let ?K = "λ s. reachNT s ∧ K s v"
  show ?thesis using assms unfolding invarNT_def noVal2_def
  by (intro exit_coind[of ?K]) (metis IO_Automaton.validTrans reachNT.Step trans.exhaust_sel)+
qed

(* end binary version *)

lemma exit_validFrom:
assumes vl: "vl ≠ []" and i: "exit s (hd vl)" and v: "validFrom s tr" and V: "V tr = vl"
and T: "never T tr"
shows False
using i v V T proof(induction tr arbitrary: s)
  case Nil thus ?case by (metis V_simps(1) vl)
next
  case (Cons trn tr s)
  show ?case
  proof(cases "φ trn")
    case True
    hence "f trn = hd vl" using Cons by (metis V_simps(3) hd_Cons_tl list.inject vl)
    moreover have "validFrom s [trn]" using ‹validFrom s (trn # tr)›
    unfolding validFrom_def by auto
    ultimately show ?thesis using Cons True unfolding exit_def
    by (elim allE[of _ "[]"]) auto
  next
    case False
    hence "V tr = vl" using Cons by auto
    moreover have "never T tr" by (metis Cons.prems list_all_simps)
    moreover from ‹validFrom s (trn # tr)› have "validFrom (tgtOf trn) tr" and s: "s = srcOf trn"
    by (metis list.distinct(1) validFrom_def valid_ConsE Cons.prems(2)
              validFrom_def list.discI list.sel(1))+
    moreover have "exit (tgtOf trn) (hd vl)" using ‹exit s (hd vl)›
    unfolding exit_def s by simp
    (metis (no_types) Cons.prems(2) Cons.prems(4) append_Cons list.sel(1)
           list.distinct list_all_simps valid.Cons validFrom_def valid_ConsE)
    ultimately show ?thesis using Cons(1) by auto
  qed
qed

definition unwind where
"unwind Δ ≡
 ∀ s vl s1 vl1.
   reachNT s ∧ reach s1 ∧ Δ s vl s1 vl1
   ⟶
   (vl ≠ [] ∧ exit s (hd vl))
   ∨
   iaction Δ s vl s1 vl1
   ∨
   ((vl ≠ [] ∨ vl1 = []) ∧ reaction Δ s vl s1 vl1)"

lemma unwindI[intro?]:
assumes
"⋀ s vl s1 vl1.
   ⟦reachNT s; reach s1; Δ s vl s1 vl1⟧
   ⟹
   (vl ≠ [] ∧ exit s (hd vl))
   ∨
   iaction Δ s vl s1 vl1
   ∨
   ((vl ≠ [] ∨ vl1 = []) ∧ reaction Δ s vl s1 vl1)"
shows "unwind Δ"
using assms unfolding unwind_def by auto

lemma unwind_trace:
assumes unwind: "unwind Δ" and "reachNT s" and "reach s1" and "Δ s vl s1 vl1"
and "validFrom s tr" and "never T tr" and "V tr = vl"
shows "∃tr1. validFrom s1 tr1 ∧ O tr1 = O tr ∧ V tr1 = vl1"
proof-
  let ?S = "λ tr vl1.
  ∀ s vl s1. reachNT s ∧ reach s1 ∧ Δ s vl s1 vl1 ∧ validFrom s tr ∧ never T tr ∧ V tr = vl ⟶
          (∃tr1. validFrom s1 tr1 ∧ O tr1 = O tr ∧ V tr1 = vl1)"
  let ?f = "λ tr vl1. length tr + length vl1"
  have "?S tr vl1"
  proof(induct rule: measure_induct2[of ?f ?S])
    case (IH tr vl1)
    show ?case
    proof(intro allI impI, elim conjE)
      fix s vl s1 assume rs: "reachNT s" and rs1: "reach s1" and Δ: "Δ s vl s1 vl1"
      and v: "validFrom s tr" and NT: "never T tr" and V: "V tr = vl"
      hence "(vl ≠ [] ∧ exit s (hd vl)) ∨
             iaction Δ s vl s1 vl1 ∨
             (reaction Δ s vl s1 vl1 ∧ ¬ iaction Δ s vl s1 vl1)"
      (is "?exit ∨ ?iact ∨ ?react ∧ _")
      using unwind unfolding unwind_def by metis
      thus "∃tr1. validFrom s1 tr1 ∧ O tr1 = O tr ∧ V tr1 = vl1"
      proof safe
        assume "vl ≠ []" and "exit s (hd vl)"
        hence False using v V exit_validFrom NT by auto
        thus ?thesis by auto
      next
        assume ?iact
        thus ?thesis  unfolding iaction_def Let_def proof safe
          fix al1 :: "'act list" and vl1'
          let ?tr1 = "traceOf s1 al1"  let ?s1' = "tgtOf (last ?tr1)"
          assume φ1: "list_ex φ (traceOf s1 al1)" and c: "consumeList ?tr1 vl1 vl1'"
             and γ: "never γ ?tr1" and Δ: "Δ s vl ?s1' vl1'"
          from φ1 have tr1: "?tr1 ≠ []" and len_V1: "length (V ?tr1) > 0"
            by (auto iff: list_ex_iff_length_V)
          with c have "length vl1' < length vl1" unfolding consumeList_def by auto
          moreover have "reach ?s1'" using rs1 tr1 by (intro validFrom_reach) auto
          ultimately obtain tr1' where "validFrom ?s1' tr1'" and "O tr1' = O tr" and "V tr1' = vl1'"
            using IH[of tr vl1'] rs Δ v NT V by auto
          then show ?thesis using tr1 γ c unfolding consumeList_def
            by (intro exI[of _ "?tr1 @ tr1'"])
               (auto simp: O_append O_Nil_never V_append validFrom_append)
        qed
      next
        assume react: ?react and iact: "¬ ?iact"
        show ?thesis
        proof(cases tr)
          case Nil note tr = Nil
          hence vl: "vl = []" using V by simp
          show ?thesis proof(cases vl1)
            case Nil note vl1 = Nil
            show ?thesis using IH[of tr vl1] Δ V NT V unfolding tr vl1 by auto
          next
            case Cons
            hence False using vl unwind rs rs1 Δ iact unfolding unwind_def by auto
            thus ?thesis by auto
          qed
        next
          case (Cons trn tr') note tr = Cons
          show ?thesis
          proof(cases trn)
            case (Trans ss a ou s') note trn = Trans let ?trn = "Trans s a ou s'"
            have ss: "ss = s" using trn v unfolding tr validFrom_def by auto
            have Ta: "¬ T ?trn" and s: "s = srcOf trn" and vtrans: "validTrans ?trn"
            and v': "validFrom s' tr'" and NT': "never T tr'"
            using v NT V unfolding tr validFrom_def trn by auto
            have rs': "reachNT s'" using rs vtrans Ta by (auto intro: reachNT_PairI)
            {assume "φ ?trn" hence "vl ≠ [] ∧ f ?trn = hd vl" using V unfolding tr trn ss by auto
            }
            then obtain vl' where c: "consume ?trn vl vl'"
            using ex_consume_φ ex_consume_NO by metis
            have V': "V tr' = vl'" using V c unfolding tr trn ss consume_def
            by (cases "φ ?trn") (simp_all, metis list.sel(2-3))
            have "match Δ s s1 vl1 a ou s' vl' ∨ ignore Δ s s1 vl1 a ou s' vl'" (is "?match ∨ ?ignore")
            using react unfolding reaction_def using vtrans Ta c by auto
            thus ?thesis proof safe
              assume ?match
              thus ?thesis unfolding match_def Let_def proof (elim exE conjE)
                fix al1 :: "'act list" and vl1'
                let ?tr = "traceOf s1 al1"
                let ?s1' = "tgtOf (last ?tr)"
                assume al1: "al1 ≠ []"
                   and c: "consumeList ?tr vl1 vl1'"
                   and O: "O ?tr = O [Trans s a ou s']"
                   and Δ: "Δ s' vl' ?s1' vl1'"
                from c have len: "length tr' + length vl1' < length tr + length vl1"
                  using tr unfolding consumeList_def by auto
                have "reach ?s1'" using rs1 al1 by (intro validFrom_reach) auto
                then obtain tr1' where "validFrom ?s1' tr1'" and "O tr1' = O tr'" and "V tr1' = vl1'"
                  using IH[OF len] rs' Δ v' NT' V' tr by auto
                then show ?thesis using c O al1 unfolding consumeList_def tr trn ss
                  by (intro exI[of _ "?tr @ tr1'"])
                     (cases "γ ?trn"; auto simp: O_append O_Nil_never V_append validFrom_append)
              qed
            next
              assume ?ignore
              thus ?thesis unfolding ignore_def Let_def proof (elim exE conjE)
                assume γ: "¬ γ ?trn" and Δ: "Δ s' vl' s1 vl1"
                obtain tr1 where v1: "validFrom s1 tr1" and O: "O tr1 = O tr'" and V: "V tr1 = vl1"
                using IH[of tr' vl1] rs' rs1 Δ v' NT' V' c unfolding tr by auto
                show ?thesis
                apply(intro exI[of _ tr1])
                using v1 O V γ unfolding tr trn ss by auto
              qed
            qed
          qed
        qed
      qed
    qed
  qed
  thus ?thesis using assms by auto
qed

theorem unwind_secure:
assumes init: "⋀ vl vl1. B vl vl1 ⟹ Δ istate vl istate vl1"
and unwind: "unwind Δ"
shows secure
using assms unwind_trace unfolding secure_def by (blast intro: reach.Istate reachNT.Istate)

end (* locale BD_Security_IO *)

(*<*)
end
(*>*)