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