Theory Post_Observation_Setup_RECEIVER

theory Post_Observation_Setup_RECEIVER
  imports "../Safety_Properties"
begin

subsection ‹Confidentiality for a secret receiver node›

text ‹We verify that a group of users of a given node ‹j›
can learn nothing about the updates to the content of a post
‹PID› located at a different node ‹i› beyond the
existence of an update unless ‹PID› is being shared between
the two nodes and one of the users is the admin at node ‹j› or becomes
a remote friend of ‹PID›'s owner, or ‹PID› is marked as public.
This is formulated as a BD Security
property and is proved by unwinding.

See \<^cite>‹"cosmedis-SandP2017"› for more details.
›

subsubsection‹Observation setup›

(* *)
type_synonym obs = "act * out"

(* The observers are an arbitrary, but fixed set of users *)
locale Fixed_UIDs = fixes UIDs :: "userID set"
(* The secret is PID received from AID:  *)
locale Fixed_PID = fixes PID :: "postID"
locale Fixed_AID = fixes AID :: "apiID"

locale ObservationSetup_RECEIVER = Fixed_UIDs + Fixed_PID + Fixed_AID
begin

(*  *)
fun γ :: "(state,act,out) trans ⇒ bool" where
"γ (Trans _ a _ _) ⟷
   (∃ uid. userOfA a = Some uid ∧ uid ∈ UIDs)
   ∨
   (∃ca. a = COMact ca)
   ∨
   (∃uid p. a = Sact (sSys uid p))"

(* Note: the passwords don't really have to be purged (since identity theft is not
considered in the first place); however, purging passwords looks more sane. *)

(* Purging the password in starting actions: *)
fun sPurge :: "sActt ⇒ sActt" where
"sPurge (sSys uid pwd) = sSys uid emptyPass"

(* Purging communicating actions: user-password information is removed, and post content for PID
  is removed from the only kind of action that may contain such info: comReceivePost.
  Note: server-password info is not purged --todo: discuss this.  *)
fun comPurge :: "comActt ⇒ comActt" where
 "comPurge (comSendServerReq uID p aID reqInfo) = comSendServerReq uID emptyPass aID reqInfo"
|"comPurge (comConnectClient uID p aID sp) = comConnectClient uID emptyPass aID sp"
(* *)
|"comPurge (comReceivePost aID sp pID pst uID vs) =
  (let pst' = (if aID = AID ∧ pID = PID then emptyPost else pst)
   in comReceivePost aID sp pID pst' uID vs)"
(* *)
|"comPurge (comSendPost uID p aID pID) = comSendPost uID emptyPass aID pID"
|"comPurge (comSendCreateOFriend uID p aID uID') = comSendCreateOFriend uID emptyPass aID uID'"
|"comPurge (comSendDeleteOFriend uID p aID uID') = comSendDeleteOFriend uID emptyPass aID uID'"
|"comPurge ca = ca"

(* Note: No output purge here -- only for the issuer. *)

fun g :: "(state,act,out)trans ⇒ obs" where
 "g (Trans _ (Sact sa) ou _) = (Sact (sPurge sa), ou)"
|"g (Trans _ (COMact ca) ou _) = (COMact (comPurge ca), ou)"
|"g (Trans _ a ou _) = (a,ou)"

lemma comPurge_simps:
  "comPurge ca = comSendServerReq uID p aID reqInfo ⟷ (∃p'. ca = comSendServerReq uID p' aID reqInfo ∧ p = emptyPass)"
  "comPurge ca = comReceiveClientReq aID reqInfo ⟷ ca = comReceiveClientReq aID reqInfo"
  "comPurge ca = comConnectClient uID p aID sp ⟷ (∃p'. ca = comConnectClient uID p' aID sp ∧ p = emptyPass)"
  "comPurge ca = comConnectServer aID sp ⟷ ca = comConnectServer aID sp"
  "comPurge ca = comReceivePost aID sp pID pst' uID v ⟷ (∃pst. ca = comReceivePost aID sp pID pst uID v ∧ pst' = (if pID = PID ∧ aID = AID then emptyPost else pst))"
  "comPurge ca = comSendPost uID p aID pID ⟷ (∃p'. ca = comSendPost uID p' aID pID ∧ p = emptyPass)"
  "comPurge ca = comSendCreateOFriend uID p aID uID' ⟷ (∃p'. ca = comSendCreateOFriend uID p' aID uID' ∧ p = emptyPass)"
  "comPurge ca = comReceiveCreateOFriend aID cp uID uID' ⟷ ca = comReceiveCreateOFriend aID cp uID uID'"
  "comPurge ca = comSendDeleteOFriend uID p aID uID' ⟷ (∃p'. ca = comSendDeleteOFriend uID p' aID uID' ∧ p = emptyPass)"
  "comPurge ca = comReceiveDeleteOFriend aID cp uID uID' ⟷ ca = comReceiveDeleteOFriend aID cp uID uID'"
by (cases ca; auto)+

lemma g_simps:
  "g (Trans s a ou s') = (COMact (comSendServerReq uID p aID reqInfo), ou')
⟷ (∃p'. a = COMact (comSendServerReq uID p' aID reqInfo) ∧ p = emptyPass ∧ ou = ou')"
  "g (Trans s a ou s') = (COMact (comReceiveClientReq aID reqInfo), ou')
⟷ a = COMact (comReceiveClientReq aID reqInfo) ∧ ou = ou'"
  "g (Trans s a ou s') = (COMact (comConnectClient uID p aID sp), ou')
⟷ (∃p'. a = COMact (comConnectClient uID p' aID sp) ∧ p = emptyPass ∧ ou = ou')"
  "g (Trans s a ou s') = (COMact (comConnectServer aID sp), ou')
⟷ a = COMact (comConnectServer aID sp) ∧ ou = ou'"
  "g (Trans s a ou s') = (COMact (comReceivePost aID sp pID pst' uID v), ou')
⟷ (∃pst. a = COMact (comReceivePost aID sp pID pst uID v) ∧ pst' = (if pID = PID ∧ aID = AID then emptyPost else pst) ∧ ou = ou')"
   "g (Trans s a ou s') = (COMact (comSendPost uID p aID nID), O_sendPost (aid, sp, pid, pst, own, v))
⟷ (∃p'. a = COMact (comSendPost uID p' aID nID) ∧ p = emptyPass ∧ ou = O_sendPost (aid, sp, pid, pst, own, v))"
  "g (Trans s a ou s') = (COMact (comSendCreateOFriend uID p aID uID'), ou')
⟷ (∃p'. a = (COMact (comSendCreateOFriend uID p' aID uID')) ∧ p = emptyPass ∧ ou = ou')"
  "g (Trans s a ou s') = (COMact (comReceiveCreateOFriend aID cp uID uID'), ou')
⟷ a = COMact (comReceiveCreateOFriend aID cp uID uID') ∧ ou = ou'"
  "g (Trans s a ou s') = (COMact (comSendDeleteOFriend uID p aID uID'), ou')
⟷ (∃p'. a = COMact (comSendDeleteOFriend uID p' aID uID') ∧ p = emptyPass ∧ ou = ou')"
  "g (Trans s a ou s') = (COMact (comReceiveDeleteOFriend aID cp uID uID'), ou')
⟷ a = COMact (comReceiveDeleteOFriend aID cp uID uID') ∧ ou = ou'"
by (cases a; auto simp: comPurge_simps ObservationSetup_RECEIVER.comPurge.simps)+

end

end