Theory Post
theory Post
imports "../Observation_Setup" Post_Value_Setup
begin
subsection ‹Declassification bound›
fun T :: "(state,act,out) trans ⇒ bool" where "T _ = False"
text ‹\label{sec:post-bound}
The bound may dynamically change from closed (‹B›) to open (‹BO›) access to the
confidential information (or vice versa) when the openness predicate changes value.
The bound essentially relates arbitrary value sequences in the closed phase (i.e.~observers
learn nothing about the updates during that phase) and identical value sequences in the open phase
(i.e.~observers may learn everything about the updates during that phase);
when transitioning from a closed to an open access window (‹B_BO› below),
the last update in the closed phase, i.e.~the current version of the post,
is also declassified in addition to subsequent updates.
This formalizes the ``while-or-last-before'' scheme in the informal description of the
confidentiality property.
Moreover, the empty value sequence is treated specially in order to capture harmless cases
where the observers may deduce that no secret updates have occurred,
e.g.~if the system has not been initialized yet.
See \<^cite>‹‹Section 3.4› in "cosmed-jar2018"› for a detailed discussion of the bound.›
inductive B :: "value list ⇒ value list ⇒ bool"
and BO :: "value list ⇒ value list ⇒ bool"
where
B_TVal[simp,intro!]:
"(pstl = [] ⟶ pstl1 = []) ⟹ B (map TVal pstl) (map TVal pstl1)"
|B_BO[intro]:
"BO vl vl1 ⟹ (pstl = [] ⟷ pstl1 = []) ⟹ (pstl ≠ [] ⟹ last pstl = last pstl1) ⟹
B (map TVal pstl @ OVal True # vl)
(map TVal pstl1 @ OVal True # vl1)"
|BO_TVal[simp,intro!]:
"BO (map TVal pstl) (map TVal pstl)"
|BO_B[intro]:
"B vl vl1 ⟹
BO (map TVal pstl @ OVal False # vl) (map TVal pstl @ OVal False # vl1)"
lemma B_not_Nil: "B vl vl1 ⟹ vl = [] ⟹ vl1 = []"
by(auto elim: B.cases)
lemma B_OVal_True:
assumes "B (OVal True # vl') vl1"
shows "∃ vl1'. BO vl' vl1' ∧ vl1 = OVal True # vl1'"
using assms apply(auto elim!: B.cases)
by (metis append_self_conv2 hd_append list.map_disc_iff list.map_sel(1) list.sel(1)
list.sel(3) value.distinct(1))+
no_notation relcomp (infixr "O" 75)