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