Theory Friend_Network

theory Friend_Network
  imports
    "../API_Network"
    "Friend"
    "BD_Security_Compositional.Composing_Security_Network"
begin

subsection ‹Confidentiality for the N-ary composition›

locale FriendNetwork = 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 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