Theory TopoS_withOffendingFlows
theory TopoS_withOffendingFlows
imports TopoS_Interface
begin
section ‹@{term SecurityInvariant} Instantiation Helpers›
text‹
The security invariant locales are set up hierarchically to ease instantiation proofs.
The first locale, @{term SecurityInvariant_withOffendingFlows} has no assumptions, thus instantiations is for free.
The first step focuses on monotonicity,
›
context SecurityInvariant_withOffendingFlows
begin
text‹We define the monotonicity of ‹sinvar›:
@{term "(⋀ nP N E' E. wf_graph ⦇ nodes = N, edges = E ⦈ ⟹ E' ⊆ E ⟹ sinvar ⦇ nodes = N, edges = E ⦈ nP ⟹ sinvar ⦇ nodes = N, edges = E' ⦈ nP )"}
Having a valid invariant, removing edges retains the validity. I.e.\ prohibiting more, is more or equally secure.
›
definition sinvar_mono :: "bool" where
"sinvar_mono ⟷ (∀ nP N E' E.
wf_graph ⦇ nodes = N, edges = E ⦈ ∧
E' ⊆ E ∧
sinvar ⦇ nodes = N, edges = E ⦈ nP ⟶ sinvar ⦇ nodes = N, edges = E' ⦈ nP )"
text‹
If one can show @{const sinvar_mono}, then the instantiation of the @{term SecurityInvariant_preliminaries} locale is tremendously simplified.
›
lemma sinvar_mono_I_proofrule_simple:
"⟦ (∀ G nP. sinvar G nP = (∀ (e1, e2) ∈ edges G. P e1 e2 nP) ) ⟧ ⟹ sinvar_mono"
apply(simp add: sinvar_mono_def)
apply(clarify)
apply(fast)
done
lemma sinvar_mono_I_proofrule:
"⟦ (∀ nP (G:: 'v graph). sinvar G nP = (∀ (e1, e2) ∈ edges G. P e1 e2 nP G) );
(∀ nP e1 e2 N E' E.
wf_graph ⦇ nodes = N, edges = E ⦈ ∧
(e1,e2) ∈ E ∧
E' ⊆ E ∧
P e1 e2 nP ⦇nodes = N, edges = E⦈ ⟶ P e1 e2 nP ⦇nodes = N, edges = E'⦈) ⟧ ⟹ sinvar_mono"
unfolding sinvar_mono_def
proof(clarify)
fix nP N E' E
assume AllForm: "(∀ nP (G:: 'v graph). sinvar G nP = (∀ (e1, e2) ∈ edges G. P e1 e2 nP G) )"
and Pmono: "∀nP e1 e2 N E' E. wf_graph ⦇ nodes = N, edges = E ⦈ ∧ (e1,e2) ∈ E ∧ E' ⊆ E ∧ P e1 e2 nP ⦇nodes = N, edges = E⦈ ⟶ P e1 e2 nP ⦇nodes = N, edges = E'⦈"
and wfG: "wf_graph ⦇nodes = N, edges = E⦈"
and E'subset: "E' ⊆ E"
and evalE: "sinvar ⦇nodes = N, edges = E⦈ nP"
from Pmono have Pmono1:
"⋀nP N E' E. wf_graph ⦇ nodes = N, edges = E ⦈ ⟹ E' ⊆ E ⟹ (∀(e1,e2) ∈ E. P e1 e2 nP ⦇nodes = N, edges = E⦈ ⟶ P e1 e2 nP ⦇nodes = N, edges = E'⦈)"
by blast
from AllForm have "sinvar ⦇nodes = N, edges = E⦈ nP = (∀ (e1, e2) ∈ E. P e1 e2 nP ⦇nodes = N, edges = E⦈)" by force
from this evalE have "(∀ (e1, e2) ∈ E. P e1 e2 nP ⦇nodes = N, edges = E⦈)" by simp
from Pmono1[OF wfG E'subset, of "nP"] this have "∀(e1, e2) ∈ E. P e1 e2 nP ⦇nodes = N, edges = E'⦈" by fast
from this E'subset have "∀(e1, e2) ∈ E'. P e1 e2 nP ⦇nodes = N, edges = E'⦈" by fast
from this have "∀(e1, e2) ∈ (edges ⦇nodes = N, edges = E'⦈). P e1 e2 nP ⦇nodes = N, edges = E'⦈" by simp
from this AllForm show "sinvar ⦇nodes = N, edges = E'⦈ nP" by presburger
qed
text‹Invariant violations do not disappear if we add more flows.›
lemma sinvar_mono_imp_negative_mono:
"sinvar_mono ⟹ wf_graph ⦇ nodes = N, edges = E ⦈ ⟹ E' ⊆ E ⟹
¬ sinvar ⦇ nodes = N, edges = E' ⦈ nP ⟹ ¬ sinvar ⦇ nodes = N, edges = E ⦈ nP"
unfolding sinvar_mono_def by(blast)
corollary sinvar_mono_imp_negative_delete_edge_mono:
"sinvar_mono ⟹ wf_graph G ⟹ X ⊆ Y ⟹ ¬ sinvar (delete_edges G Y) nP ⟹ ¬ sinvar (delete_edges G X) nP "
proof -
assume sinvar_mono
and "wf_graph G" and "X ⊆ Y" and "¬ sinvar (delete_edges G Y) nP"
from delete_edges_wf[OF ‹wf_graph G›] have valid_G_delete: "wf_graph ⦇nodes = nodes G, edges = edges G - X⦈" by(simp add: delete_edges_simp2)
from ‹X ⊆ Y› have "edges G - Y ⊆ edges G - X" by blast
with ‹sinvar_mono› sinvar_mono_def valid_G_delete have
"sinvar ⦇nodes = nodes G, edges = edges G - X⦈ nP ⟹ sinvar ⦇nodes = nodes G, edges = edges G - Y⦈ nP" by blast
hence "sinvar (delete_edges G X) nP ⟹ sinvar (delete_edges G Y) nP" by(simp add: delete_edges_simp2)
with ‹¬ sinvar (delete_edges G Y) nP› show ?thesis by blast
qed
lemma sinvar_mono_imp_is_offending_flows_mono:
assumes mono: "sinvar_mono"
and wfG: "wf_graph G"
shows "is_offending_flows FF G nP ⟹ is_offending_flows (FF ∪ F) G nP"
proof -
from wfG have wfG': "wf_graph ⦇nodes = nodes G, edges = {(e1, e2). (e1, e2) ∈ edges G ∧ (e1, e2) ∉ FF}⦈"
by (metis delete_edges_def delete_edges_wf)
from mono have sinvarE: "(⋀ nP N E' E. wf_graph ⦇ nodes = N, edges = E ⦈ ⟹ E' ⊆ E ⟹ sinvar ⦇ nodes = N, edges = E ⦈ nP ⟹ sinvar ⦇ nodes = N, edges = E' ⦈ nP )"
unfolding sinvar_mono_def
by metis
have "⋀ G FF F. {(e1, e2). (e1, e2) ∈ edges G ∧ (e1, e2) ∉ FF ∧ (e1, e2) ∉ F} ⊆ {(e1, e2). (e1, e2) ∈ edges G ∧ (e1, e2) ∉ FF} "
by(rule Collect_mono) (simp)
from sinvarE[OF wfG' this]
show "is_offending_flows FF G nP ⟹ is_offending_flows (FF ∪ F) G nP"
by(simp add: is_offending_flows_def delete_edges_def)
qed
lemma sinvar_mono_imp_sinvar_mono:
"sinvar_mono ⟹ wf_graph ⦇ nodes = N, edges = E ⦈ ⟹ E' ⊆ E ⟹ sinvar ⦇ nodes = N, edges = E ⦈ nP ⟹
sinvar ⦇ nodes = N, edges = E' ⦈ nP"
apply(simp add: sinvar_mono_def)
by blast
end
subsection ‹Offending Flows Not Empty Helper Lemmata›
context SecurityInvariant_withOffendingFlows
begin
text ‹Give an over-approximation of offending flows (e.g. all edges) and get back a
minimal set›
fun minimalize_offending_overapprox :: "('v × 'v) list ⇒ ('v × 'v) list ⇒
'v graph ⇒ ('v ⇒ 'a) ⇒ ('v × 'v) list" where
"minimalize_offending_overapprox [] keep _ _ = keep" |
"minimalize_offending_overapprox (f#fs) keep G nP = (if sinvar (delete_edges_list G (fs@keep)) nP then
minimalize_offending_overapprox fs keep G nP
else
minimalize_offending_overapprox fs (f#keep) G nP
)"
text‹The graph we check in @{const minimalize_offending_overapprox},
@{term "G minus (fs ∪ keep)"} is the graph from the ‹offending_flows_min_set› condition.
We add @{term f} and remove it.›
lemma minimalize_offending_overapprox_subset:
"set (minimalize_offending_overapprox ff keeps G nP) ⊆ set ff ∪ set keeps"
proof(induction ff arbitrary: keeps)
case Nil
thus ?case by simp
next
case (Cons a ff)
from Cons have case1: "(sinvar (delete_edges_list G (ff @ keeps)) nP ⟹
set (minimalize_offending_overapprox ff keeps G nP) ⊆ insert a (set ff ∪ set keeps))"
by blast
from Cons have case2: "(¬ sinvar (delete_edges_list G (ff @ keeps)) nP ⟹
set (minimalize_offending_overapprox ff (a # keeps) G nP) ⊆ insert a (set ff ∪ set keeps))"
by fastforce
from case1 case2 show ?case by simp
qed
lemma not_model_mono_imp_addedge_mono:
assumes mono: "sinvar_mono"
and vG: "wf_graph G" and ain: "(a1,a2) ∈ edges G" and xy: "X ⊆ Y" and ns: "¬ sinvar (add_edge a1 a2 (delete_edges G (Y))) nP"
shows "¬ sinvar (add_edge a1 a2 (delete_edges G X)) nP"
proof -
have wf_graph_add_delete_edge_simp:
"⋀Y. add_edge a1 a2 (delete_edges G Y) = (delete_edges G (Y - {(a1,a2)}))"
apply(simp add: delete_edges_simp2 add_edge_def)
apply(rule conjI)
using ain apply (metis insert_absorb vG wf_graph.E_wfD(1) wf_graph.E_wfD(2))
apply(auto simp add: ain)
done
from this ns have 1: "¬ sinvar (delete_edges G (Y - {(a1, a2)})) nP" by simp
have 2: "X - {(a1, a2)} ⊆ Y - {(a1, a2)}" by (metis Diff_mono subset_refl xy)
from sinvar_mono_imp_negative_delete_edge_mono[OF mono] vG have
"⋀X Y. X ⊆ Y ⟹ ¬ sinvar (delete_edges G Y) nP ⟹ ¬ sinvar (delete_edges G X) nP" by blast
from this[OF 2 1] have "¬ sinvar (delete_edges G (X - {(a1, a2)})) nP" by simp
from this wf_graph_add_delete_edge_simp[symmetric] show ?thesis by simp
qed
theorem is_offending_flows_min_set_minimalize_offending_overapprox:
assumes mono: "sinvar_mono"
and vG: "wf_graph G" and iO: "is_offending_flows (set ff) G nP" and sF: "set ff ⊆ edges G" and dF: "distinct ff"
shows "is_offending_flows_min_set (set (minimalize_offending_overapprox ff [] G nP)) G nP"
(is "is_offending_flows_min_set ?minset G nP")
proof -
from iO have "sinvar (delete_edges G (set ff)) nP" by (metis is_offending_flows_def)
{
fix keeps
have "sinvar (delete_edges G (set ff ∪ set keeps)) nP ⟹
sinvar (delete_edges G (set (minimalize_offending_overapprox ff keeps G nP))) nP"
apply(induction ff arbitrary: keeps)
apply(simp)
apply(simp)
apply(rule impI)
apply(simp add:delete_edges_list_union)
done
}
note minimalize_offending_overapprox_maintains_evalmodel=this[of "[]"]
from ‹sinvar (delete_edges G (set ff)) nP› minimalize_offending_overapprox_maintains_evalmodel have
"sinvar (delete_edges G ?minset) nP" by simp
hence 1: "is_offending_flows ?minset G nP" by (metis iO is_offending_flows_def)
txt‹We need to show minimality of @{term "minimalize_offending_overapprox ff []"}.
Minimality means @{term "∀(e1, e2)∈?minset. ¬ sinvar (add_edge e1 e2 (delete_edges G ?minset)) nP"}.
We show the following generalized fact.
›
{
fix ff keeps
have "∀ x ∈ set ff. x ∉ set keeps ⟹
∀ x ∈ set ff. x ∈ edges G ⟹
distinct ff ⟹
∀(e1, e2)∈ set keeps.
¬ sinvar (add_edge e1 e2 (delete_edges G (set (minimalize_offending_overapprox ff keeps G nP)))) nP ⟹
∀(e1, e2)∈set (minimalize_offending_overapprox ff keeps G nP).
¬ sinvar (add_edge e1 e2 (delete_edges G (set (minimalize_offending_overapprox ff keeps G nP)))) nP"
proof(induction ff arbitrary: keeps)
case Nil
from Nil show ?case by(simp)
next
case (Cons a ff)
assume not_in_keeps: "∀x∈set (a # ff). x ∉ set keeps"
hence a_not_in_keeps: "a ∉ set keeps" by simp
assume in_edges: "∀x∈set (a # ff). x ∈ edges G"
hence ff_in_edges: "∀x∈set ff. x ∈ edges G" and a_in_edges: "a ∈ edges G" by simp_all
assume distinct: "distinct (a # ff)"
hence ff_distinct: "distinct ff" and a_not_in_ff: "a ∉ set ff "by simp_all
assume minimal: "∀(e1, e2)∈set keeps.
¬ sinvar (add_edge e1 e2 (delete_edges G (set (minimalize_offending_overapprox (a # ff) keeps G nP)))) nP"
have delete_edges_list_union_insert: "⋀ f fs keep. delete_edges_list G (f#fs@keep) = delete_edges G ({f} ∪ set fs ∪ set keep)"
by(simp add: graph_ops delete_edges_list_set)
let ?goal="?case"
show ?case
proof(cases "sinvar (delete_edges_list G (ff@keeps)) nP")
case True
from True have "sinvar (delete_edges_list G (ff@keeps)) nP" .
from this Cons show ?goal using delete_edges_list_union by simp
next
case False
{
fix a ff keeps
assume mono: "sinvar_mono" and ankeeps: "a ∉ set keeps"
and anff: "a ∉ set ff" and aE: "a ∈ edges G"
and nsinvar: "¬ sinvar (delete_edges_list G (ff @ keeps)) nP"
have "¬ sinvar (add_edge (fst a) (snd a) (delete_edges G (set (minimalize_offending_overapprox (a # ff) keeps G nP)))) nP"
proof -
{ fix F Fs keep
from vG have "F ∈ edges G ⟹ F ∉ set Fs ⟹ F ∉ set keep ⟹
(add_edge (fst F) (snd F) (delete_edges_list G (F#Fs@keep))) = (delete_edges_list G (Fs@keep))"
apply(simp add:delete_edges_list_union delete_edges_list_union_insert)
apply(simp add: graph_ops)
apply(rule conjI)
apply(simp add: wf_graph_def)
apply blast
apply(simp add: wf_graph_def)
by fastforce
} note delete_edges_list_add_add_iff=this
from aE have "(fst a, snd a) ∈ edges G" by simp
from delete_edges_list_add_add_iff[of a ff keeps] have
"delete_edges_list G (ff @ keeps) = add_edge (fst a) (snd a) (delete_edges_list G (a # ff @ keeps))"
by (metis aE anff ankeeps)
from this nsinvar have "¬ sinvar (add_edge (fst a) (snd a) (delete_edges_list G (a # ff @ keeps))) nP" by simp
from this delete_edges_list_union_insert have 1:
"¬ sinvar (add_edge (fst a) (snd a) (delete_edges G (insert a (set ff ∪ set keeps)))) nP" by (metis insert_is_Un sup_assoc)
from minimalize_offending_overapprox_subset[of "ff" "a#keeps" G nP] have
"set (minimalize_offending_overapprox ff (a # keeps) G nP) ⊆ insert a (set ff ∪ set keeps)" by simp
from not_model_mono_imp_addedge_mono[OF mono vG ‹(fst a, snd a) ∈ edges G› this 1] show ?thesis
by (metis minimalize_offending_overapprox.simps(2) nsinvar)
qed
} note not_model_mono_imp_addedge_mono_minimalize_offending_overapprox=this
from not_model_mono_imp_addedge_mono_minimalize_offending_overapprox[OF mono a_not_in_keeps a_not_in_ff a_in_edges False] have a_minimal: "
¬ sinvar (add_edge (fst a) (snd a) (delete_edges G (set (minimalize_offending_overapprox (a # ff) keeps G nP)))) nP"
by simp
from minimal a_minimal
have a_keeps_minimal: "∀(e1, e2)∈set (a # keeps).
¬ sinvar (add_edge e1 e2 (delete_edges G (set (minimalize_offending_overapprox ff (a # keeps) G nP)))) nP"
using False by fastforce
from Cons.prems have a_not_in_keeps: "∀x∈set ff. x ∉ set (a#keeps)" by auto
from Cons.IH[OF a_not_in_keeps ff_in_edges ff_distinct a_keeps_minimal] have IH:
"∀(e1, e2)∈set (minimalize_offending_overapprox ff (a # keeps) G nP).
¬ sinvar (add_edge e1 e2 (delete_edges G (set (minimalize_offending_overapprox ff (a # keeps) G nP)))) nP" .
from False have "¬ sinvar (delete_edges G (set ff ∪ set keeps)) nP " using delete_edges_list_union by metis
from this have "set (minimalize_offending_overapprox (a # ff) keeps G nP) =
set (minimalize_offending_overapprox ff (a#keeps) G nP)"
by(simp add: delete_edges_list_union)
from this IH have ?goal by presburger
thus ?goal .
qed
qed
} note mono_imp_minimalize_offending_overapprox_minimal=this[of ff "[]"]
from mono_imp_minimalize_offending_overapprox_minimal[OF _ _ dF] sF have 2:
"∀(e1, e2)∈?minset. ¬ sinvar (add_edge e1 e2 (delete_edges G ?minset)) nP"
by auto
from 1 2 show ?thesis
by(simp add: is_offending_flows_def is_offending_flows_min_set_def)
qed
corollary mono_imp_set_offending_flows_not_empty:
assumes mono_sinvar: "sinvar_mono"
and vG: "wf_graph G" and iO: "is_offending_flows (set ff) G nP" and sS: "set ff ⊆ edges G" and dF: "distinct ff"
shows
"set_offending_flows G nP ≠ {}"
proof -
from iO SecurityInvariant_withOffendingFlows.is_offending_flows_def have nS: "¬ sinvar G nP" by metis
from sinvar_mono_imp_negative_delete_edge_mono[OF mono_sinvar] have negative_delete_edge_mono:
"∀ G nP X Y. wf_graph G ∧ X ⊆ Y ∧ ¬ sinvar (delete_edges G (Y)) nP ⟶ ¬ sinvar (delete_edges G X) nP" by blast
from is_offending_flows_min_set_minimalize_offending_overapprox[OF mono_sinvar vG iO sS dF]
have "is_offending_flows_min_set (set (minimalize_offending_overapprox ff [] G nP)) G nP" by simp
from this set_offending_flows_def sS have
"(set (minimalize_offending_overapprox ff [] G nP)) ∈ set_offending_flows G nP"
using minimalize_offending_overapprox_subset[where keeps="[]"] by fastforce
thus ?thesis by blast
qed
text‹
To show that @{const set_offending_flows} is not empty, the previous corollary @{thm mono_imp_set_offending_flows_not_empty} is very useful.
Just select @{term "set ff = edges G"}.
›
text‹
If there exists a security violations,
there a means to fix it if and only if the network in which nobody communicates with anyone fulfills the security requirement
›
theorem valid_empty_edges_iff_exists_offending_flows:
assumes mono: "sinvar_mono" and wfG: "wf_graph G" and noteval: "¬ sinvar G nP"
shows "sinvar ⦇ nodes = nodes G, edges = {} ⦈ nP ⟷ set_offending_flows G nP ≠ {}"
proof
assume a: "sinvar ⦇ nodes = nodes G, edges = {} ⦈ nP"
from finite_distinct_list[OF wf_graph.finiteE] wfG
obtain list_edges where list_edges_props: "set list_edges = edges G ∧ distinct list_edges" by blast
hence listedges_subseteq_edges: "set list_edges ⊆ edges G" by blast
have empty_edge_graph_simp: "(delete_edges G (edges G)) = ⦇ nodes = nodes G, edges = {} ⦈" by(auto simp add: graph_ops)
from a is_offending_flows_def noteval list_edges_props empty_edge_graph_simp
have overapprox: "is_offending_flows (set list_edges) G nP" by auto
from mono_imp_set_offending_flows_not_empty[OF mono wfG overapprox listedges_subseteq_edges] list_edges_props
show "set_offending_flows G nP ≠ {}" by simp
next
assume a: "set_offending_flows G nP ≠ {}"
from a obtain f where f_props: "f ⊆ edges G ∧ is_offending_flows_min_set f G nP" using set_offending_flows_def by fastforce
from f_props have "sinvar (delete_edges G f) nP" using is_offending_flows_min_set_def is_offending_flows_def by simp
hence evalGf: "sinvar ⦇nodes = nodes G, edges = {(e1, e2). (e1, e2) ∈ edges G ∧ (e1, e2) ∉ f}⦈ nP" by(simp add: delete_edges_def)
from delete_edges_wf[OF wfG, unfolded delete_edges_def]
have wfGf: "wf_graph ⦇nodes = nodes G, edges = {(e1, e2). (e1, e2) ∈ edges G ∧ (e1, e2) ∉ f}⦈" by simp
have emptyseqGf: "{} ⊆ {(e1, e2). (e1, e2) ∈ edges G ∧ (e1, e2) ∉ f}" by simp
from mono[unfolded sinvar_mono_def] evalGf wfGf emptyseqGf have "sinvar ⦇nodes = nodes G, edges = {}⦈ nP" by blast
thus "sinvar ⦇nodes = nodes G, edges = {}⦈ nP" .
qed
text‹
@{const minimalize_offending_overapprox} not only computes a set where @{const is_offending_flows_min_set} holds, but it also returns a subset of the input.
›
lemma minimalize_offending_overapprox_keeps_keeps: "(set keeps) ⊆ set (minimalize_offending_overapprox ff keeps G nP)"
proof(induction ff keeps G nP rule: minimalize_offending_overapprox.induct)
qed(simp_all)
lemma minimalize_offending_overapprox_subseteq_input: "set (minimalize_offending_overapprox ff keeps G nP) ⊆ (set ff) ∪ (set keeps)"
proof(induction ff keeps G nP rule: minimalize_offending_overapprox.induct)
case 1 thus ?case by simp
next
case 2 thus ?case by(simp add: delete_edges_list_set delete_edges_simp2) blast
qed
end
context SecurityInvariant_preliminaries
begin
text‹@{const sinvar_mono} naturally holds in @{const SecurityInvariant_preliminaries}›
lemma sinvar_monoI: "sinvar_mono"
unfolding sinvar_mono_def using mono_sinvar by blast
text‹Note: due to monotonicity, the minimality also holds for arbitrary subsets›
lemma assumes "wf_graph G" and "is_offending_flows_min_set F G nP" and "F ⊆ edges G" and "E ⊆ F" and "E ≠ {}"
shows "¬ sinvar ⦇ nodes = nodes G, edges = ((edges G) - F) ∪ E ⦈ nP"
proof -
from sinvar_mono_imp_negative_delete_edge_mono[OF sinvar_monoI ‹wf_graph G›] have negative_delete_edge_mono:
"⋀X Y. X ⊆ Y ⟹ ¬ sinvar ⦇ nodes = nodes G, edges = (edges G) - Y ⦈ nP ⟹ ¬ sinvar ⦇ nodes = nodes G, edges = edges G - X ⦈ nP"
using delete_edges_simp2 by metis
from assms(2) have "(∀(e1, e2)∈F. ¬ sinvar (add_edge e1 e2 (delete_edges G F)) nP)"
unfolding is_offending_flows_min_set_def by simp
with ‹wf_graph G› have min: "(∀(e1, e2)∈F. ¬ sinvar ⦇ nodes = nodes G, edges = ((edges G) - F) ∪ {(e1,e2)} ⦈ nP)"
apply(simp add: delete_edges_simp2 add_edge_def)
apply(rule, rename_tac x, case_tac x, rename_tac e1 e2, simp)
apply(erule_tac x="(e1, e2)" in ballE)
apply(simp_all)
apply(subgoal_tac "insert e1 (insert e2 (nodes G)) = nodes G")
apply(simp)
by (metis assms(3) insert_absorb rev_subsetD wf_graph.E_wfD(1) wf_graph.E_wfD(2))
from ‹E ≠ {}› obtain e where "e ∈ E" by blast
with min ‹E ⊆ F› have mine: "¬ sinvar ⦇ nodes = nodes G, edges = ((edges G) - F) ∪ {e} ⦈ nP" by fast
have e1: "edges G - (F - {e}) = insert e (edges G - F)" using DiffD2 ‹e ∈ E› assms(3) assms(4) by auto
have e2: "edges G - (F - E) = ((edges G) - F) ∪ E" using assms(3) assms(4) by auto
from negative_delete_edge_mono[where Y="F - {e}" and X="F - E"] ‹e ∈ E› have
"¬ sinvar ⦇nodes = nodes G, edges = edges G - (F - {e})⦈ nP ⟹ ¬ sinvar ⦇nodes = nodes G, edges = edges G - (F - E)⦈ nP" by blast
with mine e1 e2 show ?thesis by simp
qed
text‹The algorithm @{const minimalize_offending_overapprox} is correct›
lemma minimalize_offending_overapprox_sound:
"⟦ wf_graph G; is_offending_flows (set ff) G nP; set ff ⊆ edges G; distinct ff ⟧
⟹ is_offending_flows_min_set (set (minimalize_offending_overapprox ff [] G nP)) G nP "
using is_offending_flows_min_set_minimalize_offending_overapprox sinvar_monoI by blast
text‹
If @{term "¬ sinvar G nP"}
Given a list ff, (ff is distinct and a subset of G's edges)
such that ‹sinvar (V, E - ff) nP›
@{const minimalize_offending_overapprox} minimizes ff such that we get an offending flows
Note: choosing ff = edges G is a good choice!
›
theorem minimalize_offending_overapprox_gives_back_an_offending_flow:
"⟦ wf_graph G; is_offending_flows (set ff) G nP; set ff ⊆ edges G; distinct ff ⟧
⟹
(set (minimalize_offending_overapprox ff [] G nP)) ∈ set_offending_flows G nP"
apply(frule(3) minimalize_offending_overapprox_sound)
apply(simp add: set_offending_flows_def)
using minimalize_offending_overapprox_subseteq_input[where keeps="[]", simplified] by blast
end
text‹A version which acts on configured security invariants.
I.e. there is no type @{typ 'a} for the host attributes in it.›
fun minimalize_offending_overapprox :: "('v graph ⇒ bool) ⇒ ('v × 'v) list ⇒ ('v × 'v) list ⇒
'v graph ⇒('v × 'v) list" where
"minimalize_offending_overapprox _ [] keep _ = keep" |
"minimalize_offending_overapprox m (f#fs) keep G = (if m (delete_edges_list G (fs@keep)) then
minimalize_offending_overapprox m fs keep G
else
minimalize_offending_overapprox m fs (f#keep) G
)"
lemma minimalize_offending_overapprox_boundnP:
shows "minimalize_offending_overapprox (λG. m G nP) fs keeps G =
SecurityInvariant_withOffendingFlows.minimalize_offending_overapprox m fs keeps G nP"
apply(induction fs arbitrary: keeps)
apply(simp add: SecurityInvariant_withOffendingFlows.minimalize_offending_overapprox.simps; fail)
apply(simp add: SecurityInvariant_withOffendingFlows.minimalize_offending_overapprox.simps)
done
context SecurityInvariant_withOffendingFlows
begin
text‹If there is a violation and there are no offending flows, there does not exist a possibility to fix the violation by
tightening the policy. @{thm valid_empty_edges_iff_exists_offending_flows} already hints this.›
lemma mono_imp_emptyoffending_eq_nevervalid:
"⟦ sinvar_mono; wf_graph G; ¬ sinvar G nP; set_offending_flows G nP = {}⟧ ⟹
¬ (∃ F ⊆ edges G. sinvar (delete_edges G F) nP)"
proof -
assume mono: "sinvar_mono"
and wfG: "wf_graph G"
and a1: "¬ sinvar G nP"
and a2: "set_offending_flows G nP = {}"
from wfG have wfG': "wf_graph ⦇nodes = nodes G, edges = edges G⦈" by(simp add:wf_graph_def)
from a2 set_offending_flows_def have "∀f ⊆ edges G. ¬ is_offending_flows_min_set f G nP" by simp
from this is_offending_flows_min_set_def is_offending_flows_def a1 have notdeleteconj:
"∀f ⊆ edges G.
¬ sinvar (delete_edges G f) nP ∨
¬ ((∀(e1, e2)∈f. ¬ sinvar (add_edge e1 e2 (delete_edges G f)) nP))"
by simp
have "∀f⊆edges G. ¬ sinvar (delete_edges G f) nP"
proof (rule allI, rule impI)
fix f
assume "f ⊆ edges G"
from this notdeleteconj have
"¬ sinvar (delete_edges G f) nP ∨
¬ ((∀(e1, e2)∈f. ¬ sinvar (add_edge e1 e2 (delete_edges G f)) nP))" by simp
from this show "¬ sinvar (delete_edges G f) nP"
proof
assume "¬ sinvar (delete_edges G f) nP" thus "¬ sinvar (delete_edges G f) nP" .
next
assume "¬ (∀(e1, e2)∈f. ¬ sinvar (add_edge e1 e2 (delete_edges G f)) nP)"
hence "∃(e1,e2)∈f. sinvar (add_edge e1 e2 (delete_edges G f)) nP" by(auto)
from this obtain e1 e2 where e1e2cond: "(e1,e2)∈f ∧ sinvar (add_edge e1 e2 (delete_edges G f)) nP" by blast
from ‹f ⊆ edges G› wfG have "finite f" apply(simp add: wf_graph_def) by (metis rev_finite_subset)
from this obtain listf where listf: "set listf = f ∧ distinct listf" by (metis finite_distinct_list)
from e1e2cond ‹f ⊆ edges G› have Geq:
"(add_edge e1 e2 (delete_edges G f)) = ⦇ nodes = nodes G, edges = edges G - f ∪ {(e1,e2)}⦈"
apply(simp add: graph_ops wfG')
apply(clarify)
using wfG[unfolded wf_graph_def] by force
from this[symmetric] add_edge_wf[OF delete_edges_wf[OF wfG]] have
"wf_graph ⦇nodes = nodes G, edges = edges G - f ∪ {(e1, e2)}⦈" by simp
from mono this have mono'':
"⋀ E'. E' ⊆ edges G - f ∪ {(e1, e2)} ⟹
sinvar ⦇nodes = nodes G, edges = edges G - f ∪ {(e1, e2)}⦈ nP ⟹
sinvar ⦇nodes = nodes G, edges = E'⦈ nP" unfolding sinvar_mono_def by blast
from e1e2cond Geq have "sinvar ⦇ nodes = nodes G, edges = edges G - f ∪ {(e1,e2)}⦈ nP" by simp
from this mono'' have "sinvar ⦇ nodes = nodes G, edges = edges G - f⦈ nP" by auto
hence overapprox: "sinvar (delete_edges G f) nP" by (simp add: delete_edges_simp2)
from a1 overapprox have "is_offending_flows f G nP" by(simp add: is_offending_flows_def)
from this listf have c1: "is_offending_flows (set listf) G nP" by(simp add: is_offending_flows_def)
from listf ‹f ⊆ edges G› have c2: "set listf ⊆ edges G" by simp
from mono_imp_set_offending_flows_not_empty[OF mono wfG c1 c2 conjunct2[OF listf]] have
"set_offending_flows G nP ≠ {}" .
from this a2 have "False" by simp
thus "¬ sinvar (delete_edges G f) nP" by simp
qed
qed
thus ?thesis by simp
qed
end
subsection ‹Monotonicity of offending flows›
context SecurityInvariant_preliminaries
begin
text‹If there is some @{term "F'"} in the offending flows of a small graph and you have a bigger graph,
you can extend @{term "F'"} by some @{term "Fadd"} and minimality in @{term F} is preserved›
lemma minimality_offending_flows_mono_edges_graph_extend:
"⟦ wf_graph ⦇ nodes = V, edges = E ⦈; E' ⊆ E; Fadd ∩ E' = {}; F' ∈ set_offending_flows ⦇nodes = V, edges = E'⦈ nP ⟧ ⟹
(∀(e1, e2)∈F'. ¬ sinvar (add_edge e1 e2 (delete_edges ⦇nodes = V, edges = E ⦈ (F' ∪ Fadd))) nP)"
proof -
assume a1: "wf_graph ⦇ nodes = V, edges = E ⦈"
and a2: "E' ⊆ E"
and a3: "Fadd ∩ E' = {}"
and a4: "F' ∈ set_offending_flows ⦇nodes = V, edges = E'⦈ nP"
from a4 have "F' ⊆ E'" by(simp add: set_offending_flows_def)
obtain Eadd where Eadd_prop: "E' ∪ Eadd = E" and "E' ∩ Eadd = {}" using a2 by blast
have Fadd_notinE': "⋀Fadd. Fadd ∩ E' = {} ⟹ E' - (F' ∪ Fadd) = E' - F'" by blast
from ‹F' ⊆ E'› a1[simplified wf_graph_def] a2 have FinV1: "fst ` F' ⊆ V" and FinV2: "snd ` F' ⊆ V"
proof -
from a1 have "fst ` E ⊆ V" by(simp add: wf_graph_def)
with ‹F' ⊆ E'› a2 show "fst ` F' ⊆ V" by fast
from a1 have "snd ` E ⊆ V" by(simp add: wf_graph_def)
with ‹F' ⊆ E'› a2 show "snd ` F' ⊆ V" by fast
qed
hence insert_e1_e2_V: "∀ (e1, e2) ∈ F'. insert e1 (insert e2 V) = V" by auto
hence add_edge_F: "∀ (e1, e2) ∈ F'. add_edge e1 e2 ⦇nodes = V, edges = E' - F' ⦈ = ⦇nodes = V, edges = (E' - F') ∪ {(e1, e2)}⦈"
by(simp add: add_edge_def)
have Fadd_notinE': "⋀Fadd. Fadd ∩ E' = {} ⟹ E' - (F' ∪ Fadd) = E' - F'" by blast
from ‹F' ⊆ E'› this have Fadd_notinF: "⋀Fadd. Fadd ∩ E' = {} ⟹ F' ∩ Fadd = {}" by blast
have Fadd_subseteq_Eadd: "⋀Fadd. (Fadd ∩ E' = {} ∧ Fadd ⊆ E) = (Fadd ⊆ Eadd)"
proof(rule iffI, goal_cases)
case 1 thus ?case using Eadd_prop a2 by blast
next
case 2 thus ?case using Eadd_prop a2 ‹E' ∩ Eadd = {}› by blast
qed
from a4 have "(∀(e1, e2)∈F'. ¬ sinvar (add_edge e1 e2 ⦇nodes = V, edges = E' - F'⦈) nP)"
by(simp add: set_offending_flows_def is_offending_flows_min_set_def delete_edges_simp2)
with add_edge_F have noteval_F: "∀(e1, e2)∈F'. ¬ sinvar ⦇nodes = V, edges = (E' - F') ∪ {(e1, e2)}⦈ nP"
by fastforce
have tupleBallI: "⋀A P. (⋀e1 e2. (e1, e2)∈A ⟹ P (e1, e2)) ⟹ ALL (e1, e2):A. P (e1, e2)" by force
have "∀(e1, e2)∈F'. ¬ sinvar ⦇nodes = V, edges = (E - (F' ∪ Fadd)) ∪ {(e1, e2)}⦈ nP"
proof(rule tupleBallI)
fix e1 e2
assume f2: "(e1, e2) ∈ F'"
with a3 have gFadd1: "¬ sinvar ⦇nodes = V, edges = (E' - (F' ∪ Fadd)) ∪ {(e1, e2)}⦈ nP"
using Fadd_notinE' noteval_F by fastforce
from a1 FinV1 FinV2 a3 f2 have gFadd2:
"wf_graph ⦇nodes = V, edges = (E - (F' ∪ Fadd)) ∪ {(e1, e2)}⦈"
by(auto simp add: wf_graph_def)
from a2 a3 f2 have gFadd3:
"(E' - (F' ∪ Fadd)) ∪ {(e1, e2)} ⊆ (E - (F' ∪ Fadd)) ∪ {(e1, e2)}" by blast
from mono_sinvar[OF gFadd2 gFadd3] gFadd1
show "¬ sinvar ⦇nodes = V, edges = (E - (F' ∪ Fadd)) ∪ {(e1, e2)}⦈ nP" by blast
qed
thus ?thesis
apply(simp add: delete_edges_simp2 Fadd_notinE' add_edge_def)
apply(clarify)
using insert_e1_e2_V by fastforce
qed
text‹The minimality condition of the offending flows also holds if we increase the graph.›
corollary minimality_offending_flows_mono_edges_graph:
"⟦ wf_graph ⦇ nodes = V, edges = E ⦈;
E' ⊆ E;
F ∈ set_offending_flows ⦇nodes = V, edges = E'⦈ nP ⟧ ⟹
∀(e1, e2)∈F. ¬ sinvar (add_edge e1 e2 (delete_edges ⦇nodes = V, edges = E ⦈ F)) nP"
using minimality_offending_flows_mono_edges_graph_extend[where Fadd="{}", simplified] by presburger
text‹all sets in the set of offending flows are monotonic, hence, for a larger graph, they can be extended to match the smaller graph. I.e. everything is monotonic.›
theorem mono_extend_set_offending_flows: "⟦ wf_graph ⦇ nodes = V, edges = E ⦈; E' ⊆ E; F' ∈ set_offending_flows ⦇ nodes = V, edges = E' ⦈ nP ⟧ ⟹
∃ F ∈ set_offending_flows ⦇ nodes = V, edges = E ⦈ nP. F' ⊆ F"
proof -
fix F'V E E'
assume a1: "wf_graph ⦇ nodes = V, edges = E ⦈"
and a2: "E' ⊆ E"
and a4: "F' ∈ set_offending_flows ⦇nodes = V, edges = E'⦈ nP"
have "⋀f. wf_graph (delete_edges ⦇nodes = V, edges = E⦈ f)"
using delete_edges_wf[OF a1] by fast
hence wf1: "⋀f. wf_graph ⦇nodes = V, edges = E -f⦈"
by(simp add: delete_edges_simp2)
obtain Eadd where Eadd_prop: "E' ∪ Eadd = E" and "E' ∩ Eadd = {}" using a2 by blast
from a4 have "F' ⊆ E'" by(simp add: set_offending_flows_def)
from wf1 have wf2: "wf_graph ⦇nodes = V, edges = E' - F' ∪ Eadd⦈"
apply(subgoal_tac "E' - F' ∪ Eadd = E - F'")
apply fastforce
using Eadd_prop ‹E' ∩ Eadd = {}› ‹F' ⊆ E'› by fast
from a4 have offending_F: "¬ sinvar ⦇nodes = V, edges = E'⦈ nP"
by(simp add: set_offending_flows_def is_offending_flows_min_set_def is_offending_flows_def)
from this mono_sinvar[OF a1 a2] have
goal_noteval: "¬ sinvar ⦇nodes = V, edges = E⦈ nP" by blast
from a4 have eval_E_minus_FEadd_simp: "sinvar ⦇nodes = V, edges = E' - F'⦈ nP"
by(simp add: set_offending_flows_def is_offending_flows_min_set_def is_offending_flows_def delete_edges_simp2)
show "∃ F ∈ set_offending_flows ⦇ nodes = V, edges = E ⦈ nP. F' ⊆ F"
proof(cases "¬ sinvar ⦇nodes = V, edges = E' - F' ∪ Eadd⦈ nP")
assume assumption_new_violation: "¬ sinvar ⦇nodes = V, edges = E' - F' ∪ Eadd⦈ nP"
from a1 have "finite Eadd"
apply(simp add: wf_graph_def)
using Eadd_prop wf_graph.finiteE by blast
from this obtain Eadd_list where Eadd_list_prop: "set Eadd_list = Eadd" and "distinct Eadd_list" by (metis finite_distinct_list)
from a1 have "finite E'"
apply(simp add: wf_graph_def)
using Eadd_prop by blast
from this obtain E'_list where E'_list_prop: "set E'_list = E'" and "distinct E'_list" by (metis finite_distinct_list)
from ‹finite E'› ‹F' ⊆ E'› obtain F'_list where "set F'_list = F'" and "distinct F'_list" by (metis finite_distinct_list rev_finite_subset)
have "E' - F' ∪ Eadd - Eadd = E' - F'" using Eadd_prop ‹E' ∩ Eadd = {}› ‹F' ⊆ E'› by blast
with assumption_new_violation eval_E_minus_FEadd_simp have
"is_offending_flows (set (Eadd_list)) ⦇nodes = V, edges = (E' - F') ∪ Eadd⦈ nP"
by (simp add: Eadd_list_prop delete_edges_simp2 is_offending_flows_def)
from minimalize_offending_overapprox_sound[OF wf2 this _ ‹distinct Eadd_list›] have
"is_offending_flows_min_set
(set (minimalize_offending_overapprox Eadd_list []
⦇nodes = V, edges = E' - F' ∪ Eadd⦈ nP)) ⦇nodes = V, edges = E' - F' ∪ Eadd⦈ nP"
by(simp add: Eadd_list_prop)
with minimalize_offending_overapprox_subseteq_input[of "Eadd_list" "[]" "⦇nodes = V, edges = E' - F' ∪ Eadd⦈" "nP", simplified Eadd_list_prop]
obtain Fadd where Fadd_prop: "is_offending_flows_min_set Fadd ⦇nodes = V, edges = E' - F' ∪ Eadd⦈ nP" and "Fadd ⊆ Eadd" by auto
have graph_edges_simp_helper: "E' - F' ∪ Eadd - Fadd = E - (F' ∪ Fadd)"
using ‹E' ∩ Eadd = {}› Eadd_prop ‹F' ⊆ E'› by blast
from Fadd_prop graph_edges_simp_helper have
goal_eval_Fadd: "sinvar (delete_edges ⦇nodes = V, edges = E⦈ (F' ∪ Fadd)) nP" and
pre_goal_minimal_Fadd: "(∀(e1, e2)∈Fadd. ¬ sinvar (add_edge e1 e2 (delete_edges ⦇nodes = V, edges = E ⦈ (F' ∪ Fadd))) nP)"
by(simp add: is_offending_flows_min_set_def is_offending_flows_def delete_edges_simp2)+
from ‹E' ∩ Eadd = {}› ‹Fadd ⊆ Eadd› have "Fadd ∩ E' = {}" by blast
from minimality_offending_flows_mono_edges_graph_extend[OF a1 ‹E' ⊆ E› ‹Fadd ∩ E' = {}› a4]
have mono_delete_edges_minimal: "(∀(e1, e2)∈F'. ¬ sinvar (add_edge e1 e2 (delete_edges ⦇nodes = V, edges = E ⦈ (F' ∪ Fadd))) nP)" .
from mono_delete_edges_minimal pre_goal_minimal_Fadd have goal_minimal:
"∀(e1, e2)∈F' ∪ Fadd. ¬ sinvar (add_edge e1 e2 (delete_edges ⦇nodes = V, edges = E⦈ (F' ∪ Fadd))) nP" by fastforce
from Eadd_prop ‹Fadd ⊆ Eadd› ‹F' ⊆ E'› have goal_subset: "F' ⊆ E ∧ Fadd ⊆ E" by blast
show "∃ F ∈ set_offending_flows ⦇ nodes = V, edges = E ⦈ nP. F' ⊆ F"
apply(simp add: set_offending_flows_def is_offending_flows_min_set_def is_offending_flows_def)
apply(rule_tac x="F' ∪ Fadd" in exI)
apply(simp add: goal_noteval goal_eval_Fadd goal_minimal goal_subset)
done
next
assume "¬ ¬ sinvar ⦇nodes = V, edges = E' - F' ∪ Eadd⦈ nP"
hence assumption_no_new_violation: "sinvar ⦇nodes = V, edges = E' - F' ∪ Eadd⦈ nP" by simp
from this ‹F' ⊆ E'› ‹E' ∩ Eadd = {}› have "sinvar ⦇nodes = V, edges = E - F'⦈ nP"
proof(subst Eadd_prop[symmetric])
assume a1: "F' ⊆ E'"
assume a2: "E' ∩ Eadd = {}"
assume a3: "sinvar ⦇nodes = V, edges = E' - F' ∪ Eadd⦈ nP"
have "⋀x⇩1. x⇩1 ∩ E' - Eadd = x⇩1 ∩ E'"
using a2 Un_Diff_Int by auto
hence "F' - Eadd = F'"
using a1 by auto
hence "{} ∪ (Eadd - F') = Eadd"
using Int_Diff Un_Diff_Int sup_commute by auto
thus "sinvar ⦇nodes = V, edges = E' ∪ Eadd - F'⦈ nP"
using a3 by (metis Un_Diff sup_bot.left_neutral)
qed
from this have goal_eval: "sinvar (delete_edges ⦇nodes = V, edges = E⦈ F') nP"
by(simp add: delete_edges_simp2)
from Eadd_prop ‹F' ⊆ E'› have goal_subset: "F' ⊆ E" by(blast)
from minimality_offending_flows_mono_edges_graph[OF a1 a2 a4]
have goal_minimal: "(∀(e1, e2)∈F'. ¬ sinvar (add_edge e1 e2 (delete_edges ⦇nodes = V, edges = E ⦈ F')) nP)" .
show "∃ F ∈ set_offending_flows ⦇ nodes = V, edges = E ⦈ nP. F' ⊆ F"
apply(simp add: set_offending_flows_def is_offending_flows_min_set_def is_offending_flows_def)
apply(rule_tac x="F'" in exI)
apply(simp add: goal_noteval goal_subset goal_minimal goal_eval)
done
qed
qed
text‹The offending flows are monotonic.›
corollary offending_flows_union_mono: "⟦ wf_graph ⦇ nodes = V, edges = E ⦈; E' ⊆ E ⟧ ⟹
⋃ (set_offending_flows ⦇ nodes = V, edges = E' ⦈ nP) ⊆ ⋃ (set_offending_flows ⦇ nodes = V, edges = E ⦈ nP)"
apply(clarify)
apply(drule(2) mono_extend_set_offending_flows)
by blast
lemma set_offending_flows_insert_contains_new:
"⟦ wf_graph ⦇ nodes = V, edges = insert e E ⦈; set_offending_flows ⦇nodes = V, edges = E⦈ nP = {}; set_offending_flows ⦇nodes = V, edges = insert e E⦈ nP ≠ {} ⟧ ⟹
{e} ∈ set_offending_flows ⦇nodes = V, edges = insert e E⦈ nP"
proof -
assume wfG: "wf_graph ⦇ nodes = V, edges = insert e E ⦈"
and a1: "set_offending_flows ⦇nodes = V, edges = E⦈ nP = {}"
and a2: "set_offending_flows ⦇nodes = V, edges = insert e E⦈ nP ≠ {}"
from a1 a2 have "e ∉ E" by (metis insert_absorb)
from a1 have a1': "∀F ⊆ E. ¬ is_offending_flows_min_set F ⦇nodes = V, edges = E⦈ nP"
by(simp add: set_offending_flows_def)
from a2 have a2': "∃F ⊆ insert e E. is_offending_flows_min_set F ⦇nodes = V, edges = insert e E⦈ nP"
by(simp add: set_offending_flows_def)
from wfG have wfG': "wf_graph ⦇ nodes = V, edges = E ⦈" by(simp add:wf_graph_def)
from a1 defined_offending[OF wfG'] have evalG: "sinvar ⦇nodes = V, edges = E ⦈ nP" by blast
from sinvar_monoI[unfolded sinvar_mono_def] wfG' this
have goal_eval: "sinvar ⦇nodes = V, edges = E - {e}⦈ nP" by (metis Diff_subset)
from sinvar_no_offending a2 have goal_not_eval: "¬ sinvar ⦇nodes = V, edges = insert e E⦈ nP" by blast
obtain a b where e: "e = (a,b)" by (cases e) blast
with wfG have insert_e_V: "insert a (insert b V) = V" by(auto simp add: wf_graph_def)
from a1' a2' have min_set_e: "is_offending_flows_min_set {e} ⦇nodes = V, edges = insert e E⦈ nP"
apply(simp add: is_offending_flows_min_set_def is_offending_flows_def add_edge_def delete_edges_simp2 goal_not_eval goal_eval)
using goal_not_eval by(simp add: e insert_e_V)
thus "{e} ∈ set_offending_flows ⦇nodes = V, edges = insert e E⦈ nP"
by(simp add: set_offending_flows_def)
qed
end
value "Pow {1::int, 2, 3} ∪ {{8}, {9}}"
value "⋃ x∈Pow {1::int, 2, 3}. ⋃ y ∈ {{8::int}, {9}}. {x ∪ y}"
definition pow_combine :: "'x set ⇒ 'x set set ⇒ 'x set set" where
"pow_combine A B ≡ (⋃ X ∈ Pow A. ⋃ Y ∈ B. {X ∪ Y}) ∪ Pow A"
value "pow_combine {1::int,2} {{5::int, 6}, {8}}"
value "pow_combine {1::int,2} {}"
lemma pow_combine_mono:
fixes S :: "'a set set"
and X :: "'a set"
and Y :: "'a set"
assumes a1: "∀ F ∈ S. F ⊆ X"
shows "∀ F ∈ pow_combine Y S. F ⊆ Y ∪ X"
apply(simp add: pow_combine_def)
apply(rule)
apply(simp)
by (metis Pow_iff assms sup.coboundedI1 sup.orderE sup.orderI sup_assoc)
lemma "S ⊆ pow_combine X S" by(auto simp add: pow_combine_def)
lemma "Pow X ⊆ pow_combine X S" by(auto simp add: pow_combine_def)
lemma rule_pow_combine_fixfst: "B ⊆ C ⟹ pow_combine A B ⊆ pow_combine A C"
by(auto simp add: pow_combine_def)
value "pow_combine {1::int,2} {{5::int, 6}, {1}} ⊆ pow_combine {1::int,2} {{5::int, 6}, {8}}"
lemma rule_pow_combine_fixfst_Union: "⋃ B ⊆ ⋃ C ⟹ ⋃ (pow_combine A B) ⊆ ⋃ (pow_combine A C)"
apply(rule)
apply(fastforce simp: pow_combine_def)
done
context SecurityInvariant_preliminaries
begin
lemma offending_partition_subset_empty:
assumes a1:"∀ F ∈ (set_offending_flows ⦇nodes = V, edges = E ∪ X⦈ nP). F ⊆ X"
and wfGEX: "wf_graph ⦇nodes = V, edges = E ∪ X⦈"
and disj: "E ∩ X = {}"
shows "(set_offending_flows ⦇nodes = V, edges = E⦈ nP) = {}"
proof(rule ccontr)
assume c: "set_offending_flows ⦇nodes = V, edges = E⦈ nP ≠ {}"
from this obtain F' where F'_prop: "F' ∈ set_offending_flows ⦇nodes = V, edges = E⦈ nP" by blast
from F'_prop have "F' ⊆ E" using set_offending_flows_def by simp
from mono_extend_set_offending_flows[OF wfGEX _ F'_prop] have
"∃F∈set_offending_flows ⦇nodes = V, edges = E ∪ X⦈ nP. F' ⊆ F" by blast
from this a1 have "F' ⊆ X" by fast
from F'_prop have "{} ≠ F'" by (metis empty_offending_contra)
from ‹F' ⊆ X› ‹F' ⊆ E› disj ‹{} ≠ F'›
show "False" by blast
qed
corollary partitioned_offending_subseteq_pow_combine:
assumes wfGEX: "wf_graph ⦇nodes = V, edges = E ∪ X⦈"
and disj: "E ∩ X = {}"
and partitioned_offending: "∀ F ∈ (set_offending_flows ⦇nodes = V, edges = E ∪ X⦈ nP). F ⊆ X"
shows "(set_offending_flows ⦇nodes = V, edges = E ∪ X⦈ nP) ⊆ pow_combine X (set_offending_flows ⦇nodes = V, edges = E⦈ nP)"
apply(subst offending_partition_subset_empty[OF partitioned_offending wfGEX disj])
apply(simp add: pow_combine_def)
apply(rule)
apply(simp)
using partitioned_offending by simp
end
context SecurityInvariant_preliminaries
begin
text‹Knowing that the ‹⋃ offending is ⊆ X›, removing something from the graphs's edges,
it also disappears from the offending flows.›
lemma Un_set_offending_flows_bound_minus:
assumes wfG: "wf_graph ⦇ nodes = V, edges = E ⦈"
and Foffending: "⋃(set_offending_flows ⦇nodes = V, edges = E⦈ nP) ⊆ X"
shows "⋃(set_offending_flows ⦇nodes = V, edges = E - {f}⦈ nP) ⊆ X - {f}"
proof -
from wfG have wfG': "wf_graph ⦇ nodes = V, edges = E - {f} ⦈"
by(auto simp add: wf_graph_def finite_subset)
from offending_flows_union_mono[OF wfG, where E'="E - {f}"] have
"⋃(set_offending_flows ⦇nodes = V, edges = E - {f}⦈ nP) - {f} ⊆ ⋃(set_offending_flows ⦇nodes = V, edges = E⦈ nP) - {f}" by blast
also have
"⋃(set_offending_flows ⦇nodes = V, edges = E - {f}⦈ nP) ⊆ ⋃(set_offending_flows ⦇nodes = V, edges = E - {f}⦈ nP) - {f}"
apply(simp add: set_offending_flows_simp[OF wfG']) by blast
ultimately have Un_set_offending_flows_minus:
"⋃(set_offending_flows ⦇nodes = V, edges = E - {f}⦈ nP) ⊆ ⋃(set_offending_flows ⦇nodes = V, edges = E ⦈ nP) - {f}"
by blast
from Foffending Un_set_offending_flows_minus
show ?thesis by blast
qed
text‹
If the offending flows are bound by some @{term X},
the we can remove all finite @{term "E'"}from the graph's edges
and the offending flows from the smaller graph are bound by @{term "X - E'"}.
›
lemma Un_set_offending_flows_bound_minus_subseteq:
assumes wfG: "wf_graph ⦇ nodes = V, edges = E ⦈"
and Foffending: "⋃ (set_offending_flows ⦇nodes = V, edges = E⦈ nP) ⊆ X"
shows "⋃ (set_offending_flows ⦇nodes = V, edges = E - E'⦈ nP) ⊆ X - E'"
proof -
from wfG have wfG': "wf_graph ⦇ nodes = V, edges = E - E' ⦈"
by(auto simp add: wf_graph_def finite_subset)
from offending_flows_union_mono[OF wfG, where E'="E - E'"] have
"⋃(set_offending_flows ⦇nodes = V, edges = E - E'⦈ nP) - E' ⊆ ⋃(set_offending_flows ⦇nodes = V, edges = E⦈ nP) - E'" by blast
also have
"⋃(set_offending_flows ⦇nodes = V, edges = E - E'⦈ nP) ⊆ ⋃(set_offending_flows ⦇nodes = V, edges = E - E'⦈ nP) - E'"
apply(simp add: set_offending_flows_simp[OF wfG']) by blast
ultimately have Un_set_offending_flows_minus:
"⋃ (set_offending_flows ⦇nodes = V, edges = E - E'⦈ nP) ⊆ ⋃ (set_offending_flows ⦇nodes = V, edges = E ⦈ nP) - E'"
by blast
from Foffending Un_set_offending_flows_minus
show ?thesis by blast
qed
corollary Un_set_offending_flows_bound_minus_subseteq':
"⟦ wf_graph ⦇ nodes = V, edges = E ⦈;
⋃ (set_offending_flows ⦇ nodes = V, edges = E ⦈ nP) ⊆ X ⟧ ⟹
⋃ (set_offending_flows ⦇ nodes = V, edges = E - E' ⦈ nP) ⊆ X - E'"
apply(drule(1) Un_set_offending_flows_bound_minus_subseteq) by blast
end
end