Theory Review_RAut_NCPC_PAut
theory Review_RAut_NCPC_PAut
imports "../Observation_Setup" Review_Value_Setup "Bounded_Deducibility_Security.Compositional_Reasoning"
begin
subsection ‹Confidentiality from users who are not the review's author, a PC member, or an author of the paper›
text ‹We verify the following property:
\ \\
A group of users UIDs learn nothing
about the various updates to the N'th review of a paper PID
(save for the inexistence of any updates) unless/until
\begin{itemize}
\item a user in UIDs is the review's author, or
\item a user in UIDs becomes a PC member in the paper's conference
having no conflict with that paper and the
conference moves to the discussion phase, or
\item a user in UIDs become a PC member in the paper's conference
or an author of the paper and the conference moves to the notification phase
\end{itemize}
›
type_synonym "value" = rcontent
fun f :: "(state,act,out) trans ⇒ value" where
"f (Trans _ (Uact (uReview cid uid p pid n rc)) _ _) = rc"
|
"f (Trans _ (UUact (uuReview cid uid p pid n rc)) _ _) = rc"
fun T :: "(state,act,out) trans ⇒ bool" where
"T (Trans _ _ ou s') =
(∃ uid ∈ UIDs.
isREVNth s' uid PID N
∨
(∃ cid. PID ∈∈ paperIDs s' cid ∧ isPC s' cid uid ∧ pref s' uid PID ≠ Conflict ∧ phase s' cid ≥ disPH)
∨
(∃ cid. PID ∈∈ paperIDs s' cid ∧ isPC s' cid uid ∧ phase s' cid ≥ notifPH)
∨
isAUT s' uid PID ∧ (∃ cid. PID ∈∈ paperIDs s' cid ∧ phase s' cid ≥ notifPH)
)"
declare T.simps [simp del]
definition B :: "value list ⇒ value list ⇒ bool" where
"B vl vl1 ≡ vl ≠ []"