Theory Type_System

(*
Title: WHATandWHERE-Security
Authors: Sylvia Grewe, Alexander Lux, Heiko Mantel, Jens Sauer
*)
theory Type_System
imports Language_Composition
begin

locale Type_System =
  WWP?: WHATWHERE_Secure_Programs "E" "BMap" "DA" "lH"
  for E :: "('exp, 'id, 'val) Evalfunction"
  and BMap :: "'val ⇒ bool"
  and DA :: "('id, 'd::order) DomainAssignment"
  and lH :: "('d, 'exp) lHatches"
+ 
fixes
AssignSideCondition :: "'id ⇒ 'exp ⇒ nat ⇒ bool"
and WhileSideCondition :: "'exp ⇒ bool"
and IfSideCondition :: 
  "'exp ⇒ ('exp,'id) MWLsCom ⇒ ('exp,'id) MWLsCom ⇒ bool" 
assumes semAssignSC: "AssignSideCondition x e ι ⟹ 
  e ≡⇘DA x,(htchLoc ι)⇙ e ∧ (∀m m' d ι'. (m ∼⇘d,(htchLoc ι')⇙ m' ∧ 
  ⟦x :=⇘ι⇙ e⟧(m) =⇘d⇙ ⟦x :=⇘ι⇙ e⟧(m'))
  ⟶ ⟦x :=⇘ι⇙ e⟧(m) ∼⇘d,(htchLoc ι')⇙ ⟦x :=⇘ι⇙ e⟧(m'))" 
and semWhileSC: "WhileSideCondition e ⟹ ∀d. e ≡⇘d⇙ e"
and semIfSC: "IfSideCondition e c1 c2 ⟹ ∀d. e ≡⇘d⇙ e"
begin

― ‹Security typing rules for the language commands›
inductive
ComSecTyping :: "('exp, 'id) MWLsCom ⇒ bool"
  (‹⊢⇘𝒞⇙ _›)
and ComSecTypingL :: "('exp,'id) MWLsCom list ⇒ bool"
   (‹⊢⇘𝒱⇙ _›)
where
Skip: "⊢⇘𝒞⇙ skip⇘ι⇙" |
Assign: "⟦ AssignSideCondition x e ι ⟧ ⟹ ⊢⇘𝒞⇙ x :=⇘ι⇙ e" |
Spawn: "⟦ ⊢⇘𝒱⇙ V ⟧ ⟹ ⊢⇘𝒞⇙ spawn⇘ι⇙ V" |
Seq: "⟦ ⊢⇘𝒞⇙ c1; ⊢⇘𝒞⇙ c2 ⟧ ⟹ ⊢⇘𝒞⇙ c1;c2" |
While: "⟦ ⊢⇘𝒞⇙ c; WhileSideCondition b ⟧ 
     ⟹ ⊢⇘𝒞⇙ while⇘ι⇙ b do c od" |
If: "⟦ ⊢⇘𝒞⇙ c1; ⊢⇘𝒞⇙ c2; IfSideCondition b c1 c2 ⟧
  ⟹ ⊢⇘𝒞⇙ if⇘ι⇙ b then c1 else c2 fi" |
Parallel: "⟦ ∀i < length V. ⊢⇘𝒞⇙ V!i ⟧ ⟹ ⊢⇘𝒱⇙ V"

inductive_cases parallel_cases:
"⊢⇘𝒱⇙ V"

definition auxiliary_predicate
where
"auxiliary_predicate V ≡ unique_PPV V ⟶ WHATWHERE_Secure V" 

― ‹soundness proof of abstract type system›
theorem ComSecTyping_single_is_sound:
"⟦ ⊢⇘𝒞⇙ c; unique_PPc c ⟧
  ⟹ WHATWHERE_Secure [c]"
proof (induct rule: ComSecTyping_ComSecTypingL.inducts(1)
    [of _ _ "auxiliary_predicate"], simp_all add: auxiliary_predicate_def)
  fix ι
  show "WHATWHERE_Secure [skip⇘ι⇙]"
    by (metis WHATWHERE_Secure_Skip)
next
  fix x e ι
  assume "AssignSideCondition x e ι"
  thus "WHATWHERE_Secure [x :=⇘ι⇙ e]"
    by (metis WHATWHERE_Secure_Assign semAssignSC)
next
  fix V ι
  assume IH: "unique_PPV V ⟶ WHATWHERE_Secure V"
  assume uniPPspawn: "unique_PPc (spawn⇘ι⇙ V)"
  hence "unique_PPV V"
    by (simp add: unique_PPV_def unique_PPc_def)
  with IH have "WHATWHERE_Secure V"
    ..
  with uniPPspawn show "WHATWHERE_Secure [spawn⇘ι⇙ V]"
    by (metis Compositionality_Spawn)
next
  fix c1 c2
  assume IH1: "unique_PPc c1 ⟹ WHATWHERE_Secure [c1]"
  assume IH2: "unique_PPc c2 ⟹ WHATWHERE_Secure [c2]"
  assume uniPPc1c2: "unique_PPc (c1;c2)"
  from uniPPc1c2 have uniPPc1: "unique_PPc c1"
    by (simp add: unique_PPc_def)
  with IH1 have IS1: "WHATWHERE_Secure [c1]"
    .
  from uniPPc1c2 have uniPPc2: "unique_PPc c2"
    by (simp add: unique_PPc_def)
  with IH2 have IS2: "WHATWHERE_Secure [c2]"
    .

  from IS1 IS2 uniPPc1c2 show "WHATWHERE_Secure [c1;c2]"
    by (metis Compositionality_Seq)
next
  fix c b ι
  assume SC: "WhileSideCondition b"
  assume IH: "unique_PPc c ⟹ WHATWHERE_Secure [c]"
  assume uniPPwhile: "unique_PPc (while⇘ι⇙ b do c od)"
  hence "unique_PPc c"
    by (simp add: unique_PPc_def)
  with IH have "WHATWHERE_Secure [c]"
    .
  with uniPPwhile SC show "WHATWHERE_Secure [while⇘ι⇙ b do c od]"
    by (metis Compositionality_While semWhileSC)
next
  fix c1 c2 b ι
  assume SC: "IfSideCondition b c1 c2"  
  assume IH1: "unique_PPc c1 ⟹ WHATWHERE_Secure [c1]"
  assume IH2: "unique_PPc c2 ⟹ WHATWHERE_Secure [c2]"
  assume uniPPif: "unique_PPc (if⇘ι⇙ b then c1 else c2 fi)"
  from uniPPif have "unique_PPc c1"
    by (simp add: unique_PPc_def)
  with IH1 have IS1: "WHATWHERE_Secure [c1]"
    .
  from uniPPif have "unique_PPc c2"
    by (simp add: unique_PPc_def)
  with IH2 have IS2: "WHATWHERE_Secure [c2]"
    .
  from IS1 IS2 SC uniPPif show 
    "WHATWHERE_Secure [if⇘ι⇙ b then c1 else c2 fi]"
    by (metis Compositionality_If semIfSC)
next
  fix V
  assume IH: "∀i < length V. ⊢⇘𝒞⇙ V ! i ∧
    (unique_PPc (V!i) ⟶ WHATWHERE_Secure [V!i])"
  have "unique_PPV V ⟶ (∀i < length V. unique_PPc (V!i))"
    by (metis uniPPV_uniPPc)
  with IH have "unique_PPV V ⟶ (∀i < length V. WHATWHERE_Secure [V!i])" 
    by auto
  thus uniPPV: "unique_PPV V ⟶ WHATWHERE_Secure V"
    by (metis parallel_composition)
qed


theorem ComSecTyping_list_is_sound:
"⟦ ⊢⇘𝒱⇙ V; unique_PPV V ⟧ ⟹ WHATWHERE_Secure V"
by (metis ComSecTyping_single_is_sound parallel_cases 
  parallel_composition uniPPV_uniPPc)
  
end

end