Theory Abstract_BD_Security

(*<*)
theory Abstract_BD_Security
  imports Main
begin
(*>*)

section ‹BD Security›

subsection ‹Abstract definition›

no_notation relcomp (infixr "O" 75)

locale Abstract_BD_Security =
 fixes
  validSystemTrace :: "'traces ⇒ bool"
and ― ‹secret values:›
  V :: "'traces ⇒ 'values"
and ― ‹observations:›
  O :: "'traces ⇒ 'observations"
and ― ‹declassification bound:›
  B :: "'values ⇒ 'values ⇒ bool"
and ― ‹declassification trigger:›
  TT :: "'traces ⇒ bool"
begin

text ‹A system is considered to be secure if, for all traces that satisfy a given condition
(later instantiated to be the absence of transitions satisfying a declassification trigger
condition, releasing the secret information), the secret value can be replaced by another
secret value within the declassification bound, without changing the observation.
Hence, an observer cannot distinguish secrets related by the declassification bound,
unless and until release of the secret information is allowed by the declassification trigger.›

(* BD security: *)
definition secure :: bool where
"secure ≡
 ∀ tr vl vl1.
   validSystemTrace tr ∧ TT tr ∧ B vl vl1 ∧ V tr = vl ⟶
   (∃ tr1. validSystemTrace tr1 ∧ O tr1 = O tr ∧ V tr1 = vl1)"

lemma secureE:
assumes "secure" and "validSystemTrace tr" and "TT tr" and "B (V tr) vl1"
obtains tr1 where "validSystemTrace tr1" "O tr1 = O tr" "V tr1 = vl1"
using assms unfolding secure_def by auto

end (* context BD_Security *)

(*<*)
end
(*>*)