Theory Outer_Friend_Receiver_Observation_Setup

theory Outer_Friend_Receiver_Observation_Setup
  imports "../Outer_Friend"
begin

subsection ‹Receiver nodes›

subsubsection ‹Observation setup›

(* We now consider one arbitrary, but fixed network node receiving secrets *)
locale OuterFriendReceiver = OuterFriend +
fixes AID' :: apiID ― ‹The ID of this (arbitrary, but fixed) receiver node›
begin

(*  *)
fun γ :: "(state,act,out) trans ⇒ bool" where
"γ (Trans _ a ou _) ⟷ (∃ uid. userOfA a = Some uid ∧ uid ∈ UIDs AID') ∨
                        (∃ca. a = COMact ca ∧ ou ≠ outErr)"

(* 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: password information is removed, the user IDs of friends
   added or deleted by UID are removed, and the information whether UID added or deleted
   a friend is removed *)
fun comPurge :: "comActt ⇒ comActt" where
 "comPurge (comSendServerReq uID p aID reqInfo) = comSendServerReq uID emptyPass aID reqInfo"
|"comPurge (comReceiveClientReq aID reqInfo) = comReceiveClientReq aID reqInfo"
|"comPurge (comConnectClient uID p aID sp) = comConnectClient uID emptyPass aID sp"
|"comPurge (comConnectServer aID sp) = comConnectServer aID sp"
|"comPurge (comReceivePost aID sp nID nt uID v) = comReceivePost aID sp nID nt uID v"
|"comPurge (comSendPost uID p aID nID) = comSendPost uID emptyPass aID nID"
|"comPurge (comSendCreateOFriend uID p aID uID') = comSendCreateOFriend uID emptyPass aID uID'"
    (*(if aID = AID ∧ uID = UID ∧ uID' ∉ UIDs AID'
     then comSendCreateOFriend uID emptyPass aID emptyUserID
     else comSendCreateOFriend uID emptyPass aID uID')"*)
|"comPurge (comReceiveCreateOFriend aID cp uID uID') =
    (if aID = AID ∧ uID = UID ∧ uID' ∉ UIDs AID'
     then comReceiveCreateOFriend aID cp uID emptyUserID
     else comReceiveCreateOFriend aID cp uID uID')"
|"comPurge (comSendDeleteOFriend uID p aID uID') = comSendDeleteOFriend uID emptyPass aID uID'"
    (*(if aID = AID ∧ uID = UID ∧ uID' ∉ UIDs AID'
     then comSendCreateOFriend uID emptyPass aID emptyUserID
     else comSendDeleteOFriend uID emptyPass aID uID')"*)
|"comPurge (comReceiveDeleteOFriend aID cp uID uID') =
    (if aID = AID ∧ uID = UID ∧ uID' ∉ UIDs AID'
     then comReceiveCreateOFriend aID cp uID emptyUserID
     else comReceiveDeleteOFriend aID cp uID uID')"

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'
⟷ (∃uid''. (ca = comReceiveCreateOFriend aID cp uID uid'' ∨ ca = comReceiveDeleteOFriend aID cp uID uid'') ∧ aID = AID ∧ uID = UID ∧ uid'' ∉ UIDs AID' ∧ uID' = emptyUserID)
    ∨ (ca = comReceiveCreateOFriend aID cp uID uID' ∧ ¬(aID = AID ∧ uID = UID ∧ uID' ∉ UIDs AID'))"
  "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' ∧ ¬(aID = AID ∧ uID = UID ∧ uID' ∉ UIDs AID')"
by (cases ca; auto)+

(* Purging outputs: password information is removed, and the user IDs of friends added or deleted
   by UID are removed from the only kind of output that may contain such info: outAIDPUIDUID   *)
(*n outPurge :: "out ⇒ out" where
 "outPurge (outAIDPUIDUID (aID, sp, uID, uID')) =
  (if aID = AID ∧ uID = UID ∧ uID' ∉ UIDs AID'
   then outAIDPUIDUID (aID, sp, uID, emptyUserID)
   else outAIDPUIDUID (aID, sp, uID, uID'))"
|"outPurge ou = ou"

lemma outPurge_outErr[simp]: "outPurge ou = outErr ⟷ ou = outErr"
by (cases ou) auto*)

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 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 nID nt uID v), ou')
⟷ a = COMact (comReceivePost aID sp nID nt uID v) ∧ ou = ou'"
  "g (Trans s a ou s') = (COMact (comSendPost uID p aID nID), ou')
⟷ (∃p'. a = COMact (comSendPost uID p' aID nID) ∧ p = emptyPass ∧ ou = ou')"
  "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')
⟷ (((∃uid''. (a = COMact (comReceiveCreateOFriend aID cp uID uid'') ∨ a = COMact (comReceiveDeleteOFriend aID cp uID uid'')) ∧ aID = AID ∧ uID = UID ∧ uid'' ∉ UIDs AID' ∧ uID' = emptyUserID)
    ∨ (a = COMact (comReceiveCreateOFriend aID cp uID uID') ∧ ¬(aID = AID ∧ uID = UID ∧ uID' ∉ UIDs AID')))
    ∧ 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') ∧ ¬(aID = AID ∧ uID = UID ∧ uID' ∉ UIDs AID') ∧ ou = ou'"
by (cases a; auto simp: comPurge_simps)+

end

(*
locale FriendNetworkObservationSetup =
fixes UIDs :: "apiID ⇒ userID set"
and UID :: "userID"
begin

(*  *)
abbreviation γ :: "apiID ⇒ (state,act,out) trans ⇒ bool" where
"γ aid trn ≡ FriendObservationSetup.γ (UIDs aid) trn"

abbreviation g :: "apiID ⇒ (state,act,out)trans ⇒ obs" where
"g aid trn ≡ FriendObservationSetup.g UID trn"

end
*)

end