Theory Friend_Openness

(* The ``openness'' of the access window for the friendship confidentiality properties *)
theory Friend_Openness
  imports "Friend_State_Indistinguishability"
begin

subsection ‹Dynamic declassification trigger›

context Friend
begin

text ‹The dynamic declassification trigger condition holds, i.e.~the access window to the
confidential information is open, as long as the two users have not been created yet (so there cannot
be friendship between them) or while one of them is a local friend of an observer.›

definition openByA :: "state ⇒ bool"
where "openByA s ≡ ¬ UID1 ∈∈ userIDs s ∨ ¬ UID2 ∈∈ userIDs s"

definition openByF :: "state ⇒ bool"
where "openByF s ≡ ∃uid ∈ UIDs. uid ∈∈ friendIDs s UID1 ∨ uid ∈∈ friendIDs s UID2"

definition "open" :: "state ⇒ bool"
where "open s ≡ openByA s ∨ openByF s"

lemmas open_defs = open_def openByA_def openByF_def


lemma step_openByA_cases:
assumes "step s a = (ou, s')"
and "openByA s ≠ openByA s'"
obtains (CloseA) uid p uid' p' where "a = Cact (cUser uid p uid' p')"
                                     "uid' = UID1 ∨ uid' = UID2" "ou = outOK" "p = pass s uid"
                                     "openByA s" "¬openByA s'"
using assms proof (cases a)
  case (Dact da) then show ?thesis using assms by (cases da) (auto simp: d_defs openByA_def) next
  case (Uact ua) then show ?thesis using assms by (cases ua) (auto simp: u_defs openByA_def) next
  case (COMact ca) then show ?thesis using assms by (cases ca) (auto simp: com_defs openByA_def) next
  case (Sact sa)
    then show ?thesis using assms UID1_UID2 by (cases sa) (auto simp: s_defs openByA_def) next
  case (Cact ca)
    then show ?thesis using assms UID1_UID2 proof (cases ca)
      case (cUser uid p uid' p')
        then show ?thesis using Cact assms by (intro that) (auto simp: c_defs openByA_def)
    qed (auto simp: c_defs openByA_def)
qed auto

lemma step_openByF_cases:
assumes "step s a = (ou, s')"
and "openByF s ≠ openByF s'"
obtains
  (OpenF) uid p uid' where "a = Cact (cFriend uid p uid')" "ou = outOK" "p = pass s uid"
                           "uid ∈ UIDs ∧ uid' ∈ {UID1,UID2} ∨ uid ∈ {UID1,UID2} ∧ uid' ∈ UIDs"
                           "openByF s'" "¬openByF s"
| (CloseF) uid p uid' where "a = Dact (dFriend uid p uid')" "ou = outOK" "p = pass s uid"
                            "uid ∈ UIDs ∧ uid' ∈ {UID1,UID2} ∨ uid ∈ {UID1,UID2} ∧ uid' ∈ UIDs"
                            "openByF s" "¬openByF s'"
using assms proof (cases a)
  case (Uact ua) then show ?thesis using assms by (cases ua) (auto simp: u_defs openByF_def) next
  case (COMact ca) then show ?thesis using assms by (cases ca) (auto simp: com_defs openByF_def) next
  case (Sact sa)
    then show ?thesis using assms UID1_UID2 by (cases sa) (auto simp: s_defs openByF_def)
next
  case (Cact ca)
    then show ?thesis using assms UID1_UID2 proof (cases ca)
      case (cFriend uid p uid')
        then show ?thesis using Cact assms by (intro OpenF) (auto simp: c_defs openByF_def)
    qed (auto simp: c_defs openByF_def)
next
  case (Dact da)
    then show ?thesis using assms proof (cases da)
      case (dFriend uid p uid')
        then show ?thesis using Dact assms by (intro CloseF) (auto simp: d_defs openByF_def)
    qed
qed auto


lemma step_open_cases:
assumes step: "step s a = (ou, s')"
and op: "open s ≠ open s'"
obtains
  (CloseA) uid p uid' p' where "a = Cact (cUser uid p uid' p')"
                               "uid' = UID1 ∨ uid' = UID2" "ou = outOK" "p = pass s uid"
                               "openByA s" "¬openByA s'" "¬openByF s" "¬openByF s'"
| (OpenF) uid p uid' where "a = Cact (cFriend uid p uid')" "ou = outOK" "p = pass s uid"
                           "uid ∈ UIDs ∧ uid' ∈ {UID1,UID2} ∨ uid ∈ {UID1,UID2} ∧ uid' ∈ UIDs"
                           "openByF s'" "¬openByF s" "¬openByA s" "¬openByA s'"
| (CloseF) uid p uid' where "a = Dact (dFriend uid p uid')" "ou = outOK" "p = pass s uid"
                            "uid ∈ UIDs ∧ uid' ∈ {UID1,UID2} ∨ uid ∈ {UID1,UID2} ∧ uid' ∈ UIDs"
                            "openByF s" "¬openByF s'" "¬openByA s" "¬openByA s'"
proof -
  from op have "openByF s ≠ openByF s' ∨ openByA s ≠ openByA s'"
    unfolding open_def by auto
  then show thesis proof
    assume "openByF s ≠ openByF s'"
    with step show thesis proof (cases rule: step_openByF_cases)
      case (OpenF uid p uid')
        then have "openByA s = openByA s'" using step
          by (cases "openByA s ≠ openByA s'", elim step_openByA_cases) auto
        then have "¬openByA s ∧ ¬openByA s'" using op unfolding open_def by auto
        with OpenF show thesis by (intro that(2)) auto
    next
      case (CloseF uid p uid')
        then have "openByA s = openByA s'" using step
          by (cases "openByA s ≠ openByA s'", elim step_openByA_cases) auto
        then have "¬openByA s ∧ ¬openByA s'" using op unfolding open_def by auto
        with CloseF show thesis by (intro that(3)) auto
    qed
  next
    assume "openByA s ≠ openByA s'"
    with step show thesis proof (cases rule: step_openByA_cases)
      case (CloseA uid p uid' p')
        then have "openByF s = openByF s'" using step
          by (cases "openByF s ≠ openByF s'", elim step_openByF_cases) auto
        then have "¬openByF s ∧ ¬openByF s'" using op unfolding open_def by auto
        with CloseA show thesis by (intro that(1)) auto
    qed
  qed
qed


lemma eqButUID_openByA_eq:
assumes "eqButUID s s1"
shows "openByA s = openByA s1"
using assms unfolding openByA_def eqButUID_def by auto

lemma eqButUID_openByF_eq:
assumes ss1: "eqButUID s s1"
shows "openByF s = openByF s1"
proof -
  from ss1 have fIDs: "eqButUIDf (friendIDs s) (friendIDs s1)" unfolding eqButUID_def by auto
  have "∀uid ∈ UIDs. uid ∈∈ friendIDs s UID1 ⟷ uid ∈∈ friendIDs s1 UID1"
    using UID1_UID2_UIDs UID1_UID2 by (intro ballI eqButUIDf_not_UID'[OF fIDs]; auto)
  moreover have "∀uid ∈ UIDs. uid ∈∈ friendIDs s UID2 ⟷ uid ∈∈ friendIDs s1 UID2"
    using UID1_UID2_UIDs UID1_UID2 by (intro ballI eqButUIDf_not_UID'[OF fIDs]; auto)
  ultimately show "openByF s = openByF s1" unfolding openByF_def by auto
qed

lemma eqButUID_open_eq: "eqButUID s s1 ⟹ open s = open s1"
using eqButUID_openByA_eq eqButUID_openByF_eq unfolding open_def by blast


(* major *) lemma eqButUID_step_γ_out:
assumes ss1: "eqButUID s s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
(*and sT: "reachNT s" and s1: "reachNT s1"*)
and γ: "γ (Trans s a ou s')"
and os: "open s ⟶ friendIDs s = friendIDs s1"
shows "ou = ou1"
proof -
  obtain uid sa com_act where uid_a: "(userOfA a = Some uid ∧ uid ∈ UIDs ∧ uid ≠ UID1 ∧ uid ≠ UID2)
                                  ∨ a = COMact com_act ∨ a = Sact sa"
    using γ UID1_UID2_UIDs by fastforce
  { fix uid
    assume "uid ∈∈ friendIDs s UID1 ∨ uid ∈∈ friendIDs s UID2" and "uid ∈ UIDs"
    with os have "friendIDs s = friendIDs s1" unfolding open_def openByF_def by auto
  } note fIDs = this
  { fix uid uid'
    assume uid: "uid ≠ UID1" "uid ≠ UID2"
    have "friendIDs s uid = friendIDs s1 uid" (is ?f_eq)
     and "pendingFReqs s uid = pendingFReqs s1 uid" (is ?pFR_eq)
     and "uid ∈∈ friendIDs s uid' ⟷ uid ∈∈ friendIDs s1 uid'" (is ?f_iff)
     and "uid ∈∈ pendingFReqs s uid' ⟷ uid ∈∈ pendingFReqs s1 uid'" (is ?pFR_iff)
     and "friendReq s uid uid' = friendReq s1 uid uid'" (is ?FR_eq)
     and "friendReq s uid' uid = friendReq s1 uid' uid" (is ?FR_eq')
    proof -
      show ?f_eq ?pFR_eq using uid ss1 UID1_UID2_UIDs unfolding eqButUID_def
        by (auto intro!: eqButUIDf_not_UID)
      show ?f_iff ?pFR_iff using uid ss1 UID1_UID2_UIDs unfolding eqButUID_def
        by (auto intro!: eqButUIDf_not_UID')
      from uid have "¬ (uid,uid') ∈ {(UID1,UID2), (UID2,UID1)}" by auto
      then show ?FR_eq ?FR_eq' using ss1 UID1_UID2_UIDs unfolding eqButUID_def
        by (auto intro!: eqButUID12_not_UID)
    qed
  } note simps = this eqButUID_stateSelectors r_defs s_defs c_defs com_defs l_defs u_defs d_defs
  note facts = ss1 step step1 uid_a
  show ?thesis
  proof (cases a)
    case (Ract ra) then show ?thesis using facts by (cases ra) (auto simp add: simps)
  next
    case (Sact sa) then show ?thesis using facts by (cases sa) (auto simp add: simps)
  next
    case (Cact ca) then show ?thesis using facts by (cases ca) (auto simp add: simps)
  next
    case (COMact ca) then show ?thesis using facts by (cases ca) (auto simp add: simps)
  next
    case (Lact la)
      then show ?thesis using facts proof (cases la)
        case (lFriends uid p uid')
          with γ have uid: "uid ∈ UIDs" using Lact by auto
          then have uid_uid': "uid ∈∈ friendIDs s uid' ⟷ uid ∈∈ friendIDs s1 uid'"
            using ss1 UID1_UID2_UIDs unfolding eqButUID_def by (intro eqButUIDf_not_UID') auto
          show ?thesis
          proof (cases "(uid' = UID1 ∨ uid' = UID2) ∧ uid ∈∈ friendIDs s uid'")
            case True
              with uid have "friendIDs s = friendIDs s1" by (intro fIDs) auto
              then show ?thesis using lFriends facts Lact by (auto simp: simps)
          next
            case False
              then show ?thesis using lFriends facts Lact simps(1) uid_uid' by (auto simp: simps)
          qed
      next
        case (lInnerPosts uid p)
          then have o: "⋀nid. owner s nid = owner s1 nid"
                and n: "⋀nid. post s nid = post s1 nid"
                and nids: "postIDs s = postIDs s1"
                and vis: "vis s = vis s1"
                and fu: "⋀uid'. uid ∈∈ friendIDs s uid' ⟷ uid ∈∈ friendIDs s1 uid'"
                and e: "e_listInnerPosts s uid p ⟷ e_listInnerPosts s1 uid p"
            using ss1 uid_a Lact unfolding eqButUID_def l_defs by (auto simp add: simps(3))
          have "listInnerPosts s uid p = listInnerPosts s1 uid p"
            unfolding listInnerPosts_def o n nids vis fu ..
          with e show ?thesis using Lact lInnerPosts step step1 by auto
      qed (auto simp add: simps)
  next
    case (Uact ua) then show ?thesis using facts by (cases ua) (auto simp add: simps)
  next
    case (Dact da) then show ?thesis using facts by (cases da) (auto simp add: simps)
  qed
qed

end

end