Theory L4_Protocol_Flags
theory L4_Protocol_Flags
imports Simple_Firewall.L4_Protocol
begin
section‹Matching TCP Flags›
datatype ipt_tcp_flags = TCP_Flags "tcp_flag set"
"tcp_flag set"
definition ipt_tcp_syn :: "ipt_tcp_flags" where
"ipt_tcp_syn ≡ TCP_Flags {TCP_SYN,TCP_RST,TCP_ACK,TCP_FIN} {TCP_SYN}"
fun match_tcp_flags :: "ipt_tcp_flags ⇒ tcp_flag set ⇒ bool" where
"match_tcp_flags (TCP_Flags fmask c) flags ⟷ (flags ∩ fmask) = c"
lemma "match_tcp_flags ipt_tcp_syn {TCP_SYN, TCP_URG, TCP_PSH}" by eval
lemma match_tcp_flags_nomatch: "¬ c ⊆ fmask ⟹ ¬ match_tcp_flags (TCP_Flags fmask c) pkt" by auto
definition ipt_tcp_flags_NoMatch :: "ipt_tcp_flags" where
"ipt_tcp_flags_NoMatch ≡ TCP_Flags {} {TCP_SYN}"
lemma ipt_tcp_flags_NoMatch: "¬ match_tcp_flags ipt_tcp_flags_NoMatch pkt" by(simp add: ipt_tcp_flags_NoMatch_def)
definition ipt_tcp_flags_Any :: ipt_tcp_flags where
"ipt_tcp_flags_Any ≡ TCP_Flags {} {}"
lemma ipt_tcp_flags_Any: "match_tcp_flags ipt_tcp_flags_Any pkt" by(simp add: ipt_tcp_flags_Any_def)
lemma ipt_tcp_flags_Any_isUNIV: "fmask = {} ∧ c = {} ⟷ (∀pkt. match_tcp_flags (TCP_Flags fmask c) pkt)" by auto
fun match_tcp_flags_conjunct :: "ipt_tcp_flags ⇒ ipt_tcp_flags ⇒ ipt_tcp_flags" where
"match_tcp_flags_conjunct (TCP_Flags fmask1 c1) (TCP_Flags fmask2 c2) = (
if c1 ⊆ fmask1 ∧ c2 ⊆ fmask2 ∧ fmask1 ∩ fmask2 ∩ c1 = fmask1 ∩ fmask2 ∩ c2
then (TCP_Flags (fmask1 ∪ fmask2) (c1 ∪ c2))
else ipt_tcp_flags_NoMatch)"
lemma match_tcp_flags_conjunct: "match_tcp_flags (match_tcp_flags_conjunct f1 f2) pkt ⟷ match_tcp_flags f1 pkt ∧ match_tcp_flags f2 pkt"
apply(cases f1, cases f2, simp)
apply(rename_tac fmask1 c1 fmask2 c2)
apply(intro conjI impI)
apply(elim conjE)
apply blast
apply(simp add: ipt_tcp_flags_NoMatch)
apply fast
done
declare match_tcp_flags_conjunct.simps[simp del]
text‹Same as @{const match_tcp_flags_conjunct}, but returns @{const None} if result cannot match anyway›
definition match_tcp_flags_conjunct_option :: "ipt_tcp_flags ⇒ ipt_tcp_flags ⇒ ipt_tcp_flags option" where
"match_tcp_flags_conjunct_option f1 f2 = (case match_tcp_flags_conjunct f1 f2 of (TCP_Flags fmask c) ⇒ if c ⊆ fmask then Some (TCP_Flags fmask c) else None)"
lemma "match_tcp_flags_conjunct_option ipt_tcp_syn (TCP_Flags {TCP_RST,TCP_ACK} {TCP_RST}) = None" by eval
lemma match_tcp_flags_conjunct_option_Some: "match_tcp_flags_conjunct_option f1 f2 = Some f3 ⟹
match_tcp_flags f1 pkt ∧ match_tcp_flags f2 pkt ⟷ match_tcp_flags f3 pkt"
apply(simp add: match_tcp_flags_conjunct_option_def split: ipt_tcp_flags.split_asm if_split_asm)
using match_tcp_flags_conjunct by blast
lemma match_tcp_flags_conjunct_option_None: "match_tcp_flags_conjunct_option f1 f2 = None ⟹
¬(match_tcp_flags f1 pkt ∧ match_tcp_flags f2 pkt)"
apply(simp add: match_tcp_flags_conjunct_option_def split: ipt_tcp_flags.split_asm if_split_asm)
using match_tcp_flags_conjunct match_tcp_flags_nomatch by metis
lemma match_tcp_flags_conjunct_option: "(case match_tcp_flags_conjunct_option f1 f2 of None ⇒ False | Some f3 ⇒ match_tcp_flags f3 pkt) ⟷ match_tcp_flags f1 pkt ∧ match_tcp_flags f2 pkt"
apply(simp split: option.split)
using match_tcp_flags_conjunct_option_Some match_tcp_flags_conjunct_option_None by blast
fun ipt_tcp_flags_equal :: "ipt_tcp_flags ⇒ ipt_tcp_flags ⇒ bool" where
"ipt_tcp_flags_equal (TCP_Flags fmask1 c1) (TCP_Flags fmask2 c2) = (
if c1 ⊆ fmask1 ∧ c2 ⊆ fmask2
then c1 = c2 ∧ fmask1 = fmask2
else (¬ c1 ⊆ fmask1) ∧ (¬ c2 ⊆ fmask2))"
context
begin
private lemma funny_set_falg_fmask_helper: "c2 ⊆ fmask2 ⟹ (c1 = c2 ∧ fmask1 = fmask2) = (∀pkt. (pkt ∩ fmask1 = c1) = (pkt ∩ fmask2 = c2))"
apply rule
apply presburger
apply(subgoal_tac "fmask1 = fmask2")
apply blast
proof -
assume a1: "c2 ⊆ fmask2"
assume a2: "∀pkt. (pkt ∩ fmask1 = c1) = (pkt ∩ fmask2 = c2)"
have f3: "⋀A Aa. (A::'a set) - - Aa = Aa - - A"
by (simp add: inf_commute)
have f4: "⋀A Aa. (A::'a set) - - (- Aa) = A - Aa"
by simp
have f5: "⋀A Aa Ab. (A::'a set) - - Aa - - Ab = A - - (Aa - - Ab)"
by blast
have f6: "⋀A Aa. (A::'a set) - (- A - Aa) = A"
by fastforce
have f7: "⋀A Aa. - (A::'a set) - - Aa = Aa - A"
using f4 f3 by presburger
have f8: "⋀A Aa. - (A::'a set) = - (A - Aa) - (A - - Aa)"
by blast
have f9: "c1 = - (- c1)"
by blast
have f10: "⋀A. A - c1 - c1 = A - c1"
by blast
have "⋀A. A - - (fmask1 - - fmask2) = c2 ∨ A - - fmask1 ≠ c1"
using f6 f5 a2 by (metis (no_types) Diff_Compl)
hence f11: "⋀A. - A - - (fmask1 - - fmask2) = c2 ∨ fmask1 - A ≠ c1"
using f7 by meson
have "c2 - fmask2 = {}"
using a1 by force
hence f12: "- c2 - (fmask2 - c2) = - fmask2"
by blast
hence "fmask2 - - c2 = c2"
by blast
hence f13: "fmask1 - - c2 = c1"
using f3 a2 by simp
hence f14: "c1 = c2"
using f11 by blast
hence f15: "fmask2 - (fmask1 - c1) = c1"
using f13 f10 f9 f8 f7 f3 a2 by (metis Diff_Compl)
have "fmask1 - (fmask2 - c1) = c1"
using f14 f12 f10 f9 f8 f4 f3 a2 by (metis Diff_Compl)
thus "fmask1 = fmask2"
using f15 by blast
qed
lemma ipt_tcp_flags_equal: "ipt_tcp_flags_equal f1 f2 ⟷ (∀pkt. match_tcp_flags f1 pkt = match_tcp_flags f2 pkt)"
apply(cases f1, cases f2, simp)
apply(rename_tac fmask1 c1 fmask2 c2)
apply(intro conjI impI)
using funny_set_falg_fmask_helper apply metis
apply blast
done
end
declare ipt_tcp_flags_equal.simps[simp del]
end