Theory Friend_Intro

theory Friend_Intro
  imports "../Safety_Properties"
begin

section ‹Friendship status confidentiality›

text ‹\label{sec:friend}
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 changes in the status
of friendship between ‹UID1› and ‹UID2›

beyond what everybody knows, namely that
  ▪ there is no friendship between them before those users have been created, and
  ▪ the updates form an alternating sequence of friending and unfriending,

and beyond those updates performed while or last before
a user in the group ‹UIDs i› is friends with ‹UID1› or ‹UID2›.

\ \\
The approach to proving this is similar to that for post confidentiality (explained
in the introduction of the post confidentiality section~\ref{sec:post}), but conceptually simpler
since here secret information is not communicated between different nodes (so we
don't need to distinguish between an issuer node and the other, receiver nodes).

Moreover, here we do not consider static versions of the bounds, but go directly for
the dynamic ones. Also, we prove directly the BD security for a network of ‹n› nodes,
omitting the case of two nodes.

Note that, unlike for post confidentiality, here remote friendship plays
no role in the statement of the property. This is because, in CoSMeDis, the listing
of a user's friends is only available to local (same-node) friends of that user,
and not to the remote (outer) friends.
›

end