Theory WHATWHERE_Security

(*
Title: WHATandWHERE-Security
Authors: Sylvia Grewe, Alexander Lux, Heiko Mantel, Jens Sauer
*)
theory WHATWHERE_Security
imports Strong_Security.Types
begin

locale WHATWHERE = 
fixes SR :: "('exp, 'id, 'val, 'com) TLSteps"
and E :: "('exp, 'id, 'val) Evalfunction"
and pp :: "'com  nat"
and DA :: "('id, 'd::order) DomainAssignment"
and lH :: "('d::order, 'exp) lHatches"

begin

― ‹define when two states are indistinguishable for an observer on domain d›
definition d_equal :: "'d::order  ('id, 'val) State 
   ('id, 'val) State  bool"
where
"d_equal d m m'  x. ((DA x)  d  (m x) = (m' x))"

abbreviation d_equal' :: "('id, 'val) State 
   'd::order  ('id, 'val) State  bool" 
( "(_ =⇘_ _)" )
where
"m =⇘dm'  d_equal d m m'"

― ‹transitivity of d-equality›
lemma d_equal_trans:
" m =⇘dm'; m' =⇘dm''   m =⇘dm''"
by (simp add: d_equal_def)


abbreviation SRabbr :: "('exp, 'id, 'val, 'com) TLSteps_curry"
("(1_,/_) →⊲_/ (1_,/_)" [0,0,0,0,0] 81)
where
"c,m →⊲α p,m'  ((c,m),α,(p,m'))  SR"


― ‹function for obtaining the unique memory (state) after one step for a command and a memory (state)›
definition NextMem :: "'com  ('id, 'val) State  ('id, 'val) State"
( "_⟧'(_')" )
where
"c⟧(m)  (THE m'. (p α. c,m →⊲α p,m'))"

― ‹function getting all escape hatches for some location›
definition htchLoc :: "nat  ('d, 'exp) Hatches"
where
"htchLoc ι  {(d,e). (d,e,ι)  lH}"

― ‹function for getting all escape hatches for some set of locations›
definition htchLocSet :: "nat set  ('d, 'exp) Hatches"
where
"htchLocSet PP  {h. (ι  PP. h = htchLoc ι)}"

― ‹predicate for (d,H)-equality›
definition dH_equal :: "'d  ('d, 'exp) Hatches
   ('id, 'val) State  ('id, 'val) State  bool"
where
"dH_equal d H m m'  (m =⇘dm'  
  ((d',e)  H. (d'  d  (E e m = E e m'))))"

abbreviation dH_equal' :: "('id, 'val) State  'd  ('d, 'exp) Hatches
   ('id, 'val) State  bool"
( "(_ ∼⇘_,_ _)" )
where
"m ∼⇘d,Hm'  dH_equal d H m m'"

― ‹predicate indicating that a command is not a d-declassification command›
definition NDC :: "'d  'com  bool"
where
"NDC d c  (m m'. m =⇘dm'  c⟧(m) =⇘dc⟧(m'))"

― ‹predicate indicating an 'immediate d-declassification command' for a set of escape hatches›
definition IDC :: "'d  'com  ('d, 'exp) Hatches  bool"
where
"IDC d c H  (m m'. m =⇘dm'  
  (¬ c⟧(m) =⇘dc⟧(m')))
   (m m'. m ∼⇘d,Hm'  c⟧(m) =⇘dc⟧(m') )"

definition stepResultsinR :: "'com ProgramState  'com ProgramState 
   'com Bisimulation_type  bool"
where
"stepResultsinR p p' R  (p = None  p' = None)  
  (c c'. (p = Some c  p' = Some c'  ([c],[c'])  R))"


definition dhequality_alternative ::  "'d  nat set  nat 
   ('id, 'val) State  ('id, 'val) State  bool"
where
"dhequality_alternative d PP ι m m'  m ∼⇘d,(htchLocSet PP)m' 
            (¬ (htchLoc ι)  (htchLocSet PP))"

definition Strong_dlHPP_Bisimulation :: "'d  nat set 
   'com Bisimulation_type  bool"
where
"Strong_dlHPP_Bisimulation d PP R  
  (sym R)  (trans R) 
  ((V,V')  R. length V = length V') 
  ((V,V')  R. i < length V. 
    ((NDC d (V!i))  
     (IDC d (V!i) (htchLoc (pp (V!i)))))) 
  ((V,V')  R. i < length V. m1 m1' m2 α p.
    ( V!i,m1 →⊲α p,m2  m1 ∼⇘d,(htchLocSet PP)m1')
     (p' α' m2'. ( V'!i,m1' →⊲α' p',m2' 
        (stepResultsinR p p' R)  (α,α')  R  
        (dhequality_alternative d PP (pp (V!i)) m2 m2'))))"


― ‹predicate to define when a program is strongly secure›
definition WHATWHERE_Secure :: "'com list  bool"
where
"WHATWHERE_Secure V  (d PP. 
  (R. Strong_dlHPP_Bisimulation d PP R  (V,V)  R))"


― ‹auxiliary lemma to obtain central strong (d,lH,PP)-Bisimulation property as Lemma
 in meta logic (allows instantiating all the variables manually if necessary)›
lemma strongdlHPPB_aux: 
 "V V' m1 m1' m2 p i α.  Strong_dlHPP_Bisimulation d PP R;
  i < length V; (V,V')  R; 
  V!i,m1 →⊲α p,m2; m1 ∼⇘d,(htchLocSet PP)m1' 
  (p' α' m2'. V'!i,m1' →⊲α' p',m2'
   stepResultsinR p p' R  (α,α')  R  
  (dhequality_alternative d PP (pp (V!i)) m2 m2'))"
  by (simp add: Strong_dlHPP_Bisimulation_def, fastforce)

― ‹auxiliary lemma to obtain 'NDC or IDC' from strong (d,lH,PP)-Bisimulation as lemma
  in meta logic allowing instantiation of the variables›
lemma strongdlHPPB_NDCIDCaux:
"V V' i. Strong_dlHPP_Bisimulation d PP R;
  (V,V')  R; i < length V 
         (NDC d (V!i)  IDC d (V!i) (htchLoc (pp (V!i))))"
  by (simp add: Strong_dlHPP_Bisimulation_def, auto)

lemma WHATWHERE_empty:
"WHATWHERE_Secure []"
  by (simp add: WHATWHERE_Secure_def, auto,
  rule_tac x="{([],[])}" in exI,
  simp add: Strong_dlHPP_Bisimulation_def sym_def trans_def)


end

end