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