Theory Post_Network

theory Post_Network
imports
  "../API_Network"
  "Post_ISSUER"
  "Post_RECEIVER"
  "BD_Security_Compositional.Composing_Security_Network"
begin

subsection ‹Confidentiality for the N-ary composition›

type_synonym ttrans = "(state, act, out) trans"
type_synonym obs = Post_Observation_Setup_ISSUER.obs
type_synonym "value" = "Post_ISSUER.value + Post_RECEIVER.value"

lemma value_cases:
fixes v :: "value"
obtains (PVal) pst where "v = Inl (Post_ISSUER.PVal pst)"
      | (PValS) aid pst where "v = Inl (Post_ISSUER.PValS aid pst)"
      | (PValR) pst where "v = Inr (Post_RECEIVER.PValR pst)"
proof (cases v)
  case (Inl vl) then show thesis using PVal PValS by (cases vl rule: Post_ISSUER.value.exhaust) auto next
  case (Inr vr) then show thesis using PValR by (cases vr rule: Post_RECEIVER.value.exhaust) auto
qed

locale Post_Network = Network
+ fixes UIDs :: "apiID ⇒ userID set"
  and AID :: "apiID" and PID :: "postID"
  assumes AID_in_AIDs: "AID ∈ AIDs"
begin

sublocale Iss: Post_ISSUER "UIDs AID" PID .

abbreviation φ :: "apiID ⇒ (state, act, out) trans ⇒ bool"
where "φ aid trn ≡ (if aid = AID then Iss.φ trn else Post_RECEIVER.φ PID AID trn)"

abbreviation f :: "apiID ⇒ (state, act, out) trans ⇒ value"
where "f aid trn ≡ (if aid = AID then Inl (Iss.f trn) else Inr (Post_RECEIVER.f PID AID trn))"

abbreviation γ :: "apiID ⇒ (state, act, out) trans ⇒ bool"
where "γ aid trn ≡ (if aid = AID then Iss.γ trn else ObservationSetup_RECEIVER.γ (UIDs aid) trn)"

abbreviation g :: "apiID ⇒ (state, act, out) trans ⇒ obs"
where "g aid trn ≡ (if aid = AID then Iss.g trn else ObservationSetup_RECEIVER.g PID AID trn)"

abbreviation T :: "apiID ⇒ (state, act, out) trans ⇒ bool"
where "T aid trn ≡ (if aid = AID then Iss.T trn else Post_RECEIVER.T (UIDs aid) PID AID trn)"

abbreviation B :: "apiID ⇒ value list ⇒ value list ⇒ bool"
where "B aid vl vl1 ≡
  (if aid = AID then list_all isl vl ∧ list_all isl vl1 ∧ Iss.B (map projl vl) (map projl vl1)
   else list_all (Not o isl) vl ∧ list_all (Not o isl) vl1 ∧ Post_RECEIVER.B (map projr vl) (map projr vl1))"

fun comOfV :: "apiID ⇒ value ⇒ com" where
  "comOfV aid (Inl (Post_ISSUER.PValS aid' pst)) = (if aid' ≠ aid then Send else Internal)"
| "comOfV aid (Inl (Post_ISSUER.PVal pst)) = Internal"
| "comOfV aid (Inr v) = Recv"

fun tgtNodeOfV :: "apiID ⇒ value ⇒ apiID" where
  "tgtNodeOfV aid (Inl (Post_ISSUER.PValS aid' pst)) = aid'"
| "tgtNodeOfV aid (Inl (Post_ISSUER.PVal pst)) = undefined"
| "tgtNodeOfV aid (Inr v) = AID"

definition syncV :: "apiID ⇒ value ⇒ apiID ⇒ value ⇒ bool" where
  "syncV aid1 v1 aid2 v2 =
    (∃pst. aid1 = AID ∧ v1 = Inl (Post_ISSUER.PValS aid2 pst) ∧ v2 = Inr (Post_RECEIVER.PValR pst))"

lemma syncVI: "syncV AID (Inl (Post_ISSUER.PValS aid' pst)) aid' (Inr (Post_RECEIVER.PValR pst))"
unfolding syncV_def by auto

lemma syncVE:
assumes "syncV aid1 v1 aid2 v2"
obtains pst where "aid1 = AID" "v1 = Inl (Post_ISSUER.PValS aid2 pst)" "v2 = Inr (Post_RECEIVER.PValR pst)"
using assms unfolding syncV_def by auto

fun getTgtV where
  "getTgtV (Inl (Post_ISSUER.PValS aid pst)) = Inr (Post_RECEIVER.PValR pst)"
| "getTgtV v = v"

lemma comOfV_AID:
  "comOfV AID v = Send ⟷ isl v ∧ Iss.isPValS (projl v) ∧ Iss.PValS_tgtAPI (projl v) ≠ AID"
  "comOfV AID v = Recv ⟷ Not (isl v)"
by (cases v rule: value_cases; auto)+

lemmas φ_defs = Post_RECEIVER.φ_def2 Iss.φ_def2

sublocale Net: BD_Security_TS_Network_getTgtV
where istate = "λ_. istate" and validTrans = validTrans and srcOf = "λ_. srcOf" and tgtOf = "λ_. tgtOf"
  and nodes = AIDs and comOf = comOf and tgtNodeOf = tgtNodeOf
  and sync = sync and φ = φ and f = f and γ = γ and g = g and T = T and B = B
  and comOfV = comOfV and tgtNodeOfV = tgtNodeOfV and syncV = syncV
  and comOfO = comOfO and tgtNodeOfO = tgtNodeOfO and syncO = syncO (*and cmpO = cmpO*)
  and source = AID and getTgtV = getTgtV
using AID_in_AIDs proof (unfold_locales, goal_cases)
  case (1 nid trn) then show ?case by (cases trn) (auto simp: φ_defs split: prod.splits) next
  case (2 nid trn) then show ?case by (cases trn) (auto simp: φ_defs split: prod.splits) next
  case (3 nid trn)
    interpret Sink: Post_RECEIVER "UIDs nid" PID AID .
    show ?case using 3 by (cases "(nid,trn)" rule: tgtNodeOf.cases) (auto split: prod.splits) next
  case (4 nid trn)
    interpret Sink: Post_RECEIVER "UIDs nid" PID AID .
    show ?case using 4 by (cases "(nid,trn)" rule: tgtNodeOf.cases) (auto split: prod.splits) next
  case (5 nid1 trn1 nid2 trn2)
    interpret Sink1: Post_RECEIVER "UIDs nid1" PID AID .
    interpret Sink2: Post_RECEIVER "UIDs nid2" PID AID .
    show ?case using 5 by (elim sync_cases) (auto intro: syncVI) next
  case (6 nid1 trn1 nid2 trn2)
    interpret Sink1: Post_RECEIVER "UIDs nid1" PID AID .
    interpret Sink2: Post_RECEIVER "UIDs nid2" PID AID .
    show ?case using 6 by (elim sync_cases) auto next
  case (7 nid1 trn1 nid2 trn2)
    interpret Sink1: Post_RECEIVER "UIDs nid1" PID AID .
    interpret Sink2: Post_RECEIVER "UIDs nid2" PID AID .
    show ?case using 7 by (elim sync_cases) (auto split: prod.splits, auto simp: sendPost_def) next
  case (8 nid1 trn1 nid2 trn2)
    interpret Sink1: Post_RECEIVER "UIDs nid1" PID AID .
    interpret Sink2: Post_RECEIVER "UIDs nid2" PID AID .
    show ?case using 8
      apply (elim syncO_cases; cases trn1; cases trn2)
          apply (auto simp: Iss.g_simps ObservationSetup_RECEIVER.g_simps split: prod.splits)
      apply (auto simp: sendPost_def split: prod.splits elim: syncVE)[]
      done next
  case (9 nid trn)
    then show ?case
      by (cases "(nid,trn)" rule: tgtNodeOf.cases)
         (auto simp: ObservationSetup_RECEIVER.γ.simps) next
  case (10 nid trn) then show ?case by (cases trn) (auto simp: φ_defs) next
  case (11 vSrc nid vn) then show ?case by (cases vSrc rule: value_cases) (auto simp: syncV_def) next
  case (12 vSrc nid vn) then show ?case by (cases vSrc rule: value_cases) (auto simp: syncV_def)
qed

lemma list_all_Not_isl_projectSrcV: "list_all (Not o isl) (Net.projectSrcV aid vlSrc)"
proof (induction vlSrc)
  case (Cons vSrc vlSrc') then show ?case by (cases vSrc rule: value_cases) auto
qed auto

context
fixes AID' :: apiID
assumes AID': "AID' ∈ AIDs - {AID}"
begin

interpretation Sink: Post_RECEIVER "UIDs AID'" PID AID by unfold_locales

lemma Source_B_Sink_B_aux:
assumes "list_all isl vl"
and "list_all isl vl1"
and "map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl vl)) =
     map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl vl1))"
shows "length (map projr (Net.projectSrcV AID' vl)) = length (map projr (Net.projectSrcV AID' vl1))"
using assms proof (induction vl vl1 rule: list22_induct)
  case (ConsCons v vl v1 vl1)
    consider (SendSend) aid pst pst1 where "v = Inl (Iss.PValS aid pst)" "v1 = Inl (Iss.PValS aid pst1)"
           | (Internal) "comOfV AID v = Internal" "¬Iss.isPValS (projl v)"
           | (Internal1) "comOfV AID v1 = Internal" "¬Iss.isPValS (projl v1)"
      using ConsCons(4-6) by (cases v rule: value_cases; cases v1 rule: value_cases) auto
    then show ?case proof cases
      case (SendSend) then show ?thesis using ConsCons.IH(1) ConsCons.prems by auto
    next
      case (Internal) then show ?thesis using ConsCons.IH(2)[of "v1 # vl1"] ConsCons.prems by auto
    next
      case (Internal1) then show ?thesis using ConsCons.IH(3)[of "v # vl"] ConsCons.prems by auto
    qed
qed (auto simp: comOfV_AID)

lemma Source_B_Sink_B:
assumes "B AID vl vl1"
shows "Sink.B (map projr (Net.projectSrcV AID' vl)) (map projr (Net.projectSrcV AID' vl1))"
using assms Source_B_Sink_B_aux by (auto simp: Iss.B_def Sink.B_def)

end

lemma map_projl_Inl: "map (projl o Inl) vl = vl"
by (induction vl) auto

lemma these_map_Inl_projl: "list_all isl vl ⟹ these (map (Some o Inl o projl) vl) = vl"
by (induction vl) auto

lemma map_projr_Inr: "map (projr o Inr) vl = vl"
by (induction vl) auto

lemma these_map_Inr_projr: "list_all (Not o isl) vl ⟹ these (map (Some o Inr o projr) vl) = vl"
by (induction vl) auto

sublocale BD_Security_TS_Network_Preserve_Source_Security_getTgtV
where istate = "λ_. istate" and validTrans = validTrans and srcOf = "λ_. srcOf" and tgtOf = "λ_. tgtOf"
  and nodes = AIDs and comOf = comOf and tgtNodeOf = tgtNodeOf
  and sync = sync and φ = φ and f = f and γ = γ and g = g and T = T and B = B
  and comOfV = comOfV and tgtNodeOfV = tgtNodeOfV and syncV = syncV
  and comOfO = comOfO and tgtNodeOfO = tgtNodeOfO and syncO = syncO (*and cmpO = cmpO*)
  and source = AID and getTgtV = getTgtV
proof (unfold_locales, goal_cases)
  case 1 show ?case using AID_in_AIDs . next
  case 2
    interpret Iss': BD_Security_TS_Trans
      istate System_Specification.validTrans srcOf tgtOf Iss.φ Iss.f Iss.γ Iss.g Iss.T Iss.B
      istate System_Specification.validTrans srcOf tgtOf Iss.φ "λtrn. Inl (Iss.f trn)" Iss.γ Iss.g Iss.T "B AID"
      id id Some "Some o Inl"
    proof (unfold_locales, goal_cases)
      case (11 vl' vl1' tr) then show ?case
        by (intro exI[of _ "map projl vl1'"]) (auto simp: map_projl_Inl these_map_Inl_projl)
    qed auto
    show ?case using Iss.Post_secure Iss'.translate_secure by auto
next
  case (3 aid tr vl' vl1)
    then show ?case
      using Source_B_Sink_B[of aid "(Net.lV AID tr)" vl1] list_all_Not_isl_projectSrcV
      by auto
qed

theorem secure: "secure"
proof (intro preserve_source_secure ballI)
  fix aid
  assume aid: "aid ∈ AIDs - {AID}"
  interpret Node: Post_RECEIVER "UIDs aid" PID AID .
  interpret Node': BD_Security_TS_Trans
    istate System_Specification.validTrans srcOf tgtOf Node.φ Node.f Node.γ Node.g Node.T Node.B
    istate System_Specification.validTrans srcOf tgtOf Node.φ "λtrn. Inr (Node.f trn)" Node.γ Node.g Node.T "B aid"
    id id Some "Some o Inr"
  proof (unfold_locales, goal_cases)
    case (11 vl' vl1' tr) then show ?case using aid
      by (intro exI[of _ "map projr vl1'"]) (auto simp: map_projr_Inr these_map_Inr_projr)
  qed auto
  show "Net.lsecure aid"
    using aid Node.Post_secure Node'.translate_secure by auto
qed

end  (* context Post_Network *)

end