Theory Relative_Security

section ‹Relative Security›

text ‹ This theory formalizes the general notion of relative security, 
applicable to possibly infinite traces.  ›


theory Relative_Security
imports Relative_Security_fin "Preliminaries/Trivia"
begin

no_notation relcomp (infixr "O" 75)
no_notation relcompp (infixr "OO" 75)


subsection ‹Leakage models and attacker models ›

(* Everything extended to lazy lists (possibly infinite traces) has prefix "l". *)

locale Leakage_Mod = System_Mod istate validTrans final
for istate :: "'state ⇒ bool" and validTrans :: "'state × 'state ⇒ bool" and final :: "'state ⇒ bool"
+
fixes lleakVia :: "'state llist ⇒ 'state llist ⇒ 'leak ⇒ bool" 


locale Attacker_Mod = System_Mod istate validTrans final
for istate :: "'state ⇒ bool" and validTrans :: "'state × 'state ⇒ bool" and final :: "'state ⇒ bool"
+
fixes S :: "'state llist ⇒ 'secret llist"
and A :: "'state ltrace ⇒ 'act llist" 
and O :: "'state ltrace ⇒ 'obs llist"
begin

fun lleakVia :: "'state llist ⇒ 'state llist ⇒ 'secret llist × 'secret llist ⇒ bool" 
where 
"lleakVia tr tr' (sl,sl') = (S tr = sl ∧ S tr' = sl' ∧ A tr = A tr' ∧ O tr ≠ O tr')"

lemmas lleakVia_def = lleakVia.simps 

end 

sublocale Attacker_Mod < Leakage_Mod 
where lleakVia = lleakVia
by standard 


subsection ‹Locales for increasingly concrete notions of relative security ›

(* Very abstract relative security, based on leakage models (as in the paper's section 2.3) *)
locale Relative_Security'' = 
  Van: Leakage_Mod istateV validTransV finalV lleakViaV
+
  Opt: Leakage_Mod istateO validTransO finalO lleakViaO
  for validTransV :: "'stateV × 'stateV ⇒ bool"
  and istateV :: "'stateV ⇒ bool" and finalV :: "'stateV ⇒ bool"
  and lleakViaV :: "'stateV llist ⇒ 'stateV llist ⇒ '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 lleakViaO :: "'stateO llist ⇒ 'stateO llist ⇒ '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 lrsecure :: bool where 
"lrsecure ≡ ∀l s1 tr1 s2 tr2. 
   istateO s1 ∧ Opt.lvalidFromS s1 tr1 ∧ Opt.lcompletedFrom s1 tr1 ∧ 
   istateO s2 ∧ Opt.lvalidFromS s2 tr2 ∧ Opt.lcompletedFrom s2 tr2 ∧  
   lleakViaO tr1 tr2 l 
   ⟶ 
   (∃sv1 trv1 sv2 trv2. 
      istateV sv1 ∧ istateV sv2 ∧ corrState sv1 s1 ∧ corrState sv2 s2 ∧ 
      Van.lvalidFromS sv1 trv1 ∧ Van.lcompletedFrom sv1 trv1 ∧ 
      Van.lvalidFromS sv2 trv2 ∧ Van.lcompletedFrom sv2 trv2 ∧  
      lleakViaV 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' = 
  Van: Attacker_Mod istateV validTransV finalV SV AV OV 
+
  Opt: Attacker_Mod istateO validTransO finalO SO AO OO 
  for validTransV :: "'stateV × 'stateV ⇒ bool"
  and istateV :: "'stateV ⇒ bool" and finalV :: "'stateV ⇒ bool"
  and SV :: "'stateV llist ⇒ 'secret llist"
  and AV :: "'stateV ltrace ⇒ 'actV llist" 
  and OV :: "'stateV ltrace ⇒ 'obsV llist"
  (* 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 llist ⇒ 'secret llist"
  and AO :: "'stateO ltrace ⇒ 'actO llist" 
  and OO :: "'stateO ltrace ⇒ 'obsO llist"
  and corrState :: "'stateV ⇒ 'stateO ⇒ bool"

sublocale Relative_Security' <  Relative_Security''  
where lleakViaV = Van.lleakVia and lleakViaO = Opt.lleakVia 
by standard


context Relative_Security'
begin

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

lemma lrsecure_def2:
"lrsecure ⟷ 
 (∀s1 tr1 s2 tr2.
     istateO s1 ∧ Opt.lvalidFromS s1 tr1 ∧ Opt.lcompletedFrom s1 tr1 ∧ 
     istateO s2 ∧ Opt.lvalidFromS s2 tr2 ∧ Opt.lcompletedFrom 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.lvalidFromS sv1 trv1 ∧ Van.lcompletedFrom sv1 trv1 ∧ 
        Van.lvalidFromS sv2 trv2 ∧ Van.lcompletedFrom sv2 trv2 ∧ 
        SV trv1 = SO tr1 ∧ SV trv2 = SO tr2 ∧ 
        AV trv1 = AV trv2 ∧ OV trv1 ≠ OV trv2))" 
unfolding lrsecure_def 
unfolding Van.lleakVia_def Opt.lleakVia_def
by auto metis

end (* context Relative_Security' *)



context Statewise_Attacker_Mod begin

(* Infinitary (lazy list) versions of the operators: *)

(* The action function: *)
definition lA :: "'state ltrace ⇒ 'act llist" where 
"lA tr ≡ lfiltermap isInt getAct (lbutlast tr)"

sublocale lA: LfiltermapBL isInt getAct lA
  apply standard unfolding lA_def ..

lemma lA: "lcompletedFrom s tr ⟹ lA tr = lmap getAct (lfilter isInt tr)"
apply(cases "lfinite tr")
  subgoal unfolding lA.lmap_lfilter lbutlast_def  
  by simp (metis final_not_isInt lbutlast_lfinite lcompletedFrom_def lfilter_llist_of lfiltermap_lmap_lfilter lfinite_lfiltermap_butlast llast_llist_of llist_of_list_of lmap_llist_of)
  subgoal unfolding lA.lmap_lfilter lbutlast_def by auto .

(* The observation function: *)
definition lO :: "'state ltrace ⇒ 'obs llist" where  
"lO tr ≡ lfiltermap isInt getObs (lbutlast tr)"

(* lemma lO_LfiltermapBL: ‹LfiltermapBL isInt getObs lO›
  unfolding lO_def by (standard, auto)
*)

sublocale lO: LfiltermapBL isInt getObs lO
  apply standard unfolding lO_def ..

lemma lO: "lcompletedFrom s tr ⟹ lO tr = lmap getObs (lfilter isInt tr)"
apply(cases "lfinite tr")
  subgoal unfolding lO.lmap_lfilter lbutlast_def 
  by simp (metis List_Filtermap.filtermap_def butlast.simps(1) filtermap_butlast final_not_isInt lcompletedFrom_def lfilter_llist_of llist_of_list_of lmap_llist_of)
  subgoal unfolding lO.lmap_lfilter lbutlast_def by auto .

(* The secrecy function: *)
definition lS :: "'state llist ⇒ 'secret llist" where 
"lS tr ≡ lfiltermap isSec getSec (lbutlast tr)"

sublocale lS: LfiltermapBL isSec getSec lS
  apply standard unfolding lS_def ..

lemma lS: "lcompletedFrom s tr ⟹ lS tr = lmap getSec (lfilter isSec tr)"
apply(cases "lfinite tr")
  subgoal unfolding lS.lmap_lfilter lbutlast_def 
  by simp (metis List_Filtermap.filtermap_def filtermap_butlast final_not_isSec lcompletedFrom_def lfilter_llist_of llist_of_eq_LNil_conv llist_of_list_of lmap_llist_of)
  subgoal unfolding lS.lmap_lfilter lbutlast_def by auto .


end (* context Statewise_Attacker_Mod *)


sublocale Statewise_Attacker_Mod < Attacker_Mod 
where S = lS and A = lA and O = lO
by standard


sublocale Rel_Sec < Relative_Security'
where SV = Van.lS and AV = Van.lA and OV = Van.lO
and SO = Opt.lS and AO = Opt.lA and OO = Opt.lO
by standard



context Rel_Sec 
begin 

abbreviation lcompletedFromV :: "'stateV ⇒ 'stateV llist ⇒ bool" where "lcompletedFromV ≡ Van.lcompletedFrom"
abbreviation lcompletedFromO :: "'stateO ⇒ 'stateO llist ⇒ bool" where "lcompletedFromO ≡ Opt.lcompletedFrom"


lemma eqSec_lS_Cons': 
"eqSec trnO trnA ⟹ 
 (Van.lS (trnO $ trO') = Opt.lS (trnA $ trA')) ⟹ Van.lS trO' = Opt.lS 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_lS_Cons[simp]: 
"eqSec trnO trnA ⟹ trO' = [[]] ⟷ trA' = [[]] ⟹
 (Van.lS (trnO $ trO') = Opt.lS (trnA $ trA')) ⟷ (Van.lS trO' = Opt.lS 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 *)

end