Theory Parallel_Composition

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

locale WHATWHERE_Secure_Programs =
L? : MWLs_semantics "E" "BMap"
+ WWs? : WHATWHERE "MWLsSteps_det" "E" "pp" "DA" "lH"
for E :: "('exp, 'id, 'val) Evalfunction"
and BMap :: "'val ⇒ bool"
and DA :: "('id, 'd::order) DomainAssignment"
and lH :: "('d, 'exp) lHatches"
begin

lemma SdlHPPB_restricted_on_PP_is_SdlHPPB:
  assumes SdlHPPB: "SdlHPPB d PP R'"
  assumes inR': "(V,V) ∈ R'"
  assumes Rdef: "R = {(V',V''). (V',V'') ∈ R' 
    ∧ set (PPV V') ⊆ set (PPV V)
    ∧ set (PPV V'') ⊆ set (PPV V)}"
  shows "SdlHPPB d PP R"
proof (simp add: Strong_dlHPP_Bisimulation_def, auto)
  from SdlHPPB have "sym R'" 
    by (simp add: Strong_dlHPP_Bisimulation_def)
  with Rdef show "sym R" 
    by (simp add: sym_def)
next
  from SdlHPPB have "trans R'" 
    by (simp add: Strong_dlHPP_Bisimulation_def)
  with Rdef show "trans R" 
    by (simp add: trans_def, auto)
next
  fix V' V''
  assume inR_part: "(V',V'') ∈ R"
  with SdlHPPB Rdef show "length V' = length V''"
    by (simp add: Strong_dlHPP_Bisimulation_def, auto)
next
  fix V' V'' i
  assume inR_part: "(V',V'') ∈ R"
  assume irange: "i < length V'"
  assume notIDC: 
    "¬ IDC d (V'!i) (htchLoc (pp (V'!i)))"
  with SdlHPPB inR_part irange Rdef 
  show "NDC d (V'!i)"
    by (simp add: Strong_dlHPP_Bisimulation_def, auto)
next
  fix V' V'' i α p m1 m1' m2
  assume inR_part: "(V',V'') ∈ R"
  assume irange: "i < length V'"
  assume step: "⟨V'!i,m1⟩ →⊲α⊳ ⟨p,m2⟩"
  assume dhequal: "m1 ∼⇘d,(htchLocSet PP)⇙ m1'"
  
  from inR_part SdlHPPB Rdef have eqlen: "length V' = length V''"
    by (simp add: Strong_dlHPP_Bisimulation_def, auto)
  
  from inR_part Rdef 
  have "set (PPV V') ⊆ set (PPV V) ∧ set (PPV V'') ⊆ set (PPV V)"
    by auto
  
  with irange PPc_in_PPV_version eqlen
  have PPc_Vs_at_i: 
    "set (PPc (V'!i)) ⊆ set (PPV V) ∧ set (PPc (V''!i)) ⊆ set (PPV V)"
    by (metis subset_trans)
  
  from SdlHPPB inR_part Rdef irange step dhequal
    strongdlHPPB_aux[of "d" "PP" "R'" "i" 
    "V'" "V''" "m1" "α" "p" "m2" "m1'"]
  obtain p' α' m2' where stepreq: "⟨V''!i,m1'⟩ →⊲α'⊳ ⟨p',m2'⟩ ∧
    stepResultsinR p p' R' ∧ (α,α') ∈ R' ∧
    dhequality_alternative d PP (pp (V'!i)) m2 m2'"
    by auto
  have Rpp': "stepResultsinR p p' R"
  proof -
    {
      fix c c'
      assume step1: "⟨V'!i,m1⟩ →⊲α⊳ ⟨Some c,m2⟩"
      assume step2: "⟨V''!i,m1'⟩ →⊲α'⊳ ⟨Some c',m2'⟩"
      assume inR'_res: "([c],[c']) ∈ R'"
      
      from PPc_Vs_at_i step1 step2 PPsc_of_step
      have "set (PPc c) ⊆ set (PPV V) ∧ set (PPc c') ⊆ set (PPV V)"
        by (metis (no_types) option.sel xt1(6))
      
      with inR'_res Rdef have "([c],[c']) ∈ R"
        by auto
    }
    thus ?thesis      
      by (metis step stepResultsinR_def stepreq)
  qed
             
  have Rαα': "(α,α') ∈ R"
  proof - 
    from PPc_Vs_at_i step stepreq PPsα_of_step have 
      "set (PPV α) ⊆ set (PPV V) ∧ set (PPV α') ⊆ set (PPV V)"
      by (metis (no_types) xt1(6))
    with stepreq Rdef show ?thesis
      by auto
  qed
  
  from stepreq Rpp' Rαα' show 
    "∃p' α' m2'. ⟨V''!i,m1'⟩ →⊲α'⊳ ⟨p',m2'⟩ ∧
    stepResultsinR p p' R ∧ (α,α') ∈ R ∧
    dhequality_alternative d PP (pp (V'!i)) m2 m2'"
    by auto
qed


theorem parallel_composition:
  "⟦ ∀i < length V. WHATWHERE_Secure [V!i]; unique_PPV V ⟧
  ⟹ WHATWHERE_Secure V"
proof (simp add: WHATWHERE_Secure_def, induct V, auto)
  fix d PP
  from WHATWHERE_empty 
  show "∃R. SdlHPPB d PP R ∧ ([],[]) ∈ R"
    by (simp add: WHATWHERE_Secure_def)
next
  fix c V d PP
  assume IH: "⟦ ∀i < length V.
    ∀d PP. ∃R. SdlHPPB d PP R ∧ ([V!i],[V!i]) ∈ R;
    unique_PPV V ⟧
    ⟹ ∀d PP. ∃R. SdlHPPB d PP R ∧ (V,V) ∈ R"
  assume ISassump: "∀i < Suc (length V).
    ∀d PP. ∃R. SdlHPPB d PP R ∧ ([(c#V)!i],[(c#V)!i]) ∈ R"
  assume uniPPcV: "unique_PPV (c#V)"
  
  hence IHassump1: "unique_PPV V"
    by (simp add: unique_PPV_def)

  from uniPPcV have nocommonPP: "set (PPc c) ∩ set (PPV V) = {}"
    by (simp add: unique_PPV_def)
  
  from ISassump have IHassump2: "∀i < length V. 
    ∀d PP. ∃R. SdlHPPB d PP R ∧ ([V!i],[V!i]) ∈ R"
    by auto

  with IHassump1 IH obtain RV' where RV'assump:
    "SdlHPPB d PP RV' ∧ (V,V) ∈ RV'"
    by blast

  define RV where "RV = {(V',V''). (V',V'') ∈ RV' ∧ set (PPV V') ⊆ set (PPV V)
    ∧ set (PPV V'') ⊆ set (PPV V)}"

  with RV'assump RV_def SdlHPPB_restricted_on_PP_is_SdlHPPB
  have SdlHPPRV: "SdlHPPB d PP RV"
    by force

  from ISassump obtain Rc' where Rc'assump: 
    "SdlHPPB d PP Rc' ∧ ([c],[c]) ∈ Rc'"
    by (metis append_Nil drop_Nil neq0_conv not_Cons_self 
      nth_append_length Cons_nth_drop_Suc zero_less_Suc)
 
  define Rc where "Rc = {(V',V''). (V',V'') ∈ Rc' ∧ set (PPV V') ⊆ set (PPc c)
    ∧ set (PPV V'') ⊆ set (PPc c)}"

  with Rc'assump Rc_def SdlHPPB_restricted_on_PP_is_SdlHPPB
  have SdlHPPRc: "SdlHPPB d PP Rc"
    by force

  from nocommonPP have "Domain RV ∩ Domain Rc ⊆ {[]}"
    by (simp add: RV_def Rc_def, auto,
      metis Int_mono inf_commute inf_idem le_bot nocommonPP unique_V_uneq)

  with commonArefl_subset_commonDomain
  have Areflassump1: "Arefl RV ∩ Arefl Rc ⊆ {[]}"
    by force
    
  define R where "R = {(V',V''). ∃c c' W W'. V' = c#W ∧ V'' = c'#W' ∧ W ≠ []
    ∧ W' ≠ [] ∧ ([c],[c']) ∈ Rc ∧ (W,W') ∈ RV}"

  with RV_def RV'assump Rc_def Rc'assump have inR: 
    "V ≠ [] ⟹ (c#V,c#V) ∈ R"
    by auto
    
  from R_def Rc_def RV_def nocommonPP
  have "Domain R ∩ Domain (Rc ∪ RV) = {}"
    by (simp add: R_def Rc_def RV_def, auto,
      metis inf_bot_right le_inf_iff subset_empty unique_V_uneq,
      metis (opaque_lifting, no_types) inf_absorb1 inf_bot_right le_inf_iff unique_c_uneq)
            
  with commonArefl_subset_commonDomain
  have Areflassump2: "Arefl R ∩ Arefl (Rc ∪ RV) ⊆ {[]}"
    by force

  have disjuptoR: 
    "disj_dlHPP_Bisimulation_Up_To_R' d PP (Rc ∪ RV) R"
    proof (simp add: disj_dlHPP_Bisimulation_Up_To_R'_def, auto)
        from Areflassump1 SdlHPPRc SdlHPPRV Union_Strong_dlHPP_Bisim
        show "SdlHPPB d PP (Rc ∪ RV)"
          by force
      next
        from SdlHPPRV have symRV: "sym RV"
          by (simp add: Strong_dlHPP_Bisimulation_def)
        from SdlHPPRc have symRc: "sym Rc"
          by (simp add: Strong_dlHPP_Bisimulation_def)
        with symRV R_def show "sym R"
          by (simp add: sym_def, auto)
      next
        from SdlHPPRV have transRV: "trans RV"
          by (simp add: Strong_dlHPP_Bisimulation_def)
        from SdlHPPRc have transRc: "trans Rc"
          by (simp add: Strong_dlHPP_Bisimulation_def)
        show "trans R"
           proof -
            {
            fix V V' V''
            assume p1: "(V,V') ∈ R"
            assume p2: "(V',V'') ∈ R"
            have "(V,V'') ∈ R"
              proof -
                from p1 R_def obtain c c' W W' where p1assump:
                  "V = c#W ∧ V' = c'#W' ∧ W ≠ [] ∧ W' ≠ [] ∧
                  ([c],[c']) ∈ Rc ∧ (W,W') ∈ RV"
                  by auto
                with p2 R_def obtain c'' W'' where p2assump:
                  "V'' = c''#W'' ∧ W'' ≠ [] ∧
                  ([c'],[c'']) ∈ Rc ∧ (W',W'') ∈ RV"
                  by auto
                with p1assump transRc transRV have 
                  trans_assump: "([c],[c'']) ∈ Rc ∧ (W,W'') ∈ RV"
                  by (simp add: trans_def, blast)
                with p1assump p2assump R_def show ?thesis
                  by auto
              qed
             }
            thus ?thesis unfolding trans_def by blast
           qed
      next
        fix V V'
        assume "(V,V') ∈ R"
        with R_def SdlHPPRV show "length V = length V'"
          by (simp add: Strong_dlHPP_Bisimulation_def, auto)
      next
        fix V V' i
        assume inR: "(V,V') ∈ R"
        assume irange: "i < length V"
        assume notIDC: "¬ IDC d (V!i) 
          (htchLoc (pp (V!i)))"
        from inR R_def obtain c c' W W' where VV'assump:
          "V = c#W ∧ V'=c'#W' ∧ W ≠ [] ∧ W' ≠ [] ∧
          ([c],[c']) ∈ Rc ∧ (W,W') ∈ RV"
          by auto
        ― ‹Case separation for i›
        from VV'assump SdlHPPRc have Case_i0:
          "i = 0 ⟹ (NDC d (V!i) ∨
            IDC d (V!i) (htchLoc (pp (V!i))))"
          by (simp add: Strong_dlHPP_Bisimulation_def, auto)

        from VV'assump SdlHPPRV have "∀i < length W. 
          (NDC d (W!i) ∨
            IDC d (W!i) (htchLoc (pp (W!i))))"
          by (simp add: Strong_dlHPP_Bisimulation_def, auto)

        with irange VV'assump have Case_in0:
          "i > 0 ⟹ (NDC d (V!i) ∨ 
          IDC d (V!i) (htchLoc (pp (V!i))))"
          by simp
        from notIDC Case_i0 Case_in0 
        show "NDC d (V!i)"
          by auto
      next
        fix V V' m1 m1' m2 α p i
        assume inR: "(V,V') ∈ R"
        assume irange: "i < length V"
        assume step: "⟨V!i,m1⟩ →⊲α⊳ ⟨p,m2⟩"
        assume dhequal: "m1 ∼⇘d,(htchLocSet PP)⇙ m1'"
        
        from inR R_def obtain c c' W W' where VV'assump:
          "V = c#W ∧ V'=c'#W' ∧ W ≠ [] ∧ W' ≠ [] ∧
          ([c],[c']) ∈ Rc ∧ (W,W') ∈ RV"
          by auto
        ― ‹Case separation for i›
        from VV'assump SdlHPPRc strongdlHPPB_aux[of "d" "PP" 
          "Rc" "0" "[c]" "[c']"] step dhequal
        have Case_i0:
          "i = 0 ⟹ ∃p' α' m2'.
          ⟨V'!i,m1'⟩ →⊲α'⊳ ⟨p',m2'⟩ ∧
          stepResultsinR p p' (R ∪ (Rc ∪ RV)) ∧
          ((α,α') ∈ R ∨ (α,α') ∈ Rc ∨ (α,α') ∈ RV) ∧
          dhequality_alternative d PP (pp (V!i)) m2 m2'"
          by (simp add: stepResultsinR_def, blast)

        from step VV'assump irange have rewV: 
          "i > 0 ⟹ (i-Suc 0) < length W ∧ V!i = W!(i-Suc 0)"
          by simp

        with irange VV'assump step dhequal SdlHPPRV 
          strongdlHPPB_aux[of "d" "PP" "RV" _ "W" "W'"]
        have Case_in0:
          "i > 0 ⟹  ∃p' α' m2'.
          ⟨V'!i,m1'⟩ →⊲α'⊳ ⟨p',m2'⟩ ∧
          stepResultsinR p p' (R ∪ (Rc ∪ RV)) ∧
          ((α,α') ∈ R ∨ (α,α') ∈ Rc ∨ (α,α') ∈ RV) ∧
          dhequality_alternative d PP (pp (V!i)) m2 m2'"
          by (simp add: stepResultsinR_def, blast)
        
        from Case_i0 Case_in0 
        show "∃p' α' m2'.
          ⟨V'!i,m1'⟩ →⊲α'⊳ ⟨p',m2'⟩ ∧
          stepResultsinR p p' (R ∪ (Rc ∪ RV)) ∧
          ((α,α') ∈ R ∨ (α,α') ∈ Rc ∨ (α,α') ∈ RV) ∧
          dhequality_alternative d PP (pp (V!i)) m2 m2'"
          by auto
      qed
  with Areflassump2 Rc'assump Up_To_Technique
  show "∃R. SdlHPPB d PP R ∧ (c#V, c#V) ∈ R"
    by (metis UnCI inR)

qed

end

end