Theory Type_System_example

(*
Title: WHATandWHERE-Security
Authors: Sylvia Grewe, Alexander Lux, Heiko Mantel, Jens Sauer
*)
theory Type_System_example
imports Type_System Strong_Security.Expr Strong_Security.Domain_example
begin

― ‹When interpreting, we have to instantiate the type for domains. As an example, we take a type containing 'low' and 'high' as domains.›

consts DA :: "('id,Dom) DomainAssignment"
consts BMap :: "'val ⇒ bool"
consts lH :: "(Dom,('id,'val) Expr) lHatches"

― ‹redefine all the abbreviations necessary for auxiliary lemmas with the 
  correct parameter instantiation›

abbreviation MWLsStepsdet' :: 
  "(('id,'val) Expr, 'id, 'val, (('id,'val) Expr,'id) MWLsCom) TLSteps_curry"
("(1⟨_,/_⟩) →⊲_⊳/ (1⟨_,/_⟩)" [0,0,0,0,0] 81)
where
"⟨c1,m1⟩ →⊲α⊳ ⟨c2,m2⟩ ≡ 
  ((c1,m1),α,(c2,m2)) ∈ MWLs_semantics.MWLsSteps_det ExprEval BMap"

abbreviation d_equal' :: "('id, 'val) State 
  ⇒ Dom ⇒ ('id, 'val) State ⇒ bool" 
( "(_ =⇘_⇙ _)" )
where
"m =⇘d⇙ m' ≡ WHATWHERE.d_equal DA d m m'"

abbreviation dH_equal' :: "('id, 'val) State ⇒ Dom 
  ⇒ (Dom,('id,'val) Expr) Hatches
  ⇒ ('id, 'val) State ⇒ bool"
( "(_ ∼⇘_,_⇙ _)" )
where
"m ∼⇘d,H⇙ m' ≡ WHATWHERE.dH_equal ExprEval DA d H m m'"

abbreviation NextMem' :: "(('id,'val) Expr, 'id) MWLsCom 
  ⇒ ('id,'val) State ⇒ ('id,'val) State"
("⟦_⟧'(_')")
where
"⟦c⟧(m) 
  ≡ WHATWHERE.NextMem (MWLs_semantics.MWLsSteps_det ExprEval BMap) c m"

abbreviation dH_indistinguishable' :: "('id,'val) Expr ⇒ Dom 
  ⇒ (Dom,('id,'val) Expr) Hatches ⇒ ('id,'val) Expr ⇒ bool" 
( "(_ ≡⇘_,_⇙ _)" )
where
"e1 ≡⇘d,H⇙ e2 
  ≡ WHATWHERE_Secure_Programs.dH_indistinguishable ExprEval DA d H e1 e2"

abbreviation htchLoc :: "nat ⇒ (Dom, ('id,'val) Expr) Hatches"
where 
"htchLoc ι ≡ WHATWHERE.htchLoc lH ι"


― ‹Security typing rules for expressions›
inductive 
ExprSecTyping :: "(Dom, ('id,'val) Expr) Hatches
  ⇒ ('id, 'val) Expr ⇒ Dom ⇒ bool"
("_ ⊢⇘ℰ⇙ _ : _")
for H :: "(Dom, ('id, 'val) Expr) Hatches"
where 
Consts: "H ⊢⇘ℰ⇙ (Const v) : d" |
Vars: "DA x = d ⟹ H ⊢⇘ℰ⇙ (Var x) : d" |
Hatch: "(d,e) ∈ H ⟹ H ⊢⇘ℰ⇙ e : d" |
Ops: "⟦ ∀i < length arglist. H ⊢⇘ℰ⇙ (arglist!i) : (dl!i) ∧ (dl!i) ≤ d ⟧
  ⟹ H ⊢⇘ℰ⇙ (Op f arglist) : d"

― ‹function substituting a certain expression with another expression 
  in expressions›
primrec Subst :: "('id, 'val) Expr ⇒ ('id, 'val) Expr 
  ⇒ ('id, 'val) Expr ⇒ ('id, 'val) Expr"
("_<_\\_>")
and SubstL :: "('id, 'val) Expr list ⇒ ('id, 'val) Expr 
  ⇒ ('id, 'val) Expr ⇒ ('id, 'val) Expr list"
where
"(Const v)<e1\\e2> = (if e1=(Const v) then e2 else (Const v))" |
"(Var x)<e1\\e2> = (if e1=(Var x) then e2 else (Var x))" |
"(Op f arglist)<e1\\e2> = (if e1=(Op f arglist) then e2 else 
  (Op f (SubstL arglist e1 e2)))" |

"SubstL [] e1 e2 = []" |
"SubstL (e#V) e1 e2 = (e<e1\\e2>)#(SubstL V e1 e2)"


definition SubstClosure :: "'id ⇒ ('id, 'val) Expr ⇒ bool"
where
"SubstClosure x e ≡ ∀(d',e',ι') ∈ lH. (d',e'<(Var x)\\e>,ι') ∈ lH"

definition synAssignSC :: "'id ⇒ ('id, 'val) Expr ⇒ nat ⇒ bool"
where
"synAssignSC x e ι ≡ ∃d. ((htchLoc ι) ⊢⇘ℰ⇙ e : d ∧ d ≤ DA x)
  ∧ (SubstClosure x e)"

definition synWhileSC :: "('id, 'val) Expr ⇒ bool"
where
"synWhileSC e ≡ (∃d. ({} ⊢⇘ℰ⇙ e : d) ∧ (∀d'. d ≤ d'))"

definition synIfSC :: "('id, 'val) Expr
  ⇒ (('id, 'val) Expr, 'id) MWLsCom 
  ⇒ (('id, 'val) Expr, 'id) MWLsCom ⇒ bool" 
where
"synIfSC e c1 c2 ≡ ∃d. ({} ⊢⇘ℰ⇙ e : d ∧ (∀d'. d ≤ d'))"


― ‹auxiliary lemma for locale interpretation (theorem 7 in original paper)›
lemma ExprTypable_with_smallerd_implies_dH_indistinguishable:
  "⟦ H ⊢⇘ℰ⇙ e : d'; d' ≤ d ⟧ ⟹ e ≡⇘d,H⇙ e"
proof (induct rule: ExprSecTyping.induct, 
    simp_all add: WHATWHERE_Secure_Programs.dH_indistinguishable_def 
    WHATWHERE.dH_equal_def WHATWHERE.d_equal_def, auto)
  fix dl arglist f m1 m2 d' d
  assume main: "∀i < length arglist.
    (H ⊢⇘ℰ⇙ (arglist!i) : (dl!i)) ∧ (dl!i ≤ d ⟶
    (∀m1 m2. (∀x. DA x ≤ d ⟶ m1 x = m2 x) ∧
    (∀(d',e)∈H. d' ≤ d ⟶ ExprEval e m1 = ExprEval e m2) ⟶
    ExprEval (arglist!i) m1 = ExprEval (arglist!i) m2)) ∧ dl!i ≤ d'"
  assume smaller: "d' ≤ d"
  assume eqeval: "∀(d',e) ∈ H. d' ≤ d ⟶ ExprEval e m1 = ExprEval e m2"
  assume eqstate: "∀x. DA x ≤ d ⟶ m1 x = m2 x"
  
  from main smaller have irangesubst:
    "∀i < length arglist. dl!i ≤ d"
    by (metis order_trans)

  with eqstate eqeval main have 
    "∀i < length arglist. ExprEval (arglist!i) m1 
       = ExprEval (arglist!i) m2"
    by force

  hence substmap: "(ExprEvalL arglist m1) = (ExprEvalL arglist m2)" 
    by (induct arglist, auto, force)

  show "f (ExprEvalL arglist m1) = f (ExprEvalL arglist m2)"
    by (subst substmap, auto)

qed

― ‹auxiliary lemma about substitutions in expressions and in memories›
lemma substexp_substmem:
"ExprEval e'<Var x\\e> m = ExprEval e' (m(x := ExprEval e m))
  ∧ ExprEvalL (SubstL elist (Var x) e) m
  = ExprEvalL elist (m(x := ExprEval e m))"
by (induct_tac e' and elist rule: ExprEval.induct ExprEvalL.induct, simp_all)


― ‹another auxiliary lemma for locale interpretation (lemma 8 in original paper)›
lemma SubstClosure_implications:
"⟦ SubstClosure x e; m ∼⇘d,(htchLoc ι')⇙ m'; 
  ⟦x :=⇘ι⇙ e⟧(m) =⇘d⇙ ⟦x :=⇘ι⇙ e⟧(m') ⟧
  ⟹ ⟦x :=⇘ι⇙ e⟧(m) ∼⇘d,(htchLoc ι')⇙ ⟦x :=⇘ι⇙ e⟧(m')"
proof -
  fix m1 m1'
  assume substclosure: "SubstClosure x e"
  assume dequalm2: "⟦x :=⇘ι⇙ e⟧(m1) =⇘d⇙ ⟦x :=⇘ι⇙ e⟧(m1')"
  assume dhequalm1: "m1 ∼⇘d,(htchLoc ι')⇙ m1'"  
  
  from MWLs_semantics.nextmem_exists_and_unique obtain m2 where m1step:
    "(∃p α. ⟨x :=⇘ι⇙ e,m1⟩ →⊲α⊳ ⟨p,m2⟩) 
    ∧ (∀m''. (∃p α. ⟨x :=⇘ι⇙ e,m1⟩ →⊲α⊳ ⟨p,m''⟩) ⟶ m'' = m2)"
    by force
  hence m2_is_next: "⟦x :=⇘ι⇙ e⟧(m1) = m2"
    by (simp add: WHATWHERE.NextMem_def, auto)
  from m1step MWLs_semantics.MWLsSteps_det.assign
     [of "ExprEval" "e" "m1" _ "x" "ι" "BMap"]
  have m2eq: "m2 = m1(x := (ExprEval e m1))"
    by auto

  from MWLs_semantics.nextmem_exists_and_unique obtain m2' where m1'step:
    "(∃p α. ⟨x :=⇘ι⇙ e,m1'⟩ →⊲α⊳ ⟨p,m2'⟩) 
    ∧ (∀m''. (∃p α. ⟨x :=⇘ι⇙ e,m1'⟩ →⊲α⊳ ⟨p,m''⟩) ⟶ m'' = m2')"
    by force
  hence m2'_is_next: "⟦x :=⇘ι⇙ e⟧(m1') = m2'"
    by (simp add: WHATWHERE.NextMem_def, auto)
  from m1'step MWLs_semantics.MWLsSteps_det.assign
     [of "ExprEval" "e" "m1'" _ "x" "ι" "BMap"]
  have m2'eq: "m2' = m1'(x := (ExprEval e m1'))"
    by auto

  from m2eq substexp_substmem
  have substeval1: "∀e'. ExprEval (e'<Var x\\e>) m1 = ExprEval e' m2"
    by force

  from m2'eq substexp_substmem
  have substeval2: "∀e'. ExprEval e'<Var x\\e> m1' = ExprEval e' m2'"
    by force
   
  from substclosure have 
    "∀(d',e') ∈ htchLoc ι'. (d',e'<Var x\\e>) ∈ (htchLoc ι')"
    by (simp add: SubstClosure_def WHATWHERE.htchLoc_def, auto)

  with dhequalm1 have 
    "∀(d',e') ∈ htchLoc ι'. 
    d' ≤ d ⟶ ExprEval e'<Var x\\e> m1 = ExprEval e'<Var x\\e> m1'"
    by (simp add: WHATWHERE.dH_equal_def, auto)

  with substeval1 substeval2 have 
    "∀(d',e') ∈ htchLoc ι'.
    d' ≤ d ⟶ ExprEval e' m2 = ExprEval e' m2'"
    by auto

  with dequalm2 m2_is_next m2'_is_next
  show "⟦x :=⇘ι⇙ e⟧(m1) ∼⇘d,htchLoc ι'⇙ ⟦x :=⇘ι⇙ e⟧(m1')"
    by (simp add: WHATWHERE.dH_equal_def)
qed

― ‹interpretation of the abstract type system using the above definitions for the side conditions›
interpretation Type_System_example: Type_System ExprEval BMap DA lH
  synAssignSC synWhileSC synIfSC
by (unfold_locales, auto,
  metis ExprTypable_with_smallerd_implies_dH_indistinguishable 
  synAssignSC_def,
  metis SubstClosure_implications synAssignSC_def, 
  simp add: synWhileSC_def,
  metis ExprTypable_with_smallerd_implies_dH_indistinguishable 
  WHATWHERE_Secure_Programs.empH_implies_dHindistinguishable_eq_dindistinguishable, 
  simp add: synIfSC_def,
  metis ExprTypable_with_smallerd_implies_dH_indistinguishable 
  WHATWHERE_Secure_Programs.empH_implies_dHindistinguishable_eq_dindistinguishable)

end