Theory Friend_Request_Intro

theory Friend_Request_Intro
  imports "../Safety_Properties" "../Observation_Setup"
begin

section ‹Friendship request confidentiality›

text ‹We prove the following property:

\ \\
Given a group of users ‹UIDs› and given two users ‹UID1› and ‹UID2› not in that group,

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

beyond what everybody knows, namely that
  ▪ there is no friendship between ‹UID1› and ‹UID2› before those users have been created, and
  ▪ friendship status updates form an alternating sequence of friending and unfriending,
    every successful friend creation is preceded by at least one and at most two requests,

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

end