Theory Generic_SimpleFw
section‹Generalize Simple Firewall›
theory Generic_SimpleFw
imports SimpleFw_Semantics "Common/List_Product_More" "Common/Option_Helpers"
begin
subsection‹Semantics›
text‹The semantics of the @{term simple_fw} is quite close to @{const List.find}.
The idea of the generalized @{term simple_fw} semantics is that you can have anything as the
resulting action, not only a @{type simple_action}.›
definition generalized_sfw
:: "('i::len simple_match × 'a) list ⇒ ('i, 'pkt_ext) simple_packet_scheme ⇒ ('i simple_match × 'a) option"
where
"generalized_sfw l p ≡ find (λ(m,a). simple_matches m p) l"
subsection‹Lemmas›
lemma generalized_sfw_simps:
"generalized_sfw [] p = None"
"generalized_sfw (a # as) p = (if (case a of (m,_) ⇒ simple_matches m p) then Some a else generalized_sfw as p)"
unfolding generalized_sfw_def by simp_all
lemma generalized_sfw_append:
"generalized_sfw (a @ b) p = (case generalized_sfw a p of Some x ⇒ Some x
| None ⇒ generalized_sfw b p)"
by(induction a) (simp_all add: generalized_sfw_simps)
lemma simple_generalized_undecided:
"simple_fw fw p ≠ Undecided ⟹ generalized_sfw (map simple_rule_dtor fw) p ≠ None"
by(induction fw)
(clarsimp simp add: generalized_sfw_def simple_fw_alt simple_rule_dtor_def
split: prod.splits if_splits simple_action.splits simple_rule.splits)+
lemma generalized_sfwSomeD: "generalized_sfw fw p = Some (r,d) ⟹ (r,d) ∈ set fw ∧ simple_matches r p"
unfolding generalized_sfw_def
by(induction fw) (simp split: if_split_asm)+
lemma generalized_sfw_NoneD: "generalized_sfw fw p = None ⟹ ∀(a,b) ∈ set fw. ¬ simple_matches a p"
by(induction fw) (clarsimp simp add: generalized_sfw_simps split: if_splits)+
lemma generalized_fw_split: "generalized_sfw fw p = Some r ⟹ ∃fw1 fw3. fw = fw1 @ r # fw3 ∧ generalized_sfw fw1 p = None"
apply(induction fw rule: rev_induct)
apply(simp add: generalized_sfw_simps generalized_sfw_append split: option.splits;fail)
apply(clarsimp simp add: generalized_sfw_simps generalized_sfw_append split: option.splits if_splits)
apply blast+
done
lemma generalized_sfw_filterD:
"generalized_sfw (filter f fw) p = Some (r,d) ⟹ simple_matches r p ∧ f (r,d)"
by(induction fw) (simp_all add: generalized_sfw_simps split: if_splits)
lemma generalized_sfw_mapsnd:
"generalized_sfw (map (apsnd f) fw) p = map_option (apsnd f) (generalized_sfw fw p)"
by(induction fw) (simp add: generalized_sfw_simps split: prod.splits)+
subsection‹Equality with the Simple Firewall›
text‹A matching action of the simple firewall directly corresponds to a filtering decision›
definition simple_action_to_decision :: "simple_action ⇒ state" where
"simple_action_to_decision a ≡ case a of Accept ⇒ Decision FinalAllow
| Drop ⇒ Decision FinalDeny"
text‹The @{const simple_fw} and the @{const generalized_sfw} are equal, if the state is translated appropriately.›
lemma simple_fw_iff_generalized_fw:
"simple_fw fw p = simple_action_to_decision a ⟷ (∃r. generalized_sfw (map simple_rule_dtor fw) p = Some (r,a))"
by(induction fw)
(clarsimp simp add: generalized_sfw_simps simple_rule_dtor_def simple_fw_alt simple_action_to_decision_def
split: simple_rule.splits if_splits simple_action.splits)+
lemma simple_fw_iff_generalized_fw_accept:
"simple_fw fw p = Decision FinalAllow ⟷ (∃r. generalized_sfw (map simple_rule_dtor fw) p = Some (r, Accept))"
by(fact simple_fw_iff_generalized_fw[where a = simple_action.Accept,
unfolded simple_action_to_decision_def simple_action.simps])
lemma simple_fw_iff_generalized_fw_drop:
"simple_fw fw p = Decision FinalDeny ⟷ (∃r. generalized_sfw (map simple_rule_dtor fw) p = Some (r, Drop))"
by(fact simple_fw_iff_generalized_fw[where a = simple_action.Drop,
unfolded simple_action_to_decision_def simple_action.simps])
subsection‹Joining two firewalls, i.e. a packet is send through both sequentially.›
definition generalized_fw_join
:: "('i::len simple_match × 'a) list ⇒ ('i simple_match × 'b) list ⇒ ('i simple_match × 'a × 'b) list"
where
"generalized_fw_join l1 l2 ≡ [(u,(a,b)). (m1,a) ← l1, (m2,b) ← l2, u ← option2list (simple_match_and m1 m2)]"
lemma generalized_fw_join_1_Nil[simp]: "generalized_fw_join [] f2 = []"
unfolding generalized_fw_join_def by(induction f2) simp+
lemma generalized_fw_join_2_Nil[simp]: "generalized_fw_join f1 [] = []"
unfolding generalized_fw_join_def by(induction f1) simp+
lemma generalized_fw_join_cons_1:
"generalized_fw_join ((am,ad) # l1) l2 =
[(u,(ad,b)). (m2,b) ← l2, u ← option2list (simple_match_and am m2)] @ generalized_fw_join l1 l2"
unfolding generalized_fw_join_def by(simp)
lemma generalized_fw_join_1_nomatch:
"¬ simple_matches am p ⟹
generalized_sfw [(u,(ad,b)). (m2,b) ← l2, u ← option2list (simple_match_and am m2)] p = None"
by(induction l2)
(clarsimp simp add: generalized_sfw_simps generalized_sfw_append option2list_def simple_match_and_SomeD
split: prod.splits option.splits)+
lemma generalized_fw_join_2_nomatch:
"¬ simple_matches bm p ⟹
generalized_sfw (generalized_fw_join as ((bm, bd) # bs)) p = generalized_sfw (generalized_fw_join as bs) p"
proof(induction as)
case (Cons a as)
note mIH = Cons.IH[OF Cons.prems]
obtain am ad where a[simp]: "a = (am, ad)" by(cases a)
have *: "generalized_sfw (concat (map (λ(m2, b). map (λu. (u, ad, b)) (option2list (simple_match_and am m2))) ((bm, bd) # bs))) p =
generalized_sfw (concat (map (λ(m2, b). map (λu. (u, ad, b)) (option2list (simple_match_and am m2))) bs)) p"
unfolding list.map prod.simps
apply(cases "simple_match_and am bm")
apply(simp add: option2list_def; fail)
apply(frule simple_match_and_SomeD[of _ _ _ p])
apply(subst option2list_def)
apply(unfold concat.simps)
apply(simp add: generalized_sfw_simps Cons.prems)
done
show ?case
unfolding a
unfolding generalized_fw_join_cons_1
unfolding generalized_sfw_append
unfolding mIH
unfolding *
..
qed(simp add: generalized_fw_join_def)
lemma generalized_fw_joinI:
"⟦generalized_sfw f1 p = Some (r1,d1); generalized_sfw f2 p = Some (r2,d2)⟧ ⟹
generalized_sfw (generalized_fw_join f1 f2) p = Some (the (simple_match_and r1 r2), d1,d2)"
proof(induction f1)
case (Cons a as)
obtain am ad where a[simp]: "a = Pair am ad" by(cases a)
show ?case proof(cases "simple_matches am p")
case True
hence dra: "d1 = ad" "r1 = am" using Cons.prems by(simp_all add: generalized_sfw_simps)
from Cons.prems(2) show ?thesis unfolding a dra
proof(induction f2)
case (Cons b bs)
obtain bm bd where b[simp]: "b = Pair bm bd" by(cases b)
thus ?case
proof(cases "simple_matches bm p")
case True
hence drb: "d2 = bd" "r2 = bm" using Cons.prems by(simp_all add: generalized_sfw_simps)
from True ‹simple_matches am p› obtain ruc where sma[simp]:
"simple_match_and am bm = Some ruc" "simple_matches ruc p"
using simple_match_and_correct[of am p bm]
by(simp split: option.splits)
show ?thesis unfolding b
by(simp add: generalized_fw_join_def option2list_def generalized_sfw_simps drb)
next
case False
with Cons.prems have bd:
"generalized_sfw (b # bs) p = generalized_sfw bs p"
"generalized_sfw (b # bs) p = Some (r2, d2)"
by(simp_all add: generalized_sfw_simps)
note mIH = Cons.IH[OF bd(2)[unfolded bd(1)]]
show ?thesis
unfolding mIH[symmetric] b
using generalized_fw_join_2_nomatch[OF False, of "(am, ad) # as" bd bs]
.
qed
qed(simp add: generalized_sfw_simps generalized_fw_join_def)
next
case False
with Cons.prems have "generalized_sfw (a # as) p = generalized_sfw as p"
by(simp add: generalized_sfw_simps)
with Cons.prems have "generalized_sfw as p = Some (r1, d1)" by simp
note mIH = Cons.IH[OF this Cons.prems(2)]
show ?thesis
unfolding mIH[symmetric] a
unfolding generalized_fw_join_cons_1
unfolding generalized_sfw_append
unfolding generalized_fw_join_1_nomatch[OF False, of ad f2]
by simp
qed
qed(simp add: generalized_fw_join_def generalized_sfw_simps;fail)
lemma generalized_fw_joinD:
"generalized_sfw (generalized_fw_join f1 f2) p = Some (u, d1,d2) ⟹
∃r1 r2. generalized_sfw f1 p = Some (r1,d1) ∧ generalized_sfw f2 p = Some (r2,d2) ∧ Some u = simple_match_and r1 r2"
proof(induction f1)
case (Cons a as)
obtain am ad where a[simp]: "a = Pair am ad" by(cases a)
show ?case proof(cases "simple_matches am p", rule exI)
case True
show "∃r2. generalized_sfw (a # as) p = Some (am, d1) ∧ generalized_sfw f2 p = Some (r2, d2) ∧ Some u = simple_match_and am r2"
using Cons.prems
proof(induction f2)
case (Cons b bs)
obtain bm bd where b[simp]: "b = Pair bm bd" by(cases b)
show ?case
proof(cases "simple_matches bm p", rule exI)
case True
with ‹simple_matches am p› obtain u'
where sma: "simple_match_and am bm = Some u' ∧ simple_matches u' p"
using simple_match_and_correct[of am p bm] by(simp split: option.splits)
show "generalized_sfw (a # as) p = Some (am, d1) ∧ generalized_sfw (b # bs) p = Some (bm, d2) ∧ Some u = simple_match_and am bm"
using Cons.prems True ‹simple_matches am p›
by(simp add: generalized_fw_join_def generalized_sfw_append sma generalized_sfw_simps)
next
case False
have "generalized_sfw (generalized_fw_join (a # as) bs) p = Some (u, d1, d2)"
using Cons.prems unfolding b unfolding generalized_fw_join_2_nomatch[OF False] .
note Cons.IH[OF this]
moreover have "generalized_sfw (b # bs) p = generalized_sfw bs p" using False by(simp add: generalized_sfw_simps)
ultimately show ?thesis by presburger
qed
qed(simp add: generalized_sfw_simps)
next
case False
with Cons.prems have "generalized_sfw (generalized_fw_join as f2) p = Some (u, d1, d2)" by(simp add: generalized_fw_join_cons_1 generalized_sfw_append generalized_fw_join_1_nomatch)
note Cons.IH[OF this]
moreover have "generalized_sfw (a # as) p = generalized_sfw as p" using False by(simp add: generalized_sfw_simps)
ultimately show ?thesis by presburger
qed
qed(simp add: generalized_fw_join_def generalized_sfw_simps)
text‹We imagine two firewalls are positioned directly after each other.
The first one has ruleset rs1 installed, the second one has ruleset rs2 installed.
A packet needs to pass both firewalls.›
theorem simple_fw_join:
defines "rule_translate ≡
map (λ(u,a,b). SimpleRule u (if a = Accept ∧ b = Accept then Accept else Drop))"
shows
"simple_fw rs1 p = Decision FinalAllow ∧ simple_fw rs2 p = Decision FinalAllow ⟷
simple_fw (rule_translate (generalized_fw_join (map simple_rule_dtor rs1) (map simple_rule_dtor rs2))) p = Decision FinalAllow"
proof -
have hlp1:
"simple_rule_dtor ∘ (λ(u, a, b). SimpleRule u (if a = Accept ∧ b = Accept then Accept else Drop)) =
apsnd (λ(a, b). if a = Accept ∧ b = Accept then Accept else Drop)"
unfolding fun_eq_iff comp_def by(simp add: simple_rule_dtor_def)
show ?thesis
unfolding simple_fw_iff_generalized_fw_accept
apply(rule)
apply(clarify)
apply(drule (1) generalized_fw_joinI)
apply(simp add: hlp1 rule_translate_def generalized_sfw_mapsnd ;fail)
apply(clarsimp simp add: hlp1 generalized_sfw_mapsnd rule_translate_def)
apply(drule generalized_fw_joinD)
apply(clarsimp split: if_splits)
done
qed
theorem simple_fw_join2:
defines "to_simple_rule_list ≡ map (apsnd (λ(a,b) ⇒ (case a of Accept ⇒ b
| Drop ⇒ Drop)))"
shows "simple_fw rs1 p = Decision FinalAllow ∧ simple_fw rs2 p = Decision FinalAllow ⟷
(∃m. (generalized_sfw (to_simple_rule_list
(generalized_fw_join (map simple_rule_dtor rs1) (map simple_rule_dtor rs2))) p) = Some (m, Accept))"
unfolding simple_fw_iff_generalized_fw_accept
apply(rule)
apply(clarify)
apply(drule (1) generalized_fw_joinI)
apply(clarsimp simp add: to_simple_rule_list_def generalized_sfw_mapsnd; fail)
apply(clarsimp simp add: to_simple_rule_list_def generalized_sfw_mapsnd)
apply(drule generalized_fw_joinD)
apply(clarsimp split: if_splits simple_action.splits)
done
lemma generalized_fw_join_1_1:
"generalized_fw_join [(m1,d1)] fw2 = foldr (λ(m2,d2). (@) (case simple_match_and m1 m2 of None ⇒ [] | Some mu ⇒ [(mu,d1,d2)])) fw2 []"
proof -
have concat_map_foldr: "concat (map (λx. f x) l) = foldr (λx. (@) (f x)) l []" for f :: "'x ⇒ 'y list" and l
by(induction l) simp_all
show ?thesis
apply(simp add: generalized_fw_join_cons_1 option2list_def)
apply(simp add: concat_map_foldr)
apply(unfold list.map prod.case_distrib option.case_distrib)
by simp
qed
lemma generalized_sfw_2_join_None:
"generalized_sfw fw2 p = None ⟹ generalized_sfw (generalized_fw_join fw1 fw2) p = None"
by(induction fw2) (simp_all add: generalized_sfw_simps generalized_sfw_append generalized_fw_join_2_nomatch split: if_splits option.splits prod.splits)
lemma generalized_sfw_1_join_None:
"generalized_sfw fw1 p = None ⟹ generalized_sfw (generalized_fw_join fw1 fw2) p = None"
by(induction fw1) (simp_all add: generalized_sfw_simps generalized_fw_join_cons_1 generalized_sfw_append generalized_fw_join_1_nomatch split: if_splits option.splits prod.splits)
lemma generalized_sfw_join_set: "(a, b1, b2) ∈ set (generalized_fw_join f1 f2) ⟷
(∃a1 a2. (a1, b1) ∈ set f1 ∧ (a2, b2) ∈ set f2 ∧ simple_match_and a1 a2 = Some a)"
unfolding generalized_fw_join_def
apply(rule iffI)
subgoal unfolding generalized_fw_join_def by(clarsimp simp: option2set_def split: option.splits) blast
by(clarsimp simp: option2set_def split: option.splits) fastforce
subsection‹Validity›
text‹There's validity of matches on @{const generalized_sfw}, too, even on the join.›
definition gsfw_valid :: "('i::len simple_match × 'c) list ⇒ bool" where
"gsfw_valid ≡ list_all (simple_match_valid ∘ fst)"
lemma gsfw_join_valid: "gsfw_valid f1 ⟹ gsfw_valid f2 ⟹ gsfw_valid (generalized_fw_join f1 f2)"
unfolding gsfw_valid_def
apply(induction f1)
apply(simp;fail)
apply(simp)
apply(rename_tac a f1)
apply(case_tac a)
apply(simp add: generalized_fw_join_cons_1)
apply(clarify)
apply(thin_tac "list_all _ f1")
apply(thin_tac "list_all _ (generalized_fw_join _ _)")
apply(induction f2)
apply(simp;fail)
apply(simp)
apply(clarsimp simp add: option2list_def list_all_iff)
using simple_match_and_valid apply metis
done
lemma gsfw_validI: "simple_fw_valid fw ⟹ gsfw_valid (map simple_rule_dtor fw)"
unfolding gsfw_valid_def simple_fw_valid_def
by(clarsimp simp add: simple_rule_dtor_def list_all_iff split: simple_rule.splits) fastforce
end