Theory Type_System

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

locale Type_System = 
  SSP? : Strongly_Secure_Programs "E" "BMap" "DA" 
  for E :: "('exp, 'id, 'val) Evalfunction"
  and BMap :: "'val ⇒ bool"
  and DA :: "('id, 'd::order) DomainAssignment"
+
fixes
AssignSideCondition :: "'id ⇒ 'exp ⇒ bool"
and WhileSideCondition :: "'exp ⇒ bool"
and IfSideCondition :: 
  "'exp ⇒ ('exp,'id) MWLfCom ⇒ ('exp,'id) MWLfCom ⇒ bool" 
assumes semAssignSC: "AssignSideCondition x e ⟹ e ≡⇘DA x⇙ e"
and semWhileSC: "WhileSideCondition e ⟹ ∀d. e ≡⇘d⇙ e"
and semIfSC: "IfSideCondition e c1 c2 ⟹ ∀d. e ≡⇘d⇙ e ∨ [c1] ≈⇘d⇙ [c2]"
begin

― ‹Security typing rules for the language commands›
inductive
ComSecTyping :: "('exp, 'id) MWLfCom ⇒ bool"
  (‹⊢⇘𝒞⇙ _›)
and ComSecTypingL :: "('exp,'id) MWLfCom list ⇒ bool"
   (‹⊢⇘𝒱⇙ _›)
where
skip: "⊢⇘𝒞⇙ skip" |
Assign: "⟦ AssignSideCondition x e ⟧ ⟹ ⊢⇘𝒞⇙ x := e" |
Fork: "⟦ ⊢⇘𝒞⇙ c; ⊢⇘𝒱⇙ V ⟧ ⟹ ⊢⇘𝒞⇙ fork c 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"

― ‹soundness proof of abstract type system›
theorem ComSecTyping_single_is_sound:
"⊢⇘𝒞⇙ c ⟹ Strongly_Secure [c]"
by (induct rule: ComSecTyping_ComSecTypingL.inducts(1)
    [of _ _ "Strongly_Secure"],
  auto simp add: Strongly_Secure_def,
  metis Strongly_Secure_Skip,
  metis Strongly_Secure_Assign semAssignSC,
  metis Compositionality_Fork,
  metis Compositionality_Seq,
  metis Compositionality_While semWhileSC,
  metis Compositionality_If semIfSC,
  metis parallel_composition)

theorem ComSecTyping_list_is_sound:
"⊢⇘𝒱⇙ V ⟹ Strongly_Secure V"
by (metis ComSecTyping_single_is_sound Strongly_Secure_def 
  parallel_composition parallel_cases)

end

end