Theory Friend_Request_Intro

theory Friend_Request_Intro
  imports
    "../Friend_Confidentiality/Friend_Openness"
    "../Friend_Confidentiality/Friend_State_Indistinguishability"
begin

section ‹Friendship request confidentiality›

text ‹
We verify the following property:

\ \\
Given a coalition consisting of groups of users ‹UIDs j› from multiple nodes ‹j›
and given two users ‹UID1› and ‹UID2› at some node ‹i› who are not in these groups,

the coalition cannot learn anything about the the friendship requests issued between
‹UID1› and ‹UID2›

beyond what everybody knows, namely that
  ▪ every successful friend creation is preceded by at least one and at most two requests, and
  ▪ friendship status updates form an alternating sequence of friending and unfriending,

and beyond the existence of requests issued while or last before
a user in the group ‹UIDs i› is a local friend of ‹UID1› or ‹UID2›.

\ \\
The approach here is similar to that for friendship status confidentiality
(explained in the introduction of Section~\ref{sec:friend}).
Like in the case of friendship status, here secret information is not communicated
between different nodes (so again we don't need to distinguish between an issuer node
and the other, receiver nodes).
›

end