Theory Outer_Friend_Receiver

theory Outer_Friend_Receiver
  imports
    "Outer_Friend_Receiver_Value_Setup"
    "Bounded_Deducibility_Security.Compositional_Reasoning"
begin

subsubsection ‹Declassification bound›

(* We verify the following:
   Given an arbitrary but fixed user UID at node AID (who is not an observer) and a set of
   observers at each network node, the observers may learn about the *occurrence* of remote
   friendship actions of UID (because network traffic is assumed to be observable), but they
   learn nothing about the *content* of those actions (who was added or deleted as a friend)
   beyond public knowledge (friendship addition and deletion occur alternatingly),
   except if the action adds or deletes one of the observers themselves as friend.
*)

context OuterFriendReceiver
begin

fun T :: "(state,act,out) trans ⇒ bool"
where "T trn = False"

text ‹For each user ‹uid› at this receiver node ‹AID'›, the remote friendship updates with
the fixed user ‹UID› at the issuer node ‹AID› form an alternating sequence of friending and unfriending.

Note that actions involving remote users who are observers do not produce secret values;
instead, those actions are observable, and the property we verify does not protect their
confidentiality.

Moreover, there is no declassification trigger on the receiver side, so \<^term>‹OVal› values
are never produced by receiver nodes, only by the issuer node.›

definition friendsOfUID :: "state ⇒ userID set" where
  "friendsOfUID s = {uid. (AID,UID) ∈∈ recvOuterFriendIDs s uid ∧ uid ∉ UIDs AID'}"

fun validValSeq :: "value list ⇒ userID set ⇒ bool" where
  "validValSeq [] _ = True"
| "validValSeq (FrVal aid uid True # vl) uids ⟷ uid ∉ uids ∧ aid = AID' ∧ uid ∉ UIDs AID' ∧ validValSeq vl (insert uid uids)"
| "validValSeq (FrVal aid uid False # vl) uids ⟷ uid ∈ uids ∧ aid = AID' ∧ uid ∉ UIDs AID' ∧ validValSeq vl (uids - {uid})"
| "validValSeq (OVal ov # vl) uids ⟷ False"

abbreviation "validValSeqFrom vl s ≡ validValSeq vl (friendsOfUID s)"

text ‹Observers may learn about the occurrence of
remote friendship actions (by observing network traffic), but not their content;
remote friendship actions at a receiver node ‹AID'› can be replaced by different actions
involving different users of that node (who are not observers)
without affecting the observations.›

inductive BC :: "value list ⇒ value list ⇒ bool"
where
  BC_Nil[simp,intro]: "BC [] []"
| BC_FrVal[intro]:
    "BC vl vl1 ⟹ uid' ∉ UIDs AID' ⟹ BC (FrVal aid uid st # vl) (FrVal AID' uid' st' # vl1)"

definition "B vl vl1 ≡ BC vl vl1 ∧ validValSeqFrom vl1 istate"


lemma BC_Nil_Nil: "BC vl vl1 ⟹ vl1 = [] ⟷ vl = []"
by (induction rule: BC.induct) auto

lemma BC_id: "validValSeq vl uids ⟹ BC vl vl"
by (induction rule: validValSeq.induct) auto

lemma BC_append: "BC vl vl1 ⟹ BC vl' vl1' ⟹ BC (vl @ vl') (vl1 @ vl1')"
by (induction rule: BC.induct) auto


sublocale BD_Security_IO where
istate = istate and step = step and
φ = φ and f = f and γ = γ and g = g and T = T and B = B
done


subsubsection ‹Unwinding proof›

definition Δ0 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ0 s vl s1 vl1 ≡ BC vl vl1 ∧ eqButUID s s1 ∧ validValSeqFrom vl1 s1"

lemma istate_Δ0:
assumes B: "B vl vl1"
shows "Δ0 istate vl istate vl1"
using assms unfolding Δ0_def B_def
by auto

lemma friendsOfUID_cong:
assumes "recvOuterFriendIDs s = recvOuterFriendIDs s'"
shows "friendsOfUID s = friendsOfUID s'"
using assms unfolding friendsOfUID_def by auto

lemma friendsOfUID_step_not_UID:
assumes "uid ≠ UID ∨ aid ≠ AID ∨ uid' ∈ UIDs AID'"
shows "friendsOfUID (receiveCreateOFriend s aid sp uid uid') = friendsOfUID s"
and "friendsOfUID (receiveDeleteOFriend s aid sp uid uid') = friendsOfUID s"
using assms unfolding friendsOfUID_def by (auto simp: com_defs)

lemma friendsOfUID_step_Create_UID:
assumes "uid' ∉ UIDs AID'"
shows "friendsOfUID (receiveCreateOFriend s AID sp UID uid') = insert uid' (friendsOfUID s)"
using assms unfolding friendsOfUID_def by (auto simp: com_defs)

lemma friendsOfUID_step_Delete_UID:
assumes "e_receiveDeleteOFriend s AID sp UID uid'"
and rs: "reach s"
shows "friendsOfUID (receiveDeleteOFriend s AID sp UID uid') = friendsOfUID s - {uid'}"
using assms reach_distinct_friends_reqs(4) unfolding friendsOfUID_def by (auto simp: com_defs)

lemma step_validValSeqFrom:
assumes step: "step s a = (ou, s')"
and rs: "reach s"
and c: "consume (Trans s a ou s') vl vl'" (is "consume ?trn vl vl'")
and vVS: "validValSeqFrom vl s"
shows "validValSeqFrom vl' s'"
proof cases
  assume "φ ?trn"
  moreover then obtain v where "vl = v # vl'" using c by (cases vl, auto simp: consume_def)
  ultimately show ?thesis using assms
    by (elim φ.elims) (auto simp: consume_def friendsOfUID_step_Create_UID friendsOfUID_step_Delete_UID)
next
  assume nφ: "¬φ ?trn"
  then have vl': "vl' = vl" using c by (auto simp: consume_def)
  then show ?thesis using vVS step proof (cases a)
    case (Sact sa) then show ?thesis using assms vl' by (cases sa) (auto simp: s_defs cong: friendsOfUID_cong) next
    case (Cact ca) then show ?thesis using assms vl' by (cases ca) (auto simp: c_defs cong: friendsOfUID_cong) next
    case (Dact da) then show ?thesis using assms vl' by (cases da) (auto simp: d_defs cong: friendsOfUID_cong) next
    case (Uact ua) then show ?thesis using assms vl' by (cases ua) (auto simp: u_defs cong: friendsOfUID_cong) next
    case (COMact ca)
      then show ?thesis using assms vl' nφ proof (cases ca)
        case (comReceiveCreateOFriend aid sp uid uid')
          then show ?thesis using COMact assms nφ by (auto simp: friendsOfUID_step_not_UID consume_def)
      next
        case (comReceiveDeleteOFriend aid sp uid uid')
          then show ?thesis using COMact assms nφ by (auto simp: friendsOfUID_step_not_UID consume_def)
      qed (auto simp: com_defs cong: friendsOfUID_cong)
  qed auto
qed



lemma unwind_cont_Δ0: "unwind_cont Δ0 {Δ0}"
proof(rule, simp)
  fix s s1 :: state and vl vl1 :: "value list"
  assume rsT: "reachNT s" and rs1: "reach s1" and Δ0: "Δ0 s vl s1 vl1"
  then have rs: "reach s" and ss1: "eqButUID s s1" and BC: "BC vl vl1"
        and vVS1: "validValSeqFrom vl1 s1"
    using reachNT_reach unfolding Δ0_def by auto
  show "iaction Δ0 s vl s1 vl1 ∨
        ((vl = [] ⟶ vl1 = []) ∧ reaction Δ0 s vl s1 vl1)" (is "?iact ∨ (_ ∧ ?react)")
  proof-
    have ?react proof
      fix a :: act and ou :: out and s' :: state and vl'
      let ?trn = "Trans s a ou s'"
      assume step: "step s a = (ou, s')" and T: "¬ T ?trn" and c: "consume ?trn vl vl'"
      show "match Δ0 s s1 vl1 a ou s' vl' ∨ ignore Δ0 s s1 vl1 a ou s' vl'" (is "?match ∨ ?ignore")
      proof cases
        assume φ: "φ ?trn"
        with BC c have "?match" proof (cases rule: BC.cases)
          case (BC_FrVal vl'' vl1'' uid' aid uid st st')
            then show ?thesis proof (cases st')
              case True
                let ?a1 = "COMact (comReceiveCreateOFriend AID (serverPass s AID) UID uid')"
                let ?ou1 = "outOK"
                let ?s1' = "receiveCreateOFriend s1 AID (serverPass s AID) UID uid'"
                let ?trn1 = "Trans s1 ?a1 ?ou1 ?s1'"
                have c1: "consume ?trn1 vl1 vl1''" and "vl' = vl''" and "f ?trn = FrVal AID' uid st"
                  using φ c BC_FrVal True by (auto elim: φ.elims simp: consume_def)
                moreover then have a: "a = COMact (comReceiveCreateOFriend AID (serverPass s AID) UID uid)
                                     ∨ a = COMact (comReceiveDeleteOFriend AID (serverPass s AID) UID uid)"
                               and ou: "ou = outOK"
                               and IDs: "IDsOK s [] [] [(AID,[])] []"
                               and uid: "uid ∉ UIDs AID'"
                  using φ step rs by (auto elim!: φ.elims split: prod.splits simp: com_defs)
                moreover have step1: "step s1 ?a1 = (?ou1, ?s1')"
                  using IDs vVS1 BC_FrVal True ss1 by (auto simp: com_defs eqButUID_def friendsOfUID_def)
                moreover then have "validValSeqFrom vl1'' ?s1'"
                  using vVS1 rs1 c1 by (intro step_validValSeqFrom[OF step1]) auto
                moreover have "eqButUID s' ?s1'"
                  using ss1 recvOFriend_eqButUID[OF step rs a uid]
                  using recvOFriend_eqButUID[OF step1 rs1, of "serverPass s AID" uid'] BC_FrVal(4)
                  by (auto intro: eqButUID_sym eqButUID_trans)
                moreover have "γ ?trn = γ ?trn1" and "g ?trn = g ?trn1"
                  using BC_FrVal a ou uid by (auto simp: com_defs)
                ultimately show "?match"
                  using BC_FrVal by (intro matchI[of s1 ?a1 ?ou1 ?s1' vl1 vl1'']) (auto simp: Δ0_def)
            next
              case False
                let ?a1 = "COMact (comReceiveDeleteOFriend AID (serverPass s AID) UID uid')"
                let ?ou1 = "outOK"
                let ?s1' = "receiveDeleteOFriend s1 AID (serverPass s AID) UID uid'"
                let ?trn1 = "Trans s1 ?a1 ?ou1 ?s1'"
                have c1: "consume ?trn1 vl1 vl1''" and "vl' = vl''" and "f ?trn = FrVal AID' uid st"
                  using φ c BC_FrVal False by (auto elim: φ.elims simp: consume_def)
                moreover then have a: "a = COMact (comReceiveCreateOFriend AID (serverPass s AID) UID uid)
                                     ∨ a = COMact (comReceiveDeleteOFriend AID (serverPass s AID) UID uid)"
                               and ou: "ou = outOK"
                               and IDs: "IDsOK s [] [] [(AID,[])] []"
                               and uid: "uid ∉ UIDs AID'"
                  using φ step rs by (auto elim!: φ.elims split: prod.splits simp: com_defs)
                moreover have step1: "step s1 ?a1 = (?ou1, ?s1')"
                  using IDs vVS1 BC_FrVal False ss1 by (auto simp: com_defs eqButUID_def friendsOfUID_def)
                moreover then have "validValSeqFrom vl1'' ?s1'"
                  using vVS1 rs1 c1 by (intro step_validValSeqFrom[OF step1]) auto
                moreover have "eqButUID s' ?s1'"
                  using ss1 recvOFriend_eqButUID[OF step rs a uid]
                  using recvOFriend_eqButUID[OF step1 rs1, of "serverPass s AID" uid'] BC_FrVal(4)
                  by (auto intro: eqButUID_sym eqButUID_trans)
                moreover have "γ ?trn = γ ?trn1" and "g ?trn = g ?trn1"
                  using BC_FrVal a ou uid by (auto simp: com_defs)
                ultimately show "?match"
                  using BC_FrVal by (intro matchI[of s1 ?a1 ?ou1 ?s1' vl1 vl1'']) (auto simp: Δ0_def)
            qed
        qed (auto simp: consume_def)
        then show "?match ∨ ?ignore" ..
      next
        assume nφ: "¬φ ?trn"
        then have vl': "vl' = vl" using c by (auto simp: consume_def)
        obtain ou1 s1' where step1: "step s1 a = (ou1, s1')" by (cases "step s1 a")
        let ?trn1 = "Trans s1 a ou1 s1'"
        show "?match ∨ ?ignore"
        proof (cases "∀uID'. uID' ∉ UIDs AID' ⟶
                             a ≠ COMact (comReceiveCreateOFriend AID (serverPass s1 AID) UID uID') ∧
                             a ≠ COMact (comReceiveDeleteOFriend AID (serverPass s1 AID) UID uID')")
          case True
            then have nφ1: "¬φ ?trn1" using step1 by (auto elim!: φ.elims simp: com_defs)
            have "?match" using step1 unfolding vl' proof (intro matchI[of s1 a ou1 s1' vl1 vl1])
              show c1: "consume ?trn1 vl1 vl1" using nφ1 by (auto simp: consume_def)
              show "Δ0 s' vl s1' vl1" using BC unfolding Δ0_def proof (intro conjI)
                show "eqButUID s' s1'" using eqButUID_step[OF ss1 step step1 rs rs1] .
                show "validValSeqFrom vl1 s1'"
                  using c1 rs1 vVS1 by (intro step_validValSeqFrom[OF step1]) auto
              qed auto
              show "γ ?trn = γ ?trn1" using ss1 rs rs1 step step1 True nφ nφ1
                by (intro eqButUID_step_γ) auto
            next
              assume "γ ?trn"
              then have "ou = ou1" using nφ nφ1 by (intro eqButUID_step_γ_out[OF ss1 step step1]) auto
              then show "g ?trn = g ?trn1" by (cases a) auto
            qed auto
            then show "?match ∨ ?ignore" ..
        next
          case False
            with nφ have "?ignore"
              using UID_UIDs BC step ss1 vVS1 unfolding vl'
              by (intro ignoreI) (auto simp: Δ0_def split: prod.splits)
            then show "?match ∨ ?ignore" ..
        qed
      qed
    qed
    with BC show ?thesis by (cases rule: BC.cases) auto
  qed
qed



definition Gr where
"Gr =
 {
 (Δ0, {Δ0})
 }"


theorem secure: secure
apply (rule unwind_decomp_secure_graph[of Gr Δ0])
unfolding Gr_def
(* apply (simp, smt insert_subset order_refl) *)
using
istate_Δ0 unwind_cont_Δ0
unfolding Gr_def by (auto intro: unwind_cont_mono)


end

end