Theory TopoS_Stateful_Policy

theory TopoS_Stateful_Policy
imports TopoS_Composition_Theory
begin

section‹Stateful Policy›


text‹Details described in \<^cite>‹"diekmann2014esss"›.›


text‹Algorithm›
term TopoS_Composition_Theory.generate_valid_topology
text‹generates a valid high-level topology. Now we discuss how to turn this into
       a stateful policy.›

text‹
Example:
  SensorNode produces data and has no security level.
  SensorSink has high security level
  SensorNode -> SensorSink, but not the other way round.
  Implementation: UDP in one direction

  Alice is in internal protected subnet. Google can not arbitrarily access Alice.
  Alice sends requests to google.
  It is desirable that Alice gets the response back
  Implementation: TCP and stateful packet filter that allows, once Alice establishes a connection, to get a response back via this connection.

Result:
  IFS violations undesirable.
  ACS violations may be okay under certain conditions.
›

term all_security_requirements_fulfilled

text‹@{term "G = (V, E⇩f⇩i⇩x, E⇩s⇩t⇩a⇩t⇩e)"}›
record 'v stateful_policy =
    hosts :: "'v set" ― ‹nodes, vertices›
    flows_fix :: "('v ×'v) set" ― ‹edges in high-level policy›
    flows_state :: "('v ×'v) set" ― ‹edges that can have stateful flows, i.e. backflows›

text‹All the possible ways packets can travel in a @{typ "'v stateful_policy"}.
        They can either choose the fixed links;
        Or use a stateful link, i.e. establish state.
        Once state is established, packets can flow back via the established link.›
definition all_flows :: "'v stateful_policy ⇒ ('v × 'v) set" where
  "all_flows 𝒯 ≡ flows_fix 𝒯 ∪ flows_state 𝒯 ∪ backflows (flows_state 𝒯)"


definition stateful_policy_to_network_graph :: "'v stateful_policy ⇒ 'v graph" where
  "stateful_policy_to_network_graph 𝒯 = ⦇ nodes = hosts 𝒯, edges = all_flows 𝒯 ⦈"


text‹@{typ "'v stateful_policy"} syntactically well-formed›
locale wf_stateful_policy = 
  fixes 𝒯 :: "'v stateful_policy"
  assumes E_wf: "fst ` (flows_fix 𝒯) ⊆ (hosts 𝒯)"
                   "snd ` (flows_fix 𝒯) ⊆ (hosts 𝒯)"
  and E_state_fix: "flows_state 𝒯 ⊆ flows_fix 𝒯"
  and finite_Hosts: "finite (hosts 𝒯)"
begin

  lemma E_wfD: assumes "(v,v') ∈ flows_fix 𝒯"
    shows "v ∈ hosts 𝒯" "v' ∈ hosts 𝒯"
    apply -
     apply (rule subsetD[OF E_wf(1)])
     using assms apply force
    apply (rule subsetD[OF E_wf(2)])
    using assms apply force
    done
 
  lemma E_state_valid: "fst ` (flows_state 𝒯) ⊆ (hosts 𝒯)"
                       "snd ` (flows_state 𝒯) ⊆ (hosts 𝒯)"
   apply -
   using E_wf(1) E_state_fix apply(blast)
   using E_wf(2) E_state_fix apply(blast)
   done

  lemma E_state_validD: assumes "(v,v') ∈ flows_state 𝒯"
    shows "v ∈ hosts 𝒯" "v' ∈ hosts 𝒯"
    apply -
     apply (rule subsetD[OF E_state_valid(1)])
     using assms apply force
    apply (rule subsetD[OF E_state_valid(2)])
    using assms apply force
    done

  lemma finite_fix: "finite (flows_fix 𝒯)"
  proof -
    from finite_subset[OF E_wf(1) finite_Hosts] have 1: "finite (fst ` flows_fix 𝒯)" .
    from finite_subset[OF E_wf(2) finite_Hosts] have 2: "finite (snd ` flows_fix 𝒯)" .
    have s: "flows_fix 𝒯 ⊆ (fst ` flows_fix 𝒯 × snd ` flows_fix 𝒯)" by force
    from finite_cartesian_product[OF 1 2] have "finite (fst ` flows_fix 𝒯 × snd ` flows_fix 𝒯)" .
    from finite_subset[OF s this] show ?thesis .
  qed

  lemma finite_state: "finite (flows_state 𝒯)"
    using finite_subset[OF E_state_fix finite_fix] by assumption


  lemma finite_backflows_state: "finite (backflows (flows_state 𝒯))"
    using [[simproc add: finite_Collect]] by(simp add: backflows_def finite_state)

  lemma E_state_backflows_wf: "fst ` backflows (flows_state 𝒯) ⊆ (hosts 𝒯)"
                         "snd ` backflows (flows_state 𝒯) ⊆ (hosts 𝒯)"
    by(auto simp add: backflows_def E_state_valid E_state_validD)

end


text‹Minimizing stateful flows such that only newly added backflows remain›
  definition filternew_flows_state :: "'v stateful_policy ⇒ ('v × 'v) set" where
    "filternew_flows_state 𝒯 ≡ {(s, r) ∈ flows_state 𝒯. (r, s) ∉ flows_fix 𝒯}"

  lemma filternew_subseteq_flows_state: "filternew_flows_state 𝒯 ⊆ flows_state 𝒯"
    by(auto simp add: filternew_flows_state_def)

  ― ‹alternative definitions, all are equal›
  lemma filternew_flows_state_alt: "filternew_flows_state 𝒯  = flows_state 𝒯 - (backflows (flows_fix 𝒯))"
    apply(simp add: backflows_def filternew_flows_state_def)
    apply(rule)
     apply blast+
    done
  lemma filternew_flows_state_alt2: "filternew_flows_state 𝒯  = {e ∈ flows_state 𝒯. e ∉ backflows (flows_fix 𝒯)}"
    apply(simp add: backflows_def filternew_flows_state_def)
    apply(rule)
     apply blast+
    done
  lemma backflows_filternew_flows_state: "backflows (filternew_flows_state 𝒯) = (backflows (flows_state 𝒯)) - (flows_fix 𝒯)"
    by(simp add: filternew_flows_state_alt backflows_minus_backflows)

  lemma stateful_policy_to_network_graph_filternew: "⟦ wf_stateful_policy 𝒯 ⟧ ⟹ 
    stateful_policy_to_network_graph 𝒯 = 
    stateful_policy_to_network_graph ⦇hosts = hosts 𝒯, flows_fix = flows_fix 𝒯, flows_state = filternew_flows_state 𝒯 ⦈"
    apply(drule wf_stateful_policy.E_state_fix)
    apply(simp add: stateful_policy_to_network_graph_def all_flows_def)
    apply(rule Set.equalityI)
     apply(simp add: filternew_flows_state_def backflows_def)
     apply(rule, blast)+
    apply(simp add: filternew_flows_state_def backflows_def)
    apply fastforce
    done

  lemma backflows_filternew_disjunct_flows_fix: 
    "∀ b ∈ (backflows (filternew_flows_state 𝒯)). b ∉ flows_fix 𝒯"
    by(simp add: filternew_flows_state_def backflows_def)





text‹Given a high-level policy, we can construct a pretty large syntactically valid low level policy. However, the stateful policy will
       almost certainly violate security requirements!›
  lemma "wf_graph G ⟹ wf_stateful_policy ⦇ hosts = nodes G, flows_fix = nodes G × nodes G, flows_state = nodes G × nodes G ⦈"
    by(simp add: wf_stateful_policy_def wf_graph_def)


text‹@{const wf_stateful_policy} implies @{term wf_graph}›
  lemma wf_stateful_policy_is_wf_graph: "wf_stateful_policy 𝒯 ⟹ wf_graph ⦇nodes = hosts 𝒯, edges = all_flows 𝒯⦈"
    apply(frule wf_stateful_policy.E_state_backflows_wf)
    apply(frule wf_stateful_policy.E_state_backflows_wf(2))
    apply(frule wf_stateful_policy.E_state_valid)
    apply(frule wf_stateful_policy.E_state_valid(2))
    apply(frule wf_stateful_policy.E_wf)
    apply(frule wf_stateful_policy.E_wf(2))
    apply(simp add: all_flows_def wf_graph_def wf_stateful_policy_def 
          wf_stateful_policy.finite_fix wf_stateful_policy.finite_state wf_stateful_policy.finite_backflows_state)
    apply(rule conjI)
     apply (metis image_Un sup.bounded_iff)+
    done


(*we use the second way of writing it in the paper*)
lemma "(∀F ∈ get_offending_flows (get_ACS M) (stateful_policy_to_network_graph 𝒯 ). F ⊆ backflows (filternew_flows_state 𝒯)) ⟷
    ⋃(get_offending_flows (get_ACS M) (stateful_policy_to_network_graph 𝒯)) ⊆ (backflows (flows_state 𝒯)) - (flows_fix 𝒯)"
    by(simp add: filternew_flows_state_alt backflows_minus_backflows, blast)


text‹When is a stateful policy @{term "𝒯"} compliant with a high-level policy @{term "G"} and the security requirements @{term "M"}?›
locale stateful_policy_compliance =  
  fixes 𝒯 :: "('v::vertex) stateful_policy"
  fixes G :: "'v graph"
  fixes M :: "('v) SecurityInvariant_configured list"
  assumes
    ― ‹the graph must be syntactically valid›
    wfG: "wf_graph G"
    and
    ― ‹security requirements must be valid›
    validReqs: "valid_reqs M"
    and
    ― ‹the high-level policy must be valid›
    high_level_policy_valid: "all_security_requirements_fulfilled M G"
    and
    ― ‹the stateful policy must be syntactically valid›
    stateful_policy_wf:
    "wf_stateful_policy 𝒯"
    and
    ― ‹the stateful policy must talk about the same nodes as the high-level policy›
    hosts_nodes:
    "hosts 𝒯 = nodes G"
    and
    ― ‹only flows that are allowed in the high-level policy are allowed in the stateful policy›
    flows_edges:
    "flows_fix 𝒯 ⊆ edges G"
    and
    ― ‹the low level policy must comply with the high-level policy›
      ― ‹all information flow strategy requirements must be fulfilled, i.e. no leaks!›
      compliant_stateful_IFS: 
        "all_security_requirements_fulfilled (get_IFS M) (stateful_policy_to_network_graph 𝒯)"
      and
      ― ‹No Access Control side effects must occur›
      compliant_stateful_ACS: 
        "∀F ∈ get_offending_flows (get_ACS M) (stateful_policy_to_network_graph 𝒯 ). F ⊆ backflows (filternew_flows_state 𝒯)"
        
  begin
    lemma compliant_stateful_ACS_no_side_effects_filternew_helper: 
      "∀ E ⊆ backflows (filternew_flows_state 𝒯). ∀ F ∈ get_offending_flows (get_ACS M) ⦇ nodes = hosts 𝒯, edges = flows_fix 𝒯 ∪ E ⦈. F ⊆ E"
    proof(rule, rule)
      fix E
      assume a1: "E ⊆ backflows (filternew_flows_state 𝒯)"
      from validReqs have valid_ReqsACS: "valid_reqs (get_ACS M)" by(simp add: get_ACS_def valid_reqs_def)

      from compliant_stateful_ACS stateful_policy_to_network_graph_filternew[OF stateful_policy_wf] have compliant_stateful_ACS_only_state_violations_filternew: 
      "∀F ∈ get_offending_flows (get_ACS M) (stateful_policy_to_network_graph ⦇hosts = hosts 𝒯, flows_fix = flows_fix 𝒯, flows_state = filternew_flows_state 𝒯 ⦈). F ⊆ backflows (filternew_flows_state 𝒯)" by simp
    
      from wf_stateful_policy_is_wf_graph[OF stateful_policy_wf] have wfGfilternew: 
        "wf_graph ⦇nodes = hosts 𝒯, edges = flows_fix 𝒯 ∪ filternew_flows_state 𝒯 ∪ backflows (filternew_flows_state 𝒯)⦈"
        apply(simp add: all_flows_def filternew_flows_state_alt backflows_minus_backflows)
        by(auto simp add: wf_graph_def)
    
      from wf_stateful_policy.E_state_fix[OF stateful_policy_wf] filternew_subseteq_flows_state have flows_fix_un_filternew_simp: "flows_fix 𝒯 ∪ filternew_flows_state 𝒯 = flows_fix 𝒯" by blast
    
      from compliant_stateful_ACS_only_state_violations_filternew have 
        "⋀m. m ∈ set (get_ACS M) ⟹ 
        ⋃(c_offending_flows m ⦇nodes = hosts 𝒯, edges = flows_fix 𝒯 ∪ filternew_flows_state 𝒯 ∪ backflows (filternew_flows_state 𝒯)⦈) ⊆ backflows (filternew_flows_state 𝒯)"
        by(simp add: stateful_policy_to_network_graph_def all_flows_def get_offending_flows_def, blast)
    
      ― ‹idea: use @{thm compliant_stateful_ACS} with the @{thm configured_SecurityInvariant.Un_set_offending_flows_bound_minus_subseteq} 
        lemma and substract @{term "backflows (filternew_flows_state 𝒯) - E"}, on the right hand side @{term E} remains, as Graph's edges @{term "flows_fix 𝒯  ∪ E"} remains›

      from configured_SecurityInvariant.Un_set_offending_flows_bound_minus_subseteq[where X="backflows (filternew_flows_state 𝒯)", OF _ wfGfilternew this]
        ‹valid_reqs (get_ACS M)›
        have
        "⋀ m E. m ∈ set (get_ACS M) ⟹
        ∀F∈c_offending_flows m ⦇nodes = hosts 𝒯, edges = flows_fix 𝒯 ∪ filternew_flows_state 𝒯 ∪ backflows (filternew_flows_state 𝒯) - E⦈. F ⊆ backflows (filternew_flows_state 𝒯) - E"
        by(auto simp add: all_flows_def valid_reqs_def)
      from this flows_fix_un_filternew_simp have rule:
        "⋀ m E. m ∈ set (get_ACS M) ⟹
        ∀F∈c_offending_flows m ⦇nodes = hosts 𝒯, edges = flows_fix 𝒯 ∪ backflows (filternew_flows_state 𝒯) - E⦈. F ⊆ backflows (filternew_flows_state 𝒯) - E"  
        by simp
    
      from  backflows_finite rev_finite_subset[OF wf_stateful_policy.finite_state[OF stateful_policy_wf] filternew_subseteq_flows_state] have
        "finite (backflows (filternew_flows_state 𝒯))" by blast
      from a1 this have "finite E" by (metis rev_finite_subset)
    
      from a1 obtain E' where E'_prop1: "backflows (filternew_flows_state 𝒯) - E' = E" and E'_prop2: "E' = backflows (filternew_flows_state 𝒯) - E" by blast
      from E'_prop2 ‹finite (backflows (filternew_flows_state 𝒯))› ‹finite E› have "finite E'" by blast
    
      from Set.double_diff[where B="backflows (filternew_flows_state 𝒯)" and C="backflows (filternew_flows_state 𝒯)" and A="E", OF a1, simplified] have Ebackflowssimp:
        "backflows (filternew_flows_state 𝒯) - (backflows (filternew_flows_state 𝒯) - E) = E" .
    
      have "flows_fix 𝒯 ∪ backflows (filternew_flows_state 𝒯) - (backflows (filternew_flows_state 𝒯) - E) = 
          (flows_fix 𝒯 - (backflows (filternew_flows_state 𝒯))) ∪ E"
          apply(simp add: Set.Un_Diff)
          apply(simp add: Ebackflowssimp)
          by blast
      also have "(flows_fix 𝒯 - (backflows (filternew_flows_state 𝒯))) ∪ E = flows_fix 𝒯  ∪ E" using backflows_filternew_disjunct_flows_fix by blast
      finally have flows_E_simp: "flows_fix 𝒯 ∪ backflows (filternew_flows_state 𝒯) - (backflows (filternew_flows_state 𝒯) - E) = flows_fix 𝒯  ∪ E" .
    
      from rule[simplified E'_prop1 E'_prop2] have
      "⋀m. m ∈ set (get_ACS M) ⟹
      ∀F∈c_offending_flows m ⦇nodes = hosts 𝒯, edges = flows_fix 𝒯 ∪ backflows (filternew_flows_state 𝒯) - (backflows (filternew_flows_state 𝒯) - E)⦈.
       F ⊆ backflows (filternew_flows_state 𝒯) - (backflows (filternew_flows_state 𝒯) - E)"
       by(simp)
      from this Ebackflowssimp flows_E_simp have
      "⋀m. m ∈ set (get_ACS M) ⟹
        ∀F∈c_offending_flows m ⦇nodes = hosts 𝒯, edges = flows_fix 𝒯 ∪ E⦈. F ⊆ E"
       by simp
      thus  "∀F∈get_offending_flows (get_ACS M) ⦇nodes = hosts 𝒯, edges = flows_fix 𝒯 ∪ E⦈. F ⊆ E"
        by(simp add: get_offending_flows_def)
      qed
    
    
    theorem compliant_stateful_ACS_no_side_effects:
      "∀ E ⊆ backflows (flows_state 𝒯). ∀ F ∈ get_offending_flows(get_ACS M) ⦇ nodes = hosts 𝒯, edges = flows_fix 𝒯 ∪ E ⦈. F ⊆ E"
    proof -
      from compliant_stateful_ACS stateful_policy_to_network_graph_filternew[OF stateful_policy_wf] have a1: 
      "∀F ∈ get_offending_flows (get_ACS M) (stateful_policy_to_network_graph ⦇hosts = hosts 𝒯, flows_fix = flows_fix 𝒯, flows_state = filternew_flows_state 𝒯 ⦈). F ⊆ backflows (filternew_flows_state 𝒯)" by simp
    
      have backflows_split: "backflows (filternew_flows_state 𝒯) ∪ (backflows (flows_state 𝒯) - backflows (filternew_flows_state 𝒯)) = backflows (flows_state 𝒯)"
        by (metis Diff_subset Un_Diff_cancel Un_absorb1 backflows_minus_backflows filternew_flows_state_alt)
    
      have 
        "∀E⊆backflows (filternew_flows_state 𝒯) ∪ (backflows (flows_state 𝒯) - backflows (filternew_flows_state 𝒯)). 
             ∀F∈get_offending_flows (get_ACS M) ⦇nodes = hosts 𝒯, edges = flows_fix 𝒯 ∪ E⦈. F ⊆ E"
        proof(rule allI, rule impI)
          fix E
          assume h1: "E ⊆ backflows (filternew_flows_state 𝒯) ∪ (backflows (flows_state 𝒯) - backflows (filternew_flows_state 𝒯))"
    
          have "∃ E1 E2. E1 ⊆ backflows (filternew_flows_state 𝒯) ∧ E2 ⊆ (backflows (flows_state 𝒯) - backflows (filternew_flows_state 𝒯)) ∧ E1 ∪ E2 = E ∧ E1 ∩ E2 = {}"
            apply(rule_tac x="{e ∈ E. e ∈ backflows (filternew_flows_state 𝒯)}" in exI)
            apply(rule_tac x="{e ∈ E. e ∈(backflows (flows_state 𝒯) - backflows (filternew_flows_state 𝒯))}" in exI)
            apply(simp)
            apply(rule)
             apply blast
            apply(rule)
             apply blast
            apply(rule)
             using h1 apply blast
            using backflows_filternew_disjunct_flows_fix by blast
    
          from this obtain E1 E2 where E1_prop: "E1 ⊆ backflows (filternew_flows_state 𝒯)" and E2_prop: "E2 ⊆ (backflows (flows_state 𝒯) - backflows (filternew_flows_state 𝒯))" and "E = E1 ∪ E2" and "E1 ∩ E2 = {}" by blast
    
          ― ‹the stateful flows are @{text "⊆"} fix flows. If substracting the new stateful flows, onyly the existing fix flows remain›
          from E2_prop filternew_flows_state_alt have "E2 ⊆ flows_fix 𝒯" by (metis (opaque_lifting, no_types) Diff_subset_conv Un_Diff_cancel2 backflows_minus_backflows inf_sup_ord(3) order.trans)
          ― ‹hence, E2 disappears›
          from Set.Un_absorb1[OF this] have E2_absorb: "flows_fix 𝒯 ∪ E2 = flows_fix 𝒯" by blast
    
          from ‹E = E1 ∪ E2› have E2E1eq: "E2 ∪ E1 = E" by blast
    
          from ‹E = E1 ∪ E2› ‹E1 ∩ E2 = {}› have "E1 ⊆ E" by simp
    
          from compliant_stateful_ACS_no_side_effects_filternew_helper E1_prop have "∀F∈get_offending_flows (get_ACS M) ⦇nodes = hosts 𝒯, edges = flows_fix 𝒯 ∪ E1 ⦈. F ⊆ E1" by simp
          hence "∀F∈get_offending_flows (get_ACS M) ⦇nodes = hosts 𝒯, edges = flows_fix 𝒯 ∪ E2 ∪ E1 ⦈. F ⊆ E1" using E2_absorb[symmetric] by simp
          hence "∀F∈get_offending_flows (get_ACS M) ⦇nodes = hosts 𝒯, edges = flows_fix 𝒯 ∪ E ⦈. F ⊆ E1" using E2E1eq by (metis Un_assoc)
    
          from this ‹E1 ⊆ E› show "∀F∈get_offending_flows (get_ACS M) ⦇nodes = hosts 𝒯, edges = flows_fix 𝒯 ∪ E⦈. F ⊆ E" by blast
        qed
    
      from this backflows_split show ?thesis by presburger
    qed


    corollary compliant_stateful_ACS_no_side_effects': "∀ E ⊆ backflows (flows_state 𝒯). ∀ F ∈ get_offending_flows(get_ACS M) ⦇ nodes = hosts 𝒯, edges = flows_fix 𝒯 ∪ flows_state 𝒯 ∪ E ⦈. F ⊆ E"
      using compliant_stateful_ACS_no_side_effects wf_stateful_policy.E_state_fix[OF stateful_policy_wf] by (metis Un_absorb2)


    text‹The high level graph generated from the low level policy is a valid graph›
    lemma valid_stateful_policy: "wf_graph ⦇nodes = hosts 𝒯, edges = all_flows 𝒯⦈"
      by(rule wf_stateful_policy_is_wf_graph,fact stateful_policy_wf)

    text‹The security requirements are definitely fulfilled if we consider only the fixed flows and the
           normal direction of the stateful flows (i.e. no backflows).
           I.e. considering no states, everything must be fulfilled›
    lemma compliant_stateful_ACS_static_valid: "all_security_requirements_fulfilled (get_ACS M) ⦇ nodes = hosts 𝒯, edges = flows_fix 𝒯  ⦈"
    proof -
      from validReqs have valid_ReqsACS: "valid_reqs (get_ACS M)" by(simp add: get_ACS_def valid_reqs_def)
      from wfG hosts_nodes[symmetric] have wfG': "wf_graph ⦇ nodes = hosts 𝒯, edges = edges G  ⦈" by(case_tac G, simp)
      from high_level_policy_valid have "all_security_requirements_fulfilled (get_ACS M) G"
        by(simp add: get_ACS_def all_security_requirements_fulfilled_def)
      from this hosts_nodes[symmetric] have "all_security_requirements_fulfilled (get_ACS M) ⦇ nodes = hosts 𝒯, edges = edges G  ⦈"
        by(case_tac G, simp)
      from all_security_requirements_fulfilled_mono[OF valid_ReqsACS flows_edges wfG' this] show ?thesis .
    qed
    theorem compliant_stateful_ACS_static_valid':
      "all_security_requirements_fulfilled M ⦇ nodes = hosts 𝒯, edges = flows_fix 𝒯 ∪ flows_state 𝒯  ⦈"
      proof -
        from validReqs have valid_ReqsIFS: "valid_reqs (get_IFS M)" by(simp add: get_IFS_def valid_reqs_def)
    
        ― ‹show that it holds for IFS, by monotonicity as it holds for more in IFS›
        from all_security_requirements_fulfilled_mono[OF valid_ReqsIFS _ valid_stateful_policy compliant_stateful_IFS[unfolded stateful_policy_to_network_graph_def]] have
          goalIFS: "all_security_requirements_fulfilled (get_IFS M) ⦇ nodes = hosts 𝒯, edges = flows_fix 𝒯 ∪ flows_state 𝒯  ⦈" by(simp add: all_flows_def)

        from wf_stateful_policy.E_state_fix[OF stateful_policy_wf] have "flows_fix 𝒯 ∪ flows_state 𝒯 =  flows_fix 𝒯" by blast
        from this compliant_stateful_ACS_static_valid have goalACS:
          "all_security_requirements_fulfilled (get_ACS M) ⦇ nodes = hosts 𝒯, edges = flows_fix 𝒯 ∪ flows_state 𝒯  ⦈" by simp
          
        ― ‹ACS and IFS together form M, we know it holds for ACS›
        from goalACS goalIFS show ?thesis 
          apply(simp add: all_security_requirements_fulfilled_def get_IFS_def get_ACS_def)
          by fastforce
    qed

    text‹The flows with state are a subset of the flows allowed by the policy›
    theorem flows_state_edges: "flows_state 𝒯 ⊆ edges G"
      using wf_stateful_policy.E_state_fix[OF stateful_policy_wf] flows_edges by simp


    text‹All offending flows are subsets of the reveres stateful flows›
    lemma compliant_stateful_ACS_only_state_violations:
      "∀F ∈ get_offending_flows (get_ACS M) (stateful_policy_to_network_graph 𝒯). F ⊆ backflows (flows_state 𝒯)"
      proof -
        have "backflows (filternew_flows_state 𝒯) ⊆ backflows (flows_state 𝒯)" by (metis Diff_subset backflows_minus_backflows filternew_flows_state_alt)
        from compliant_stateful_ACS this have 
          "∀ F ∈ get_offending_flows (get_ACS M) (stateful_policy_to_network_graph 𝒯). F ⊆ backflows (flows_state 𝒯)"
          by (metis subset_trans)
        thus ?thesis .
      qed
    theorem compliant_stateful_ACS_only_state_violations': "∀F ∈ get_offending_flows M (stateful_policy_to_network_graph 𝒯). F ⊆ backflows (flows_state 𝒯)"
      proof -
        from validReqs have valid_ReqsIFS: "valid_reqs (get_IFS M)" by(simp add: get_IFS_def valid_reqs_def)
        have offending_split: "⋀G. get_offending_flows M G = (get_offending_flows (get_IFS M) G ∪ get_offending_flows (get_ACS M) G)"
          apply(simp add: get_offending_flows_def get_IFS_def get_ACS_def) by blast 
       show ?thesis
        apply(subst offending_split)
        using compliant_stateful_ACS_only_state_violations 
              all_security_requirements_fulfilled_imp_get_offending_empty[OF valid_ReqsIFS compliant_stateful_IFS]
        by auto
      qed


    text ‹All violations are backflows of valid flows›
    corollary compliant_stateful_ACS_only_state_violations_union: "⋃(get_offending_flows (get_ACS M) (stateful_policy_to_network_graph 𝒯)) ⊆ backflows (flows_state 𝒯)"
    using compliant_stateful_ACS_only_state_violations by fastforce

    corollary compliant_stateful_ACS_only_state_violations_union': "⋃(get_offending_flows M (stateful_policy_to_network_graph 𝒯)) ⊆ backflows (flows_state 𝒯)"
    using compliant_stateful_ACS_only_state_violations' by fastforce

    text‹All individual flows cause no side effects, i.e. each backflow causes at most itself as violation, no other
           side-effect violations are induced.›
    lemma  compliant_stateful_ACS_no_state_singleflow_side_effect:
      "∀ (v⇩1, v⇩2) ∈ backflows (flows_state 𝒯). 
       ⋃(get_offending_flows(get_ACS M) ⦇ nodes = hosts 𝒯, edges = flows_fix 𝒯 ∪ flows_state 𝒯 ∪ {(v⇩1, v⇩2)} ⦈) ⊆ {(v⇩1, v⇩2)}"
    using compliant_stateful_ACS_no_side_effects' by blast
  end


subsection‹Summarizing the important theorems›

  text‹No information flow security requirements are violated (including all added stateful flows)›
  thm stateful_policy_compliance.compliant_stateful_IFS
  
  
  text‹There are not access control side effects when allowing stateful backflows. 
          I.e. for all possible subsets of the to-allow backflows, the violations they cause are only these backflows themselves›
  thm stateful_policy_compliance.compliant_stateful_ACS_no_side_effects'
  
    text‹Also, considering all backflows individually, they cause no side effect, i.e. the only violation added is the backflow itself›
    thm stateful_policy_compliance.compliant_stateful_ACS_no_state_singleflow_side_effect
  
    text‹In particular, all introduced offending flows for access control strategies are at most the stateful backflows›
    thm stateful_policy_compliance.compliant_stateful_ACS_only_state_violations_union
    text‹Which implies: all introduced offending flows are at most the stateful backflows›
    thm stateful_policy_compliance.compliant_stateful_ACS_only_state_violations_union'
    
  
  text‹Disregarding the backflows of stateful flows, all security requirements are fulfilled.›
  thm stateful_policy_compliance.compliant_stateful_ACS_static_valid'


 
end