Theory Outer_Friend_Issuer_Observation_Setup

theory Outer_Friend_Issuer_Observation_Setup
  imports "../Outer_Friend"
begin

subsection ‹Issuer node›

subsubsection ‹Observation setup›

text ‹We now consider the network node ‹AID›, at which the user ‹UID› is registered, whose remote
   friends are to be kept confidential. ›
locale OuterFriendIssuer = OuterFriend
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)"

text ‹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') =
    (if uID = UID ∧ uID' ∉ UIDs aID
     then comSendCreateOFriend uID emptyPass aID emptyUserID
     else comSendCreateOFriend uID emptyPass aID uID')"
|"comPurge (comReceiveCreateOFriend aID cp uID uID') = comReceiveCreateOFriend aID cp uID uID'"
|"comPurge (comSendDeleteOFriend uID p aID uID') =
    (if uID = UID ∧ uID' ∉ UIDs aID
     then comSendCreateOFriend uID emptyPass aID emptyUserID
     else comSendDeleteOFriend uID emptyPass aID uID')"
|"comPurge (comReceiveDeleteOFriend aID cp uID uID') = 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' uid''. (ca = comSendCreateOFriend uID p' aID uid'' ∨ ca = comSendDeleteOFriend uID p' aID uid'') ∧ uID = UID ∧ uid'' ∉ UIDs aID ∧ uID' = emptyUserID ∧ p = emptyPass)
    ∨ (∃p'. ca = comSendCreateOFriend uID p' aID uID' ∧ ¬(uID = UID ∧ uID' ∉ UIDs aID) ∧ 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' ∧ ¬(uID = UID ∧ uID' ∉ UIDs aID) ∧ p = emptyPass)"
  "comPurge ca = comReceiveDeleteOFriend aID cp uID uID' ⟷ ca = comReceiveDeleteOFriend aID cp uID uID'"
by (cases ca; auto)+

text ‹Purging outputs: the user IDs of friends added or deleted
   by ‹UID› are removed from outer friend creation and deletion outputs.›
fun outPurge :: "out ⇒ out" where
 "outPurge (O_sendCreateOFriend (aID, sp, uID, uID')) =
  (if uID = UID ∧ uID' ∉ UIDs aID
   then O_sendCreateOFriend (aID, sp, uID, emptyUserID)
   else O_sendCreateOFriend (aID, sp, uID, uID'))"
|"outPurge (O_sendDeleteOFriend (aID, sp, uID, uID')) =
  (if uID = UID ∧ uID' ∉ UIDs aID
   then O_sendCreateOFriend (aID, sp, uID, emptyUserID)
   else O_sendDeleteOFriend (aID, sp, uID, uID'))"
|"outPurge ou = ou"

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 osn ⟷ ou = O_sendPost osn"
  "outPurge ou = O_sendCreateOFriend (aID, sp, uID, uID')
 ⟷ (∃uid''. (ou = O_sendCreateOFriend (aID, sp, uID, uid'') ∨ ou = O_sendDeleteOFriend (aID, sp, uID, uid'')) ∧ uID = UID ∧ uid'' ∉ UIDs aID ∧ uID' = emptyUserID)
     ∨ (ou = O_sendCreateOFriend (aID, sp, uID, uID') ∧ ¬(uID = UID ∧ uID' ∉ UIDs aID))"
  "outPurge ou = O_sendDeleteOFriend (aID, sp, uID, uID')
 ⟷ (ou = O_sendDeleteOFriend (aID, sp, uID, uID') ∧ ¬(uID = UID ∧ uID' ∉ UIDs aID))"
by (cases ou; cases "uID = UID"; auto)+

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

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 osn)
⟷ (∃p'. a = COMact (comSendPost uID p' aID nID) ∧ p = emptyPass ∧ ou = O_sendPost osn)"
  "g (Trans s a ou s') = (COMact (comSendCreateOFriend uID p aID uID'), O_sendCreateOFriend (aid, sp, uid, uid'))
⟷ ((∃p' uid''. (a = COMact (comSendCreateOFriend uID p' aID uid'') ∨ a = COMact (comSendDeleteOFriend uID p' aID uid'')) ∧ uID = UID ∧ uid'' ∉ UIDs aID ∧ uID' = emptyUserID ∧ p = emptyPass)
    ∨ (∃p'. a = COMact (comSendCreateOFriend uID p' aID uID') ∧ ¬(uID = UID ∧ uID' ∉ UIDs aID) ∧ p = emptyPass))
    ∧ ((∃uid''. (ou = O_sendCreateOFriend (aid, sp, uid, uid'') ∨ ou = O_sendDeleteOFriend (aid, sp, uid, uid'')) ∧ uid = UID ∧ uid'' ∉ UIDs aid ∧ uid' = emptyUserID)
     ∨ (ou = O_sendCreateOFriend (aid, sp, uid, uid') ∧ ¬(uid = UID ∧ uid' ∉ UIDs aid)))"
  "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') ∧ ¬(uID = UID ∧ uID' ∉ UIDs aID) ∧ p = emptyPass)
    ∧ (ou = O_sendDeleteOFriend (aid, sp, uid, uid') ∧ ¬(uid = UID ∧ uid' ∉ UIDs aid))"
  "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