Theory Friend
theory Friend
imports "../Observation_Setup" Friend_Value_Setup
begin
subsection ‹Declassification bound›
fun T :: "(state,act,out) trans ⇒ bool"
where "T (Trans _ _ _ _) = False"
text ‹The bound follows the same ``while-or-last-before'' scheme as the bound for post
confidentiality (Section~\ref{sec:post-bound}), alternating between open (‹BO›) and
closed (‹BC›) phases.
The access window is initially open, because the two users are known not to exist when the system
is initialized, so there cannot be friendship between them.
The bound also incorporates the static knowledge that the friendship status alternates between
‹False› and ‹True›.›
fun alternatingFriends :: "value list ⇒ bool ⇒ bool" where
"alternatingFriends [] _ = True"
| "alternatingFriends (FrVal st # vl) st' ⟷ st' = (¬st) ∧ alternatingFriends vl st"
| "alternatingFriends (OVal _ # vl) st = alternatingFriends vl st"
inductive BO :: "value list ⇒ value list ⇒ bool"
and BC :: "value list ⇒ value list ⇒ bool"
where
BO_FrVal[simp,intro!]:
"BO (map FrVal fs) (map FrVal fs)"
|BO_BC[intro]:
"BC vl vl1 ⟹
BO (map FrVal fs @ OVal False # vl) (map FrVal fs @ OVal False # vl1)"
|BC_FrVal[simp,intro!]:
"BC (map FrVal fs) (map FrVal fs1)"
|BC_BO[intro]:
"BO vl vl1 ⟹ (fs = [] ⟷ fs1 = []) ⟹ (fs ≠ [] ⟹ last fs = last fs1) ⟹
BC (map FrVal fs @ OVal True # vl)
(map FrVal fs1 @ OVal True # vl1)"
definition "B vl vl1 ≡ BO vl vl1 ∧ alternatingFriends vl1 False"
lemma BO_Nil_Nil: "BO vl vl1 ⟹ vl = [] ⟹ vl1 = []"
by (cases rule: BO.cases) auto
unbundle no relcomp_syntax