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