Theory TopoS_Stateful_Policy_Algorithm
theory TopoS_Stateful_Policy_Algorithm
imports TopoS_Stateful_Policy TopoS_Composition_Theory
begin
section‹Stateful Policy -- Algorithm›
subsection‹Some unimportant lemmata›
lemma False_set: "{(r, s). False} = {}" by simp
lemma valid_reqs_ACS_D: "valid_reqs M ⟹ valid_reqs (get_ACS M)"
by(simp add: valid_reqs_def get_ACS_def)
lemma valid_reqs_IFS_D: "valid_reqs M ⟹ valid_reqs (get_IFS M)"
by(simp add: valid_reqs_def get_IFS_def)
lemma all_security_requirements_fulfilled_ACS_D: "all_security_requirements_fulfilled M G ⟹
all_security_requirements_fulfilled (get_ACS M) G"
by(simp add: all_security_requirements_fulfilled_def get_ACS_def)
lemma all_security_requirements_fulfilled_IFS_D: "all_security_requirements_fulfilled M G ⟹
all_security_requirements_fulfilled (get_IFS M) G"
by(simp add: all_security_requirements_fulfilled_def get_IFS_def)
lemma all_security_requirements_fulfilled_mono_stateful_policy_to_network_graph:
"⟦ valid_reqs M; E' ⊆ E; wf_graph ⦇ nodes = V, edges = Efix ∪ E ⦈ ⟧ ⟹
all_security_requirements_fulfilled M
(stateful_policy_to_network_graph ⦇ hosts = V, flows_fix = Efix, flows_state = E ⦈)⟹
all_security_requirements_fulfilled M
(stateful_policy_to_network_graph ⦇ hosts = V, flows_fix = Efix, flows_state = E' ⦈)"
apply(simp add: stateful_policy_to_network_graph_def all_flows_def)
apply(drule all_security_requirements_fulfilled_mono[where E="Efix ∪ E ∪ backflows E" and E'="Efix ∪ E' ∪ backflows E'" and V="V"])
apply(thin_tac "wf_graph G" for G)
apply(thin_tac "all_security_requirements_fulfilled M G" for M G)
apply(simp add: backflows_def, blast)
apply(thin_tac "all_security_requirements_fulfilled M G" for M G)
apply(simp add: wf_graph_def)
apply(simp add: backflows_def)
using [[simproc add: finite_Collect]] apply(auto)[1]
apply(simp_all)
done
subsection ‹Sketch for generating a stateful policy from a simple directed policy›
text‹Having no stateful flows, we trivially get a valid stateful policy.›
lemma trivial_stateful_policy_compliance:
"⟦ wf_graph ⦇ nodes = V, edges = E ⦈; valid_reqs M; all_security_requirements_fulfilled M ⦇ nodes = V, edges = E ⦈ ⟧ ⟹
stateful_policy_compliance ⦇ hosts = V, flows_fix = E, flows_state = {} ⦈ ⦇ nodes = V, edges = E ⦈ M"
apply(unfold_locales)
apply(simp_all add: wf_graph_def stateful_policy_to_network_graph_def all_flows_def backflows_def False_set)
apply(simp add: get_IFS_def get_ACS_def all_security_requirements_fulfilled_def)
apply(clarify)
apply(drule valid_reqs_ACS_D)
apply(drule all_security_requirements_fulfilled_ACS_D)
apply(drule(1) all_security_requirements_fulfilled_imp_get_offending_empty)
by force
text‹trying better›
text‹First, filtering flows that cause no IFS violations›
fun filter_IFS_no_violations_accu :: "'v::vertex graph ⇒ 'v SecurityInvariant_configured list ⇒ ('v × 'v) list ⇒ ('v × 'v) list ⇒ ('v × 'v) list" where
"filter_IFS_no_violations_accu G M accu [] = accu" |
"filter_IFS_no_violations_accu G M accu (e#Es) = (if
all_security_requirements_fulfilled (get_IFS M) (stateful_policy_to_network_graph ⦇ hosts = nodes G, flows_fix = edges G, flows_state = set (e#accu) ⦈)
then filter_IFS_no_violations_accu G M (e#accu) Es
else filter_IFS_no_violations_accu G M accu Es)"
definition filter_IFS_no_violations :: "'v::vertex graph ⇒ 'v SecurityInvariant_configured list ⇒ ('v × 'v) list ⇒ ('v × 'v) list" where
"filter_IFS_no_violations G M Es = filter_IFS_no_violations_accu G M [] Es"
lemma filter_IFS_no_violations_subseteq_input: "set (filter_IFS_no_violations G M Es) ⊆ set Es"
apply(subgoal_tac "∀ accu. set (filter_IFS_no_violations_accu G M accu Es) ⊆ set Es ∪ set accu")
apply(erule_tac x="[]" in allE)
apply(simp add: filter_IFS_no_violations_def)
unfolding filter_IFS_no_violations_def
apply(induct_tac Es)
apply(simp_all)
apply force
done
lemma filter_IFS_no_violations_accu_correct_induction: "valid_reqs (get_IFS M) ⟹ wf_graph ⦇ nodes = V, edges = E ⦈ ⟹
all_security_requirements_fulfilled (get_IFS M) (stateful_policy_to_network_graph ⦇ hosts = V, flows_fix = E, flows_state = set (accu) ⦈) ⟹
(set accu) ∪ (set edgesList) ⊆ E ⟹
all_security_requirements_fulfilled (get_IFS M) (stateful_policy_to_network_graph ⦇ hosts = V, flows_fix = E, flows_state = set (filter_IFS_no_violations_accu ⦇ nodes = V, edges = E ⦈ M accu edgesList) ⦈)"
apply(induction edgesList arbitrary: accu)
by(simp_all)
lemma filter_IFS_no_violations_correct: "⟦valid_reqs (get_IFS M); wf_graph G;
all_security_requirements_fulfilled (get_IFS M) G;
(set edgesList) ⊆ edges G ⟧ ⟹
all_security_requirements_fulfilled (get_IFS M) (stateful_policy_to_network_graph ⦇ hosts = nodes G, flows_fix = edges G, flows_state = set (filter_IFS_no_violations G M edgesList) ⦈)"
unfolding filter_IFS_no_violations_def
apply(case_tac G, simp)
apply(drule(1) filter_IFS_no_violations_accu_correct_induction[where accu="[]", simplified])
apply(simp_all)
by(simp add: stateful_policy_to_network_graph_def all_flows_def backflows_def False_set)
lemma filter_IFS_no_violations_accu_no_IFS: "valid_reqs (get_IFS M) ⟹ wf_graph G ⟹ get_IFS M = [] ⟹
(set accu) ∪ (set edgesList) ⊆ edges G ⟹
filter_IFS_no_violations_accu G M accu edgesList = rev(edgesList)@accu"
apply(induction edgesList arbitrary: accu)
by(simp_all add: all_security_requirements_fulfilled_def)
lemma filter_IFS_no_violations_accu_maximal_induction: "valid_reqs (get_IFS M) ⟹ wf_graph ⦇ nodes = V, edges = E ⦈ ⟹
set accu ⊆ E ⟹ set edgesList ⊆ E ⟹
∀ e ∈ E - (set accu ∪ set edgesList).
¬ all_security_requirements_fulfilled (get_IFS M) (stateful_policy_to_network_graph ⦇ hosts = V, flows_fix = E, flows_state = {e} ∪ (set accu) ⦈)
⟹
let stateful = set (filter_IFS_no_violations_accu ⦇ nodes = V, edges = E ⦈ M accu edgesList) in
(∀ e ∈ E - stateful.
¬ all_security_requirements_fulfilled (get_IFS M) (stateful_policy_to_network_graph ⦇ hosts = V, flows_fix = E, flows_state = {e} ∪ stateful ⦈))"
proof(induction edgesList arbitrary: accu)
case Nil thus ?case by(simp add: Let_def)
next
case(Cons e Es)
from Cons.prems(3) Cons.prems(2) have "fst ` set accu ⊆ V" and "snd ` set accu ⊆ V"
by(auto simp add: wf_graph_def)
from Cons.prems(2) this Cons.prems(4) have "⋀ea. ea∈E ⟹ wf_graph ⦇ nodes = V, edges = insert e (insert ea (set accu)) ⦈"
by(auto simp add: wf_graph_def)
from backflows_wf[OF this] wf_graph_union_edges[OF Cons.prems(2)]
have "⋀ea. ea∈E ⟹ wf_graph ⦇ nodes = V, edges = E ∪ backflows (insert e (insert ea (set accu))) ⦈" by (simp)
hence "⋀ea. ea∈E ⟹ wf_graph ⦇ nodes = V, edges = E ∪ set accu ∪ backflows (insert e (insert ea (set accu))) ⦈"
by (metis Cons.prems(3) sup.order_iff)
from this Cons.prems(4)
have "⋀ea. ea∈E ⟹ wf_graph ⦇ nodes = V, edges = insert e (insert ea (E ∪ set accu ∪ backflows (insert e (insert ea (set accu))))) ⦈"
by(simp add: insert_absorb)
hence validgraph1: "⋀ea. ea∈E - (set (e # accu) ∪ set Es) ⟹
wf_graph ⦇ nodes = V, edges = insert e (insert ea (E ∪ set accu ∪ backflows (insert e (insert ea (set accu))))) ⦈" by(simp)
have validgraph2: "⋀ ea.
insert ea (E ∪ set accu ∪ backflows (insert ea (set accu))) ⊆ insert e (insert ea (E ∪ set accu ∪ backflows (insert e (insert ea (set accu)))))"
apply(simp add: backflows_def)
by blast
from all_security_requirements_fulfilled_mono[OF Cons.prems(1) validgraph2 validgraph1] have neg_mono:
"⋀ea. ea ∈ E - (set (e # accu) ∪ set Es) ⟹
¬ all_security_requirements_fulfilled (get_IFS M)
⦇nodes = V, edges = insert ea (E ∪ set accu ∪ backflows (insert ea (set accu)))⦈
⟹
¬ all_security_requirements_fulfilled (get_IFS M)
⦇nodes = V, edges = insert e (insert ea (E ∪ set accu ∪ backflows (insert e (insert ea (set accu)))))⦈"
apply(simp)
by blast
from Cons.prems(5) have "⋀ea. ea∈E - (set (e # accu) ∪ set Es) ⟹
¬ all_security_requirements_fulfilled (get_IFS M) (stateful_policy_to_network_graph
⦇hosts = V, flows_fix = E, flows_state = {ea} ∪ set (e # accu)⦈)"
apply(erule_tac x="ea" in ballE)
prefer 2
apply simp
apply(simp only: stateful_policy_to_network_graph_def all_flows_def stateful_policy.select_convs)
apply(simp)
apply(frule(1) neg_mono[simplified])
by(simp)
hence goalTrue:
"∀ ea∈E - (set (e # accu) ∪ set Es).
¬ all_security_requirements_fulfilled (get_IFS M)
(stateful_policy_to_network_graph ⦇hosts = V, flows_fix = E, flows_state = {ea} ∪ set (e # accu)⦈)"
by simp
show ?case
apply(simp add: Let_def)
apply(rule conjI)
apply(rule impI)
apply(thin_tac "_")
using Cons.IH[where accu="e # accu", OF Cons.prems(1) Cons.prems(2) _ _ goalTrue, simplified Let_def] Cons.prems(3) Cons.prems(4)
apply(auto) [1]
apply(rule impI)
using Cons.IH[where accu="accu", OF Cons.prems(1) Cons.prems(2), simplified Let_def] Cons.prems(5) Cons.prems(3) Cons.prems(4)
apply(auto)
done
qed
lemma filter_IFS_no_violations_maximal: "⟦valid_reqs (get_IFS M); wf_graph G;
(set edgesList) = edges G ⟧ ⟹
let stateful = set (filter_IFS_no_violations G M edgesList) in
∀ e ∈ edges G - stateful.
¬ all_security_requirements_fulfilled (get_IFS M) (stateful_policy_to_network_graph ⦇ hosts = nodes G, flows_fix = edges G, flows_state = {e} ∪ stateful ⦈)"
unfolding filter_IFS_no_violations_def
apply(case_tac G, simp)
apply(drule(1) filter_IFS_no_violations_accu_maximal_induction[where accu="[]" and edgesList="edgesList"])
by(simp_all)
corollary filter_IFS_no_violations_maximal_allsubsets:
assumes a1: "valid_reqs (get_IFS M)"
and a2: "wf_graph G"
and a4: "(set edgesList) = edges G"
shows "let stateful = set (filter_IFS_no_violations G M edgesList) in
∀ E ⊆ edges G - stateful. E ≠ {} ⟶
¬ all_security_requirements_fulfilled (get_IFS M) (stateful_policy_to_network_graph ⦇ hosts = nodes G, flows_fix = edges G, flows_state = E ∪ stateful ⦈)"
proof -
let ?stateful = "set (filter_IFS_no_violations G M edgesList)"
from filter_IFS_no_violations_maximal[OF a1 a2 a4] have not_fulfilled_single:
"∀e∈edges G - ?stateful. ¬ all_security_requirements_fulfilled (get_IFS M)
(stateful_policy_to_network_graph ⦇hosts = nodes G, flows_fix = edges G, flows_state = {e} ∪ ?stateful⦈)"
by(simp add: Let_def)
have neg_mono:
"⋀ e E. e ∈ E ⟹ E ⊆ edges G - ?stateful ⟹ E ≠ {} ⟹
¬ all_security_requirements_fulfilled (get_IFS M)
(stateful_policy_to_network_graph ⦇hosts = nodes G, flows_fix = edges G, flows_state = {e} ∪ ?stateful⦈) ⟹
¬ all_security_requirements_fulfilled (get_IFS M)
(stateful_policy_to_network_graph ⦇hosts = nodes G, flows_fix = edges G, flows_state = E ∪ ?stateful⦈)"
proof -
fix e E
assume h1: "e ∈ E"
and h2: "E ⊆ edges G - ?stateful"
and h3: "E ≠ {}"
and h4: "¬ all_security_requirements_fulfilled (get_IFS M)
(stateful_policy_to_network_graph ⦇hosts = nodes G, flows_fix = edges G, flows_state = {e} ∪ ?stateful⦈)"
from filter_IFS_no_violations_subseteq_input a4 have "?stateful ⊆ edges G" by blast
hence "edges G ∪ (E ∪ ?stateful) = edges G" using h2 by blast
from a2 this have validgraph1: "wf_graph ⦇nodes = nodes G, edges = edges G ∪ (E ∪ ?stateful)⦈"
by(case_tac G, simp)
from h1 h2 h3 have subseteq: "({e} ∪ ?stateful) ⊆ (E ∪ ?stateful)" by blast
have revimp: "⋀A B. (A ⟹ B) ⟹ (¬ B ⟹ ¬ A)" by fast
from all_security_requirements_fulfilled_mono_stateful_policy_to_network_graph[OF a1 subseteq validgraph1] h4
show "¬ all_security_requirements_fulfilled (get_IFS M)
(stateful_policy_to_network_graph ⦇hosts = nodes G, flows_fix = edges G, flows_state = E ∪ ?stateful⦈)"
apply(rule revimp)
by assumption
qed
show ?thesis
proof(simp add: Let_def,rule allI,rule impI, rule impI)
fix E
assume h1: "E ⊆ edges G - ?stateful"
and h2: "E ≠ {}"
from h1 h2 obtain e where e_prop1: "e ∈ E" by blast
from this h1 have "e ∈ edges G - ?stateful" by blast
from this not_fulfilled_single have e_prop2: "¬ all_security_requirements_fulfilled (get_IFS M)
(stateful_policy_to_network_graph ⦇hosts = nodes G, flows_fix = edges G, flows_state = {e} ∪ ?stateful⦈)"
by simp
from neg_mono[OF e_prop1 h1 h2 e_prop2]
show " ¬ all_security_requirements_fulfilled (get_IFS M)
(stateful_policy_to_network_graph ⦇hosts = nodes G, flows_fix = edges G, flows_state = E ∪ set (filter_IFS_no_violations G M edgesList)⦈)"
.
qed
qed
thm filter_IFS_no_violations_correct filter_IFS_no_violations_maximal
text‹Next›
fun filter_compliant_stateful_ACS_accu :: "'v::vertex graph ⇒ 'v SecurityInvariant_configured list ⇒ ('v × 'v) list ⇒ ('v × 'v) list ⇒ ('v × 'v) list" where
"filter_compliant_stateful_ACS_accu G M accu [] = accu" |
"filter_compliant_stateful_ACS_accu G M accu (e#Es) = (if
e ∉ backflows (edges G) ∧ (∀F ∈ get_offending_flows (get_ACS M) (stateful_policy_to_network_graph ⦇ hosts = nodes G, flows_fix = edges G, flows_state = set (e#accu) ⦈). F ⊆ backflows (set (e#accu)))
then filter_compliant_stateful_ACS_accu G M (e#accu) Es
else filter_compliant_stateful_ACS_accu G M accu Es)"
definition filter_compliant_stateful_ACS :: "'v::vertex graph ⇒ 'v SecurityInvariant_configured list ⇒ ('v × 'v) list ⇒ ('v × 'v) list" where
"filter_compliant_stateful_ACS G M Es = filter_compliant_stateful_ACS_accu G M [] Es"
lemma filter_compliant_stateful_ACS_subseteq_input: "set (filter_compliant_stateful_ACS G M Es) ⊆ set Es"
apply(subgoal_tac "∀ accu. set (filter_compliant_stateful_ACS_accu G M accu Es) ⊆ set Es ∪ set accu")
apply(erule_tac x="[]" in allE)
apply(simp add: filter_compliant_stateful_ACS_def)
apply(induct_tac Es)
apply(simp_all)
apply (metis Un_insert_right set_simps(2) set_subset_Cons set_union subset_trans)
done
lemma filter_compliant_stateful_ACS_accu_correct_induction: "valid_reqs (get_ACS M) ⟹ wf_graph ⦇ nodes = V, edges = E ⦈ ⟹
(set accu) ∪ (set edgesList) ⊆ E ⟹
∀F ∈ get_offending_flows (get_ACS M) (stateful_policy_to_network_graph ⦇ hosts = V, flows_fix = E, flows_state = set (accu) ⦈). F ⊆ backflows (set accu) ⟹
(∀a ∈ set accu. a ∉ (backflows E)) ⟹
𝒯 = ⦇ hosts = V, flows_fix = E, flows_state = set (filter_compliant_stateful_ACS_accu ⦇ nodes = V, edges = E ⦈ M accu edgesList) ⦈ ⟹
∀F ∈ get_offending_flows (get_ACS M) (stateful_policy_to_network_graph 𝒯). F ⊆ backflows (filternew_flows_state 𝒯)"
proof(induction edgesList arbitrary: accu)
case Nil
from Nil(5) have "backflows (set accu) = backflows {e ∈ set accu. e ∉ backflows E}" by (metis (lifting) Collect_cong Collect_mem_eq)
from this Nil(4) have "∀F∈get_offending_flows (get_ACS M) (stateful_policy_to_network_graph ⦇hosts = V, flows_fix = E, flows_state = set accu⦈). F ⊆ backflows {e ∈ set accu. e ∉ backflows E}" by simp
from this Nil(6) show ?case by(simp add: filternew_flows_state_alt2)
next
case (Cons e Es)
from Cons.IH[OF Cons.prems(1) Cons.prems(2)] Cons.prems(3) Cons.prems(4) Cons.prems(5) Cons.prems(6)
show ?case by(simp add: filternew_flows_state_alt2 split: if_split_asm)
qed
lemma filter_compliant_stateful_ACS_accu_no_side_effects: "valid_reqs (get_ACS M) ⟹ wf_graph G ⟹
∀F ∈ get_offending_flows (get_ACS M) ⦇nodes = nodes G, edges = edges G ∪ backflows (edges G)⦈. F ⊆ (backflows (edges G)) - (edges G) ⟹
(set accu) ∪ (set edgesList) ⊆ edges G ⟹
(∀a ∈ set accu. a ∉ (backflows (edges G))) ⟹
filter_compliant_stateful_ACS_accu G M accu edgesList = rev([ e ← edgesList. e ∉ backflows (edges G)])@accu"
apply(simp add: backflows_minus_backflows)
apply(induction edgesList arbitrary: accu)
apply(simp)
apply(simp add: stateful_policy_to_network_graph_def all_flows_def)
apply(rule impI)
apply(case_tac G, simp, rename_tac V E)
thm Un_set_offending_flows_bound_minus_subseteq'[where X="backflows E - E" and E="E ∪ backflows E"]
apply(drule_tac X="backflows E - E" and E="E ∪ backflows E" and E'="(E ∪ backflows E) - (insert a (E ∪ set accu ∪ backflows (insert a (set accu))))" in Un_set_offending_flows_bound_minus_subseteq')
defer
prefer 2
apply blast
apply auto[1]
apply(subgoal_tac "E ∪ backflows E - (E ∪ backflows E - insert a (E ∪ set accu ∪ backflows (insert a (set accu)))) = insert a (E ∪ set accu ∪ backflows (insert a (set accu)))")
apply(simp)
prefer 2
apply (metis Un_assoc Un_least Un_mono backflows_subseteq double_diff insert_def insert_subset subset_refl)
apply(subgoal_tac "backflows (insert a (set accu)) ⊆ backflows E - E - (E ∪ backflows E - insert a (E ∪ set accu ∪ backflows (insert a (set accu))))")
apply(blast)
apply(simp add: backflows_def)
apply fast
using FiniteGraph.backflows_wf FiniteGraph.wf_graph_union_edges by metis
lemma filter_compliant_stateful_ACS_correct:
assumes a1: "valid_reqs (get_ACS M)"
and a2: "wf_graph G"
and a3: "set edgesList ⊆ edges G"
and a4: "all_security_requirements_fulfilled (get_ACS M) G"
and a5: "𝒯 = ⦇ hosts = nodes G, flows_fix = edges G, flows_state = set (filter_compliant_stateful_ACS G M edgesList) ⦈"
shows "∀F ∈ get_offending_flows (get_ACS M) (stateful_policy_to_network_graph 𝒯). F ⊆ backflows (filternew_flows_state 𝒯)"
proof -
obtain V E where VE: "G = ⦇ nodes = V, edges = E ⦈" by(case_tac G, blast)
from VE a2 have wfVE: "wf_graph ⦇ nodes = V, edges = E ⦈" by simp
from VE a3 have "set edgesList ⊆ E" by simp
from a5 VE have a5': "𝒯 = ⦇hosts = V, flows_fix = E, flows_state = set (filter_compliant_stateful_ACS_accu ⦇nodes = V, edges = E⦈ M [] edgesList)⦈"
unfolding filter_compliant_stateful_ACS_def
by(simp)
from all_security_requirements_fulfilled_imp_get_offending_empty[OF a1 a4] VE
have "∀F∈get_offending_flows (get_ACS M) (stateful_policy_to_network_graph ⦇hosts = V, flows_fix = E, flows_state = {}⦈). F ⊆ backflows {}"
by(simp add: stateful_policy_to_network_graph_def all_flows_def backflows_def False_set)
from filter_compliant_stateful_ACS_accu_correct_induction[where accu="[]" and edgesList="edgesList", simplified, OF a1 wfVE ‹set edgesList ⊆ E› this a5']
show ?thesis .
qed
lemma filter_compliant_stateful_ACS_accu_induction_maximal:"⟦ valid_reqs (get_ACS M); wf_graph ⦇ nodes = V, edges = E ⦈;
(set edgesList) ⊆ E;
(set accu) ⊆ E;
stateful = set (filter_compliant_stateful_ACS_accu ⦇ nodes = V, edges = E ⦈ M accu edgesList);
∀e ∈ E - (set edgesList ∪ set accu ∪ {e ∈ E. e ∈ backflows E}).
¬ ⋃(get_offending_flows (get_ACS M) (stateful_policy_to_network_graph ⦇ hosts = V, flows_fix = E, flows_state = set accu ∪ {e} ⦈))
⊆ backflows (filternew_flows_state ⦇ hosts = V, flows_fix = E, flows_state = set accu ∪ {e} ⦈)
⟧ ⟹
∀e ∈ E - (stateful ∪ {e ∈ E. e ∈ backflows E}).
¬ ⋃(get_offending_flows (get_ACS M) (stateful_policy_to_network_graph ⦇ hosts = V, flows_fix = E, flows_state = stateful ∪ {e} ⦈))
⊆ backflows (filternew_flows_state ⦇ hosts = V, flows_fix = E, flows_state = stateful ∪ {e} ⦈)"
proof(induction edgesList arbitrary: accu E)
case Nil from Nil(5)[simplified] Nil(6) show ?case by(simp)
next
case (Cons a Es)
let ?caseDistinction="a ∉ backflows (E) ∧ (∀F∈get_offending_flows (get_ACS M)
(stateful_policy_to_network_graph ⦇hosts = V, flows_fix = E, flows_state = set (a # accu)⦈).
F ⊆ backflows (set (a # accu)))"
from Cons.prems(3) have "set Es ⊆ E" by simp
show ?case
proof(cases ?caseDistinction)
assume CaseTrue: ?caseDistinction
from CaseTrue have
"set (filter_compliant_stateful_ACS_accu ⦇nodes = V, edges = E⦈ M accu (a # Es)) =
set (filter_compliant_stateful_ACS_accu ⦇nodes = V, edges = E⦈ M (a # accu) Es)"
by(simp)
from this Cons.prems(5) have statefulsimp:
"stateful = set (filter_compliant_stateful_ACS_accu ⦇nodes = V, edges = E⦈ M (a # accu) Es)" by simp
from Cons.prems(3) Cons.prems(4) have "set (a # accu) ⊆ E" by simp
have "∀e∈E - (set Es ∪ set (a # accu) ∪ {e ∈ E. e ∈ backflows E}).
¬ ⋃(get_offending_flows (get_ACS M) (stateful_policy_to_network_graph ⦇hosts = V, flows_fix = E, flows_state = set (a # accu) ∪ {e}⦈))
⊆ backflows (filternew_flows_state ⦇hosts = V, flows_fix = E, flows_state = set (a # accu) ∪ {e}⦈)"
proof(rule ballI)
fix e
assume h1: "e ∈ E - (set Es ∪ set (a # accu) ∪ {e ∈ E. e ∈ backflows E})"
from conjunct1[OF CaseTrue] have filternew_flows_state_moveout_a:
"filternew_flows_state ⦇hosts = V, flows_fix = E, flows_state = set (a # accu) ∪ {e}⦈ =
{a} ∪ filternew_flows_state ⦇hosts = V, flows_fix = E, flows_state = set accu ∪ {e}⦈"
apply(simp add: filternew_flows_state_alt) by blast
have backflowssubseta: "⋀X. backflows X ⊆ backflows ({a} ∪ X)" by(simp add: backflows_def, blast)
from Cons.prems(6) h1 have
"¬ ⋃(get_offending_flows (get_ACS M) (stateful_policy_to_network_graph ⦇hosts = V, flows_fix = E, flows_state = set accu ∪ {e}⦈))
⊆ backflows (filternew_flows_state ⦇hosts = V, flows_fix = E, flows_state = set accu ∪ {e}⦈)" by simp
from this obtain dat_offender where
dat_in: "dat_offender ∈ ⋃(get_offending_flows (get_ACS M) (stateful_policy_to_network_graph ⦇hosts = V, flows_fix = E, flows_state = set accu ∪ {e}⦈))"
and dat_offends: "dat_offender ∉ backflows (filternew_flows_state ⦇hosts = V, flows_fix = E, flows_state = set accu ∪ {e}⦈)" by blast
have wfGraphA: "wf_graph (stateful_policy_to_network_graph ⦇hosts = V, flows_fix = E, flows_state = set (a # accu) ∪ {e}⦈)"
proof(simp add: stateful_policy_to_network_graph_def all_flows_def)
from Cons.prems(2) h1 Cons.prems(3) Cons.prems(4)
have "wf_graph ⦇nodes=V, edges = insert e (insert a (set accu)) ⦈"
apply(auto simp add: wf_graph_def) by force
from this backflows_wf
have vgh1: "wf_graph ⦇nodes = V, edges = backflows (insert e (insert a (set accu)))⦈" by auto
from Cons.prems(2) wf_graph_add_subset_edges h1 Cons.prems(3) Cons.prems(4)
have vgh2: "wf_graph ⦇nodes = V, edges = insert e ((insert a E) ∪ set accu)⦈"
proof -
have f1: "e ∈ E - (set Es ∪ insert a (set accu) ∪ {R ∈ E. R ∈ backflows E})"
using h1 by simp
have f2: "insert a (set accu) ⊆ E"
using ‹set (a # accu) ⊆ E› by simp
have f3: "e ∈ E"
using f1 by fastforce
have "E ∪ insert a (set accu) = E"
using f2 by fastforce
thus "wf_graph ⦇nodes = V, edges = insert e (insert a E ∪ set accu)⦈"
using f3 Cons.prems(2) Un_insert_right insert_absorb sup_commute by fastforce
qed
from vgh1 vgh2 wf_graph_union_edges
show "wf_graph ⦇nodes = V, edges = insert e (insert a (E ∪ set accu ∪ backflows (insert e (insert a (set accu)))))⦈" by fastforce
qed
from dat_in have dat_in_simplified:
"dat_offender ∈ ⋃(get_offending_flows (get_ACS M) ⦇nodes = V, edges = insert e (E ∪ set accu ∪ backflows (insert e (set accu)))⦈)"
by(simp add: stateful_policy_to_network_graph_def all_flows_def)
have subsethlp: "insert e (E ∪ set accu ∪ backflows (insert e (set accu))) ⊆ E ∪ (set (a # accu) ∪ {e}) ∪ backflows (set (a # accu) ∪ {e})"
apply(simp)
apply(rule, blast)
apply(rule, blast)
apply(rule)
apply(simp add: backflows_def, fast)
done
from get_offending_flows_union_mono[OF
Cons.prems(1)
wfGraphA[simplified stateful_policy_to_network_graph_def all_flows_def graph.select_convs stateful_policy.select_convs],
OF subsethlp]
dat_in_simplified have dat_in_a: "dat_offender ∈ ⋃(get_offending_flows (get_ACS M)
(stateful_policy_to_network_graph ⦇hosts = V, flows_fix = E, flows_state = set (a # accu) ∪ {e}⦈))"
by(simp add: stateful_policy_to_network_graph_def all_flows_def, fast)
have "dat_offender ≠ (snd a, fst a)"
proof(rule ccontr)
assume "¬ dat_offender ≠ (snd a, fst a)"
hence hlpassm: "dat_offender = (snd a, fst a)" by simp
from this obtain a1 a2 where "dat_offender = (a2, a1)" by blast
have "⋃(get_offending_flows (get_ACS M) ⦇nodes = V, edges = insert e (E ∪ set accu ∪ backflows (insert e (set accu)))⦈) ⊆
insert e (E ∪ set accu ∪ backflows (insert e (set accu)))"
by (metis Cons.prems(1) Sup_le_iff get_offending_flows_subseteq_edges)
from this h1 have UN_get_subset:
"⋃(get_offending_flows (get_ACS M) ⦇nodes = V, edges = insert e (E ∪ set accu ∪ backflows (insert e (set accu)))⦈) ⊆
(E ∪ set accu ∪ backflows (insert e (set accu)))"
by blast
from dat_offends have dat_offends_simplified:
"dat_offender ∉ backflows (insert e (set accu)) - E"
by(simp only: filternew_flows_state_alt stateful_policy.select_convs backflows_minus_backflows, simp)
from conjunct1[OF CaseTrue] hlpassm have "dat_offender ∉ E"
by(simp add: backflows_def, fastforce)
from dat_in_simplified UN_get_subset this have "dat_offender ∈ set accu ∪ backflows (insert e (set accu))" by blast
from this Cons.prems(4) ‹dat_offender ∉ E› have "dat_offender ∈ backflows (insert e (set accu))" by blast
from dat_offends_simplified[simplified] this have "dat_offender ∈ E" by simp
from ‹dat_offender ∉ E› ‹dat_offender ∈ E› show False by simp
qed
from this dat_offends have
"dat_offender ∉ backflows ({a} ∪ filternew_flows_state ⦇hosts = V, flows_fix = E, flows_state = set accu ∪ {e}⦈)"
apply(simp add: backflows_def) by force
from dat_in_a this
show "¬ ⋃(get_offending_flows (get_ACS M) (stateful_policy_to_network_graph ⦇hosts = V, flows_fix = E, flows_state = set (a # accu) ∪ {e}⦈))
⊆ backflows (filternew_flows_state ⦇hosts = V, flows_fix = E, flows_state = set (a # accu) ∪ {e}⦈)"
apply(subst filternew_flows_state_moveout_a) by blast
qed
from Cons.IH[OF Cons.prems(1) Cons.prems(2) ‹set Es ⊆ E› ‹set (a # accu) ⊆ E› statefulsimp this ] show "?case"
by(simp)
next
assume CaseFalse: "¬ ?caseDistinction"
from CaseFalse have funapplysimp:
"set (filter_compliant_stateful_ACS_accu ⦇nodes = V, edges = E⦈ M accu (a # Es)) =
set (filter_compliant_stateful_ACS_accu ⦇nodes = V, edges = E⦈ M accu Es)"
by auto
from this Cons.prems(5) have statefulsimp:
"stateful = set (filter_compliant_stateful_ACS_accu ⦇nodes = V, edges = E⦈ M accu Es)" by simp
from Cons.prems(4) have "set accu ⊆ E" .
have "a ∈ E - (set Es ∪ set accu ∪ {e ∈ E. e ∈ backflows E})⟹ ¬ ⋃(get_offending_flows (get_ACS M) (stateful_policy_to_network_graph ⦇hosts = V, flows_fix = E, flows_state = set accu ∪ {a}⦈))
⊆ backflows (filternew_flows_state ⦇hosts = V, flows_fix = E, flows_state = set accu ∪ {a}⦈)"
proof(rule ccontr)
assume h1: "a ∈ E - (set Es ∪ set accu ∪ {e ∈ E. e ∈ backflows E})"
and "¬ ¬⋃(get_offending_flows (get_ACS M) (stateful_policy_to_network_graph ⦇hosts = V, flows_fix = E, flows_state = set accu ∪ {a}⦈)) ⊆ backflows (filternew_flows_state ⦇hosts = V, flows_fix = E, flows_state = set accu ∪ {a}⦈)"
hence hccontr: "⋃(get_offending_flows (get_ACS M) (stateful_policy_to_network_graph ⦇hosts = V, flows_fix = E, flows_state = set accu ∪ {a}⦈)) ⊆ backflows (filternew_flows_state ⦇hosts = V, flows_fix = E, flows_state = set accu ∪ {a}⦈)" by simp
moreover from h1 have stateful_to_graph: "stateful_policy_to_network_graph ⦇hosts = V, flows_fix = E, flows_state = set accu ∪ {a}⦈ = ⦇nodes = V, edges = E ∪ set accu ∪ backflows (insert a (set accu))⦈"
by(simp add: stateful_policy_to_network_graph_def all_flows_def, blast)
moreover have "backflows (filternew_flows_state ⦇hosts = V, flows_fix = E, flows_state = set accu ∪ {a}⦈) = backflows (insert a (set accu)) - E"
by(simp add: filternew_flows_state_alt backflows_minus_backflows)
ultimately have hccontr_simp:
"⋃(get_offending_flows (get_ACS M) ⦇nodes = V, edges = E ∪ set accu ∪ backflows (insert a (set accu))⦈) ⊆ backflows (insert a (set accu)) - E" by simp
from Cons.prems(3) Cons.prems(4) have backaaccusubE: "backflows (set (a # accu)) ⊆ backflows E" by(simp add: backflows_def, fastforce)
from h1 have "a ∉ backflows E" by fastforce
from backaaccusubE ‹a ∉ backflows E› have "a ∉ backflows (insert a (set accu))" by auto
from ‹a ∉ backflows E› CaseFalse have "¬ (∀F∈get_offending_flows (get_ACS M) (stateful_policy_to_network_graph ⦇hosts = V, flows_fix = E, flows_state = set (a # accu)⦈). F ⊆ backflows (set (a # accu)))" by(simp)
from this stateful_to_graph have "¬ (∀F∈get_offending_flows (get_ACS M) ⦇nodes = V, edges = E ∪ set accu ∪ backflows (insert a (set accu))⦈. F ⊆ backflows (insert a (set accu)))" by(simp)
from this hccontr_simp show False by blast
qed
from Cons.prems(6)[simplified funapplysimp statefulsimp] this
have "∀e∈E - (set Es ∪ set accu ∪ {e ∈ E. e ∈ backflows E}).
¬ ⋃(get_offending_flows (get_ACS M) (stateful_policy_to_network_graph ⦇hosts = V, flows_fix = E, flows_state = set accu ∪ {e}⦈))
⊆ backflows (filternew_flows_state ⦇hosts = V, flows_fix = E, flows_state = set accu ∪ {e}⦈)"
by auto
from Cons.IH[OF Cons.prems(1) Cons.prems(2) ‹set Es ⊆ E› ‹set accu ⊆ E› statefulsimp this]
show ?case by simp
qed
qed
lemma filter_compliant_stateful_ACS_maximal: "⟦ valid_reqs (get_ACS M); wf_graph ⦇ nodes = V, edges = E ⦈;
(set edgesList) = E;
stateful = set (filter_compliant_stateful_ACS ⦇ nodes = V, edges = E ⦈ M edgesList)
⟧ ⟹
∀e ∈ E - (stateful ∪ {e ∈ E. e ∈ backflows E}).
¬ ⋃ (get_offending_flows (get_ACS M) (stateful_policy_to_network_graph ⦇ hosts = V, flows_fix = E, flows_state = stateful ∪ {e} ⦈))
⊆ backflows (filternew_flows_state ⦇ hosts = V, flows_fix = E, flows_state = stateful ∪ {e} ⦈)"
apply(drule(1) filter_compliant_stateful_ACS_accu_induction_maximal[where accu="[]", simplified])
apply(blast)
apply(simp add: filter_compliant_stateful_ACS_def)
apply(simp)
apply fastforce
apply(simp add: filter_compliant_stateful_ACS_def)
done
lemma filter_compliant_stateful_ACS_maximal_allsubsets:
assumes a1: "valid_reqs (get_ACS M)" and a2: "wf_graph ⦇ nodes = V, edges = E ⦈"
and a3: "(set edgesList) = E"
and a4: "stateful = set (filter_compliant_stateful_ACS ⦇ nodes = V, edges = E ⦈ M edgesList)"
and a5: "X ⊆ E - (stateful ∪ backflows E)" and a6: "X ≠ {}"
shows "
¬ ⋃(get_offending_flows (get_ACS M) (stateful_policy_to_network_graph ⦇ hosts = V, flows_fix = E, flows_state = stateful ∪ X ⦈))
⊆ backflows (filternew_flows_state ⦇ hosts = V, flows_fix = E, flows_state = stateful ∪ X ⦈)"
proof(rule ccontr, simp)
from a5 have "X ⊆ E" by blast
assume accontr: "⋃(get_offending_flows (get_ACS M) (stateful_policy_to_network_graph ⦇hosts = V, flows_fix = E, flows_state = stateful ∪ X⦈)) ⊆ backflows (filternew_flows_state ⦇hosts = V, flows_fix = E, flows_state = stateful ∪ X⦈)"
hence "⋃(get_offending_flows (get_ACS M) ⦇nodes = V, edges = E ∪ (stateful ∪ X) ∪ backflows (stateful ∪ X)⦈) ⊆ backflows (stateful ∪ X) - E"
by(simp add: stateful_policy_to_network_graph_def all_flows_def filternew_flows_state_alt backflows_minus_backflows)
hence "⋃(get_offending_flows (get_ACS M) ⦇nodes = V, edges = E ∪ X ∪ backflows (stateful ∪ X)⦈) ⊆ backflows (stateful ∪ X) - E"
using a4 a3 filter_compliant_stateful_ACS_subseteq_input by (metis Diff_subset_conv Un_Diff_cancel Un_assoc a3 bot.extremum_unique sup_bot_right)
hence accontr_simp: "⋃(get_offending_flows (get_ACS M) ⦇nodes = V, edges = E ∪ (backflows stateful) ∪ (backflows X)⦈) ⊆ backflows (stateful ∪ X) - E"
using Set.Un_absorb2[OF ‹X ⊆ E›] backflows_un[of "stateful" "X"] by (metis Un_assoc)
from a2 a5 have "finite X" apply(simp add: wf_graph_def) by (metis (full_types) finite_Diff finite_subset)
from a6 obtain x where "x ∈ X" by blast
from ‹x ∈ X› a5 have xX_simp1: "(backflows X) - (backflows (X - {x}) - E) = backflows {x}"
apply(simp add: backflows_def) by fast
from a5 have "X ∩ stateful = {}" by auto
from ‹x ∈ X› this have xX_simp2: "(backflows stateful) - (backflows (X - {x}) - E) = backflows stateful"
apply(simp add: backflows_def) by fast
have xX_simp3:"backflows (stateful ∪ X) - (backflows (X - {x}) - E) = backflows (stateful ∪ {x})"
apply(simp only: backflows_un)
using xX_simp1 xX_simp2 by blast
have xX_simp4: "backflows (stateful ∪ X) - E - (backflows (X - {x}) - E) = backflows (filternew_flows_state ⦇hosts = V, flows_fix = E, flows_state = stateful ∪ {x}⦈)"
apply(simp add: filternew_flows_state_alt backflows_minus_backflows)
using xX_simp3 by auto
have xX_simp5: "(E ∪ backflows stateful ∪ backflows X) - (backflows (X - {x}) - E) = E ∪ backflows stateful ∪ backflows {x}"
using xX_simp3[simplified backflows_un] by blast
have Eexpand: "E ∪ stateful ∪ {x} = E"
using a4 a3 filter_compliant_stateful_ACS_subseteq_input a5 ‹x∈X› by blast
have "backflows (stateful ∪ X) - E - backflows (X - {x}) = (backflows (stateful ∪ X) - E) - backflows (X - {x})" by simp
from ‹finite X› backflows_finite have finite: "finite (backflows (X - {x}) - E)" by auto
from a2 a4 a3 filter_compliant_stateful_ACS_subseteq_input have "wf_graph ⦇nodes = V, edges = stateful⦈" by (metis Diff_partition wf_graph_remove_edges_union)
from backflows_wf[OF this] have "wf_graph ⦇nodes = V, edges = backflows stateful⦈" .
from a2 ‹X ⊆ E› have "wf_graph ⦇nodes = V, edges = X⦈" by (metis double_diff dual_order.refl wf_graph_remove_edges)
from backflows_wf[OF this] have "wf_graph ⦇nodes = V, edges = backflows X⦈" .
from this wf_graph_union_edges ‹wf_graph ⦇nodes = V, edges = backflows stateful⦈› a2 have wfG:
"wf_graph ⦇nodes = V, edges = E ∪ backflows stateful ∪ backflows X⦈" by metis
from ‹x∈X› have subset: "backflows (X - {x}) - E ⊆ E ∪ backflows stateful ∪ backflows X" apply(simp add: backflows_def) by fast
from Un_set_offending_flows_bound_minus_subseteq'[OF a1 wfG subset accontr_simp] have
"⋃(get_offending_flows (get_ACS M) ⦇nodes = V, edges = (E ∪ backflows stateful ∪ backflows X) - (backflows (X - {x}) - E)⦈) ⊆ (backflows (stateful ∪ X) - E) - (backflows (X - {x}) - E)" by simp
from this xX_simp4 xX_simp5 have trans1:
"⋃(get_offending_flows (get_ACS M) ⦇nodes = V, edges = E ∪ backflows stateful ∪ backflows {x}⦈) ⊆ backflows (filternew_flows_state ⦇hosts = V, flows_fix = E, flows_state = stateful ∪ {x}⦈)" by simp
hence "⋃(get_offending_flows (get_ACS M) ⦇nodes = V, edges = E ∪ backflows (stateful ∪ {x})⦈) ⊆ backflows (filternew_flows_state ⦇hosts = V, flows_fix = E, flows_state = stateful ∪ {x}⦈)"
apply(simp only: backflows_un) by (metis Un_assoc)
hence contr1: "⋃(get_offending_flows (get_ACS M) (stateful_policy_to_network_graph ⦇hosts = V, flows_fix = E, flows_state = stateful ∪ {x}⦈)) ⊆ backflows (filternew_flows_state ⦇hosts = V, flows_fix = E, flows_state = stateful ∪ {x}⦈)"
apply(simp only: stateful_policy_to_network_graph_def all_flows_def stateful_policy.select_convs)
using Eexpand by (metis Un_assoc)
from filter_compliant_stateful_ACS_maximal[OF a1 a2 a3 a4] have
"∀e∈E - (stateful ∪ {e ∈ E. e ∈ backflows E}). ¬ ⋃(get_offending_flows (get_ACS M) (stateful_policy_to_network_graph ⦇hosts = V, flows_fix = E, flows_state = stateful ∪ {e}⦈)) ⊆ backflows (filternew_flows_state ⦇hosts = V, flows_fix = E, flows_state = stateful ∪ {e}⦈)" .
from this a5 ‹x ∈ X› have contr2: "¬ ⋃(get_offending_flows (get_ACS M) (stateful_policy_to_network_graph ⦇hosts = V, flows_fix = E, flows_state = stateful ∪ {x}⦈)) ⊆ backflows (filternew_flows_state ⦇hosts = V, flows_fix = E, flows_state = stateful ∪ {x}⦈)" by blast
from contr1 contr2
show "False" by simp
qed
text‹@{term filter_compliant_stateful_ACS} is correct and maximal›
thm filter_compliant_stateful_ACS_correct filter_compliant_stateful_ACS_maximal
text‹Getting those together. We cannot say ‹edgesList = E› here because one filters first. I guess filtering ACS first is easier, ...›
definition generate_valid_stateful_policy_IFSACS :: "'v::vertex graph ⇒ 'v SecurityInvariant_configured list ⇒ ('v × 'v) list ⇒ 'v stateful_policy" where
"generate_valid_stateful_policy_IFSACS G M edgesList ≡ (let filterIFS = filter_IFS_no_violations G M edgesList in
(let filterACS = filter_compliant_stateful_ACS G M filterIFS in ⦇ hosts = nodes G, flows_fix = edges G, flows_state = set filterACS ⦈))"
lemma generate_valid_stateful_policy_IFSACS_wf_stateful_policy: assumes wfG: "wf_graph G"
and edgesList: "(set edgesList) = edges G"
shows "wf_stateful_policy (generate_valid_stateful_policy_IFSACS G M edgesList)"
proof -
from wfG show ?thesis
apply(simp add: generate_valid_stateful_policy_IFSACS_def wf_stateful_policy_def)
apply(auto simp add: wf_graph_def)
using edgesList filter_IFS_no_violations_subseteq_input filter_compliant_stateful_ACS_subseteq_input by (metis rev_subsetD)
qed
lemma generate_valid_stateful_policy_IFSACS_select_simps:
shows "hosts (generate_valid_stateful_policy_IFSACS G M edgesList) = nodes G"
and "flows_fix (generate_valid_stateful_policy_IFSACS G M edgesList) = edges G"
and "flows_state (generate_valid_stateful_policy_IFSACS G M edgesList) ⊆ set edgesList"
proof -
show "hosts (generate_valid_stateful_policy_IFSACS G M edgesList) = nodes G"
by(simp add: generate_valid_stateful_policy_IFSACS_def)
show "flows_fix (generate_valid_stateful_policy_IFSACS G M edgesList) = edges G"
by(simp add: generate_valid_stateful_policy_IFSACS_def)
show "flows_state (generate_valid_stateful_policy_IFSACS G M edgesList) ⊆ set edgesList"
apply(simp add: generate_valid_stateful_policy_IFSACS_def)
using filter_IFS_no_violations_subseteq_input filter_compliant_stateful_ACS_subseteq_input by (metis subset_trans)
qed
lemma generate_valid_stateful_policy_IFSACS_all_security_requirements_fulfilled_IFS: assumes validReqs: "valid_reqs M"
and wfG: "wf_graph G"
and high_level_policy_valid: "all_security_requirements_fulfilled M G"
and edgesList: "(set edgesList) ⊆ edges G"
shows "all_security_requirements_fulfilled (get_IFS M) (stateful_policy_to_network_graph (generate_valid_stateful_policy_IFSACS G M edgesList))"
proof -
have simp3: "flows_state (generate_valid_stateful_policy_IFSACS G M edgesList) ⊆ edges G" using generate_valid_stateful_policy_IFSACS_select_simps(3) edgesList by fast
have "set (filter_compliant_stateful_ACS G M (filter_IFS_no_violations G M edgesList)) ⊆ set (filter_IFS_no_violations G M edgesList)"
using filter_compliant_stateful_ACS_subseteq_input edgesList by (metis)
from backflows_subseteq this have
"backflows (set (filter_compliant_stateful_ACS G M (filter_IFS_no_violations G M edgesList))) ⊆ backflows (set (filter_IFS_no_violations G M edgesList))" by metis
hence subseteqhlp1:
"edges G ∪ backflows (set (filter_compliant_stateful_ACS G M (filter_IFS_no_violations G M edgesList))) ⊆ edges G ∪ backflows (set (filter_IFS_no_violations G M edgesList))" by blast
from high_level_policy_valid have "all_security_requirements_fulfilled (get_IFS M) G" by(simp add: all_security_requirements_fulfilled_def get_IFS_def)
from filter_IFS_no_violations_correct[OF valid_reqs_IFS_D[OF validReqs] wfG this edgesList] have
"all_security_requirements_fulfilled (get_IFS M) (stateful_policy_to_network_graph ⦇hosts = nodes G, flows_fix = edges G, flows_state = set (filter_IFS_no_violations G M edgesList)⦈)" .
from this edgesList have goalIFS:
"all_security_requirements_fulfilled (get_IFS M) ⦇nodes = nodes G, edges = edges G ∪ backflows (set (filter_IFS_no_violations G M edgesList))⦈"
apply(simp add: stateful_policy_to_network_graph_def all_flows_def)
by (metis Un_absorb2 filter_IFS_no_violations_subseteq_input order_trans)
from wfG filter_IFS_no_violations_subseteq_input[where Es="edgesList" and G="G" and M="M"] edgesList have
"wf_graph ⦇nodes = nodes G, edges = set (filter_IFS_no_violations G M edgesList)⦈"
apply(case_tac G, simp)
by (metis le_iff_sup wf_graph_remove_edges_union)
from backflows_wf[OF this] have
"wf_graph ⦇nodes = nodes G, edges = backflows (set (filter_IFS_no_violations G M edgesList))⦈" by(simp)
from this wf_graph_union_edges wfG have
"wf_graph ⦇nodes = nodes G, edges = edges G ∪ backflows (set (filter_IFS_no_violations G M edgesList))⦈"
by (metis graph.cases graph.select_convs(1) graph.select_convs(2))
from all_security_requirements_fulfilled_mono[OF valid_reqs_IFS_D[OF validReqs] subseteqhlp1 this goalIFS]
have "all_security_requirements_fulfilled (get_IFS M) ⦇nodes = nodes G, edges = edges G ∪ backflows (set (filter_compliant_stateful_ACS G M (filter_IFS_no_violations G M edgesList)))⦈"
.
thus ?thesis
apply(simp add: stateful_policy_to_network_graph_def all_flows_def generate_valid_stateful_policy_IFSACS_select_simps simp3 Un_absorb2)
by(simp add: generate_valid_stateful_policy_IFSACS_def)
qed
theorem generate_valid_stateful_policy_IFSACS_stateful_policy_compliance:
assumes validReqs: "valid_reqs M"
and wfG: "wf_graph G"
and high_level_policy_valid: "all_security_requirements_fulfilled M G"
and edgesList: "(set edgesList) = edges G"
and Tau: "𝒯 = generate_valid_stateful_policy_IFSACS G M edgesList"
shows "stateful_policy_compliance 𝒯 G M"
proof -
have 1: "wf_stateful_policy 𝒯"
apply(simp add: Tau)
by(simp add: generate_valid_stateful_policy_IFSACS_wf_stateful_policy[OF wfG edgesList])
have 2: "wf_stateful_policy (generate_valid_stateful_policy_IFSACS G M edgesList)"
by(simp add: generate_valid_stateful_policy_IFSACS_wf_stateful_policy[OF wfG edgesList])
have 3: "hosts 𝒯 = nodes G"
apply(simp add: Tau)
by(simp add: generate_valid_stateful_policy_IFSACS_select_simps(1))
have 4: "flows_fix 𝒯 ⊆ edges G"
apply(simp add: Tau)
by(simp add: generate_valid_stateful_policy_IFSACS_select_simps(2))
have 5: " all_security_requirements_fulfilled (get_IFS M) (stateful_policy_to_network_graph 𝒯)"
apply(simp add: Tau)
using generate_valid_stateful_policy_IFSACS_all_security_requirements_fulfilled_IFS[OF validReqs wfG high_level_policy_valid] edgesList by blast
have 6: "∀F∈get_offending_flows (get_ACS M) (stateful_policy_to_network_graph 𝒯). F ⊆ backflows (filternew_flows_state 𝒯)"
using filter_compliant_stateful_ACS_correct[OF valid_reqs_ACS_D[OF validReqs] wfG _ _ Tau[simplified generate_valid_stateful_policy_IFSACS_def Let_def]] all_security_requirements_fulfilled_ACS_D[OF high_level_policy_valid]
edgesList filter_IFS_no_violations_subseteq_input by metis
from 1 2 3 4 5 6 validReqs high_level_policy_valid wfG
show ?thesis
unfolding stateful_policy_compliance_def by simp
qed
definition generate_valid_stateful_policy_IFSACS_2 :: "'v::vertex graph ⇒ 'v SecurityInvariant_configured list ⇒ ('v × 'v) list ⇒ 'v stateful_policy" where
"generate_valid_stateful_policy_IFSACS_2 G M edgesList ≡
⦇ hosts = nodes G, flows_fix = edges G, flows_state = set (filter_IFS_no_violations G M edgesList) ∩ set (filter_compliant_stateful_ACS G M edgesList) ⦈"
lemma generate_valid_stateful_policy_IFSACS_2_wf_stateful_policy: assumes wfG: "wf_graph G"
and edgesList: "(set edgesList) = edges G"
shows "wf_stateful_policy (generate_valid_stateful_policy_IFSACS_2 G M edgesList)"
proof -
from wfG show ?thesis
apply(simp add: generate_valid_stateful_policy_IFSACS_2_def wf_stateful_policy_def)
apply(auto simp add: wf_graph_def)
using edgesList filter_IFS_no_violations_subseteq_input by (metis rev_subsetD)
qed
lemma generate_valid_stateful_policy_IFSACS_2_select_simps:
shows "hosts (generate_valid_stateful_policy_IFSACS_2 G M edgesList) = nodes G"
and "flows_fix (generate_valid_stateful_policy_IFSACS_2 G M edgesList) = edges G"
and "flows_state (generate_valid_stateful_policy_IFSACS_2 G M edgesList) ⊆ set edgesList"
proof -
show "hosts (generate_valid_stateful_policy_IFSACS_2 G M edgesList) = nodes G"
by(simp add: generate_valid_stateful_policy_IFSACS_2_def)
show "flows_fix (generate_valid_stateful_policy_IFSACS_2 G M edgesList) = edges G"
by(simp add: generate_valid_stateful_policy_IFSACS_2_def)
show "flows_state (generate_valid_stateful_policy_IFSACS_2 G M edgesList) ⊆ set edgesList"
apply(simp add: generate_valid_stateful_policy_IFSACS_2_def)
using filter_compliant_stateful_ACS_subseteq_input by (metis inf.coboundedI2)
qed
lemma generate_valid_stateful_policy_IFSACS_2_all_security_requirements_fulfilled_IFS: assumes validReqs: "valid_reqs M"
and wfG: "wf_graph G"
and high_level_policy_valid: "all_security_requirements_fulfilled M G"
and edgesList: "(set edgesList) ⊆ edges G"
shows "all_security_requirements_fulfilled (get_IFS M) (stateful_policy_to_network_graph (generate_valid_stateful_policy_IFSACS_2 G M edgesList))"
proof -
have subseteq: "set (filter_IFS_no_violations G M edgesList) ∩ set (filter_compliant_stateful_ACS G M edgesList) ⊆ set (filter_IFS_no_violations G M edgesList)" by blast
from wfG filter_IFS_no_violations_subseteq_input edgesList
have wfG': "wf_graph ⦇nodes = nodes G, edges = edges G ∪ set (filter_IFS_no_violations G M edgesList)⦈"
by (metis graph_eq_intro Un_absorb2 graph.select_convs(1) graph.select_convs(2) order.trans)
from high_level_policy_valid have "all_security_requirements_fulfilled (get_IFS M) G" by(simp add: all_security_requirements_fulfilled_def get_IFS_def)
from filter_IFS_no_violations_correct[OF valid_reqs_IFS_D[OF validReqs] wfG this edgesList] have
"all_security_requirements_fulfilled (get_IFS M) (stateful_policy_to_network_graph ⦇hosts = nodes G, flows_fix = edges G, flows_state = set (filter_IFS_no_violations G M edgesList)⦈)" .
from all_security_requirements_fulfilled_mono_stateful_policy_to_network_graph[OF valid_reqs_IFS_D[OF validReqs] subseteq wfG' this]
have "all_security_requirements_fulfilled (get_IFS M) (stateful_policy_to_network_graph (generate_valid_stateful_policy_IFSACS_2 G M edgesList))"
by(simp add: generate_valid_stateful_policy_IFSACS_2_def)
thus ?thesis .
qed
lemma generate_valid_stateful_policy_IFSACS_2_filter_compliant_stateful_ACS:
assumes validReqs: "valid_reqs M"
and wfG: "wf_graph G"
and high_level_policy_valid: "all_security_requirements_fulfilled M G"
and edgesList: "(set edgesList) ⊆ edges G"
and Tau: "𝒯 = generate_valid_stateful_policy_IFSACS_2 G M edgesList"
shows "∀F∈get_offending_flows (get_ACS M) (stateful_policy_to_network_graph 𝒯). F ⊆ backflows (filternew_flows_state 𝒯)"
proof-
let ?filterACS = "set (filter_compliant_stateful_ACS G M edgesList)"
let ?filterIFS = "set (filter_IFS_no_violations G M edgesList)"
from all_security_requirements_fulfilled_ACS_D[OF high_level_policy_valid] have "all_security_requirements_fulfilled (get_ACS M) G" .
from filter_compliant_stateful_ACS_correct[OF valid_reqs_ACS_D[OF validReqs] wfG edgesList this] have
"∀F∈get_offending_flows (get_ACS M) (stateful_policy_to_network_graph ⦇hosts = nodes G, flows_fix = edges G, flows_state = ?filterACS⦈).
F ⊆ backflows (?filterACS) - edges G"
apply(simp)
apply(simp add: backflows_minus_backflows[symmetric])
by(simp add: filternew_flows_state_alt)
hence "∀F∈get_offending_flows (get_ACS M) ⦇nodes = nodes G, edges = edges G ∪ backflows (?filterACS)⦈. F ⊆ backflows (?filterACS) - edges G"
apply(simp add: stateful_policy_to_network_graph_def all_flows_def)
using filter_compliant_stateful_ACS_subseteq_input by (metis (lifting, no_types) Un_absorb2 edgesList order_trans)
from this validReqs have offending_filterACS_upperbound:
"⋀m. m ∈ set (get_ACS M) ⟹
⋃(c_offending_flows m ⦇nodes = nodes G, edges = edges G ∪ backflows (?filterACS)⦈) ⊆
backflows (?filterACS) - edges G"
by(simp add: valid_reqs_def get_offending_flows_def, blast)
from wfG filter_compliant_stateful_ACS_subseteq_input edgesList have "wf_graph ⦇nodes = nodes G, edges = ?filterACS⦈"
by (metis graph.cases graph.select_convs(1) graph.select_convs(2) le_iff_sup wf_graph_remove_edges_union)
from this backflows_wf have "wf_graph ⦇nodes = nodes G, edges = backflows (?filterACS)⦈" by blast
moreover have "wf_graph ⦇nodes = nodes G, edges = edges G⦈" using wfG by(case_tac G, simp)
ultimately have wfG1: "wf_graph ⦇nodes = nodes G, edges = edges G ∪ backflows (?filterACS)⦈"
using wf_graph_union_edges by blast
from edgesList have edgesUnsimp: "edges G ∪ (?filterACS ∩ ?filterIFS) = edges G"
using filter_IFS_no_violations_subseteq_input filter_compliant_stateful_ACS_subseteq_input by blast
let ?REM = "(backflows (?filterACS) - backflows (?filterIFS)) - edges G"
have REM_gives_desired_upper_bound: "(backflows (?filterACS) - edges G) - ?REM = backflows (?filterACS ∩ ?filterIFS) - edges G"
by(simp add: backflows_def, blast)
have REM_gives_desired_edges: "(edges G ∪ backflows (?filterACS)) - ?REM = edges G ∪ (backflows (?filterACS ∩ ?filterIFS))"
by(simp add: backflows_def, blast)
from wfG have "finite (edges G)" using wf_graph_def by blast
hence "finite (backflows ?filterACS)" using backflows_finite by (metis List.finite_set)
hence finite1: "finite (backflows (?filterACS) - backflows (?filterIFS) - edges G)" by fast
from configured_SecurityInvariant.Un_set_offending_flows_bound_minus_subseteq[where E'="?REM" and X="(backflows (?filterACS) - edges G)",
OF _ wfG1 offending_filterACS_upperbound, simplified REM_gives_desired_upper_bound REM_gives_desired_edges
] valid_reqs_ACS_D[OF validReqs, unfolded valid_reqs_def]
have "⋀m. m ∈ set (get_ACS M) ⟹
∀F∈c_offending_flows m ⦇nodes = nodes G, edges = edges G ∪ backflows (?filterACS ∩ ?filterIFS)⦈.
F ⊆ backflows (?filterACS ∩ ?filterIFS) - edges G" by blast
hence "∀F∈get_offending_flows (get_ACS M)
⦇nodes = nodes G, edges = edges G ∪ (backflows (?filterACS ∩ ?filterIFS))⦈. F ⊆ backflows (?filterACS ∩ ?filterIFS) - edges G"
using get_offending_flows_def by fast
hence "∀F∈get_offending_flows (get_ACS M)
⦇nodes = nodes G, edges = edges G ∪ (?filterACS ∩ ?filterIFS) ∪ (backflows (?filterACS ∩ ?filterIFS))⦈.
F ⊆ backflows (?filterACS ∩ ?filterIFS) - edges G"
by(simp add: edgesUnsimp)
hence "∀F∈get_offending_flows (get_ACS M) (stateful_policy_to_network_graph ⦇hosts = nodes G, flows_fix = edges G, flows_state = ?filterACS ∩ ?filterIFS⦈).
F ⊆ backflows (?filterACS ∩ ?filterIFS) - edges G"
by(simp add: stateful_policy_to_network_graph_def all_flows_def)
thus ?thesis
apply(simp add: Tau generate_valid_stateful_policy_IFSACS_2_def)
apply(simp add: filternew_flows_state_alt backflows_minus_backflows)
by (metis inf_commute)
qed
theorem generate_valid_stateful_policy_IFSACS_2_stateful_policy_compliance:
assumes validReqs: "valid_reqs M"
and wfG: "wf_graph G"
and high_level_policy_valid: "all_security_requirements_fulfilled M G"
and edgesList: "(set edgesList) = edges G"
and Tau: "𝒯 = generate_valid_stateful_policy_IFSACS_2 G M edgesList"
shows "stateful_policy_compliance 𝒯 G M"
proof -
have 1: "wf_stateful_policy 𝒯"
apply(simp add: Tau)
by(simp add: generate_valid_stateful_policy_IFSACS_2_wf_stateful_policy[OF wfG edgesList])
have 2: "wf_stateful_policy (generate_valid_stateful_policy_IFSACS G M edgesList)"
by(simp add: generate_valid_stateful_policy_IFSACS_wf_stateful_policy[OF wfG edgesList])
have 3: "hosts 𝒯 = nodes G"
apply(simp add: Tau)
by(simp add: generate_valid_stateful_policy_IFSACS_2_select_simps(1))
have 4: "flows_fix 𝒯 ⊆ edges G"
apply(simp add: Tau)
by(simp add: generate_valid_stateful_policy_IFSACS_2_select_simps(2))
have 5: "all_security_requirements_fulfilled (get_IFS M) (stateful_policy_to_network_graph 𝒯)"
apply(simp add: Tau)
using generate_valid_stateful_policy_IFSACS_2_all_security_requirements_fulfilled_IFS[OF validReqs wfG high_level_policy_valid] edgesList by blast
have 6: "∀F∈get_offending_flows (get_ACS M) (stateful_policy_to_network_graph 𝒯). F ⊆ backflows (filternew_flows_state 𝒯)"
using generate_valid_stateful_policy_IFSACS_2_filter_compliant_stateful_ACS[OF
validReqs wfG high_level_policy_valid]
Tau edgesList by auto
from 1 2 3 4 5 6 validReqs high_level_policy_valid wfG
show ?thesis
unfolding stateful_policy_compliance_def by simp
qed
text‹
If there are no IFS requirements and the ACS requirements cause no side effects,
effectively, the graph can be considered as undirected graph!
›
lemma generate_valid_stateful_policy_IFSACS_2_noIFS_noACSsideeffects_imp_fullgraph:
assumes validReqs: "valid_reqs M"
and wfG: "wf_graph G"
and high_level_policy_valid: "all_security_requirements_fulfilled M G"
and edgesList: "(set edgesList) = edges G"
and no_ACS_sideeffects: "∀F ∈ get_offending_flows (get_ACS M) ⦇nodes = nodes G, edges = edges G ∪ backflows (edges G)⦈. F ⊆ (backflows (edges G)) - (edges G)"
and no_IFS: "get_IFS M = []"
shows "stateful_policy_to_network_graph (generate_valid_stateful_policy_IFSACS_2 G M edgesList) = undirected G"
proof -
from filter_IFS_no_violations_accu_no_IFS[OF valid_reqs_IFS_D[OF validReqs] wfG no_IFS] edgesList
have "filter_IFS_no_violations G M edgesList = rev edgesList"
by(simp add: filter_IFS_no_violations_def)
from this filter_compliant_stateful_ACS_subseteq_input have flows_state_IFS: "flows_state (generate_valid_stateful_policy_IFSACS_2 G M edgesList) = set (filter_compliant_stateful_ACS G M edgesList)"
by(auto simp add: generate_valid_stateful_policy_IFSACS_2_def)
have flowsfix: "flows_fix (generate_valid_stateful_policy_IFSACS_2 G M edgesList) = edges G" by(simp add: generate_valid_stateful_policy_IFSACS_2_def)
have hosts: "hosts (generate_valid_stateful_policy_IFSACS_2 G M edgesList) = nodes G" by(simp add: generate_valid_stateful_policy_IFSACS_2_def)
from filter_compliant_stateful_ACS_accu_no_side_effects[OF valid_reqs_ACS_D[OF validReqs] wfG no_ACS_sideeffects] have
"filter_compliant_stateful_ACS G M edgesList = rev [e←edgesList . e ∉ backflows (edges G)]"
by(simp add: filter_compliant_stateful_ACS_def edgesList)
hence filterACS: "set (filter_compliant_stateful_ACS G M edgesList) = edges G - (backflows (edges G))" using edgesList by force
show ?thesis
apply(simp add: undirected_backflows stateful_policy_to_network_graph_def all_flows_def)
apply(simp add: hosts filterACS flows_state_IFS flowsfix)
apply(simp add: backflows_minus_backflows)
by fast
qed
lemma generate_valid_stateful_policy_IFSACS_noIFS_noACSsideeffects_imp_fullgraph:
assumes validReqs: "valid_reqs M"
and wfG: "wf_graph G"
and high_level_policy_valid: "all_security_requirements_fulfilled M G"
and edgesList: "(set edgesList) = edges G"
and no_ACS_sideeffects: "∀F ∈ get_offending_flows (get_ACS M) ⦇nodes = nodes G, edges = edges G ∪ backflows (edges G)⦈. F ⊆ (backflows (edges G)) - (edges G)"
and no_IFS: "get_IFS M = []"
shows "stateful_policy_to_network_graph (generate_valid_stateful_policy_IFSACS G M edgesList) = undirected G"
proof -
from filter_IFS_no_violations_accu_no_IFS[OF valid_reqs_IFS_D[OF validReqs] wfG no_IFS] edgesList
have "filter_IFS_no_violations G M edgesList = rev edgesList"
by(simp add: filter_IFS_no_violations_def)
from this filter_compliant_stateful_ACS_subseteq_input have flows_state_IFS: "flows_state (generate_valid_stateful_policy_IFSACS G M edgesList) = set (filter_compliant_stateful_ACS G M (rev edgesList))"
by(simp add: generate_valid_stateful_policy_IFSACS_def)
have flowsfix: "flows_fix (generate_valid_stateful_policy_IFSACS G M edgesList) = edges G" by(simp add: generate_valid_stateful_policy_IFSACS_def)
have hosts: "hosts (generate_valid_stateful_policy_IFSACS G M edgesList) = nodes G" by(simp add: generate_valid_stateful_policy_IFSACS_def)
from filter_compliant_stateful_ACS_accu_no_side_effects[OF valid_reqs_ACS_D[OF validReqs] wfG no_ACS_sideeffects] have
"filter_compliant_stateful_ACS G M (rev edgesList) = [e←edgesList . e ∉ backflows (edges G)]"
apply(simp add: filter_compliant_stateful_ACS_def edgesList) by (metis rev_filter rev_swap)
hence filterACS: "set (filter_compliant_stateful_ACS G M (rev edgesList)) = edges G - (backflows (edges G))" using edgesList by force
show ?thesis
apply(simp add: undirected_backflows stateful_policy_to_network_graph_def all_flows_def)
apply(simp add: hosts filterACS flows_state_IFS flowsfix)
apply(simp add: backflows_minus_backflows)
by fast
qed
end