Theory Trivial_Security

section ‹Trivial security properties›

text ‹Here we formalize some cases when BD Security holds trivially. ›

theory Trivial_Security
imports Bounded_Deducibility_Security.Abstract_BD_Security
begin

definition B_id :: "'value ⇒ 'value ⇒ bool"
where "B_id vl vl1 ≡ (vl1 = vl)"

context Abstract_BD_Security
begin

(* ... when the bound is as fine-grained as equality: *)
lemma B_id_secure:
assumes "⋀tr vl vl1. B (V tr) vl1 ⟹ validSystemTrace tr ⟹ B_id (V tr) vl1"
shows "secure"
using assms unfolding secure_def B_id_def by auto

(* ... when the observation function is constant: *)
lemma O_const_secure:
assumes "⋀tr. validSystemTrace tr ⟹ O tr = ol"
and "⋀tr vl vl1. B (V tr) vl1 ⟹ validSystemTrace tr ⟹ (∃tr1. validSystemTrace tr1 ∧ V tr1 = vl1)"
shows "secure"
unfolding secure_def proof (intro allI impI, elim conjE)
  fix tr vl vl1
  assume "B vl vl1" and "validSystemTrace tr" and "V tr = vl"
  moreover then obtain tr1 where "validSystemTrace tr1" "V tr1 = vl1" using assms(2) by auto
  ultimately show "∃tr1. validSystemTrace tr1 ∧ O tr1 = O tr ∧ V tr1 = vl1" using assms(1) by auto
qed

definition OV_compatible :: "'observations ⇒ 'values ⇒ bool" where
  "OV_compatible obs vl ≡ (∃tr. O tr = obs ∧ V tr = vl)"

definition V_compatible :: "'values ⇒ 'values ⇒ bool" where
  "V_compatible vl vl1 ≡ (∀obs. OV_compatible obs vl ⟶ OV_compatible obs vl1)"

definition validObs :: "'observations ⇒ bool" where
  "validObs obs ≡ (∃tr. validSystemTrace tr ∧ O tr = obs)"

definition validVal :: "'values ⇒ bool" where
  "validVal vl ≡ (∃tr. validSystemTrace tr ∧ V tr = vl)"

lemma OV_total_secure:
assumes OV: "⋀obs vl. validObs obs ⟹ validVal vl ⟹ OV_compatible obs vl
                  ⟹ (∃tr. validSystemTrace tr ∧ O tr = obs ∧ V tr = vl)"
and BV: "⋀vl vl1. B vl vl1 ⟹ validVal vl ⟹ V_compatible vl vl1 ∧ validVal vl1"
shows "secure"
unfolding secure_def proof (intro allI impI, elim conjE)
  fix tr vl vl1
  assume tr: "validSystemTrace tr" and B: "B vl vl1" and vl: "V tr = vl"
  then have "validObs (O tr)" and "validVal (V tr)" and "OV_compatible (O tr) (V tr)"
    unfolding validObs_def validVal_def OV_compatible_def by blast+
  moreover then have "validVal vl1" and "OV_compatible (O tr) vl1"
    using B BV unfolding V_compatible_def vl by blast+
  ultimately show "∃tr1. validSystemTrace tr1 ∧ O tr1 = O tr ∧ V tr1 = vl1"
    using OV by blast
qed

lemma unconstrained_secure:
assumes "⋀tr. validSystemTrace tr"
and BV: "⋀vl vl1. B vl vl1 ⟹ validVal vl ⟹ V_compatible vl vl1 ∧ validVal vl1"
shows "secure"
using assms by (intro OV_total_secure) (auto simp: OV_compatible_def)

end

end