Theory Friend_Request_Network

theory Friend_Request_Network
  imports
    "../API_Network"
    "Friend_Request"
    "BD_Security_Compositional.Composing_Security_Network"
begin

subsection ‹Confidentiality for the N-ary composition›

locale FriendRequestNetwork = Network + FriendNetworkObservationSetup +
fixes
  AID :: apiID
and
  UID1 :: userID
and
  UID2 :: userID
assumes
  UID1_UID2_UIDs: "{UID1,UID2}  (UIDs AID) = {}"
and
  UID1_UID2: "UID1  UID2"
and
  AID_AIDs: "AID  AIDs"
begin

sublocale Issuer: Friend "UIDs AID" UID1 UID2 using UID1_UID2_UIDs UID1_UID2 by unfold_locales

abbreviation φ :: "apiID  (state, act, out) trans  bool"
where "φ aid trn  (Issuer.φ trn  aid = AID)"

abbreviation f :: "apiID  (state, act, out) trans  Friend.value"
where "f aid trn  Friend.f UID1 UID2 trn"

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

abbreviation B :: "apiID  Friend.value list  Friend.value list  bool"
where "B aid vl vl1  (if aid = AID then Issuer.B vl vl1 else (vl = []  vl1 = []))"

abbreviation "comOfV aid vl  Internal"
abbreviation "tgtNodeOfV aid vl  undefined"
abbreviation "syncV aid1 vl1 aid2 vl2  False"

lemma [simp]: "validTrans aid trn  lreach aid (srcOf trn)  φ aid trn  comOf aid trn = Internal"
by (cases trn) (auto elim: Issuer.φE)

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 srcNodeOf = srcNodeOf*) 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) then show ?case by auto next
  case (2 aid trn) then show ?case by auto next
  case (3 aid trn) then show ?case by (cases trn) auto next
  case (4 aid trn) then show ?case by (cases "(aid,trn)" rule: tgtNodeOf.cases) auto next
  case (5 aid1 trn1 aid2 trn2) then show ?case by auto next
  case (6 aid1 trn1 aid2 trn2) then show ?case by (cases trn1; cases trn2; auto) next
  case (7 aid1 trn1 aid2 trn2) then show ?case by auto next
  case (8 aid1 trn1 aid2 trn2) then show ?case by (cases trn1; cases trn2; auto) next
  case (9 aid trn) then show ?case by (cases "(aid,trn)" rule: tgtNodeOf.cases) (auto simp: FriendObservationSetup.γ.simps) next
  case (10 aid trn) then show ?case by auto
qed 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 = id
using AID_AIDs Issuer.secure
by unfold_locales auto

theorem secure: "secure"
proof (intro preserve_source_secure ballI)
  fix aid
  assume "aid  AIDs - {AID}"
  then show "Net.lsecure aid" by (intro Abstract_BD_Security.B_id_secure) (auto simp: B_id_def)
qed

end

end