Theory Outer_Friend_Network

theory Outer_Friend_Network
imports
  "../API_Network"
  "Issuer/Outer_Friend_Issuer"
  "Receiver/Outer_Friend_Receiver"
  "BD_Security_Compositional.Composing_Security_Network"
begin

subsection ‹Confidentiality for the N-ary composition›

locale OuterFriendNetwork = OuterFriend + Network +
assumes AID_AIDs: "AID ∈ AIDs"
begin

sublocale Issuer: OuterFriendIssuer UIDs AID UID using UID_UIDs by unfold_locales

abbreviation φ :: "apiID ⇒ (state, act, out) trans ⇒ bool"
where "φ aid trn ≡ (if aid = AID then Issuer.φ trn else OuterFriendReceiver.φ UIDs AID UID aid trn)"

abbreviation f :: "apiID ⇒ (state, act, out) trans ⇒ value"
where "f aid trn ≡ (if aid = AID then Issuer.f trn else OuterFriendReceiver.f aid trn)"

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

abbreviation g :: "apiID ⇒ (state, act, out) trans ⇒ obs"
where "g aid trn ≡ (if aid = AID then Issuer.g trn else OuterFriendReceiver.g UIDs AID UID aid trn)"

abbreviation T :: "apiID ⇒ (state, act, out) trans ⇒ bool"
where "T aid trn ≡ False"

abbreviation B :: "apiID ⇒ value list ⇒ value list ⇒ bool"
where "B aid vl vl1 ≡ (if aid = AID then Issuer.B vl vl1 else OuterFriendReceiver.B UIDs AID UID aid vl vl1)"

fun comOfV where
  "comOfV aid (FrVal aid' uid' st) = (if aid ≠ AID then Recv else (if aid' ≠ aid then Send else Internal))"
| "comOfV aid (OVal ov) = Internal"

fun tgtNodeOfV where
  "tgtNodeOfV aid (FrVal aid' uid' st) = (if aid = AID then aid' else AID)"
| "tgtNodeOfV aid (OVal ov) = AID"

abbreviation "syncV aid1 v1 aid2 v2 ≡ (v1 = v2)"

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 = id
proof (unfold_locales, goal_cases)
  case (1 aid trn)
    interpret Receiver: OuterFriendReceiver UIDs AID UID aid by unfold_locales
    from 1 show ?case by (cases trn) (auto elim!: Issuer.φE Receiver.φ.elims split: prod.splits)
next
  case (2 aid trn)
    interpret Receiver: OuterFriendReceiver UIDs AID UID aid by unfold_locales
    from 2 show ?case by (cases trn) (auto elim!: Issuer.φE Receiver.φ.elims)
next
  case (3 aid trn)
    interpret Receiver: OuterFriendReceiver UIDs AID UID aid by unfold_locales
    from 3 show ?case by (cases "(aid,trn)" rule: tgtNodeOf.cases) (auto)
next
  case (4 aid trn)
    interpret Receiver: OuterFriendReceiver UIDs AID UID aid by unfold_locales
    from 4 show ?case by (cases "(aid,trn)" rule: tgtNodeOf.cases) auto
next
  case (5 aid1 trn1 aid2 trn2)
    interpret Receiver1: OuterFriendReceiver UIDs AID UID aid1 by unfold_locales
    interpret Receiver2: OuterFriendReceiver UIDs AID UID aid2 by unfold_locales
    from 5 show ?case by (elim sync_cases) (auto simp: com_defs)
next
  case (6 aid1 trn1 aid2 trn2)
    interpret Receiver1: OuterFriendReceiver UIDs AID UID aid1 by unfold_locales
    interpret Receiver2: OuterFriendReceiver UIDs AID UID aid2 by unfold_locales
    from 6 show ?case by (elim sync_cases) (auto)
next
  case (7 aid1 trn1 aid2 trn2)
    interpret Receiver1: OuterFriendReceiver UIDs AID UID aid1 by unfold_locales
    interpret Receiver2: OuterFriendReceiver UIDs AID UID aid2 by unfold_locales
    from 7 show ?case
      using Issuer.COMact_open[of "srcOf trn1" "actOf trn1" "outOf trn1" "tgtOf trn1"]
      using Issuer.COMact_open[of "srcOf trn2" "actOf trn2" "outOf trn2" "tgtOf trn2"]
      by (elim sync_cases) auto
next
  case (8 aid1 trn1 aid2 trn2)
    interpret Receiver1: OuterFriendReceiver UIDs AID UID aid1 by unfold_locales
    interpret Receiver2: OuterFriendReceiver UIDs AID UID aid2 by unfold_locales
    assume "comOf aid1 trn1 = Send" "comOf aid2 trn2 = Recv" "syncO aid1 (g aid1 trn1) aid2 (g aid2 trn2)"
           "φ aid1 trn1 ⟹ φ aid2 trn2 ⟹ f aid1 trn1 = f aid2 trn2"
           "validTrans aid1 trn1" "validTrans aid2 trn2"
    then show ?case using emptyUserID_not_UIDs
      by (elim syncO_cases; cases trn1; cases trn2)
         (auto simp: Issuer.g_simps Receiver1.g_simps Receiver2.g_simps simp: com_defs)
next
  case (9 aid trn)
    interpret Receiver: OuterFriendReceiver UIDs AID UID aid by unfold_locales
    from 9 show ?case by (cases "(aid,trn)" rule: tgtNodeOf.cases) (auto)
next
  case (10 aid trn)
    interpret Receiver: OuterFriendReceiver UIDs AID UID aid by unfold_locales
    from 10 show ?case using AID_AIDs by (auto elim!: Receiver.φ.elims)
next
  case (11 vSrc nid vn) then show ?case by (cases vSrc) auto
next
  case (12 vSrc nid vn) then show ?case by (cases vSrc) auto
qed

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

interpretation Receiver: OuterFriendReceiver UIDs AID UID AID' by unfold_locales

lemma Issuer_BC_Receiver_BC:
assumes "Issuer.BC vl vl1"
shows "Receiver.BC (Net.projectSrcV AID' vl) (Net.projectSrcV AID' vl1)"
using assms by (induction rule: Issuer.BC.induct) auto

lemma Collect_setminus: "Collect P - A = {u. u ∉ A ∧ P u}"
by auto

lemma Issuer_vVS_Receiver_vVS:
assumes "Issuer.validValSeq vl auidl"
shows "Receiver.validValSeq (Net.projectSrcV AID' vl) {uid. (AID',uid) ∈∈ auidl}"
using assms AID'
proof (induction vl auidl rule: Issuer.validValSeq.induct)
  case (2 aid uid vl auidl)
  then show ?case by (auto simp: insert_Collect Collect_setminus, linarith, smt Collect_cong)
next
  case (3 aid uid vl auidl)
  then show ?case by (auto simp: insert_Collect Collect_setminus; smt Collect_cong)
qed auto

lemma Issuer_B_Receiver_B:
assumes "Issuer.B vl vl1"
shows "Receiver.B (Net.projectSrcV AID' vl) (Net.projectSrcV AID' vl1)"
using assms Issuer_BC_Receiver_BC Issuer_vVS_Receiver_vVS[of _ "[]"]
unfolding Issuer.B_def Issuer.BO_def Receiver.B_def Receiver.friendsOfUID_def
by (auto simp: istate_def intro!: Receiver.BC_append Receiver.BC_id, blast dest: Issuer.validValSeq_prefix)

end


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 = id
using AID_AIDs Issuer_B_Receiver_B Issuer.secure
by unfold_locales auto

theorem secure: "secure"
proof (intro preserve_source_secure ballI)
  fix aid
  interpret Receiver: OuterFriendReceiver UIDs AID UID aid by unfold_locales
  assume "aid ∈ AIDs - {AID}"
  then show "Net.lsecure aid" using Receiver.secure by auto
qed

end

end