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 ›

(* Very abstract relative security, based on leakage models (as in the paper's section 2.3) *)
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"   
  (* NB: we have the same notion of secret, but everything else can be different  *)
  and validTransO :: "'stateO × 'stateO ⇒ bool"
  and istateO :: "'stateO ⇒ bool" and finalO :: "'stateO ⇒ bool"
  and leakViaO :: "'stateO list ⇒ 'stateO list ⇒ 'leak ⇒ bool"  
  (* We also parameterize the relative security notion by a "corresponding state" 
  relationship between states, which in the examples so far has always been taken to 
  be vacuously true. *)
  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 (* context Relative_Security'' *)

(* Less abstract relative security, instantiated to attacker models (as in the paper's section 2.4) *)
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"
  (* NB: we have the same notion of secret, but everything else can be different  *)
  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

(* For attacker models, relative security has the following more intuitive formulation 
(expression (⋆) from the paper's section 2.4) *)

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 (* context Relative_Security'_fin *)


locale Statewise_Attacker_Mod = System_Mod istate validTrans final
 for istate :: "'state ⇒ bool" and validTrans :: "'state × 'state ⇒ bool" and final :: "'state ⇒ bool"
+
fixes (* secret filtering and production:  *)
   isSec :: "'state ⇒ bool" and getSec :: "'state ⇒ 'secret"
 and (* interaction (action and/or observation) filtering and production: *)
   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)"

(* THE VERSIONS FOR FINITE TRACES FIRST: *)
(* The action function: *)
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 ..


(* The observation function: *)
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 ..


(* The secrecy function: *)
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 (* context Statewise_Attacker_Mod *)


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"  
  (* NB: we have the same notion of secret, but everything else can be different  *)
  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" 
  (* We also parameterize the relative security notion by a "corresponding state" 
  relationship between states, which in the examples so far has always been taken to 
  be vacuously true. 
  *)
  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 (* context Relative_Security *)

(* DETERMINISTIC VERSION *)

(* Assuming the original transition system is deterministic: *)
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