Theory Outer_Friend_Intro

theory Outer_Friend_Intro
  imports "../Safety_Properties"
begin

section ‹Remote (outer) friendship status confidentiality›

text ‹
We verify the following property, which is specific to CosMeDis,
in that it does not have a CoSMed counterpart:
Given a coalition consisting of groups of users ‹UIDs j› from multiple nodes ‹j›
and a user ‹UID› at some node ‹i› not in these groups,

the coalition may learn about the ∗‹occurrence› of remote friendship actions of ‹UID›
(because network traffic is assumed to be observable),

but they learn nothing about the ∗‹content› (who was added or deleted as a friend)
of remote friendship actions between ‹UID› and remote users who are not in the coalition

beyond what everybody knows, namely that, with respect to each other user ‹uid'›,
those actions form an alternating sequence of friending and unfriending,

unless a user in ‹UIDs i› becomes a local friend of ‹UID›.

\ \\
Similarly to the other properties, this property is proved using the
system compositionality and transport theorems for BD security.

Note that, unlike inner friendship, outer friendship is not necessarily symmetric.
It is always established from a user of a server to a user of a client, the former giving
the latter unilateral access to his friend-only posts. These unilateral friendship permissions
are stored on the client.

When proving the single-node BD security properties, the bound refers to
outer friendship-status changes issued by the user ‹UID›
concerning friending or unfriending some user ‹UID'› located at a node ‹j›
different from ‹i›. Such changes occur as communicating actions between
the ``secret issuer'' node ‹i› and the ``secret receiver'' nodes ‹j›.
›

end