Quelle  ContextVS.thy

(*File: ContextVS.thy*)
(*Authors: Lennart Beringer and Martin Hofmann, LMU Munich 2008*)
theory ContextVS imports VS begin
subsection‹Contextual closure›

text‹\label{sec:contextVS}We show that the notion of security is closed w.r.t.~low
  contexts, i.e.~contextual programs into which a
  program can be substituted and which itself employs only
 emph{obviously} low variables.›

text‹Contexts are {\bf IMP} programs with (multiple) designated holes
 represented by constructor $\mathit{Ctxt\_Here}$).›

datatype CtxtProg =
  Ctxt_Hole
| Ctxt_Skip
| Ctxt_Assign Var Expr
| Ctxt_Comp CtxtProg CtxtProg
| Ctxt_If BExpr CtxtProg CtxtProg
| Ctxt_While BExpr CtxtProg
| Ctxt_Call

text‹We let $C$, $D$ range over contextual programs. The substitution
  is defined by structural recursion.›

primrec Fill::"CtxtProg ==> IMP ==> IMP"
where
"Fill Ctxt_Hole c = c" |
"Fill Ctxt_Skip c = Skip" |
"Fill (Ctxt_Assign x e) c = Assign x e" |
"Fill (Ctxt_Comp C1 C2) c = Comp (Fill C1 c) (Fill C2 c)" |
"Fill (Ctxt_If b C1 C2) c = Iff b (Fill C1 c) (Fill C2 c)" |
"Fill (Ctxt_While b C) c = While b (Fill C c)" |
"Fill Ctxt_Call c = Call"

text‹Equally obvious are the definitions of the (syntactically)
  variables of arithmetic and boolean expressions.›

primrec EVars::"Expr ==> Var set"
where
"EVars (varE x) = {x}" |
"EVars (valE v) = {}" |
"EVars (opE f e1 e2) = EVars e1 ∪ EVars e2"

lemma low_Eval[rule_format]:
 "(∀ x . x ∈ EVars e ⟶ CONTEXT x = low) ⟶
  (∀ s t . s ≈ t ⟶ evalE e s = evalE e t)"
(*<*)
apply (induct e)
apply (simp add: twiddle_def)
apply simp
apply clarsimp
done
(*>*)

primrec BVars::"BExpr ==> Var set"
where
"BVars (compB f e1 e2) = EVars e1 ∪ EVars e2"

lemma low_EvalB[rule_format]:
 "(∀ x . x ∈ BVars b ⟶ CONTEXT x = low) ⟶
  (∀ s t . s ≈ t ⟶ evalB b s = evalB b t)"
(*<*)
apply (induct b)
apply (rename_tac Expr1 Expr2)
apply clarsimp
apply (subgoal_tac "evalE Expr1 s = evalE Expr1 t")
prefer 2 apply (rule low_Eval) apply fast apply assumption
apply (subgoal_tac "evalE Expr2 s = evalE Expr2 t")
prefer 2 apply (rule low_Eval) apply fast apply assumption
apply simp
done
(*>*) 

text‹The variables possibly read from during the evaluation of $c$
  denoted by $\mathit{Vars\; c}$. Note that in the clause for
  the variable that is assigned to is not included in the
 .›

primrec Vars::"IMP ==> Var set"
where
"Vars Skip = {}" |
"Vars (Assign x e) = EVars e" |
"Vars (Comp c d) = Vars c ∪ Vars d" |
"Vars (While b c) = BVars b ∪ Vars c" |
"Vars (Iff b c d) = BVars b ∪ Vars c ∪ Vars d" |
"Vars Call = {}"

text‹For contexts, we define when a set $X$ of variables is an upper
  for the variables read from.›

primrec CtxtVars::"Var set ==> CtxtProg ==> bool"
where
"CtxtVars X Ctxt_Hole = True" |
"CtxtVars X Ctxt_Skip = True" |
"CtxtVars X (Ctxt_Assign x e) = (EVars e ⊆ X)" |
"CtxtVars X (Ctxt_Comp C1 C2) = (CtxtVars X C1 ∧ CtxtVars X C2)" |
"CtxtVars X (Ctxt_If b C1 C2) = (BVars b ⊆ X ∧ CtxtVars X C1
                                             ∧ CtxtVars X C2)" |
"CtxtVars X (Ctxt_While b C) = (BVars b ⊆ X ∧ CtxtVars X C)" |
"CtxtVars X Ctxt_Call = True"

(*<*)
lemma Secure_comp: "[secure c1; secure c2] ==> secure (Comp c1 c2)"
apply (unfold secure_def)
apply (rule, rule, rule, rule)
apply (rule, rule, rule)
apply (unfold Sem_def)
apply (erule exE)+
apply (erule Sem_eval_cases)
apply (erule Sem_eval_cases)
apply (erule_tac x=s in allE, rotate_tac -1)
apply (erule_tac x=t in allE, rotate_tac -1)
apply (erule_tac x=r in allE, rotate_tac -1)
apply (erule_tac x=ra in allE)
apply (erule impE, assumption)
apply (erule impE, rule, assumption)
apply (erule impE, rule, assumption)
apply (erule_tac x=r in allE, rotate_tac -1)
apply (erule_tac x=ra in allE, rotate_tac -1)
apply (erule_tac x=ss in allE, rotate_tac -1)
apply (erule_tac x=tt in allE)
apply (erule impE, assumption)
apply (erule impE, rule, assumption)
apply (erule impE, rule, assumption)
apply assumption
done

lemma Secure_iff:
" [secure c1; secure c2;
   ∀ s ss. s ≈ ss ⟶ evalB b s = evalB b ss]
  ==> secure (Iff b c1 c2)"
apply (unfold secure_def)
apply (rule, rule, rule, rule)
apply (rule, rule, rule)
apply (unfold Sem_def)
apply (erule exE)+
apply (erule_tac x=s in allE, erule_tac x=t in allE, erule impE, assumption)
apply (erule Sem_eval_cases)
apply (erule Sem_eval_cases)
apply (erule_tac x=s in allE, rotate_tac -1)
apply (erule_tac x=t in allE, rotate_tac -1)
apply (erule_tac x=ss in allE, rotate_tac -1)
apply (erule_tac x=tt in allE)
apply (erule impE, assumption)
apply (erule impE, rule, assumption)
apply (erule impE, rule, assumption)
apply assumption
apply fast
apply (erule Sem_eval_cases)
apply fast
apply (erule thin_rl)
apply (erule_tac x=s in allE, rotate_tac -1)
apply (erule_tac x=t in allE, rotate_tac -1)
apply (erule_tac x=ss in allE, rotate_tac -1)
apply (erule_tac x=tt in allE)
apply (erule impE, assumption)
apply (erule impE, rule, assumption)
apply (erule impE, rule, assumption)
apply assumption
done

lemma secure_while_aux[rule_format]:
"∀ n m . n ≤ k ⟶ m ≤ k ⟶
  (∀ s t ss tt . (s , While b c →_n ss) ⟶
                 (t , While b c →_m tt) ⟶
                 secure c ⟶
                 (∀s ss. s ≈ ss ⟶ evalB b s = evalB b ss) ⟶
                 s ≈ t ⟶ ss ≈ tt)"
apply (induct k)
apply clarsimp apply (drule Sem_no_zero_height_derivs, clarsimp)
apply clarsimp
  apply (subgoal_tac "evalB b s = evalB b t")
  prefer 2 apply (erule thin_rl, fast)
  apply (erule Sem_eval_cases)
  prefer 2 apply (erule Sem_eval_cases, simp, simp) 
  apply (erule Sem_eval_cases) prefer 2 apply simp
    apply clarsimp 
    apply (subgoal_tac "r ≈ ra", clarsimp) 
    apply (erule thin_rl, unfold secure_def Sem_def) apply fast
done

lemma Secure_while:
" [secure c;
   ∀ s ss. s ≈ ss ⟶ evalB b s = evalB b ss]
  ==> secure (While b c)"
apply (simp (no_asm_simp) add: secure_def)
apply (rule, rule, rule, rule)
apply (rule, rule, rule)
apply (unfold Sem_def) apply (erule exE)+
apply (rule secure_while_aux) 
prefer 3 apply assumption
prefer 6 apply assumption
prefer 3 apply assumption
prefer 3 apply assumption
prefer 3 apply fast
apply (subgoal_tac "n ≤ n + na", assumption) apply (simp, simp)
done
(*>*)

text‹A constant representing the procedure body with holes.›

consts Ctxt_Body::CtxtProg

text‹The following predicate expresses that all variables read from
  a command $c$ are contained in the set $X$ of low variables.›

definition LOW::"Var set ==> CtxtProg ==> bool"
where "LOW X C = (CtxtVars X C ∧ (∀ x . x : X ⟶ CONTEXT x = low))"

(*<*)
lemma secureI_secureFillI_Aux[rule_format]:
"∀ n m . n ≤ k ⟶ m ≤ k ⟶
       (∀ C d s t ss tt X . (s , d →_n t) ⟶
                          (ss , d →_m tt) ⟶
                          s ≈ ss ⟶
                          d = Fill C c ⟶
                          LOW X C ⟶
                          LOW X Ctxt_Body ⟶
                          body = Fill Ctxt_Body c ⟶ secure c ⟶ t ≈ tt)"
apply (induct k)
apply clarsimp apply (drule Sem_no_zero_height_derivs, clarsimp)
apply clarsimp
apply (case_tac C)
(*Ctxt_Hole*)
apply clarsimp defer 1 
(*Ctxt_Skip*)
apply clarsimp
  apply (erule Sem_eval_cases)+ apply clarsimp
(*Ctxt_Assign*)
apply clarsimp
  apply (erule thin_rl)
  apply (erule Sem_eval_cases)+ apply clarsimp
  apply (simp add: update_def LOW_def twiddle_def) apply clarsimp apply (rule low_Eval) 
      apply fast
    apply (simp add: twiddle_def)
(*Ctxt_Comp*)
apply clarsimp apply (erule Sem_eval_cases) apply (erule Sem_eval_cases) apply clarsimp 
  apply (subgoal_tac "r ≈ ra")
  prefer 2 apply (simp add: LOW_def) 
           apply (erule_tac x=na in allE, clarsimp)
  apply (simp add: LOW_def) 
           apply (erule_tac x=ma in allE, clarsimp)
(*Ctxt_If*)
apply (rename_tac BExpr u v)
apply clarsimp
  apply (subgoal_tac "evalB BExpr s = evalB BExpr ss")
  prefer 2 apply (erule thin_rl, case_tac BExpr, clarsimp)
           apply (rename_tac Expr1 Expr2)
           apply (subgoal_tac "evalE Expr1 s = evalE Expr1 ss", clarsimp)
           apply (subgoal_tac "evalE Expr2 s = evalE Expr2 ss", clarsimp)
           apply (rule low_Eval) apply (simp add: LOW_def) apply fast apply clarsimp
           apply (rule low_Eval) apply (simp add: LOW_def) apply fast apply clarsimp
  apply (erule Sem_eval_cases) apply (erule Sem_eval_cases) prefer 2 apply clarsimp apply clarsimp
  apply (simp add: LOW_def) 
           apply (erule_tac x=na in allE, clarsimp)
  apply (erule Sem_eval_cases) apply clarsimp
  apply (simp add: LOW_def) 
           apply (erule_tac x=na in allE, clarsimp)
(*Ctxt_While*)
apply (rename_tac BExpr CtxtProg)
apply clarsimp 
  apply (subgoal_tac "evalB BExpr s = evalB BExpr ss")
  prefer 2 apply (erule thin_rl, case_tac BExpr, clarsimp)
           apply (rename_tac Expr1 Expr2)
           apply (subgoal_tac "evalE Expr1 s = evalE Expr1 ss", clarsimp)
           apply (subgoal_tac "evalE Expr2 s = evalE Expr2 ss", clarsimp)
           apply (rule low_Eval) apply (simp add: LOW_def) apply fast apply clarsimp
           apply (rule low_Eval) apply (simp add: LOW_def) apply fast apply clarsimp 
  apply (erule Sem_eval_cases) apply (erule Sem_eval_cases) prefer 2 apply clarsimp
  apply (subgoal_tac "r ≈ ra")
  prefer 2 
    apply (simp add: LOW_def)
           apply (erule_tac x=na in allE, clarsimp)
  apply (erule_tac x=ma in allE, clarsimp)
           apply (erule_tac x=mb in allE, clarsimp)
           apply (erule_tac x="Ctxt_While BExpr CtxtProg" in allE)
           apply (erule_tac x="While BExpr (Fill CtxtProg c)" in allE, clarsimp)

  apply (erule Sem_eval_cases) apply clarsimp
  apply clarsimp
(*Ctxt_Call*)
apply clarsimp apply (erule Sem_eval_cases) apply (erule Sem_eval_cases)
  apply (erule_tac x=na in allE, clarsimp) 

(*The deferred goal from Ctxt\_Hole*)
  apply (unfold secure_def Sem_def) 
  apply (erule thin_rl) apply fast
done
(*>*)

text‹By induction on the maximal height of the operational judgement
 hidden in the definition of $\mathit{secure}$) we can prove that the
  of $c$ implies that of $\mathit{Fill}\ C\ c$, provided that
  context and the procedure-context satisfy the $\mathit{LOW}$
  for some $X$, and that the "real" body is obtained by
  $c$ into the procedure context.›

lemma secureI_secureFillI: 
  "[secure c; LOW X C; LOW X Ctxt_Body; body = Fill Ctxt_Body c]
  ==> secure (Fill C c)"
(*<*)
apply (simp (no_asm_simp) add: secure_def Sem_def) 
apply clarsimp
apply (rule secureI_secureFillI_Aux) 
prefer 3 apply assumption
prefer 4 apply assumption
prefer 3 apply assumption
apply (subgoal_tac "n ≤ n+na", assumption)
apply (erule thin_rl, simp)
apply (erule thin_rl, simp)
apply (erule thin_rl,fastforce)
apply assumption
apply assumption
apply assumption
apply assumption
done
(*>*)

text‹Consequently, a (low) variable representing the result of
  attacking context does not leak any unwanted information.›

consts res::Var

theorem
  "[ secure c; LOW X C; LOW X Ctxt_Body; s ≈ ss; s,(Fill C c)⇓t;
     ss,(Fill C c)⇓tt; body = Fill Ctxt_Body c; CONTEXT res = low]
  ==> t res = tt res"
(*<*)
apply (drule secureI_secureFillI) apply assumption apply assumption apply assumption
apply (unfold secure_def)
apply (erule_tac x=s in allE, erule_tac x=ss in allE)
apply (erule_tac x=t in allE, erule_tac x=tt in allE, clarsimp)
apply (simp add: twiddle_def)
done
(*>*)
text‹End of theory ContextVS›
end