Theory Post_Observation_Setup_ISSUER

(* Strengthened observation setup, customized for post confidentiality *)
theory Post_Observation_Setup_ISSUER
  imports Post_Intro
begin

subsection ‹Confidentiality for a secret issuer node›


text ‹\label{sec:post-issuer}
We verify that a group of users of a given node ‹i›
can learn nothing about the updates to the content of a post
‹PID› located at that node beyond the existence of an update
unless one of them is the admin or the owner of ‹PID›,
or becomes friends with the 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: *)
locale Fixed_PID = fixes PID :: "postID"

locale ObservationSetup_ISSUER = Fixed_UIDs + Fixed_PID
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.
  Note: comReceivePost is not affected by the purging, in that post content
  is not removed; this only happens on the receiving end.
  (Also, nothing to purge in comSendPost either -- the output will be purged here, since
   only the output contains an actual post.)


  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 (comConnectServer aID sp) = comConnectServer aID sp"
|"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"

(* Purging outputs: post content for PID
  is removed from the post sending outputs
  (Again, server-password info is not purged.)   *)
fun outPurge :: "out ⇒ out" where
 "outPurge (O_sendPost (aID, sp, pID, pst, uID, vs)) =
  (let pst' = (if pID = PID then emptyPost else pst)
   in O_sendPost (aID, sp, pID, pst', uID, vs))"
|"outPurge ou = ou"

fun g :: "(state,act,out)trans ⇒ obs" where
 "g (Trans _ (Sact sa) ou _) = (Sact (sPurge sa), outPurge ou)"
|"g (Trans _ (COMact ca) ou _) = (COMact (comPurge ca), outPurge 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 nID nt uID v ⟷ ca = comReceivePost aID sp nID nt uID v"
  "comPurge ca = comSendPost uID p aID nID ⟷ (∃p'. ca = comSendPost uID p' aID nID ∧ 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 outPurge_simps[simp]:
  "outPurge ou = outErr ⟷ ou = outErr"
  "outPurge ou = outOK ⟷ ou = outOK"
  "outPurge ou = O_sendServerReq ossr ⟷ ou = O_sendServerReq ossr"
  "outPurge ou = O_connectClient occ ⟷ ou = O_connectClient occ"
  "outPurge ou = O_sendPost (aid, sp, pid, pst', uid, vs) ⟷ (∃pst.
     ou = O_sendPost (aid, sp, pid, pst, uid, vs) ∧
     pst' = (if pid = PID then emptyPost else pst))"
  "outPurge ou = O_sendCreateOFriend oscf ⟷ ou = O_sendCreateOFriend oscf"
  "outPurge ou = O_sendDeleteOFriend osdf ⟷ ou = O_sendDeleteOFriend osdf"
by (cases ou; auto simp: ObservationSetup_ISSUER.outPurge.simps)+


lemma g_simps:
  "g (Trans s a ou s') = (COMact (comSendServerReq uID p aID reqInfo), O_sendServerReq ossr)
⟷ (∃p'. a = COMact (comSendServerReq uID p' aID reqInfo) ∧ p = emptyPass ∧ ou = O_sendServerReq ossr)"
  "g (Trans s a ou s') = (COMact (comReceiveClientReq aID reqInfo), outOK)
⟷ a = COMact (comReceiveClientReq aID reqInfo) ∧ ou = outOK"
  "g (Trans s a ou s') = (COMact (comConnectClient uID p aID sp), O_connectClient occ)
⟷ (∃p'. a = COMact (comConnectClient uID p' aID sp) ∧ p = emptyPass ∧ ou = O_connectClient occ)"
  "g (Trans s a ou s') = (COMact (comConnectServer aID sp), outOK)
⟷ a = COMact (comConnectServer aID sp) ∧ ou = outOK"
  "g (Trans s a ou s') = (COMact (comReceivePost aID sp nID nt uID v), outOK)
⟷ a = COMact (comReceivePost aID sp nID nt uID v) ∧ ou = outOK"
  "g (Trans s a ou s') = (COMact (comSendPost uID p aID nID), O_sendPost (aid, sp, pid, pst', uid, vs))
⟷ (∃pst p'. a = COMact (comSendPost uID p' aID nID) ∧ p = emptyPass ∧ ou = O_sendPost (aid, sp, pid, pst, uid, vs) ∧ pst' = (if pid = PID then emptyPost else pst))"
  "g (Trans s a ou s') = (COMact (comSendCreateOFriend uID p aID uID'), O_sendCreateOFriend (aid, sp, uid, uid'))
⟷ (∃p'. a = (COMact (comSendCreateOFriend uID p' aID uID')) ∧ p = emptyPass ∧ ou = O_sendCreateOFriend (aid, sp, uid, uid'))"
  "g (Trans s a ou s') = (COMact (comReceiveCreateOFriend aID cp uID uID'), outOK)
⟷ a = COMact (comReceiveCreateOFriend aID cp uID uID') ∧ ou = outOK"
  "g (Trans s a ou s') = (COMact (comSendDeleteOFriend uID p aID uID'), O_sendDeleteOFriend (aid, sp, uid, uid'))
⟷ (∃p'. a = COMact (comSendDeleteOFriend uID p' aID uID') ∧ p = emptyPass ∧ ou = O_sendDeleteOFriend (aid, sp, uid, uid'))"
  "g (Trans s a ou s') = (COMact (comReceiveDeleteOFriend aID cp uID uID'), outOK)
⟷ a = COMact (comReceiveDeleteOFriend aID cp uID uID') ∧ ou = outOK"
by (cases a; auto simp: comPurge_simps)+

end

end