Theory Composing_Security_Network

section ‹N-ary compositionality theorem›

text ‹This theory provides the n-ary version of
the compositionality theorem for BD security.
It corresponds to Theorem 3 from \<^cite>‹"cosmedis-SandP2017"›
and to Theorem 7 (the System Compositionality Theorem, n-ary case) from
\<^cite>‹"BDsecurity-ITP2021"›.
›

theory Composing_Security_Network
imports Trivial_Security Transporting_Security Composing_Security
begin

text ‹Definition of n-ary system composition:›

type_synonym ('nodeid, 'state) nstate = "'nodeid ⇒ 'state"
datatype ('nodeid, 'state, 'trans) ntrans =
  LTrans "('nodeid, 'state) nstate" 'nodeid 'trans
| CTrans "('nodeid, 'state) nstate" 'nodeid 'trans 'nodeid 'trans
datatype ('nodeid, 'obs) nobs = LObs 'nodeid 'obs | CObs 'nodeid 'obs 'nodeid 'obs
datatype ('nodeid, 'val) nvalue = LVal 'nodeid 'val | CVal 'nodeid 'val 'nodeid 'val
datatype com = Send | Recv | Internal

locale TS_Network =
fixes
   istate :: "('nodeid, 'state) nstate" and validTrans :: "'nodeid ⇒ 'trans ⇒ bool"
 and
   srcOf :: "'nodeid ⇒ 'trans ⇒ 'state" and tgtOf :: "'nodeid ⇒ 'trans ⇒ 'state"
 and
   nodes :: "'nodeid set"
 and
   comOf :: "'nodeid ⇒ 'trans ⇒ com"
 and
   tgtNodeOf :: "'nodeid ⇒ 'trans ⇒ 'nodeid"
 and
   sync :: "'nodeid ⇒ 'trans ⇒ 'nodeid ⇒ 'trans ⇒ bool"
assumes
   finite_nodes: "finite nodes"
and
  isCom_tgtNodeOf: "⋀nid trn.
    ⟦validTrans nid trn; comOf nid trn = Send ∨ comOf nid trn = Recv;
    Transition_System.reach (istate nid) (validTrans nid) (srcOf nid) (tgtOf nid) (srcOf nid trn)⟧
    ⟹ tgtNodeOf nid trn ≠ nid"
begin

abbreviation isCom :: "'nodeid ⇒ 'trans ⇒ bool"
where "isCom nid trn ≡ (comOf nid trn = Send ∨ comOf nid trn = Recv) ∧ tgtNodeOf nid trn ∈ nodes"

abbreviation lreach :: "'nodeid ⇒ 'state ⇒ bool"
where "lreach nid s ≡ Transition_System.reach (istate nid) (validTrans nid) (srcOf nid) (tgtOf nid) s"

text ‹Two types of valid transitions in the network:

       ▪ Local transitions of network nodes, i.e. transitions that are not communicating
         (with another node in the network. There might be external communication transitions
         with the outside world. These are kept as local transitions, and turn into
         synchronized communication transitions when the target node joins the network during
         the inductive proofs later on.)

       ▪ Communication transitions between two network nodes; these are allowed if they are
         synchronized.›

fun nValidTrans :: "('nodeid, 'state, 'trans) ntrans ⇒ bool" where
  Local: "nValidTrans (LTrans s nid trn) =
     (validTrans nid trn ∧ srcOf nid trn = s nid ∧ nid ∈ nodes ∧ ¬isCom nid trn)"
| Comm: "nValidTrans (CTrans s nid1 trn1 nid2 trn2) =
     (validTrans nid1 trn1 ∧ srcOf nid1 trn1 = s nid1 ∧ comOf nid1 trn1 = Send ∧ tgtNodeOf nid1 trn1 = nid2 ∧
      validTrans nid2 trn2 ∧ srcOf nid2 trn2 = s nid2 ∧ comOf nid2 trn2 = Recv ∧ tgtNodeOf nid2 trn2 = nid1 ∧
      nid1 ∈ nodes ∧ nid2 ∈ nodes ∧ nid1 ≠ nid2 ∧
      sync nid1 trn1 nid2 trn2)"

fun nSrcOf :: "('nodeid, 'state, 'trans) ntrans ⇒ ('nodeid, 'state) nstate" where
  "nSrcOf (LTrans s nid trn) = s"
| "nSrcOf (CTrans s nid1 trn1 nid2 trn2) = s"

fun nTgtOf :: "('nodeid, 'state, 'trans) ntrans ⇒ ('nodeid, 'state) nstate" where
  "nTgtOf (LTrans s nid trn) = s(nid := tgtOf nid trn)"
| "nTgtOf (CTrans s nid1 trn1 nid2 trn2) = s(nid1 := tgtOf nid1 trn1, nid2 := tgtOf nid2 trn2)"

sublocale Transition_System istate nValidTrans nSrcOf nTgtOf .

fun nSrcOfTrFrom where
  "nSrcOfTrFrom s [] = s"
| "nSrcOfTrFrom s (trn # tr) = nSrcOf trn"

lemma nSrcOfTrFrom_nSrcOf_hd:
  "tr ≠ [] ⟹ nSrcOfTrFrom s tr = nSrcOf (hd tr)"
  by (cases tr) auto

fun nTgtOfTrFrom where
  "nTgtOfTrFrom s [] = s"
| "nTgtOfTrFrom s (trn # tr) = nTgtOfTrFrom (nTgtOf trn) tr"

lemma nTgtOfTrFrom_nTgtOf_last:
  "tr ≠ [] ⟹ nTgtOfTrFrom s tr = nTgtOf (last tr)"
  by (induction s tr rule: nTgtOfTrFrom.induct) auto

lemma reach_lreach:
assumes "reach s"
obtains "lreach nid (s nid)"
proof -
  interpret Node: Transition_System "istate nid" "validTrans nid" "srcOf nid" "tgtOf nid" .
  from assms that show thesis
  proof induction
    case Istate then show thesis using Node.reach.Istate by auto
  next
    case (Step s trn s')
      show thesis proof (rule Step.IH)
        assume "Node.reach (s nid)"
        then show thesis using Step.hyps Node.reach.Step[of "s nid" _ "s' nid"]
          by (intro Step.prems, cases trn) (auto)
      qed
  qed
qed

text ‹Alternative characterization of valid network traces as composition of valid node traces.›

inductive comp :: "('nodeid, 'state) nstate ⇒ ('nodeid, 'state, 'trans) ntrans list ⇒ bool"
where
  Nil: "comp s []"
| Local: "⋀s trn s' tr nid.
    ⟦comp s tr; tgtOf nid trn = s nid; s' = s(nid := srcOf nid trn); nid ∈ nodes; ¬isCom nid trn⟧
    ⟹ comp s' (LTrans s' nid trn # tr)"
| Comm: "⋀s trn1 trn2 s' tr nid1 nid2.
    ⟦comp s tr; tgtOf nid1 trn1 = s nid1; tgtOf nid2 trn2 = s nid2;
    s' = s(nid1 := srcOf nid1 trn1, nid2 := srcOf nid2 trn2);
    nid1 ∈ nodes; nid2 ∈ nodes; nid1 ≠ nid2;
    comOf nid1 trn1 = Send; tgtNodeOf nid1 trn1 = nid2;
    comOf nid2 trn2 = Recv; tgtNodeOf nid2 trn2 = nid1;
    sync nid1 trn1 nid2 trn2⟧
    ⟹ comp s' (CTrans s' nid1 trn1 nid2 trn2 # tr)"

abbreviation lValidFrom :: "'nodeid ⇒ 'state ⇒ 'trans list ⇒ bool" where
  "lValidFrom nid ≡ Transition_System.validFrom (validTrans nid) (srcOf nid) (tgtOf nid)"

fun decomp where
  "decomp (LTrans s nid' trn' # tr) nid = (if nid' = nid then trn' # decomp tr nid else decomp tr nid)"
| "decomp (CTrans s nid1 trn1 nid2 trn2 # tr) nid = (if nid1 = nid then trn1 # decomp tr nid else
                                                    (if nid2 = nid then trn2 # decomp tr nid else
                                                     decomp tr nid))"
| "decomp [] nid = []"

lemma decomp_append: "decomp (tr1 @ tr2) nid = decomp tr1 nid @ decomp tr2 nid"
proof (induction tr1)
  case (Cons trn tr1) then show ?case by (cases trn) auto
qed auto

lemma validFrom_comp: "validFrom s tr ⟹ comp s tr"
proof (induction tr arbitrary: s)
  case Nil show ?case by (intro comp.Nil)
next
  case (Cons trn tr s)
  then have IH: "comp (nTgtOf trn) tr" by (auto simp: validFrom_Cons)
  then show ?case using Cons.prems by (cases trn) (auto simp: validFrom_Cons intro: comp.intros)
qed

lemma validFrom_lValidFrom:
assumes "validFrom s tr"
shows "lValidFrom nid (s nid) (decomp tr nid)"
proof -
  interpret Node: Transition_System "istate nid" "validTrans nid" "srcOf nid" "tgtOf nid" .
  from assms show ?thesis proof (induction tr arbitrary: s)
    case (Cons trn tr)
      have "lValidFrom nid (nTgtOf trn nid) (decomp tr nid)"
        using Cons.prems by (intro Cons.IH) (auto simp: validFrom_Cons)
      then show ?case using Cons.prems by (cases trn) (auto simp: validFrom_Cons Node.validFrom_Cons)
  qed auto
qed

lemma comp_validFrom:
assumes "comp s tr" and "⋀nid. lValidFrom nid (s nid) (decomp tr nid)"
shows "validFrom s tr"
using assms proof induction
  case (Local s trn s' tr nid)
  interpret Node: Transition_System "istate nid" "validTrans nid" "srcOf nid" "tgtOf nid" .
  have "Node.validFrom (s' nid) (decomp (LTrans s' nid trn # tr) nid)" using Local by blast
  then have "nValidTrans (LTrans s' nid trn)" using Local by (auto simp: Node.validFrom_Cons)
  moreover have "validFrom s tr" proof (intro Local.IH)
    fix nid'
    have "lValidFrom nid' (s' nid') (decomp (LTrans s' nid trn # tr) nid')" using Local(7) .
    then show "lValidFrom nid' (s nid') (decomp tr nid')" using Local(2,3)
      by (cases "nid' = nid") (auto split: if_splits simp: Node.validFrom_Cons)
  qed
  ultimately show ?case using Local(2,3) unfolding validFrom_Cons by auto
next
  case (Comm s trn1 trn2 s' tr nid1 nid2)
  interpret Node1: Transition_System "istate nid1" "validTrans nid1" "srcOf nid1" "tgtOf nid1" .
  interpret Node2: Transition_System "istate nid2" "validTrans nid2" "srcOf nid2" "tgtOf nid2" .
  have "Node1.validFrom (s' nid1) (decomp (CTrans s' nid1 trn1 nid2 trn2 # tr) nid1)"
   and "Node2.validFrom (s' nid2) (decomp (CTrans s' nid1 trn1 nid2 trn2 # tr) nid2)" using Comm by blast+
  then have "nValidTrans (CTrans s' nid1 trn1 nid2 trn2)" using Comm
    by (auto simp: Node1.validFrom_Cons Node2.validFrom_Cons)
  moreover have "validFrom s tr" proof (intro Comm.IH)
    fix nid'
    have "lValidFrom nid' (s' nid') (decomp (CTrans s' nid1 trn1 nid2 trn2 # tr) nid')" using Comm(14) .
    then show "lValidFrom nid' (s nid') (decomp tr nid')"
      using Comm(2,3,4) Node1.validFrom_Cons Node2.validFrom_Cons
      by (cases "nid' = nid1 ∨ nid' = nid2") (auto split: if_splits)
  qed
  ultimately show ?case using Comm(2,3,4) unfolding validFrom_Cons by auto
qed auto


lemma validFrom_iff_comp:
"validFrom s tr ⟷ comp s tr ∧ (∀nid. lValidFrom nid (s nid) (decomp tr nid))"
using validFrom_comp validFrom_lValidFrom comp_validFrom by blast

end

locale Empty_TS_Network = TS_Network where nodes = "{}"
begin

lemma nValidTransE: "nValidTrans trn ⟹ P" by (cases trn) auto
lemma validE: "valid tr ⟹ P" by (induction rule: valid.induct) (auto elim: nValidTransE)
lemma validFrom_iff_Nil: "validFrom s tr ⟷ tr = []" unfolding validFrom_def by (auto elim: validE)
lemma reach_istate: "reach s ⟹ s = istate" by (induction rule: reach.induct) (auto elim: nValidTransE)

end

text ‹Definition of n-ary security property composition:›

locale BD_Security_TS_Network = TS_Network istate validTrans srcOf tgtOf nodes comOf tgtNodeOf sync
for
   istate :: "('nodeid, 'state) nstate" and validTrans :: "'nodeid ⇒ 'trans ⇒ bool"
 and
   srcOf :: "'nodeid ⇒ 'trans ⇒ 'state" and tgtOf :: "'nodeid ⇒ 'trans ⇒ 'state"
 and
   nodes :: "'nodeid set"
 and
   comOf :: "'nodeid ⇒ 'trans ⇒ com"
 and
   tgtNodeOf :: "'nodeid ⇒ 'trans ⇒ 'nodeid"
 and
   sync :: "'nodeid ⇒ 'trans ⇒ 'nodeid ⇒ 'trans ⇒ bool"
+
fixes
   φ :: "'nodeid ⇒ 'trans ⇒ bool" and f :: "'nodeid ⇒ 'trans ⇒ 'val"
 and
   γ :: "'nodeid ⇒ 'trans ⇒ bool" and g :: "'nodeid ⇒ 'trans ⇒ 'obs"
 and
   T :: "'nodeid ⇒ 'trans ⇒ bool" and B :: "'nodeid ⇒ 'val list ⇒ 'val list ⇒ bool"
and
  comOfV :: "'nodeid ⇒ 'val ⇒ com"
and
  tgtNodeOfV :: "'nodeid ⇒ 'val ⇒ 'nodeid"
and
  syncV :: "'nodeid ⇒ 'val ⇒ 'nodeid ⇒ 'val ⇒ bool"
and
  comOfO :: "'nodeid ⇒ 'obs ⇒ com"
and
  tgtNodeOfO :: "'nodeid ⇒ 'obs ⇒ 'nodeid"
and
  syncO :: "'nodeid ⇒ 'obs ⇒ 'nodeid ⇒ 'obs ⇒ bool"
(*and
  cmpO :: "'nodeid ⇒ 'obs ⇒ 'nodeid ⇒ 'obs ⇒ 'nobs"*)
and
  source :: "'nodeid"
(*  *)
assumes
  comOfV_comOf[simp]:
  "⋀nid trn. ⟦validTrans nid trn; lreach nid (srcOf nid trn); φ nid trn⟧ ⟹ comOfV nid (f nid trn) = comOf nid trn"
and
  tgtNodeOfV_tgtNodeOf[simp]:
  "⋀nid trn. ⟦validTrans nid trn; lreach nid (srcOf nid trn); φ nid trn; comOf nid trn = Send ∨ comOf nid trn = Recv⟧
          ⟹ tgtNodeOfV nid (f nid trn) = tgtNodeOf nid trn"
and
  comOfO_comOf[simp]:
  "⋀nid trn. ⟦validTrans nid trn; lreach nid (srcOf nid trn); γ nid trn⟧ ⟹ comOfO nid (g nid trn) = comOf nid trn"
and
  tgtNodeOfO_tgtNodeOf[simp]:
  "⋀nid trn. ⟦validTrans nid trn; lreach nid (srcOf nid trn); γ nid trn; comOf nid trn = Send ∨ comOf nid trn = Recv⟧
         ⟹ tgtNodeOfO nid (g nid trn) = tgtNodeOf nid trn"
and
  sync_syncV:
  "⋀nid1 trn1 nid2 trn2.
       validTrans nid1 trn1 ⟹ lreach nid1 (srcOf nid1 trn1) ⟹
       validTrans nid2 trn2 ⟹ lreach nid2 (srcOf nid2 trn2) ⟹
       comOf nid1 trn1 = Send ⟹ tgtNodeOf nid1 trn1 = nid2 ⟹
       comOf nid2 trn2 = Recv ⟹ tgtNodeOf nid2 trn2 = nid1 ⟹
       φ nid1 trn1 ⟹ φ nid2 trn2 ⟹
       sync nid1 trn1 nid2 trn2 ⟹ syncV nid1 (f nid1 trn1) nid2 (f nid2 trn2)"
and
  sync_syncO:
  "⋀nid1 trn1 nid2 trn2.
       validTrans nid1 trn1 ⟹ lreach nid1 (srcOf nid1 trn1) ⟹
       validTrans nid2 trn2 ⟹ lreach nid2 (srcOf nid2 trn2) ⟹
       comOf nid1 trn1 = Send ⟹ tgtNodeOf nid1 trn1 = nid2 ⟹
       comOf nid2 trn2 = Recv ⟹ tgtNodeOf nid2 trn2 = nid1 ⟹
       γ nid1 trn1 ⟹ γ nid2 trn2 ⟹
       sync nid1 trn1 nid2 trn2 ⟹ syncO nid1 (g nid1 trn1) nid2 (g nid2 trn2)"
and
  sync_φ1_φ2:
  "⋀nid1 trn1 nid2 trn2.
       validTrans nid1 trn1 ⟹ lreach nid1 (srcOf nid1 trn1) ⟹
       validTrans nid2 trn2 ⟹ lreach nid2 (srcOf nid2 trn2) ⟹
       comOf nid1 trn1 = Send ⟹ tgtNodeOf nid1 trn1 = nid2 ⟹
       comOf nid2 trn2 = Recv ⟹ tgtNodeOf nid2 trn2 = nid1 ⟹
       sync nid1 trn1 nid2 trn2 ⟹ φ nid1 trn1 ⟷ φ nid2 trn2"
and
  sync_φ_γ:
  "⋀nid1 trn1 nid2 trn2.
     validTrans nid1 trn1 ⟹ lreach nid1 (srcOf nid1 trn1) ⟹
     validTrans nid2 trn2 ⟹ lreach nid2 (srcOf nid2 trn2) ⟹
     comOf nid1 trn1 = Send ⟹ tgtNodeOf nid1 trn1 = nid2 ⟹
     comOf nid2 trn2 = Recv ⟹ tgtNodeOf nid2 trn2 = nid1 ⟹
     γ nid1 trn1 ⟹ γ nid2 trn2 ⟹
     syncO nid1 (g nid1 trn1) nid2 (g nid2 trn2) ⟹
     (φ nid1 trn1 ⟹ φ nid2 trn2 ⟹ syncV nid1 (f nid1 trn1) nid2 (f nid2 trn2))
     ⟹
     sync nid1 trn1 nid2 trn2"
and  (* Every communication is observable (which does not mean that everything in
       a communication is observable!): *)
  isCom_γ: "⋀nid trn. validTrans nid trn ⟹ lreach nid (srcOf nid trn) ⟹ comOf nid trn = Send ∨ comOf nid trn = Recv ⟹ γ nid trn"
and (* Lack of symmetry here: all the value-producing transitions of nodes that are not the primary
       source of values need to be communication transitions *with the source* (and hence proceed
       only synchronously) -- This tames shuffling... *)
  φ_source: "⋀nid trn. ⟦validTrans nid trn; lreach nid (srcOf nid trn); φ nid trn; nid ≠ source; nid ∈ nodes⟧
                        ⟹ isCom nid trn ∧ tgtNodeOf nid trn = source ∧ source ∈ nodes"
begin

abbreviation "isComO nid obs ≡ (comOfO nid obs = Send ∨ comOfO nid obs = Recv) ∧ tgtNodeOfO nid obs ∈ nodes"
abbreviation "isComV nid val ≡ (comOfV nid val = Send ∨ comOfV nid val = Recv) ∧ tgtNodeOfV nid val ∈ nodes"

(* Observation and value setup for the network *)
fun nφ :: "('nodeid, 'state, 'trans) ntrans ⇒ bool" where
  "nφ (LTrans s nid trn) = φ nid trn"
| "nφ (CTrans s nid1 trn1 nid2 trn2) = (φ nid1 trn1 ∨ φ nid2 trn2)"

fun nf :: "('nodeid, 'state, 'trans) ntrans ⇒ ('nodeid, 'val) nvalue" where
  "nf (LTrans s nid trn) = LVal nid (f nid trn)"
| "nf (CTrans s nid1 trn1 nid2 trn2) = CVal nid1 (f nid1 trn1) nid2 (f nid2 trn2)"

fun nγ :: "('nodeid, 'state, 'trans) ntrans ⇒ bool" where
  "nγ (LTrans s nid trn) = γ nid trn"
| "nγ (CTrans s nid1 trn1 nid2 trn2) = (γ nid1 trn1 ∨ γ nid2 trn2)"

fun ng :: "('nodeid, 'state, 'trans) ntrans ⇒ ('nodeid, 'obs) nobs" where
  "ng (LTrans s nid trn) = LObs nid (g nid trn)"
| "ng (CTrans s nid1 trn1 nid2 trn2) = CObs nid1 (g nid1 trn1) nid2 (g nid2 trn2)"

fun nT :: "('nodeid, 'state, 'trans) ntrans ⇒ bool" where
  "nT (LTrans s nid trn) = T nid trn"
| "nT (CTrans s nid1 trn1 nid2 trn2) = (T nid1 trn1 ∨ T nid2 trn2)"
(* *)

fun decompV :: "('nodeid, 'val) nvalue list ⇒ 'nodeid ⇒ 'val list" where
  "decompV (LVal nid' v # vl) nid = (if nid' = nid then v # decompV vl nid else decompV vl nid)"
| "decompV (CVal nid1 v1 nid2 v2 # vl) nid = (if nid1 = nid then v1 # decompV vl nid else
                                             (if nid2 = nid then v2 # decompV vl nid else
                                              decompV vl nid))"
| "decompV [] nid = []"

fun nValidV :: "('nodeid, 'val) nvalue ⇒ bool" where
  "nValidV (LVal nid v) = (nid ∈ nodes ∧ ¬isComV nid v)"
| "nValidV (CVal nid1 v1 nid2 v2) =
    (nid1 ∈ nodes ∧ nid2 ∈ nodes ∧ nid1 ≠ nid2 ∧ syncV nid1 v1 nid2 v2 ∧
     comOfV nid1 v1 = Send ∧ tgtNodeOfV nid1 v1 = nid2 ∧ comOfV nid2 v2 = Recv ∧ tgtNodeOfV nid2 v2 = nid1)"


fun decompO :: "('nodeid, 'obs) nobs list ⇒ 'nodeid ⇒ 'obs list" where
  "decompO (LObs nid' obs # obsl) nid = (if nid' = nid then obs # decompO obsl nid else decompO obsl nid)"
| "decompO (CObs nid1 obs1 nid2 obs2 # obsl) nid = (if nid1 = nid then obs1 # decompO obsl nid else
                                                   (if nid2 = nid then obs2 # decompO obsl nid else
                                                    decompO obsl nid))"
| "decompO [] nid = []"

(* The declassification bound for the network *)
definition nB :: "('nodeid, 'val) nvalue list ⇒ ('nodeid, 'val) nvalue list ⇒ bool" where
"nB vl vl' ≡ (∀nid ∈ nodes. B nid (decompV vl nid) (decompV vl' nid)) ∧
             (list_all nValidV vl ⟶ list_all nValidV vl')"
(* *)

fun subDecompV :: "('nodeid, 'val) nvalue list ⇒ 'nodeid set ⇒ ('nodeid, 'val) nvalue list" where
  "subDecompV (LVal nid' v # vl) nds =
    (if nid' ∈ nds then LVal nid' v # subDecompV vl nds else subDecompV vl nds)"
| "subDecompV (CVal nid1 v1 nid2 v2 # vl) nds =
    (if nid1 ∈ nds ∧ nid2 ∈ nds then CVal nid1 v1 nid2 v2 # subDecompV vl nds else
    (if nid1 ∈ nds then LVal nid1 v1 # subDecompV vl nds else
    (if nid2 ∈ nds then LVal nid2 v2 # subDecompV vl nds else
     subDecompV vl nds)))"
| "subDecompV [] nds = []"

lemma decompV_subDecompV[simp]: "nid ∈ nds ⟹ decompV (subDecompV vl nds) nid = decompV vl nid"
proof (induction vl)
  case (Cons v vl) then show ?case by (cases v) (auto split: if_splits)
qed auto

sublocale BD_Security_TS istate nValidTrans nSrcOf nTgtOf nφ nf nγ ng nT nB .

(* Abbreviations for local BD Security setup of individual nodes *)
abbreviation lV :: "'nodeid ⇒ 'trans list ⇒ 'val list" where
  "lV nid ≡ BD_Security_TS.V (φ nid) (f nid)"

abbreviation lO :: "'nodeid ⇒ 'trans list ⇒ 'obs list" where
  "lO nid ≡ BD_Security_TS.O (γ nid) (g nid)"

abbreviation lTT :: "'nodeid ⇒ 'trans list ⇒ bool" where
  "lTT nid ≡ never (T nid)"

abbreviation lsecure :: "'nodeid ⇒ bool" where
  "lsecure nid ≡ Abstract_BD_Security.secure (lValidFrom nid (istate nid)) (lV nid) (lO nid) (B nid) (lTT nid)"


lemma decompV_decomp:
assumes "validFrom s tr"
and "reach s"
shows "decompV (V tr) nid = lV nid (decomp tr nid)"
proof -
  interpret Node: BD_Security_TS "istate nid" "validTrans nid" "srcOf nid" "tgtOf nid"
                                 "φ nid" "f nid" "γ nid" "g nid" "T nid" "B nid" .
  from assms show ?thesis proof (induction tr arbitrary: s)
    case (Cons trn tr s)
      then have tr: "decompV (V tr) nid = Node.V (decomp tr nid)"
        by (intro Cons.IH[of "nTgtOf trn"]) (auto intro: reach.Step)
      show ?case proof (cases trn)
        case (LTrans s' nid' trn') with Cons.prems tr show ?thesis by (cases "nφ trn") auto
      next
        case (CTrans s' nid1 trn1 nid2 trn2)
          then have "lreach nid1 (s' nid1)" and "lreach nid2 (s' nid2)"
            using Cons.prems by (auto elim: reach_lreach)
          then have "φ nid1 trn1 ⟷ φ nid2 trn2"
            using Cons.prems CTrans by (intro sync_φ1_φ2) auto
          then show ?thesis using Cons.prems CTrans tr Node.V_Cons_unfold by (cases "nφ trn") auto
      qed
  qed auto
qed

lemma decompO_decomp:
assumes "validFrom s tr"
and "reach s"
shows "decompO (O tr) nid = lO nid (decomp tr nid)"
proof -
  interpret Node: BD_Security_TS "istate nid" "validTrans nid" "srcOf nid" "tgtOf nid"
                                 "φ nid" "f nid" "γ nid" "g nid" "T nid" "B nid" .
  from assms show ?thesis proof (induction tr arbitrary: s)
    case (Cons trn tr s)
      then have tr: "decompO (O tr) nid = Node.O (decomp tr nid)"
        by (intro Cons.IH[of "nTgtOf trn"]) (auto intro: reach.Step)
      show ?case proof (cases trn)
        case (LTrans s' nid' trn') with Cons.prems tr show ?thesis by (cases "nγ trn") auto
      next
        case (CTrans s' nid1 trn1 nid2 trn2)
          then have "lreach nid1 (s' nid1)" and "lreach nid2 (s' nid2)"
            using Cons.prems by (auto elim: reach_lreach)
          then have "γ nid1 trn1" and "γ nid2 trn2"
            using Cons.prems CTrans by (auto intro: isCom_γ)
          then show ?thesis using Cons.prems CTrans tr Node.O_Cons_unfold by (cases "nγ trn") auto
      qed
  qed auto
qed

lemma nTT_TT: "never nT tr ⟹ never (T nid) (decomp tr nid)"
proof (induction tr)
  case (Cons trn tr) then show ?case by (cases trn) auto
qed auto

lemma validFrom_nValidV:
assumes "validFrom s tr"
and "reach s"
shows "list_all nValidV (V tr)"
using assms proof (induction tr arbitrary: s)
  case (Cons trn tr s)
    have tr: "list_all nValidV (V tr)" using Cons.IH[of "nTgtOf trn"] Cons.prems
      by (auto intro: reach.Step)
    then show ?case proof (cases trn)
      case (LTrans s' nid' trn')
        moreover then have "lreach nid' (s' nid')" using Cons.prems by (auto elim: reach_lreach)
        ultimately show ?thesis using Cons.prems tr by (cases "nφ trn") auto
    next
      case (CTrans s' nid1 trn1 nid2 trn2)
        moreover then have "lreach nid1 (s' nid1)" and "lreach nid2 (s' nid2)"
          using Cons.prems by (auto elim: reach_lreach)
        moreover then have "φ nid1 trn1 ⟷ φ nid2 trn2"
          using Cons.prems CTrans by (intro sync_φ1_φ2) auto
        ultimately show ?thesis using Cons.prems tr by (cases "nφ trn") (auto intro: sync_syncV)
    qed
qed auto

end

text ‹An empty network is trivially secure.  This is useful as a base case in proofs.›

locale BD_Security_Empty_TS_Network = BD_Security_TS_Network where nodes = "{}"
begin

sublocale Empty_TS_Network ..

lemma nValidVE: "nValidV v ⟹ P" by (cases v) auto
lemma list_all_nValidV_Nil: "list_all nValidV vl ⟹ vl = []" by (cases vl) (auto elim: nValidVE)

lemma trivially_secure: "secure"
by (intro B_id_secure) (auto iff: validFrom_iff_Nil simp: nB_def B_id_def elim: list_all_nValidV_Nil)

end

text ‹Another useful base case: a singleton network with just the secret source node.›

locale BD_Security_Singleton_Source_Network = BD_Security_TS_Network where nodes = "{source}"
begin

sublocale Node: BD_Security_TS "istate source" "validTrans source" "srcOf source" "tgtOf source"
                               "φ source" "f source" "γ source" "g source" "T source" "B source" .

lemma [simp]: "decompV (map (LVal source) vl) source = vl"
by (induction vl) auto

lemma [simp]: "list_all nValidV vl' ⟹ map (LVal source) (decompV vl' source) = vl'"
proof (induction vl')
  case (Cons v vl') then show ?case by (cases v) auto
qed auto

lemma Node_validFrom_nValidV:
  "Node.validFrom s tr ⟹ Node.reach s ⟹ list_all nValidV (map (LVal source) (Node.V tr))"
proof (induction tr arbitrary: s)
  case (Cons trn tr)
    then have "Node.reach (tgtOf source trn)" using Node.reach.Step[of s trn "tgtOf source trn"] by auto
    then show ?case using Cons.prems Cons.IH[of "tgtOf source trn"]
      using isCom_tgtNodeOf by (cases "φ source trn") auto
qed auto

sublocale Trans?: BD_Security_TS_Trans
  where istate = "istate source" and validTrans = "validTrans source" and srcOf = "srcOf source" and tgtOf = "tgtOf source"
  and φ = "φ source" and f = "f source" and γ = "γ source" and g = "g source" and T = "T source" and B = "B source"
  and istate' = istate and validTrans' = nValidTrans and srcOf' = nSrcOf and tgtOf' = nTgtOf
  and φ' = nφ and f' = nf and γ' = nγ and g' = ng and T' = nT and B' = nB
  and translateState = "λs. istate(source := s)"
  and translateTrans = "λtrn. LTrans (istate(source := srcOf source trn)) source trn"
  and translateObs = "λobs. Some (LObs source obs)"
  and translateVal = "Some o LVal source"
using isCom_tgtNodeOf
proof (unfold_locales, goal_cases)
  case (2 trn' s) then show ?case by (cases trn') auto next
  case (11 vl' vl1' tr)
    then show ?case using Node.reach.Istate
      by (intro exI[of _ "decompV vl1' source"]) (auto simp: nB_def intro: Node_validFrom_nValidV)
qed auto

end

text ‹Setup for changing the set of nodes in a network, e.g. adding a new one.
We re-check unique secret polarization, while the other assumptions about the observation and
secret infrastructure are inherited from the original setup.›

locale BD_Security_TS_Network_Change_Nodes = Orig: BD_Security_TS_Network +
fixes nodes'
assumes finite_nodes': "finite nodes'"
and φ_source':
    "⋀nid trn. ⟦validTrans nid trn; Orig.lreach nid (srcOf nid trn); φ nid trn; nid ≠ source; nid ∈ nodes'⟧
            ⟹ Orig.isCom nid trn ∧ tgtNodeOf nid trn = source ∧ source ∈ nodes'"
begin

sublocale BD_Security_TS_Network where nodes = nodes'
proof (unfold_locales, goal_cases)
  case 1 show ?case using finite_nodes' . next
  case 2 then show ?case using "Orig.isCom_tgtNodeOf" by auto next
  case 3 then show ?case by auto next
  case 4 then show ?case by auto next
  case 5 then show ?case by auto next
  case 6 then show ?case by auto next
  case 7 then show ?case using "Orig.sync_syncV" by auto next
  case 8 then show ?case using "Orig.sync_syncO" by auto next
  case 9 then show ?case using "Orig.sync_φ1_φ2" by auto next
  case 10 then show ?case using "Orig.sync_φ_γ" by auto next
  case 11 then show ?case using "Orig.isCom_γ" by auto next
  case 12 then show ?case using φ_source' by auto
qed

end

text ‹Adding a new node to a network that is not the secret source:›

locale BD_Security_TS_Network_New_Node_NoSource = Sub: BD_Security_TS_Network
where istate = istate and nodes = nodes and f = f and g = g (*and cmpV = cmpV and cmpO = cmpO*)
for istate :: "'nodeid ⇒ 'state" and nodes :: "'nodeid set"
and f :: "'nodeid ⇒ 'trans ⇒ 'val" and g :: "'nodeid ⇒ 'trans ⇒ 'obs"
(*and cmpV :: "'nodeid ⇒ 'val ⇒ 'nodeid ⇒ 'val ⇒ 'cval"
and cmpO :: "'nodeid ⇒ 'obs ⇒ 'nodeid ⇒ 'obs ⇒ 'cobs"*)
+
fixes NID :: "'nodeid"
assumes new_node: "NID ∉ nodes"
and no_source: "NID ≠ source"
and φ_NID_source:
    "⋀trn. ⟦validTrans NID trn; Sub.lreach NID (srcOf NID trn); φ NID trn⟧
        ⟹ Sub.isCom NID trn ∧ tgtNodeOf NID trn = source ∧ source ∈ nodes"
begin

sublocale Node: BD_Security_TS "istate NID" "validTrans NID" "srcOf NID" "tgtOf NID"
                               "φ NID" "f NID" "γ NID" "g NID" "T NID" "B NID" .

sublocale BD_Security_TS_Network_Change_Nodes where nodes' = "insert NID nodes"
  using φ_NID_source Sub.φ_source Sub.finite_nodes
  by (unfold_locales) auto

fun isCom1 :: "('nodeid,'state,'trans) ntrans ⇒ bool" where
  "isCom1 (LTrans s nid trn) = (nid ∈ nodes ∧ isCom nid trn ∧ tgtNodeOf nid trn = NID)"
| "isCom1 _ = False"

definition "isCom2 trn = (∃nid. nid ∈ nodes ∧ isCom NID trn ∧ tgtNodeOf NID trn = nid)"

fun Sync :: "('nodeid,'state,'trans) ntrans ⇒ 'trans ⇒ bool" where
  "Sync (LTrans s nid trn) trn' = (tgtNodeOf nid trn = NID ∧ tgtNodeOf NID trn' = nid ∧
                                  ((sync nid trn NID trn' ∧ comOf nid trn = Send ∧ comOf NID trn' = Recv)
                                 ∨ (sync NID trn' nid trn ∧ comOf NID trn' = Send ∧ comOf nid trn = Recv)))"
| "Sync _ _ = False"

fun isComV1 :: "('nodeid,'val) nvalue ⇒ bool" where
  "isComV1 (LVal nid v) = (nid ∈ nodes ∧ isComV nid v ∧ tgtNodeOfV nid v = NID)"
| "isComV1 _ = False"

definition "isComV2 v = (∃nid. nid ∈ nodes ∧ isComV NID v ∧ tgtNodeOfV NID v = nid)"

fun SyncV :: "('nodeid,'val) nvalue ⇒ 'val ⇒ bool" where
  "SyncV (LVal nid v1) v2 = (tgtNodeOfV nid v1 = NID ∧ tgtNodeOfV NID v2 = nid ∧
                            ((syncV nid v1 NID v2 ∧ comOfV nid v1 = Send ∧ comOfV NID v2 = Recv)
                            ∨ (syncV NID v2 nid v1 ∧ comOfV NID v2 = Send ∧ comOfV nid v1 = Recv)))"
| "SyncV _ _ = False"

fun CmpV :: "('nodeid,'val) nvalue ⇒ 'val ⇒ ('nodeid,'val) nvalue" where
  "CmpV (LVal nid v1) v2 = (if comOfV nid v1 = Send then CVal nid v1 NID v2 else CVal NID v2 nid v1)"
| "CmpV cv v2 = cv"

fun isComO1 :: "('nodeid,'obs) nobs ⇒ bool" where
  "isComO1 (LObs nid obs) = (nid ∈ nodes ∧ isComO nid obs ∧ tgtNodeOfO nid obs = NID)"
| "isComO1 _ = False"

definition "isComO2 obs = (∃nid. nid ∈ nodes ∧ isComO NID obs ∧ tgtNodeOfO NID obs = nid)"

fun SyncO :: "('nodeid,'obs) nobs ⇒ 'obs ⇒ bool" where
  "SyncO (LObs nid obs1) obs2 = (tgtNodeOfO nid obs1 = NID ∧ tgtNodeOfO NID obs2 = nid ∧
                                ((syncO nid obs1 NID obs2 ∧ comOfO nid obs1 = Send ∧ comOfO NID obs2 = Recv)
                                ∨ (syncO NID obs2 nid obs1 ∧ comOfO NID obs2 = Send ∧ comOfO nid obs1 = Recv)))"
| "SyncO _ _ = False"

text ‹We prove security using the binary composition theorem,
composing the existing network with the new node.›

sublocale Comp: BD_Security_TS_Comp istate Sub.nValidTrans Sub.nSrcOf Sub.nTgtOf
  Sub.nφ Sub.nf Sub.nγ Sub.ng Sub.nT Sub.nB
  "istate NID" "validTrans NID" "srcOf NID" "tgtOf NID" "φ NID" "f NID" "γ NID" "g NID" "T NID" "B NID"
  isCom1 isCom2 Sync isComV1 isComV2 SyncV isComO1 isComO2 SyncO
proof
  fix trn1
  assume trn1: "Sub.nValidTrans trn1" "Sub.reach (Sub.nSrcOf trn1)" "Sub.nφ trn1"
  then show "isCom1 trn1 = isComV1 (Sub.nf trn1)"
  proof (cases trn1)
    case (LTrans s nid trn)
      with trn1 have "lreach nid (srcOf nid trn)" by (auto elim!: Sub.reach_lreach)
      with trn1 show ?thesis using LTrans by auto
  qed auto
next
  fix trn1
  assume trn1: "Sub.nValidTrans trn1" "Sub.reach (Sub.nSrcOf trn1)" "Sub.nγ trn1"
  then show "isCom1 trn1 = isComO1 (Sub.ng trn1)"
  proof (cases trn1)
    case (LTrans s nid trn)
      with trn1 have "lreach nid (srcOf nid trn)" by (auto elim!: Sub.reach_lreach)
      with trn1 show ?thesis using LTrans by auto
  qed auto
next
  fix trn2
  assume trn2: "validTrans NID trn2" "Node.reach (srcOf NID trn2)" "φ NID trn2"
  then show "isCom2 trn2 = isComV2 (f NID trn2)"
    unfolding isCom2_def isComV2_def by auto
next
  fix trn2
  assume trn2: "validTrans NID trn2" "Node.reach (srcOf NID trn2)" "γ NID trn2"
  then show "isCom2 trn2 = isComO2 (g NID trn2)"
    unfolding isCom2_def isComO2_def by auto
next
  fix trn1 trn2
  assume trn12: "Sub.nValidTrans trn1" "Sub.reach (Sub.nSrcOf trn1)" "validTrans NID trn2"
       "Node.reach (srcOf NID trn2)" "isCom1 trn1" "isCom2 trn2" "Sub.nφ trn1" "φ NID trn2" "Sync trn1 trn2"
  then show "SyncV (Sub.nf trn1) (f NID trn2)" proof (cases trn1)
    case (LTrans s nid trn)
      with trn12 have "lreach nid (srcOf nid trn)" by (auto elim: Sub.reach_lreach)
      with trn12 show ?thesis using LTrans by (auto intro: Sub.sync_syncV)
  qed auto
next
  fix trn1 trn2
  assume trn12: "Sub.nValidTrans trn1" "Sub.reach (Sub.nSrcOf trn1)" "validTrans NID trn2"
       "Node.reach (srcOf NID trn2)" "isCom1 trn1" "isCom2 trn2" "Sub.nγ trn1" "γ NID trn2" "Sync trn1 trn2"
  then show "SyncO (Sub.ng trn1) (g NID trn2)" proof (cases trn1)
    case (LTrans s nid trn)
      with trn12 have "lreach nid (srcOf nid trn)" by (auto elim: Sub.reach_lreach)
      with trn12 show ?thesis using LTrans by (auto intro: Sub.sync_syncO)
  qed auto
next
  fix trn1 trn2
  assume trn12: "Sub.nValidTrans trn1" "Sub.reach (Sub.nSrcOf trn1)" "validTrans NID trn2"
       "Node.reach (srcOf NID trn2)" "isCom1 trn1" "isCom2 trn2" "Sync trn1 trn2"
  then show "Sub.nφ trn1 = φ NID trn2" proof (cases trn1)
    case (LTrans s nid trn)
      with trn12 show ?thesis using Sub.sync_φ1_φ2[of nid trn NID trn2] Sub.sync_φ1_φ2[of NID trn2 nid trn]
        by (auto elim: Sub.reach_lreach)
  qed auto
next
  fix trn1 trn2
  assume trn12: "Sub.nValidTrans trn1" "Sub.reach (Sub.nSrcOf trn1)" "validTrans NID trn2"
       "Node.reach (srcOf NID trn2)" "isCom1 trn1" "isCom2 trn2"
       "Sub.nγ trn1" "γ NID trn2" "SyncO (Sub.ng trn1) (g NID trn2)"
       "Sub.nφ trn1 ⟹ φ NID trn2 ⟹ SyncV (Sub.nf trn1) (f NID trn2)"
  then show "Sync trn1 trn2" proof (cases trn1)
    case (LTrans s nid trn)
      with trn12 have "lreach nid (srcOf nid trn)" by (auto elim: Sub.reach_lreach)
      with trn12 show ?thesis using LTrans by (auto intro: Sub.sync_φ_γ)
  qed auto
next
  fix trn1
  assume trn1: "Sub.nValidTrans trn1" "Sub.reach (Sub.nSrcOf trn1)" "isCom1 trn1"
  then show "Sub.nγ trn1" proof (cases trn1)
    case (LTrans s nid trn)
      with trn1 show ?thesis using Sub.isCom_γ[of nid trn] by (auto elim: Sub.reach_lreach)
  qed auto
next
  fix trn2
  assume "validTrans NID trn2" "Node.reach (srcOf NID trn2)" "isCom2 trn2"
  then show "γ NID trn2" unfolding isCom2_def by (auto intro: Sub.isCom_γ)
next
  fix trn2
  assume "validTrans NID trn2" "Node.reach (srcOf NID trn2)" "φ NID trn2"
  then show "isCom2 trn2" using φ_NID_source unfolding isCom2_def by auto
qed auto

text ‹We then translate the canonical security property obtained from the binary compositionality
result back to the original observation and secret infrastructure using the transport theorem.›

fun translateState :: "(('nodeid ⇒ 'state) × 'state) ⇒ ('nodeid ⇒ 'state)" where
  "translateState (sSub, sNode) = (sSub(NID := sNode))"

fun translateTrans :: "('nodeid ⇒ 'state, ('nodeid, 'state, 'trans) ntrans, 'state, 'trans) ctrans ⇒ ('nodeid, 'state, 'trans) ntrans" where
  "translateTrans (Trans1 sNode (LTrans s nid trn)) = LTrans (s(NID := sNode)) nid trn"
| "translateTrans (Trans1 sNode (CTrans s nid1 trn1 nid2 trn2)) = CTrans (s(NID := sNode)) nid1 trn1 nid2 trn2"
| "translateTrans (Trans2 sSub trn) = LTrans (sSub(NID := srcOf NID trn)) NID trn"
| "translateTrans (ctrans.CTrans (LTrans s nid trn) trnNode) =
      (if comOf nid trn = Send
       then CTrans (s(NID := srcOf NID trnNode)) nid trn NID trnNode
       else CTrans (s(NID := srcOf NID trnNode)) NID trnNode nid trn)"
| "translateTrans _ = undefined"

fun translateObs :: "(('nodeid, 'obs) nobs, 'obs) cobs ⇒ ('nodeid, 'obs) nobs" where
  "translateObs (Obs1 obs) = obs"
| "translateObs (Obs2 obs) = (LObs NID obs)"
| "translateObs (cobs.CObs (LObs nid1 obs1) obs2) =
    (if comOfO nid1 obs1 = Send then CObs nid1 obs1 NID obs2 else CObs NID obs2 nid1 obs1)"
| "translateObs _ = undefined"

fun translateVal :: "(('nodeid, 'val) nvalue, 'val) cvalue ⇒ ('nodeid, 'val) nvalue" where
  "translateVal (Value1 v) = v"
| "translateVal (Value2 v) = (LVal NID v)"
| "translateVal (cvalue.CValue (LVal nid1 v1) v2) =
    (if comOfV nid1 v1 = Send then CVal nid1 v1 NID v2 else CVal NID v2 nid1 v1)"
| "translateVal _ = undefined"

fun invTranslateVal :: "('nodeid, 'val) nvalue ⇒ (('nodeid, 'val) nvalue, 'val) cvalue" where
  "invTranslateVal (LVal nid v) = (if nid = NID then Value2 v else Value1 (LVal nid v))"
| "invTranslateVal (CVal nid1 v1 nid2 v2) =
    (if nid1 ∈ nodes ∧ nid2 ∈ nodes then Value1 (CVal nid1 v1 nid2 v2)
     else (if nid1 = NID then CValue (LVal nid2 v2) v1
           else CValue (LVal nid1 v1) v2))"

lemma translateVal_invTranslateVal[simp]: "nValidV v ⟹ (translateVal (invTranslateVal v)) = v"
by (elim nValidV.elims) auto

lemma map_translateVal_invTranslateVal[simp]:
  "list_all nValidV vl ⟹ map (translateVal o invTranslateVal) vl = vl"
by (induction vl) auto

fun compValidV :: "(('nodeid, 'val) nvalue, 'val) cvalue ⇒ bool" where
  "compValidV (Value1 (LVal nid v)) = (Sub.nValidV (LVal nid v) ∧ (isComV nid v ⟶ tgtNodeOfV nid v ≠ NID))"
| "compValidV (Value1 (CVal nid1 v1 nid2 v2)) = Sub.nValidV (CVal nid1 v1 nid2 v2)"
| "compValidV (Value2 v2) = nValidV (LVal NID v2)"
| "compValidV (CValue (CVal nid1 v1 nid2 v2) v) = False"
| "compValidV (CValue (LVal nid1 v1) v2) = (nValidV (CVal nid1 v1 NID v2) ∨ nValidV (CVal NID v2 nid1 v1))"

lemma nValidV_compValidV: "nValidV v ⟹ compValidV (invTranslateVal v)"
by (cases v) auto

lemma list_all_nValidV_compValidV: "list_all nValidV vl ⟹ list_all compValidV (map invTranslateVal vl)"
by (induction vl) (auto intro: nValidV_compValidV)

lemma compValidV_nValidV: "compValidV v ⟹ nValidV (translateVal v)"
by (cases v rule: "compValidV.cases") auto

lemma list_all_compValidV_nValidV: "list_all compValidV vl ⟹ list_all nValidV (map translateVal vl)"
by (induction vl) (auto intro: compValidV_nValidV)

lemma nValidV_subDecompV: "list_all nValidV vl ⟹ list_all Sub.nValidV (subDecompV vl nodes)"
proof (induction vl)
  case (Cons v vl) then show ?case by (cases v) auto
qed auto

lemma validTrans_compValidV:
assumes "Comp.validTrans trn" and "Comp.reach (Comp.srcOf trn)" and "Comp.φ trn"
shows "compValidV (Comp.f trn)"
proof (cases trn)
  case (Trans1 sNode trnSub)
    show ?thesis proof (cases trnSub)
      case (LTrans s nid1 trn1)
        then have "lreach nid1 (s nid1)"
          using Trans1 assms Comp.reach_reach12[of "Comp.srcOf trn"]
          by (auto elim!: Sub.reach_lreach)
        then show ?thesis using LTrans Trans1 assms by auto
    next
      case (CTrans s nid1 trn1 nid2 trn2)
        then have "lreach nid1 (s nid1)" and "lreach nid2 (s nid2)"
          using Trans1 assms Comp.reach_reach12[of "Comp.srcOf trn"]
          by (auto elim!: Sub.reach_lreach)
        then show ?thesis using CTrans Trans1 assms
          using sync_syncV[of nid1 trn1 nid2 trn2] sync_φ1_φ2[of nid1 trn1 nid2 trn2] by auto
    qed
next
  case (Trans2 sSub trnNode)
    then have "lreach NID (srcOf NID trnNode)" using assms Comp.reach_reach12[of "Comp.srcOf trn"] by auto
    with assms Trans2 show ?thesis using φ_NID_source by (auto simp: isCom2_def)
next
  case (CTrans trnSub trnNode)
    then obtain sSub nid1 trn1 where "trnSub = LTrans sSub nid1 trn1" using assms
      by (cases trnSub) auto
    moreover then have "lreach nid1 (sSub nid1)" and "lreach NID (srcOf NID trnNode)"
      using assms Comp.reach_reach12[of "Comp.srcOf trn"] CTrans by (auto elim!: Sub.reach_lreach)
    ultimately show ?thesis using assms CTrans
      using sync_syncV[of nid1 trn1 NID trnNode] sync_φ1_φ2[of nid1 trn1 NID trnNode]
      using sync_syncV[of NID trnNode nid1 trn1] sync_φ1_φ2[of NID trnNode nid1 trn1]
      by (cases "comOf NID trnNode = Send") auto
qed

lemma validFrom_compValidV: "Comp.reach s ⟹ Comp.validFrom s tr ⟹ list_all compValidV (Comp.V tr)"
proof (induction tr arbitrary: s)
  case (Cons trn tr)
    then have "Comp.reach (Comp.tgtOf trn)" using Comp.reach.Step[of s trn "Comp.tgtOf trn"] by auto
    then show ?case using Cons.prems Cons.IH[of "Comp.tgtOf trn"] validTrans_compValidV
      by (cases "Comp.φ trn") auto
qed auto

lemma validFrom_istate_compValidV: "Comp.validFrom Comp.icstate tr ⟹ list_all compValidV (Comp.V tr)"
using validFrom_compValidV Comp.reach.Istate by blast

lemma compV_decompV:
assumes "list_all compValidV vl"
shows "Comp.compV vl1 vl2 vl
   ⟷ vl1 = subDecompV (map translateVal vl) nodes ∧ vl2 = decompV (map translateVal vl) NID"
proof
  assume "Comp.compV vl1 vl2 vl"
  then show "vl1 = subDecompV (map translateVal vl) nodes ∧ vl2 = decompV (map translateVal vl) NID"
    using assms new_node
  proof (induction rule: Comp.compV.induct)
    case (Step1 vl1 vl2 vl v1) then show ?case by (cases v1) auto next
    case (Com vl1 vl2 vl v1 v2) then show ?case by (cases v1) auto
  qed auto
next
  assume "vl1 = subDecompV (map translateVal vl) nodes ∧ vl2 = decompV (map translateVal vl) NID"
  moreover have "Comp.compV (subDecompV (map translateVal vl) nodes) (decompV (map translateVal vl) NID) vl"
    using assms new_node
  proof (induction vl)
    case (Cons v vl)
      then show ?case proof (cases v)
        case (Value1 v1) with Cons show ?thesis by (cases v1) auto
      next
        case (Value2 v2)
          then have "¬ isComV2 v2" using Cons unfolding isComV2_def by auto
          then show ?thesis using Cons Value2 by auto
      next
        case (CValue cv v2)
          then show ?thesis using Cons.prems proof (cases cv)
            case (LVal nid1 v1)
              then have "isComV2 v2" using LVal CValue Cons unfolding isComV2_def by auto
              then have "Comp.compV (LVal nid1 v1 # subDecompV (map translateVal vl) nodes)
                                    (v2 # decompV (map translateVal vl) NID)
                                    (CValue (LVal nid1 v1) v2 # vl)"
                using LVal CValue Cons by (intro Comp.compV.Com) auto
              then show ?thesis using LVal CValue Cons by auto
          qed auto
      qed
  qed auto
  ultimately show "Comp.compV vl1 vl2 vl" by auto
qed


sublocale Trans?: BD_Security_TS_Trans