Theory Friend_Intro

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

section ‹Friendship status 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 changes in the status
of friendship 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
  ▪ the updates form an alternating sequence of friending and unfriending,

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


end