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 Comp.icstate Comp.validTrans Comp.srcOf Comp.tgtOf
  Comp.φ Comp.f Comp.γ Comp.g Comp.T Comp.B
  istate nValidTrans nSrcOf nTgtOf nφ nf nγ ng nT nB
  translateState translateTrans "Some o translateObs" "Some o translateVal"
proof
  fix trn
  assume trn: "Comp.validTrans trn" "Comp.reach (Comp.srcOf trn)"
  then show "nValidTrans (translateTrans trn)" using new_node
  proof (cases trn)
    case (Trans2 sSub trnNode)
      with trn have "Node.reach (srcOf NID trnNode)" by (auto elim: Comp.reach_reach12)
      with trn Trans2 show ?thesis using Sub.isCom_tgtNodeOf[of NID _] by (auto simp: isCom2_def)
  next
    case (CTrans trnSub trnNode)
      with trn obtain sSub nid trn1 where trnSub: "trnSub = LTrans sSub nid trn1"
        by (auto elim: Sync.elims)
      then have "lreach nid (srcOf nid trn1)" and "lreach NID (srcOf NID trnNode)"
        using CTrans trn by (auto elim!: Comp.reach_reach12 Sub.reach_lreach)
      (*then have "srcNodeOf trn1 = nid" and "srcNodeOf trnNode = NID"
        using trn trnSub CTrans by (auto simp: Sub.isCom_srcNodeOf)*)
      then show ?thesis using CTrans trn trnSub by (auto elim: Sub.nValidTrans.elims)
  qed (auto elim!: Sub.nValidTrans.elims split: if_split_asm)
next
  fix trn' s
  assume trn': "nValidTrans trn'" "nSrcOf trn' = translateState s" "Comp.reach s"
  then obtain trn where "Comp.validTrans trn" "Comp.srcOf trn = s" "translateTrans trn = trn'"
  proof (cases trn')
    case (LTrans s' nid trn)
      show thesis proof cases
        assume "nid = NID"
        then show thesis using trn' LTrans
          by (cases s; intro that[of "Trans2 (fst s) trn"]) (auto simp: isCom2_def)
      next
        assume "nid ≠ NID"
        then show thesis using trn' LTrans
          by (cases s;intro that[of "Trans1 (snd s) (LTrans (fst s) nid trn)"]) auto
      qed
  next
    case (CTrans s' nid1 trn1 nid2 trn2)
      show thesis proof cases
        assume "nid1 = NID ∨ nid2 = NID"
        then show thesis proof
          assume "nid1 = NID"
          then show thesis using trn' CTrans new_node
            by (cases s; intro that[of "ctrans.CTrans (LTrans (fst s) nid2 trn2) trn1"])
               (auto simp: isCom2_def)
        next
          assume "nid2 = NID"
          then show thesis using trn' CTrans new_node
            by (cases s; intro that[of "ctrans.CTrans (LTrans (fst s) nid1 trn1) trn2"])
               (auto simp: isCom2_def)
        qed
      next
        assume "¬ (nid1 = NID ∨ nid2 = NID)"
        then show thesis using trn' CTrans
          by (cases s; intro that[of "Trans1 (snd s) (CTrans (fst s) nid1 trn1 nid2 trn2)"]) auto
      qed
  qed
  then show "∃trn. Comp.validTrans trn ∧ Comp.srcOf trn = s ∧ translateTrans trn = trn'" by auto
next
  fix trn
  assume trn: "Comp.validTrans trn" "Comp.reach (Comp.srcOf trn)"
  show "nSrcOf (translateTrans trn) = translateState (Comp.srcOf trn)"
    using trn by (cases trn rule: translateTrans.cases) auto
  show "nTgtOf (translateTrans trn) = translateState (Comp.tgtOf trn)"
    using trn new_node by (cases trn rule: translateTrans.cases) (auto intro: fun_upd_twist)
next
  show "istate = translateState Comp.icstate" unfolding Comp.icstate_def by auto
next
  fix trn
  assume trn: "Comp.validTrans trn" "Comp.reach (Comp.srcOf trn)" "nγ (translateTrans trn)"
  then show "Comp.γ trn ∧ (Some o translateObs) (Comp.g trn) = Some (ng (translateTrans trn))"
  proof (cases trn rule: translateTrans.cases)
    case (4 sSub nid trnSub trnNode)
      with trn have "lreach nid (srcOf nid trnSub)" and "lreach NID (srcOf NID trnNode)"
        by (auto elim!: Comp.reach_reach12 Sub.reach_lreach)
      with trn 4 show ?thesis using isCom_γ[of nid trnSub] isCom_γ[of NID trnNode] by auto
  qed auto
next
  fix trn
  assume trn: "Comp.validTrans trn" "Comp.reach (Comp.srcOf trn)" "Comp.γ trn"
  then show "nγ (translateTrans trn) ∨ (Some o translateObs) (Comp.g trn) = None"
  proof (cases trn rule: translateTrans.cases)
    case (4 sSub nid trnSub trnNode)
      with trn have "lreach nid (srcOf nid trnSub)" and "lreach NID (srcOf NID trnNode)"
        by (auto elim!: Comp.reach_reach12 Sub.reach_lreach)
      with trn 4 show ?thesis by auto
  qed auto
next
  fix trn
  assume trn: "Comp.validTrans trn" "Comp.reach (Comp.srcOf trn)" "nφ (translateTrans trn)"
  then show "Comp.φ trn ∧ (Some o translateVal) (Comp.f trn) = Some (nf (translateTrans trn))"
  proof (cases trn rule: translateTrans.cases)
    case (4 sSub nid trnSub trnNode)
      with trn have "lreach nid (srcOf nid trnSub)" and "lreach NID (srcOf NID trnNode)"
        by (auto elim!: Comp.reach_reach12 Sub.reach_lreach)
      with trn 4 show ?thesis
        using sync_φ1_φ2[of nid trnSub NID trnNode] sync_φ1_φ2[of NID trnNode nid trnSub] by auto
  qed auto
next
  fix trn
  assume trn: "Comp.validTrans trn" "Comp.reach (Comp.srcOf trn)" "Comp.φ trn"
  then show "nφ (translateTrans trn) ∨ (Some o translateVal) (Comp.f trn) = None"
  proof (cases trn rule: translateTrans.cases)
    case (4 sSub nid trnSub trnNode)
      with trn have "lreach nid (srcOf nid trnSub)" and "lreach NID (srcOf NID trnNode)"
        by (auto elim!: Comp.reach_reach12 Sub.reach_lreach)
      with trn 4 show ?thesis by auto
  qed auto
next
  fix trn
  assume "Comp.T trn" "Comp.validTrans trn" "Comp.reach (Comp.srcOf trn)"
  then show "nT (translateTrans trn)" by (cases trn rule: translateTrans.cases) auto
next
  fix vl' vl1' tr
  let ?vl1 = "map invTranslateVal vl1'"
  assume nB: "nB vl' vl1'" and tr: "Comp.validFrom Comp.icstate tr"
     and vl':  "these (map (Some o translateVal) (Comp.V tr)) = vl'"
  moreover then have "list_all compValidV (Comp.V tr)" and "list_all compValidV ?vl1"
    by (auto intro: validFrom_istate_compValidV list_all_nValidV_compValidV list_all_compValidV_nValidV simp: nB_def)
  ultimately have "Comp.B (Comp.V tr) ?vl1" and "list_all nValidV vl1'"
    unfolding nB_def Comp.B_def Sub.nB_def
    by (auto simp: compV_decompV intro: nValidV_subDecompV list_all_compValidV_nValidV)
  then show "∃vl1. these (map (Some o translateVal) vl1) = vl1' ∧ Comp.B (Comp.V tr) vl1"
    by (intro exI[of _ "?vl1"], auto)
       (metis list.map_comp map_translateVal_invTranslateVal these_map_Some)
qed

text ‹Security for the composition of the network with the new node:›

lemma secure_new_node:
assumes "Sub.secure" and "lsecure NID"
shows secure
using assms by (auto intro: Trans.translate_secure Comp.secure1_secure2_secure)

end

text ‹Composing two sub-networks:›

locale BD_Security_TS_Cut_Network = BD_Security_TS_Network
+
fixes nodesLeft and nodesRight
assumes
  nodesLeftRight_disjoint: "nodesLeft ∩ nodesRight = {}"
and
  nodes_nodesLeftRight: "nodes = nodesLeft ∪ nodesRight"
and
  no_source_right: "source ∉ nodesRight"
begin

lemma finite_nodesLeft: "finite nodesLeft" using finite_nodes nodes_nodesLeftRight by auto
lemma finite_nodesRight: "finite nodesRight" using finite_nodes nodes_nodesLeftRight by auto

sublocale Left: BD_Security_TS_Network_Change_Nodes where nodes' = "nodesLeft"
  using finite_nodesLeft no_source_right φ_source nodes_nodesLeftRight
  by (unfold_locales) auto

text ‹If the sub-network (potentially) containing the secret source is secure and all the nodes in
the other sub-network are locally secure, then the composition is secure.

The proof proceeds by finite set induction on the set of non-source nodes, using the above
infrastructure for adding new nodes to a network.›

lemma merged_secure:
assumes "Left.secure"
and "∀nid ∈ nodesRight. lsecure nid"
shows "secure"
using finite_nodesRight assms no_source_right nodesLeftRight_disjoint φ_source unfolding nodes_nodesLeftRight
proof (induction rule: finite_induct)
  case (insert nid nodesMerged)
    interpret Left': BD_Security_TS_Network_Change_Nodes where nodes' = "nodesLeft ∪ nodesMerged"
      using finite_nodes nodes_nodesLeftRight insert by (unfold_locales) auto
    interpret Node: BD_Security_TS "istate nid" "validTrans nid" "srcOf nid" "tgtOf nid"
                                   "φ nid" "f nid" "γ nid" "g nid" "T nid" "B nid" .
    have secure1: "Left'.secure" and secure2: "Node.secure" using insert by auto
    interpret Comp: BD_Security_TS_Network_New_Node_NoSource
      where nodes = "nodesLeft ∪ nodesMerged" and NID = nid
      using insert.prems insert.hyps by unfold_locales auto
    show ?case using secure1 secure2 using Comp.secure_new_node by auto
qed auto

end

context BD_Security_TS_Network
begin

text ‹Putting it all together:›

theorem network_secure:
assumes "∀nid ∈ nodes. lsecure nid"
shows "secure"
proof (cases "source ∈ nodes")
  case True
    interpret BD_Security_TS_Cut_Network where nodesLeft = "{source}" and nodesRight = "nodes - {source}"
      using True by unfold_locales auto
    interpret Source_BD: BD_Security_Singleton_Source_Network by intro_locales

    show "secure" using assms Source_BD.translate_secure True by (intro merged_secure) auto
next
  case False
    interpret BD_Security_TS_Cut_Network where nodesLeft = "{}" and nodesRight = "nodes"
      using False by unfold_locales auto
    interpret Empty_BD: BD_Security_Empty_TS_Network by intro_locales

    show "secure" using assms Empty_BD.trivially_secure by (intro merged_secure)
qed

end

text ‹Translating composite secrets using a function ‹mergeSec›:›

datatype ('nodeid, 'sec, 'msec) merged_sec = LMSec 'nodeid 'sec | CMSec 'msec

locale BD_Security_TS_Network_MergeSec =
 Net?: BD_Security_TS_Network istate validTrans srcOf tgtOf nodes comOf tgtNodeOf sync φ f
for istate :: "'nodeid ⇒ 'state"
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"
and φ :: "'nodeid ⇒ 'trans ⇒ bool"
and f :: "'nodeid ⇒ 'trans ⇒ 'sec" +
fixes mergeSec :: "'nodeid ⇒ 'sec ⇒ 'nodeid ⇒ 'sec ⇒ 'msec"
begin

inductive compSec :: "('nodeid ⇒ 'sec list) ⇒ ('nodeid, 'sec, 'msec) merged_sec list ⇒ bool"
where
  Nil: "compSec (λ_. []) []"
| Local: "⟦compSec sls sl; isComV nid s ⟶ tgtNodeOfV nid s ∉ nodes; nid ∈ nodes⟧
          ⟹ compSec (sls(nid := s # sls nid)) (LMSec nid s # sl)"
| Comm: "⟦compSec sls sl; nid1 ∈ nodes; nid2 ∈ nodes; nid1 ≠ nid2;
          comOfV nid1 s1 = Send; tgtNodeOfV nid1 s1 = nid2;
          comOfV nid2 s2 = Recv; tgtNodeOfV nid2 s2 = nid1;
          syncV nid1 s1 nid2 s2⟧
          ⟹ compSec (sls(nid1 := s1 # sls nid1, nid2 := s2 # sls nid2))
                      (CMSec (mergeSec nid1 s1 nid2 s2) # sl)"

definition nB :: "('nodeid, 'sec, 'msec) merged_sec list ⇒ ('nodeid, 'sec, 'msec) merged_sec list ⇒ bool" where
"nB sl sl' ≡ ∀sls. compSec sls sl ⟶
  (∃sls'. compSec sls' sl' ∧ (∀nid ∈ nodes. B nid (sls nid) (sls' nid)))"

fun nf :: "('nodeid, 'state, 'trans) ntrans ⇒ ('nodeid, 'sec, 'msec) merged_sec" where
  "nf (LTrans s nid trn) = LMSec nid (f nid trn)"
| "nf (CTrans s nid1 trn1 nid2 trn2) = CMSec (mergeSec nid1 (f nid1 trn1) nid2 (f nid2 trn2))"


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


fun translateSec :: "('nodeid, 'sec) nvalue ⇒ ('nodeid, 'sec, 'msec) merged_sec" where
  "translateSec (LVal nid s) = LMSec nid s"
| "translateSec (CVal nid1 s1 nid2 s2) = CMSec (mergeSec nid1 s1 nid2 s2)"

lemma decompV_Cons_LVal: "decompV (LVal nid s # sl) = (decompV sl)(nid := s # decompV sl nid)"
by auto

lemma decompV_Cons_CVal:
assumes "nid1 ≠ nid2"
shows "decompV (CVal nid1 s1 nid2 s2 # sl) = (decompV sl)(nid1 := s1 # decompV sl nid1, nid2 := s2 # decompV sl nid2)"
using assms by auto

lemma nValidV_compSec:
assumes "list_all nValidV sl"
shows "compSec (decompV sl) (map translateSec sl)"
using assms proof (induction sl)
  case Nil then show ?case using compSec.Nil by auto
next
  case (Cons s sl)
  then have sl: "compSec (decompV sl) (map translateSec sl)" by auto
  show ?case proof (cases s)
    case (LVal nid1 s1)
    moreover with Cons sl have "compSec ((decompV sl)(nid1 := s1 # decompV sl nid1)) (LMSec nid1 s1 # map translateSec sl)"
      by (intro compSec.Local) auto
    ultimately show ?thesis unfolding LVal decompV_Cons_LVal[symmetric] by (auto simp del: decompV.simps)
  next
    case (CVal nid1 s1 nid2 s2)
    moreover with Cons sl have "compSec ((decompV sl)(nid1 := s1 # decompV sl nid1, nid2 := s2 # decompV sl nid2)) (CMSec (mergeSec nid1 s1 nid2 s2) # map translateSec sl)"
      by (intro compSec.Comm) auto
    moreover have n: "nid1 ≠ nid2" using CVal Cons by auto
    ultimately show ?thesis unfolding CVal decompV_Cons_CVal[OF n, symmetric] by (auto simp del: decompV.simps)
  qed
qed

lemma compSecE:
assumes "compSec sls sl"
obtains sl' where "decompV sl' = sls" and "map translateSec sl' = sl" and "list_all nValidV sl'"
using assms proof (induction)
  case Nil from this[of "[]"] show thesis by auto
next
  case (Local sls sl nid s)
  show thesis proof (rule Local.IH)
    fix sl'
    assume "decompV sl' = sls" and "map translateSec sl' = sl" and "list_all nValidV sl'"
    with Local.hyps show thesis by (intro Local.prems[of "LVal nid s # sl'"]) auto
  qed
next
  case (Comm sls sl nid1 nid2 s1 s2)
  show thesis proof (rule Comm.IH)
    fix sl'
    assume "decompV sl' = sls" and "map translateSec sl' = sl" and "list_all nValidV sl'"
    with Comm.hyps show thesis by (intro Comm.prems[of "CVal nid1 s1 nid2 s2 # sl'"]) auto
  qed
qed

interpretation Trans: BD_Security_TS_Trans istate nValidTrans nSrcOf nTgtOf nφ Net.nf nγ ng nT Net.nB
                                           istate nValidTrans nSrcOf nTgtOf nφ nf nγ ng nT nB
                                           id id Some "Some o translateSec"
proof (unfold_locales, goal_cases)
  case (8 trn)
  then show ?case by (cases trn) auto
next
  case (11 sl' sl1' tr)
  then have "list_all nValidV (Net.V tr)" by (auto intro: validFrom_nValidV reach.Istate)
  then have "compSec (decompV (Net.V tr)) (map translateSec (Net.V tr))" by (intro nValidV_compSec)
  then obtain sls1 where "compSec sls1 sl1'" and "∀nid ∈ nodes. B nid (decompV (Net.V tr) nid) (sls1 nid)"
    using ‹nB sl' sl1'› ‹these (map (Some ∘ translateSec) (Net.V tr)) = sl'› unfolding nB_def by auto
  moreover then obtain sl1 where "decompV sl1 = sls1" and "list_all nValidV sl1"
                             and "map translateSec sl1 = sl1'" by (elim compSecE)
  ultimately show ?case unfolding Net.nB_def by auto
qed auto

theorem network_secure:
assumes "∀nid ∈ nodes. lsecure nid"
shows "secure"
using assms Net.network_secure Trans.translate_secure by blast

end

context BD_Security_TS_Network
begin

text ‹In order to formalize a result about preserving the notion of secrets of the source node
upon composition, we define a notion of synchronization of secrets of the source and another node.›

inductive srcSyncV :: "'nodeid ⇒ 'val list ⇒ 'val list ⇒ bool"
for nid :: "'nodeid"
where
  Nil: "srcSyncV nid [] []"
| Other: "⟦srcSyncV nid vlSrc vlNode; ¬isComV source v ∨ tgtNodeOfV source v ≠ nid⟧
          ⟹ srcSyncV nid (v # vlSrc) vlNode"
| Send: "⟦srcSyncV nid vlSrc vlNode; comOfV source vSrc = Send; comOfV nid vNode = Recv;
          tgtNodeOfV source vSrc = nid; tgtNodeOfV nid vNode = source;
          syncV source vSrc nid vNode⟧ ⟹ srcSyncV nid (vSrc # vlSrc) (vNode # vlNode)"
| Recv: "⟦srcSyncV nid vlSrc vlNode; comOfV source vSrc = Recv; comOfV nid vNode = Send;
          tgtNodeOfV source vSrc = nid; tgtNodeOfV nid vNode = source;
          syncV nid vNode source vSrc⟧ ⟹ srcSyncV nid (vSrc # vlSrc) (vNode # vlNode)"

text ‹Sanity check that this is equivalent to a more general notion of binary secret
synchronisation applied to source secrets and target secrets, where the latter do not contain
internal secrets (in line with the assumption of unique secret polarization).›

inductive binSyncV :: "'nodeid ⇒ 'nodeid ⇒ 'val list ⇒ 'val list ⇒ bool"
for nid1 nid2 :: "'nodeid"
where
  Nil: "binSyncV nid1 nid2 [] []"
| Int1: "⟦binSyncV nid1 nid2 vl1 vl2; ¬isComV nid1 v ∨ tgtNodeOfV nid1 v ≠ nid2⟧
          ⟹ binSyncV nid1 nid2 (v # vl1) vl2"
| Int2: "⟦binSyncV nid1 nid2 vl1 vl2; ¬isComV nid2 v ∨ tgtNodeOfV nid2 v ≠ nid1⟧
          ⟹ binSyncV nid1 nid2 vl1 (v # vl2)"
| Send: "⟦binSyncV nid1 nid2 vl1 vl2; comOfV nid1 v1 = Send; comOfV nid2 v2 = Recv;
          tgtNodeOfV nid1 v1 = nid2; tgtNodeOfV nid2 v2 = nid1;
          syncV nid1 v1 nid2 v2⟧ ⟹ binSyncV nid1 nid2 (v1 # vl1) (v2 # vl2)"
| Recv: "⟦binSyncV nid1 nid2 vl1 vl2; comOfV nid1 v1 = Recv; comOfV nid2 v2 = Send;
          tgtNodeOfV nid1 v1 = nid2; tgtNodeOfV nid2 v2 = nid1;
          syncV nid2 v2 nid1 v1⟧ ⟹ binSyncV nid1 nid2 (v1 # vl1) (v2 # vl2)"

lemma srcSyncV_binSyncV:
assumes "source ∈ nodes" and "nid2 ∈ nodes"
shows "srcSyncV nid2 vl1 vl2 ⟷ (binSyncV source nid2 vl1 vl2 ∧
                                  list_all (λv. isComV nid2 v ∧ tgtNodeOfV nid2 v = source) vl2)"
  (is "?l ⟷ ?r")
proof
  assume "?l"
  then show "?r" using assms by (induction rule: srcSyncV.induct) (auto intro: binSyncV.intros)
next
  assume "?r"
  then have "binSyncV source nid2 vl1 vl2"
        and "list_all (λv. isComV nid2 v ∧ tgtNodeOfV nid2 v = source) vl2" by auto
  then show "?l" by (induction rule: binSyncV.induct) (auto intro: srcSyncV.intros)
qed

end

text ‹We can obtain a security property for the network w.r.t. the original declassification bound
of the secret issuer node, if that bound is suitably reflected in the bounds of all the other nodes,
i.e. the bounds of the receiving nodes do not declassify any more confidential information than is
already declassified by the bound of the secret issuer node.›

locale BD_Security_TS_Network_Preserve_Source_Security = Net?: BD_Security_TS_Network +
assumes source_in_nodes: "source ∈ nodes"
and source_secure: "lsecure source"
and B_source_in_B_sinks: "⋀nid tr vl' vl1.
⟦B source (lV source tr) vl1; srcSyncV nid (lV source tr) vl';
 lValidFrom source (istate source) tr; never (T source) tr;
 nid ∈ nodes; nid ≠ source⟧
⟹ (∃vl1'. B nid vl' vl1' ∧ srcSyncV nid vl1 vl1')"
begin

abbreviation "nodes' ≡ nodes - {source}"

fun nf' where
  "nf' (LTrans s nid trn) = f source trn"
| "nf' (CTrans s nid1 trn1 nid2 trn2) = (if nid1 = source then f source trn1 else f source trn2)"

fun translateVal where
  "translateVal (LVal nid v) = v"
| "translateVal (CVal nid1 v1 nid2 v2) = (if nid1 = source then v1 else v2)"

definition isProjectionOf where
  "isProjectionOf p vl = (∀nid ∈ nodes'. srcSyncV nid vl (p nid))"

lemma nValidV_tgtNodeOf:
assumes "list_all nValidV vl'"
shows "list_all (λv. isComV source v ⟶ tgtNodeOfV source v ≠ source) (decompV vl' source)"
using assms proof (induction vl')
  case (Cons v vl') then show ?case by (cases v) auto
qed auto

lemma lValidFrom_source_tgtNodeOfV:
assumes "lValidFrom source s tr"
and "lreach source s"
shows "list_all (λv. isComV source v ⟶ tgtNodeOfV source v ≠ source) (lV source tr)"
     (is "?goal tr")
proof -
  interpret Node: BD_Security_TS "istate source" "validTrans source" "srcOf source" "tgtOf source"
                                 "φ source" "f source" "γ source" "g source" "T source" "B source" .
  from assms show ?thesis proof (induction tr arbitrary: s)
    case (Cons trn tr s)
      have "?goal tr" using Cons.prems by (intro Cons.IH[of "tgtOf source trn"]) (auto intro: Node.reach.Step)
      then show ?case using Cons.prems isCom_tgtNodeOf by (cases "φ source trn") auto
  qed auto
qed

lemma merge_projection:
assumes "isProjectionOf p vl"
and "list_all (λv. isComV source v ⟶ tgtNodeOfV source v ≠ source) vl"
obtains vl' where "∀nid ∈ nodes'. decompV vl' nid = p nid"
              and "decompV vl' source = vl"
              and "map translateVal vl' = vl"
              and "list_all nValidV vl'"
using assms proof (induction vl arbitrary: p)
  case (Nil p)
    from Nil.prems(2) show thesis
      by (intro Nil.prems(1)[of "[]"]) (auto simp: isProjectionOf_def elim!: ballE srcSyncV.cases)
next
  case (Cons v vl p)
    show thesis proof (cases "isComV source v ∧ tgtNodeOfV source v ∈ nodes")
      case False
        show thesis proof (rule Cons.IH[of p])
          show "isProjectionOf p vl"
            using Cons(3) False unfolding isProjectionOf_def by (auto elim: srcSyncV.cases)
          show "list_all (λv. isComV source v ⟶ tgtNodeOfV source v ≠ source) vl"
            using Cons(4) by auto
        next
          fix vl'
          assume "∀nid∈nodes'. decompV vl' nid = p nid" and "decompV vl' source = vl"
             and "map translateVal vl' = vl" and "list_all nValidV vl'"
          then show thesis
            using False source_in_nodes by (intro Cons(2)[of "LVal source v # vl'"]) auto
        qed
    next
      case True
        let ?tgt = "tgtNodeOfV source v"
        from True Cons(4) have nodes': "?tgt ∈ nodes'" by auto
        with Cons(3) obtain vn vln
        where p: "p ?tgt = vn # vln" and cmp: "srcSyncV ?tgt (v # vl) (vn # vln)"
          using True unfolding isProjectionOf_def
          by (cases "p ?tgt") (auto elim!: ballE elim: srcSyncV.cases)
        show thesis proof (rule Cons.IH[of "p(?tgt := vln)"])
          show "isProjectionOf (p(?tgt := vln)) vl"
            using Cons(3) True cmp unfolding isProjectionOf_def by (auto elim: srcSyncV.cases)
          show "list_all (λv. isComV source v ⟶ tgtNodeOfV source v ≠ source) vl"
            using Cons(4) by auto
        next
          fix vl'
          assume vl': "∀nid∈nodes'. decompV vl' nid = (p(?tgt := vln)) nid"
                      "decompV vl' source = vl" "map translateVal vl' = vl" "list_all nValidV vl'"
          show thesis proof cases
            assume "comOfV source v = Send"
            then show thesis using vl' p source_in_nodes True nodes' cmp
              by (intro Cons(2)[of "CVal source v ?tgt vn # vl'"]) (auto elim: srcSyncV.cases)
          next
            assume "comOfV source v ≠ Send"
            then show thesis using vl' p source_in_nodes True nodes' cmp
              by (intro Cons(2)[of "CVal ?tgt vn source v # vl'"]) (auto elim: srcSyncV.cases)
          qed
        qed
    qed
qed

lemma translateVal_decompV:
assumes "validFrom s tr"
and "reach s"
shows "map translateVal (V tr) = decompV (V tr) source"
using assms proof (induction tr arbitrary: s)
  case (Cons trn tr s)
    then have tr: "validFrom (nTgtOf trn) tr" and r: "reach (nTgtOf trn)"
      unfolding validFrom_Cons by (auto intro: reach.Step[of s trn])
    show ?case proof (cases trn)
      case (LTrans s' nid trn')
        moreover then have "φ nid trn' ⟶ nid = source"
          using Cons.prems Net.φ_source[of nid trn'] reach_lreach by auto
        ultimately show ?thesis using Cons.IH[OF tr r] by (cases "nφ trn") auto
    next
      case (CTrans s' nid1 trn1 nid2 trn2)
        moreover then have "nφ trn ⟶ (nid1 = source ∨ nid2 = source)"
          using Cons.prems Net.φ_source[of nid1 trn1] Net.φ_source[of nid2 trn2] reach_lreach
          by (cases "nid1 ≠ source") auto
        ultimately show ?thesis using Cons.IH[OF tr r] by (cases "nφ trn") auto
    qed
qed auto

lemma srcSyncV_decompV:
assumes tr: "validFrom s tr"
and s: "reach s"
and "nid ∈ nodes" and "nid ≠ source"
shows "srcSyncV nid (decompV (V tr) source) (decompV (V tr) nid)"
using tr s proof (induction tr arbitrary: s)
  case (Cons trn tr s)
    then have trn: "nValidTrans trn" and tr: "validFrom (nTgtOf trn) tr" and r: "reach (nTgtOf trn)"
      unfolding validFrom_Cons by (auto intro: reach.Step[of s trn])
    show ?case proof (cases trn)
      case (LTrans s' nid' trn')
        show ?thesis proof (cases "φ nid' trn'")
          case True
            then have "nid' = source"
              using Cons.prems Net.φ_source[of nid' trn'] reach_lreach LTrans by auto
            then show ?thesis using Cons.IH[OF tr r] Cons.prems LTrans assms(3,4) True
              by (auto intro!: srcSyncV.Other elim: reach_lreach[of s nid'])
        next
          case False
            then show ?thesis using Cons.IH[OF tr r] LTrans by auto
        qed
    next
      case (CTrans s' nid1 trn1 nid2 trn2)
        have r1: "lreach nid1 (s' nid1)" and r2: "lreach nid2 (s' nid2)"
          using CTrans reach_lreach Cons.prems by auto
        show ?thesis proof (cases)
          assume φ: "nφ trn"
          then have "nid1 = source ∨ nid2 = source"
            using CTrans Cons.prems Net.φ_source[of nid1 trn1] Net.φ_source[of nid2 trn2] reach_lreach
            by (cases "nid1 ≠ source") auto
          moreover have "φ nid1 trn1" and "φ nid2 trn2" using CTrans trn r1 r2 φ sync_φ1_φ2 by auto
          moreover then have "comOfV nid1 (f nid1 trn1) = comOf nid1 trn1"
                    and "isCom nid1 trn1 ⟶ tgtNodeOfV nid1 (f nid1 trn1) = tgtNodeOf nid1 trn1"
                    and "comOfV nid2 (f nid2 trn2) = comOf nid2 trn2"
                    and "isCom nid2 trn2 ⟶ tgtNodeOfV nid2 (f nid2 trn2) = tgtNodeOf nid2 trn2"
                    and "syncV nid1 (f nid1 trn1) nid2 (f nid2 trn2)"
            using CTrans trn r1 r2 by (auto intro: sync_syncV)
          ultimately show ?thesis
            using Cons.IH[OF tr r] trn assms(3,4) CTrans
            using srcSyncV.Send[OF Cons.IH[OF tr r], of "f nid1 trn1" "f nid2 trn2"]
            using srcSyncV.Recv[OF Cons.IH[OF tr r], of "f nid2 trn2" "f nid1 trn1"]
            using srcSyncV.Other[OF Cons.IH[OF tr r], of "f nid1 trn1"]
            using srcSyncV.Other[OF Cons.IH[OF tr r], of "f nid2 trn2"]
            by auto
        next
          assume "¬nφ trn"
          with Cons.IH[OF tr r] show ?thesis by auto
        qed
    qed
qed (auto intro: srcSyncV.Nil)


sublocale BD_Security_TS_Trans istate nValidTrans nSrcOf nTgtOf nφ nf nγ ng nT nB
                               istate nValidTrans nSrcOf nTgtOf nφ nf' nγ ng nT "B source"
                               id id Some "Some o translateVal"
proof unfold_locales
  fix trn
  assume trn: "nValidTrans trn" and r: "reach (nSrcOf trn)" and φ: "nφ (id trn)"
  show "nφ trn ∧ (Some ∘ translateVal) (nf trn) = Some (nf' (id trn))"
  proof (cases trn)
    case (LTrans s nid trn')
      moreover then have "nid = source" using trn r φ Net.φ_source[of nid trn'] reach_lreach by auto
      ultimately show ?thesis using φ by auto
  next
    case (CTrans s nid1 trn1 nid2 trn2)
      moreover then have "nid1 = source ∨ nid2 = source"
        using trn r φ Net.φ_source[of nid1 trn1] Net.φ_source[of nid2 trn2] reach_lreach[OF r]
        by (cases "nid1 ≠ source") auto
      ultimately show ?thesis using φ by auto
  qed
next
  fix vl' vl1' tr
  interpret Source: Transition_System "istate source" "validTrans source" "srcOf source" "tgtOf source" .
  assume "B source vl' vl1'" and tr: "validFrom istate tr" and nT: "never nT tr"
     and vl': "these (map (Some ∘ translateVal) (V tr)) = vl'"
  then have B: "B source (decompV (V tr) source) vl1'"
    using reach.Istate by (auto simp: translateVal_decompV)
  then obtain tr1 where tr1: "lValidFrom source (istate source) tr1" and "lV source tr1 = vl1'"
    using source_secure validFrom_lValidFrom[OF tr, of source] decompV_decomp[OF tr reach.Istate] nT
    unfolding Abstract_BD_Security.secure_def by (auto intro: nTT_TT)
  then have "∀nid ∈ nodes'. srcSyncV nid (decompV (V tr) source) (decompV (V tr) nid)"
        and tgt_vl1': "list_all (λv. isComV source v ⟶ tgtNodeOfV source v ≠ source) vl1'"
    using B tr vl' reach.Istate srcSyncV_decompV nValidV_tgtNodeOf validFrom_nValidV
    using lValidFrom_source_tgtNodeOfV[OF tr1 Source.reach.Istate]
    by (auto simp: translateVal_decompV)
  then have "∃p. ∀nid ∈ nodes'. B nid (decompV (V tr) nid) (p nid) ∧ srcSyncV nid vl1' (p nid)"
    using B B_source_in_B_sinks decompV_decomp[OF tr reach.Istate] validFrom_lValidFrom[OF tr, of source]
    using nT nTT_TT by (intro bchoice) auto
  then obtain p where "isProjectionOf p vl1'" and B': "∀nid ∈ nodes'. B nid (decompV (V tr) nid) (p nid)"
    unfolding isProjectionOf_def by auto
  then obtain vl1 where p: "∀nid ∈ nodes'. decompV vl1 nid = p nid" and vl1': "decompV vl1 source = vl1'"
                    and "map translateVal vl1 = vl1'" and "list_all nValidV vl1"
    using tgt_vl1' by (elim merge_projection) auto
  moreover have "∀nid ∈ nodes. B nid (decompV (V tr) nid) (decompV vl1 nid)" proof
    fix nid
    assume "nid ∈ nodes"
    then show "B nid (decompV (V tr) nid) (decompV vl1 nid)"
      using B vl1' B' p by (cases "nid = source") auto
  qed
  ultimately show "∃vl1. these (map (Some ∘ translateVal) vl1) = vl1' ∧ nB (V tr) vl1"
    using B tr vl' reach.Istate
    by (intro exI[of _ vl1]) (auto simp: nB_def)
qed auto

theorem preserve_source_secure:
assumes "∀nid ∈ nodes'. lsecure nid"
shows "secure"
using assms source_secure
by (intro translate_secure network_secure ballI) auto

end

text ‹We can simplify the check that the bound of the source node is reflected in those of the
other nodes with the help of a function mapping secrets communicated by the source node to those
of the target nodes.›

locale BD_Security_TS_Network_getTgtV = BD_Security_TS_Network +
fixes getTgtV
assumes getTgtV_Send: "comOfV source vSrc = Send ⟹ tgtNodeOfV source vSrc = nid ⟹ nid ≠ source ⟹ (syncV source vSrc nid vn ⟷ vn = getTgtV vSrc) ∧ tgtNodeOfV nid (getTgtV vSrc) = source ∧ comOfV nid (getTgtV vSrc) = Recv"
and getTgtV_Recv: "comOfV source vSrc = Recv ⟹ tgtNodeOfV source vSrc = nid ⟹ nid ≠ source ⟹ (syncV nid vn source vSrc ⟷ vn = getTgtV vSrc) ∧ tgtNodeOfV nid (getTgtV vSrc) = source ∧ comOfV nid (getTgtV vSrc) = Send"
begin

abbreviation "projectSrcV nid vlSrc
 ≡ map getTgtV (filter (λv. isComV source v ∧ tgtNodeOfV source v = nid) vlSrc)"

lemma srcSyncV_projectSrcV:
assumes "nid ∈ nodes - {source}"
shows "srcSyncV nid vlSrc vln ⟷ vln = projectSrcV nid vlSrc"
proof
  assume "srcSyncV nid vlSrc vln"
  then show "vln = projectSrcV nid vlSrc" using assms getTgtV_Send getTgtV_Recv by induction auto
next
  assume "vln = projectSrcV nid vlSrc"
  moreover have "srcSyncV nid vlSrc (projectSrcV nid vlSrc)"
    using assms getTgtV_Send getTgtV_Recv by (induction vlSrc) (auto intro: srcSyncV.intros)
  ultimately show "srcSyncV nid vlSrc vln" by simp
qed

end

locale BD_Security_TS_Network_Preserve_Source_Security_getTgtV = Net?: BD_Security_TS_Network_getTgtV +
assumes source_in_nodes: "source ∈ nodes"
and source_secure: "lsecure source"
and B_source_in_B_sinks: "⋀nid tr vl vl1.
⟦B source vl vl1; vl = lV source tr; lValidFrom source (istate source) tr; never (T source) tr;
 nid ∈ nodes; nid ≠ source⟧
⟹ B nid (projectSrcV nid vl) (projectSrcV nid vl1)"
begin

sublocale BD_Security_TS_Network_Preserve_Source_Security
using source_in_nodes source_secure B_source_in_B_sinks srcSyncV_projectSrcV
by (unfold_locales) auto

end

text ‹An alternative composition setup that derives parameters ‹comOfV›, ‹syncV›, etc. from
‹comOf›, ‹sync›, etc.›

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
   source :: "'nodeid"
assumes
  g_comOf: "⋀nid trn1 trn2.
    ⟦validTrans nid trn1; lreach nid (srcOf nid trn1); γ nid trn1;
     validTrans nid trn2; lreach nid (srcOf nid trn2); γ nid trn2;
     g nid trn2 = g nid trn1⟧ ⟹ comOf nid trn2 = comOf nid trn1"
and
  f_comOf: "⋀nid trn1 trn2.
    ⟦validTrans nid trn1; lreach nid (srcOf nid trn1); φ nid trn1;
     validTrans nid trn2; lreach nid (srcOf nid trn2); φ nid trn2;
     f nid trn2 = f nid trn1⟧ ⟹ comOf nid trn2 = comOf nid trn1"
and
  g_tgtNodeOf: "⋀nid trn1 trn2.
    ⟦validTrans nid trn1; lreach nid (srcOf nid trn1); γ nid trn1;
     validTrans nid trn2; lreach nid (srcOf nid trn2); γ nid trn2;
     g nid trn2 = g nid trn1⟧ ⟹ tgtNodeOf nid trn2 = tgtNodeOf nid trn1"
and
  f_tgtNodeOf: "⋀nid trn1 trn2.
    ⟦validTrans nid trn1; lreach nid (srcOf nid trn1); φ nid trn1;
     validTrans nid trn2; lreach nid (srcOf nid trn2); φ nid trn2;
     f nid trn2 = f nid trn1⟧ ⟹ tgtNodeOf nid trn2 = tgtNodeOf nid trn1"
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 ⟹
      ∃trn1' trn2'.
        validTrans nid1 trn1' ∧ lreach nid1 (srcOf nid1 trn1') ∧ γ nid1 trn1' ∧ g nid1 trn1' = g nid1 trn1 ∧
        validTrans nid2 trn2' ∧ lreach nid2 (srcOf nid2 trn2') ∧ γ nid2 trn2' ∧ g nid2 trn2' = g nid2 trn2 ∧
        sync nid1 trn1' nid2 trn2') ⟹
     (φ nid1 trn1 ⟹ φ nid2 trn2 ⟹
      ∃trn1' trn2'.
        validTrans nid1 trn1' ∧ lreach nid1 (srcOf nid1 trn1') ∧ φ nid1 trn1' ∧ f nid1 trn1' = f nid1 trn1 ∧
        validTrans nid2 trn2' ∧ lreach nid2 (srcOf nid2 trn2') ∧ φ nid2 trn2' ∧ f nid2 trn2' = f nid2 trn2 ∧
        sync nid1 trn1' nid2 trn2')
     ⟹
     sync nid1 trn1 nid2 trn2"
and
  isCom_γ: "⋀nid trn. validTrans nid trn ⟹ lreach nid (srcOf nid trn) ⟹ comOf nid trn = Send ∨ comOf nid trn = Recv ⟹ γ nid trn"
and
  φ_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

definition "reachableO nid obs = (∃trn. validTrans nid trn ∧ lreach nid (srcOf nid trn) ∧ γ nid trn ∧ g nid trn = obs)"
definition "reachableV nid sec = (∃trn. validTrans nid trn ∧ lreach nid (srcOf nid trn) ∧ φ nid trn ∧ f nid trn = sec)"

definition "invO nid obs = inv_into {trn. validTrans nid trn ∧ lreach nid (srcOf nid trn) ∧ γ nid trn} (g nid) obs"
definition "invV nid sec = inv_into {trn. validTrans nid trn ∧ lreach nid (srcOf nid trn) ∧ φ nid trn} (f nid) sec"

definition "comOfO nid obs = (if reachableO nid obs then comOf nid (invO nid obs) else Internal)"
definition "tgtNodeOfO nid obs = tgtNodeOf nid (invO nid obs)"
definition "comOfV nid sec = (if reachableV nid sec then comOf nid (invV nid sec) else Internal)"
definition "tgtNodeOfV nid sec = tgtNodeOf nid (invV nid sec)"
definition "syncO nid1 obs1 nid2 obs2 =
  (∃trn1 trn2. validTrans nid1 trn1 ∧ lreach nid1 (srcOf nid1 trn1) ∧ γ nid1 trn1 ∧ g nid1 trn1 = obs1 ∧
               validTrans nid2 trn2 ∧ lreach nid2 (srcOf nid2 trn2) ∧ γ nid2 trn2 ∧ g nid2 trn2 = obs2 ∧
               sync nid1 trn1 nid2 trn2)"
definition "syncV nid1 sec1 nid2 sec2 =
  (∃trn1 trn2. validTrans nid1 trn1 ∧ lreach nid1 (srcOf nid1 trn1) ∧ φ nid1 trn1 ∧ f nid1 trn1 = sec1 ∧
               validTrans nid2 trn2 ∧ lreach nid2 (srcOf nid2 trn2) ∧ φ nid2 trn2 ∧ f nid2 trn2 = sec2 ∧
               sync nid1 trn1 nid2 trn2)"

lemmas comp_O_V_defs = comOfO_def tgtNodeOfO_def comOfV_def tgtNodeOfV_def syncO_def syncV_def
                       reachableO_def reachableV_def

lemma reachableV_D:
assumes "reachableV nid sec"
shows "validTrans nid (invV nid sec)" and "lreach nid (srcOf nid (invV nid sec))"
  and "φ nid (invV nid sec)" and "f nid (invV nid sec) = sec"
using assms unfolding reachableV_def invV_def inv_into_def by (auto intro: someI2_ex)

lemma reachableO_D:
assumes "reachableO nid obs"
shows "validTrans nid (invO nid obs)" and "lreach nid (srcOf nid (invO nid obs))"
  and "γ nid (invO nid obs)" and "g nid (invO nid obs) = obs"
using assms unfolding reachableO_def invO_def inv_into_def by (auto intro: someI2_ex)

sublocale BD_Security_TS_Network
where comOfV = comOfV and tgtNodeOfV = tgtNodeOfV and syncV = syncV
  and comOfO = comOfO and tgtNodeOfO = tgtNodeOfO and syncO = syncO
proof (unfold_locales, goal_cases)
  case (1 nid trn) then show ?case by (auto intro!: f_comOf reachableV_D simp: comp_O_V_defs) next
  case (2 nid trn) then show ?case by (auto intro!: f_tgtNodeOf reachableV_D simp: comp_O_V_defs) next
  case (3 nid trn) then show ?case by (auto intro!: g_comOf reachableO_D simp: comp_O_V_defs)
  case (4 nid trn) then show ?case by (auto intro!: g_tgtNodeOf reachableO_D simp: comp_O_V_defs) next
  case (5 nid1 trn1 nid2 trn2) then show ?case unfolding comp_O_V_defs by auto next
  case (6 nid1 trn1 nid2 trn2) then show ?case unfolding comp_O_V_defs by auto next
  case (7 nid1 trn1 nid2 trn2) then show ?case using sync_φ1_φ2 by blast next
  case (8 nid1 trn1 nid2 trn2) then show ?case unfolding comp_O_V_defs by (intro sync_φ_γ) next
  case (9 nid trn) then show ?case by (intro isCom_γ) next
  case (10 nid trn) then show ?case by (intro φ_source)
qed

lemma comOf_invV:
assumes "validTrans nid trn" and "lreach nid (srcOf nid trn)" and "φ nid trn"
shows "comOf nid (invV nid (f nid trn)) = comOf nid trn"
using assms by (auto intro!: f_comOf reachableV_D simp: reachableV_def)

lemma comOfV_SendE:
assumes "comOfV nid v = Send"
obtains trn where "validTrans nid trn" and "lreach nid (srcOf nid trn)" and "φ nid trn" and "f nid trn = v"
              and "comOf nid trn = Send"
using assms unfolding comOfV_def by (auto simp: reachableV_def comOf_invV split: if_splits)

lemma comOfV_RecvE:
assumes "comOfV nid v = Recv"
obtains trn where "validTrans nid trn" and "lreach nid (srcOf nid trn)" and "φ nid trn" and "f nid trn = v"
              and "comOf nid trn = Recv"
using assms unfolding comOfV_def by (auto simp: reachableV_def comOf_invV split: if_splits)

fun secComp :: "('nodeid, 'val) nvalue list ⇒ bool" where
  "secComp [] = True"
| "secComp (LVal nid s # sl) =
    (secComp sl ∧ nid ∈ nodes ∧
     ¬(∃trn. validTrans nid trn ∧ lreach nid (srcOf nid trn) ∧ φ nid trn ∧ f nid trn = s ∧
             (comOf nid trn = Send ∨ comOf nid trn = Recv) ∧ tgtNodeOf nid trn ∈ nodes))"
| "secComp (CVal nid1 s1 nid2 s2 # sl) =
    (secComp sl ∧ nid1 ∈ nodes ∧ nid2 ∈ nodes ∧ nid1 ≠ nid2 ∧
     (∃trn1 trn2. validTrans nid1 trn1 ∧ lreach nid1 (srcOf nid1 trn1) ∧ φ nid1 trn1 ∧ f nid1 trn1 = s1 ∧
                  validTrans nid2 trn2 ∧ lreach nid2 (srcOf nid2 trn2) ∧ φ nid2 trn2 ∧ f nid2 trn2 = s2 ∧
                  comOf nid1 trn1 = Send ∧ tgtNodeOf nid1 trn1 = nid2 ∧
                  comOf nid2 trn2 = Recv ∧ tgtNodeOf nid2 trn2 = nid1 ∧
                  sync nid1 trn1 nid2 trn2))"

lemma syncedSecs_iff_nValidV: "secComp sl ⟷ list_all nValidV sl"
proof (induction sl rule: secComp.induct)
  case 2 then show ?case by (auto elim!: comOfV_SendE comOfV_RecvE) next
  case (3 nid1 v1 nid2 v2 sl)
    have "nValidV (CVal nid1 v1 nid2 v2) =
            (∃trn1 trn2. nid1 ∈ nodes ∧ nid2 ∈ nodes ∧ nid1 ≠ nid2 ∧
               validTrans nid1 trn1 ∧ lreach nid1 (srcOf nid1 trn1) ∧ φ nid1 trn1 ∧ f nid1 trn1 = v1 ∧
               validTrans nid2 trn2 ∧ lreach nid2 (srcOf nid2 trn2) ∧ φ nid2 trn2 ∧ f nid2 trn2 = v2 ∧
               comOf nid1 trn1 = Send ∧ tgtNodeOf nid1 trn1 = nid2 ∧
               comOf nid2 trn2 = Recv ∧ tgtNodeOf nid2 trn2 = nid1 ∧
               sync nid1 trn1 nid2 trn2)"
      by (auto simp: syncV_def) blast
    with 3 show ?case by auto
qed auto

lemma nB_secComp:
  "nB sl sl1 ⟷ (∀nid ∈ nodes. B nid (decompV sl nid) (decompV sl1 nid)) ∧
                                (secComp sl ⟶ secComp sl1)"
unfolding nB_def syncedSecs_iff_nValidV ..

end


end