Theory Relative_Security_fin
section ‹Finitary Relative Security›
text ‹ This theory formalizes the finitary version of relative security,
more precisely the notion expressed in terms of finite traces. ›
theory Relative_Security_fin
imports "Preliminaries/Transition_System"
begin
declare Let_def[simp]
no_notation relcomp (infixr "O" 75)
no_notation relcompp (infixr "OO" 75)
subsection ‹Finite-trace versions of leakage models and attacker models ›
locale Leakage_Mod_fin = System_Mod istate validTrans final
for istate :: "'state ⇒ bool" and validTrans :: "'state × 'state ⇒ bool" and final :: "'state ⇒ bool"
+
fixes leakVia :: "'state list ⇒ 'state list ⇒ 'leak ⇒ bool"
locale Attacker_Mod_fin = System_Mod istate validTrans final
for istate :: "'state ⇒ bool" and validTrans :: "'state × 'state ⇒ bool" and final :: "'state ⇒ bool"
+
fixes S :: "'state list ⇒ 'secret list"
and A :: "'state trace ⇒ 'act list"
and O :: "'state trace ⇒ 'obs list"
begin
fun leakVia :: "'state list ⇒ 'state list ⇒ 'secret list × 'secret list ⇒ bool"
where
"leakVia tr tr' (sl,sl') = (S tr = sl ∧ S tr' = sl' ∧ A tr = A tr' ∧ O tr ≠ O tr')"
lemmas leakVia_def = leakVia.simps
end
sublocale Attacker_Mod_fin < Leakage_Mod_fin
where leakVia = leakVia
by standard
subsection ‹Locales for increasingly concrete notions of finitary relative security ›
locale Relative_Security''_fin =
Van: Leakage_Mod_fin istateV validTransV finalV leakViaV
+
Opt: Leakage_Mod_fin istateO validTransO finalO leakViaO
for validTransV :: "'stateV × 'stateV ⇒ bool"
and istateV :: "'stateV ⇒ bool" and finalV :: "'stateV ⇒ bool"
and leakViaV :: "'stateV list ⇒ 'stateV list ⇒ 'leak ⇒ bool"
and validTransO :: "'stateO × 'stateO ⇒ bool"
and istateO :: "'stateO ⇒ bool" and finalO :: "'stateO ⇒ bool"
and leakViaO :: "'stateO list ⇒ 'stateO list ⇒ 'leak ⇒ bool"
and corrState :: "'stateV ⇒ 'stateO ⇒ bool"
begin
definition rsecure :: bool where
"rsecure ≡ ∀l s1 tr1 s2 tr2.
istateO s1 ∧ Opt.validFromS s1 tr1 ∧ Opt.completedFrom s1 tr1 ∧
istateO s2 ∧ Opt.validFromS s2 tr2 ∧ Opt.completedFrom s2 tr2 ∧
leakViaO tr1 tr2 l
⟶
(∃sv1 trv1 sv2 trv2.
istateV sv1 ∧ istateV sv2 ∧ corrState sv1 s1 ∧ corrState sv2 s2 ∧
Van.validFromS sv1 trv1 ∧ Van.completedFrom sv1 trv1 ∧
Van.validFromS sv2 trv2 ∧ Van.completedFrom sv2 trv2 ∧
leakViaV trv1 trv2 l)"
end
locale Relative_Security'_fin =
Van: Attacker_Mod_fin istateV validTransV finalV SV AV OV
+
Opt: Attacker_Mod_fin istateO validTransO finalO SO AO OO
for validTransV :: "'stateV × 'stateV ⇒ bool"
and istateV :: "'stateV ⇒ bool" and finalV :: "'stateV ⇒ bool"
and SV :: "'stateV list ⇒ 'secret list"
and AV :: "'stateV trace ⇒ 'actV list"
and OV :: "'stateV trace ⇒ 'obsV list"
and validTransO :: "'stateO × 'stateO ⇒ bool"
and istateO :: "'stateO ⇒ bool" and finalO :: "'stateO ⇒ bool"
and SO :: "'stateO list ⇒ 'secret list"
and AO :: "'stateO trace ⇒ 'actO list"
and OO :: "'stateO trace ⇒ 'obsO list"
and corrState :: "'stateV ⇒ 'stateO ⇒ bool"
sublocale Relative_Security'_fin < Relative_Security''_fin
where leakViaV = Van.leakVia and leakViaO = Opt.leakVia
by standard
context Relative_Security'_fin
begin
lemma rsecure_def2:
"rsecure ⟷
(∀s1 tr1 s2 tr2.
istateO s1 ∧ Opt.validFromS s1 tr1 ∧ Opt.completedFrom s1 tr1 ∧
istateO s2 ∧ Opt.validFromS s2 tr2 ∧ Opt.completedFrom s2 tr2 ∧
AO tr1 = AO tr2 ∧ OO tr1 ≠ OO tr2
⟶
(∃sv1 trv1 sv2 trv2.
istateV sv1 ∧ istateV sv2 ∧ corrState sv1 s1 ∧ corrState sv2 s2 ∧
Van.validFromS sv1 trv1 ∧ Van.completedFrom sv1 trv1 ∧
Van.validFromS sv2 trv2 ∧ Van.completedFrom sv2 trv2 ∧
SV trv1 = SO tr1 ∧ SV trv2 = SO tr2 ∧
AV trv1 = AV trv2 ∧ OV trv1 ≠ OV trv2))"
unfolding rsecure_def
unfolding Van.leakVia_def Opt.leakVia_def
by auto metis
end
locale Statewise_Attacker_Mod = System_Mod istate validTrans final
for istate :: "'state ⇒ bool" and validTrans :: "'state × 'state ⇒ bool" and final :: "'state ⇒ bool"
+
fixes
isSec :: "'state ⇒ bool" and getSec :: "'state ⇒ 'secret"
and
isInt :: "'state ⇒ bool" and getInt :: "'state ⇒ 'act × 'obs"
assumes final_not_isInt: "⋀s. final s ⟹ ¬ isInt s"
and final_not_isSec: "⋀s. final s ⟹ ¬ isSec s"
begin
definition getAct :: "'state ⇒ 'act" where
"getAct = fst o getInt"
definition getObs :: "'state ⇒ 'obs" where
"getObs = snd o getInt"
definition "eqObs trn1 trn2 ≡
(isInt trn1 ⟷ isInt trn2) ∧ (isInt trn1 ⟶ getObs trn1 = getObs trn2)"
definition "eqAct trn1 trn2 ≡
(isInt trn1 ⟷ isInt trn2) ∧ (isInt trn1 ⟶ getAct trn1 = getAct trn2)"
definition A :: "'state trace ⇒ 'act list" where
"A tr ≡ filtermap isInt getAct (butlast tr)"
sublocale A: FiltermapBL isInt getAct A
apply standard unfolding A_def ..
definition O :: "'state trace ⇒ 'obs list" where
"O tr ≡ filtermap isInt getObs (butlast tr)"
sublocale O: FiltermapBL isInt getObs O
apply standard unfolding O_def ..
definition S :: "'state list ⇒ 'secret list" where
"S tr ≡ filtermap isSec getSec (butlast tr)"
sublocale S: FiltermapBL isSec getSec S
apply standard unfolding S_def ..
end
sublocale Statewise_Attacker_Mod < Attacker_Mod_fin
where S = S and A = A and O = O
by standard
locale Rel_Sec =
Van: Statewise_Attacker_Mod istateV validTransV finalV isSecV getSecV isIntV getIntV
+
Opt: Statewise_Attacker_Mod istateO validTransO finalO isSecO getSecO isIntO getIntO
for validTransV :: "'stateV × 'stateV ⇒ bool"
and istateV :: "'stateV ⇒ bool" and finalV :: "'stateV ⇒ bool"
and isSecV :: "'stateV ⇒ bool" and getSecV :: "'stateV ⇒ 'secret"
and isIntV :: "'stateV ⇒ bool" and getIntV :: "'stateV ⇒ 'actV × 'obsV"
and validTransO :: "'stateO × 'stateO ⇒ bool"
and istateO :: "'stateO ⇒ bool" and finalO :: "'stateO ⇒ bool"
and isSecO :: "'stateO ⇒ bool" and getSecO :: "'stateO ⇒ 'secret"
and isIntO :: "'stateO ⇒ bool" and getIntO :: "'stateO ⇒ 'actO × 'obsO"
and corrState :: "'stateV ⇒ 'stateO ⇒ bool"
sublocale Rel_Sec < Relative_Security'_fin
where SV = Van.S and AV = Van.A and OV = Van.O
and SO = Opt.S and AO = Opt.A and OO = Opt.O
by standard
context Rel_Sec
begin
abbreviation getObsV :: "'stateV ⇒ 'obsV" where "getObsV ≡ Van.getObs"
abbreviation getActV :: "'stateV ⇒ 'actV" where "getActV ≡ Van.getAct"
abbreviation getObsO :: "'stateO ⇒ 'obsO" where "getObsO ≡ Opt.getObs"
abbreviation getActO :: "'stateO ⇒ 'actO" where "getActO ≡ Opt.getAct"
abbreviation reachV where "reachV ≡ Van.reach"
abbreviation reachO where "reachO ≡ Opt.reach"
abbreviation completedFromV :: "'stateV ⇒ 'stateV list ⇒ bool" where "completedFromV ≡ Van.completedFrom"
abbreviation completedFromO :: "'stateO ⇒ 'stateO list ⇒ bool" where "completedFromO ≡ Opt.completedFrom"
lemmas completedFromV_def = Van.completedFrom_def
lemmas completedFromO_def = Opt.completedFrom_def
lemma rsecure_def3:
"rsecure ⟷
(∀s1 tr1 s2 tr2.
istateO s1 ∧ Opt.validFromS s1 tr1 ∧ completedFromO s1 tr1 ∧
istateO s2 ∧ Opt.validFromS s2 tr2 ∧ completedFromO s2 tr2 ∧
Opt.A tr1 = Opt.A tr2 ∧ Opt.O tr1 ≠ Opt.O tr2 ∧
(isIntO s1 ∧ isIntO s2 ⟶ getActO s1 = getActO s2)
⟶
(∃sv1 trv1 sv2 trv2.
istateV sv1 ∧ istateV sv2 ∧ corrState sv1 s1 ∧ corrState sv2 s2 ∧
Van.validFromS sv1 trv1 ∧ completedFromV sv1 trv1 ∧
Van.validFromS sv2 trv2 ∧ completedFromV sv2 trv2 ∧
Van.S trv1 = Opt.S tr1 ∧ Van.S trv2 = Opt.S tr2 ∧
Van.A trv1 = Van.A trv2 ∧ Van.O trv1 ≠ Van.O trv2))"
unfolding rsecure_def2 apply (intro iff_allI iffI impI)
subgoal by auto
subgoal
by clarsimp (metis (full_types) Opt.A.Cons_unfold
Opt.completed_Cons Opt.final_not_isInt
Simple_Transition_System.validFromS_Cons_iff
completedFromO_def list.sel(1) neq_Nil_conv) .
definition "eqSec trnO trnA ≡
(isSecV trnO = isSecO trnA) ∧ (isSecV trnO ⟶ getSecV trnO = getSecO trnA)"
lemma eqSec_S_Cons':
"eqSec trnO trnA ⟹
(Van.S (trnO # trO') = Opt.S (trnA # trA')) ⟹ Van.S trO' = Opt.S trA'"
apply(cases "trO' = []")
subgoal apply(cases "trA' = []")
subgoal by auto
subgoal unfolding eqSec_def by auto .
subgoal apply(cases "trA' = []")
subgoal by auto
subgoal unfolding eqSec_def by auto . .
lemma eqSec_S_Cons[simp]:
"eqSec trnO trnA ⟹ trO' = [] ⟷ trA' = [] ⟹
(Van.S (trnO # trO') = Opt.S (trnA # trA')) ⟷ (Van.S trO' = Opt.S trA')"
apply(cases "trO' = []")
subgoal apply(cases "trA' = []")
subgoal by auto
subgoal unfolding eqSec_def by auto .
subgoal apply(cases "trA' = []")
subgoal by auto
subgoal unfolding eqSec_def by auto . .
end
locale Relative_Security_Determ =
Rel_Sec
validTransV istateV finalV isSecV getSecV isIntV getIntV
validTransO istateO finalO isSecO getSecO isIntO getIntO
corrState
+
System_Mod_Deterministic istateV validTransV finalV nextO
for validTransV :: "'stateV × 'stateV ⇒ bool"
and istateV :: "'stateV ⇒ bool"
and finalV :: "'stateV ⇒ bool"
and nextO :: "'stateV ⇒ 'stateV"
and isSecV :: "'stateV ⇒ bool" and getSecV :: "'stateV ⇒ 'secret"
and isIntV :: "'stateV ⇒ bool" and getIntV :: "'stateV ⇒ 'actV × 'obsV"
and validTransO :: "'stateO × 'stateO ⇒ bool"
and istateO :: "'stateO ⇒ bool"
and finalO :: "'stateO ⇒ bool"
and isSecO :: "'stateO ⇒ bool" and getSecO :: "'stateO ⇒ 'secret"
and isIntO :: "'stateO ⇒ bool" and getIntO :: "'stateO ⇒ 'actO × 'obsO"
and corrState :: "'stateV ⇒ 'stateO ⇒ bool"
end