Theory Independent_Post_Observation_Setup_ISSUER

(* Strengthened observation setup, customized for post confidentiality *)
theory Independent_Post_Observation_Setup_ISSUER
  imports
    "../../Safety_Properties"
    "../Post_Observation_Setup_ISSUER"
begin

subsection ‹Variation with multiple independent secret posts›

text ‹This section formalizes the lifting of the confidentiality of one
given (arbitrary but fixed) post to the confidentiality of two posts of
arbitrary nodes of the network, as described in \<^cite>‹‹Appendix E› in "cosmedis-SandP2017"›.
›

subsubsection‹Issuer observation setup›

locale Strong_ObservationSetup_ISSUER = Fixed_UIDs + Fixed_PID
begin

(*  *)
fun γ :: "(state,act,out) trans ⇒ bool" where
"γ (Trans _ a _ _) ⟷
   (∃ uid. userOfA a = Some uid ∧ uid ∈ UIDs)
   ∨
   ― ‹Communication actions are considered to be observable in order to make the security
      properties compositional›
   (∃ca. a = COMact ca)
   ∨
   ― ‹The following actions are added to strengthen the observers in order to show that all
      posts ∗‹other than ‹PID›› are completely independent of ‹PID›;  the confidentiality of ‹PID›
      is protected even if the observers can see all updates to other posts (and actions
      contributing to the declassification triggers of those posts).›
   (∃uid p pid pst. a = Uact (uPost uid p pid pst) ∧ pid ≠ PID)
   ∨
   (∃uid p. a = Sact (sSys uid p))
   ∨
   (∃uid p uid' p'. a = Cact (cUser uid p uid' p'))
   ∨
   (∃uid p pid. a = Cact (cPost uid p pid))
   ∨
   (∃uid p uid'. a = Cact (cFriend uid p uid'))
   ∨
   (∃uid p uid'. a = Dact (dFriend uid p uid'))
   ∨
   (∃uid p pid v. a = Uact (uVisPost uid p pid v))"

(* 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 text
  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 text information for PID
  is removed from the only kind of output that may contain such info: outAIDPPIDNUID.
  (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: Strong_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