Theory Post_Intro

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

section ‹Post confidentiality›

text ‹We prove the following property:

\ \\
Given a group of users ‹UIDs› and a post ‹PID›,

that group cannot learn anything about the different versions of the post ‹PID›
(the initial created version and the later ones obtained by updating the post)

beyond the updates performed while or last before one of the following holds:
\begin{itemize}
\item either a user in ‹UIDs› is the post's owner, a friend of the owner, or the admin
\item or ‹UIDs› has at least one registered user and the post is marked as ``public''.
\end{itemize}
›


end