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⟨_,/_⟩) ->\<lhd>_\<rhd>/ (1⟨_,/_⟩)" [0,0,0,0,0] 81)
where
"⟨c1,m1⟩ ->\<lhd>α\<rhd> ⟨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"
("_ \<turnstile>⇘\<E>⇙ _ : _")
for H :: "(Dom, ('id, 'val) Expr) Hatches"
where
Consts: "H \<turnstile>⇘\<E>⇙ (Const v) : d" |
Vars: "DA x = d ==> H \<turnstile>⇘\<E>⇙ (Var x) : d" |
Hatch: "(d,e) ∈ H ==> H \<turnstile>⇘\<E>⇙ e : d" |
Ops: "[| ∀i < length arglist. H \<turnstile>⇘\<E>⇙ (arglist!i) : (dl!i) ∧ (dl!i) ≤ d |]
==> H \<turnstile>⇘\<E>⇙ (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 ι) \<turnstile>⇘\<E>⇙ e : d ∧ d ≤ DA x)
∧ (SubstClosure x e)"
definition synWhileSC :: "('id, 'val) Expr => bool"
where
"synWhileSC e ≡ (∃d. ({} \<turnstile>⇘\<E>⇙ 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. ({} \<turnstile>⇘\<E>⇙ e : d ∧ (∀d'. d ≤ d'))"
--"auxiliary lemma for locale interpretation (theorem 7 in original paper)"
lemma ExprTypable_with_smallerd_implies_dH_indistinguishable:
"[| H \<turnstile>⇘\<E>⇙ 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 \<turnstile>⇘\<E>⇙ (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, 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⟩ ->\<lhd>α\<rhd> ⟨p,m2⟩)
∧ (∀m''. (∃p α. ⟨x :=⇘ι⇙ e,m1⟩ ->\<lhd>α\<rhd> ⟨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'⟩ ->\<lhd>α\<rhd> ⟨p,m2'⟩)
∧ (∀m''. (∃p α. ⟨x :=⇘ι⇙ e,m1'⟩ ->\<lhd>α\<rhd> ⟨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