afp-mirror
/
UPF_Firewall
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Reformatting & cleanup.

This commit is contained in:
Achim D. Brucker 2016-12-28 22:40:36 +00:00
parent 90fd8493c7
commit 0697dd78f1
13 changed files with 389 additions and 646 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

35
Examples/DMZ/DMZ.thy
View File

@ -38,38 +38,9 @@
section {* A Simple DMZ Setup *} section {* A Simple DMZ Setup *}
theory theory
DMZ DMZ
imports imports
DMZDatatype DMZDatatype
DMZInteger DMZInteger
begin begin
text{* This scenario is slightly more complicated than the SimpleDMZ
one, as we now also model specific servers within one
network. Therefore, we cannot use anymore the modelling using
datatype synonym, but only use the one where an address is modelled as an
integer (with ports).
The scenario is the following:
\begin{labeling}{Networks:}
\item[Networks:]
\begin{itemize}
\item Intranet (Company intern network)
\item DMZ (demilitarised zone, servers, etc), containing
at least two distinct servers ``mail'' and ``web''
\item Internet (``all others'')
\end{itemize}
\item[Policy:]
\begin{itemize}
\item allow http(s) from Intranet to Internet
\item deny all trafic from Internet to Intranet
\item allo imaps and smtp from intranet to mailserver
\item allow smtp from Internet to mailserver
\item allow http(s) from Internet to webserver
\item deny everything else
\end{itemize}
\end{labeling}
*}
end end

72
Examples/DMZ/DMZDatatype.thy
View File

@ -38,83 +38,81 @@
subsection {* DMZ Datatype *} subsection {* DMZ Datatype *}
theory theory
DMZDatatype DMZDatatype
imports imports
"../../UPF-Firewall" "../../UPF-Firewall"
begin begin
text{*
This is the fourth scenario, slightly more complicated than the previous one, as we now also
model specific servers within one network. Therefore, we could not use anymore the modelling
using datatype synonym, but only use the one where an address is modelled as an
integer (with ports).
text{* This is the fourth scenario, slightly more complicated than the Just for comparison, this theory is the same scenario with datatype synonym anyway, but with four
previous one, as we now also model specific servers within one distinct networks instead of one contained in another. As there is no corresponding network model
network. Therefore, we could not use anymore the modelling using included, we need to define a custom one.
datatype synonym, but only use the one where an address is modelled as an *}
integer (with ports).
Just for comparison, this theory is the same scenario with datatype synonym
anyway, but with four distinct networks instead of one contained in
another. As there is no corresponding network model included, we need
to define a custom one. *}
datatype Adr = Intranet | Internet | Mail | Web | DMZ datatype Adr = Intranet | Internet | Mail | Web | DMZ
instance Adr::adr .. instance Adr::adr ..
type_synonym port = int type_synonym port = int
type_synonym Networks = "Adr \<times> port" type_synonym Networks = "Adr \<times> port"
definition definition
intranet::"Networks net" where intranet::"Networks net" where
"intranet = {{(a,b). a= Intranet}}" "intranet = {{(a,b). a= Intranet}}"
definition definition
dmz :: "Networks net" where dmz :: "Networks net" where
"dmz = {{(a,b). a= DMZ}}" "dmz = {{(a,b). a= DMZ}}"
definition definition
mail :: "Networks net" where mail :: "Networks net" where
"mail = {{(a,b). a=Mail}}" "mail = {{(a,b). a=Mail}}"
definition definition
web :: "Networks net" where web :: "Networks net" where
"web = {{(a,b). a=Web}}" "web = {{(a,b). a=Web}}"
definition definition
internet :: "Networks net" where internet :: "Networks net" where
"internet = {{(a,b). a= Internet}}" "internet = {{(a,b). a= Internet}}"
definition definition
Intranet_mail_port :: "(Networks ,DummyContent) FWPolicy" where Intranet_mail_port :: "(Networks ,DummyContent) FWPolicy" where
"Intranet_mail_port = (allow_from_ports_to {21::port,14} intranet mail)" "Intranet_mail_port = (allow_from_ports_to {21::port,14} intranet mail)"
definition definition
Intranet_Internet_port :: "(Networks,DummyContent) FWPolicy" where Intranet_Internet_port :: "(Networks,DummyContent) FWPolicy" where
"Intranet_Internet_port = allow_from_ports_to {80::port,90} intranet internet" "Intranet_Internet_port = allow_from_ports_to {80::port,90} intranet internet"
definition definition
Internet_web_port :: "(Networks,DummyContent) FWPolicy" where Internet_web_port :: "(Networks,DummyContent) FWPolicy" where
"Internet_web_port = (allow_from_ports_to {80::port,90} internet web)" "Internet_web_port = (allow_from_ports_to {80::port,90} internet web)"
definition definition
Internet_mail_port :: "(Networks,DummyContent) FWPolicy" where Internet_mail_port :: "(Networks,DummyContent) FWPolicy" where
"Internet_mail_port = (allow_all_from_port_to internet (21::port) dmz)" "Internet_mail_port = (allow_all_from_port_to internet (21::port) dmz)"
definition definition
policyPort :: "(Networks, DummyContent) FWPolicy" where policyPort :: "(Networks, DummyContent) FWPolicy" where
"policyPort = deny_all ++ "policyPort = deny_all ++
Intranet_Internet_port ++ Intranet_Internet_port ++
Intranet_mail_port ++ Intranet_mail_port ++
Internet_mail_port ++ Internet_mail_port ++
Internet_web_port" Internet_web_port"
text {*
text {* We only want to create test cases which are sent between the We only want to create test cases which are sent between the three main networks: e.g. not
three main networks --- e.g. not between the mailserver and the between the mailserver and the dmz. Therefore, the constraint looks as follows. \
dmz. Therefore, the constraint looks as follows. *} *}
definition definition
not_in_same_net :: "(Networks,DummyContent) packet \<Rightarrow> bool" where not_in_same_net :: "(Networks,DummyContent) packet \<Rightarrow> bool" where
"not_in_same_net x = ((src x \<sqsubset> internet \<longrightarrow> \<not> dest x \<sqsubset> internet) \<and> "not_in_same_net x = ((src x \<sqsubset> internet \<longrightarrow> \<not> dest x \<sqsubset> internet) \<and>
(src x \<sqsubset> intranet \<longrightarrow> \<not> dest x \<sqsubset> intranet) \<and> (src x \<sqsubset> intranet \<longrightarrow> \<not> dest x \<sqsubset> intranet) \<and>
(src x \<sqsubset> dmz \<longrightarrow> \<not> dest x \<sqsubset> dmz))" (src x \<sqsubset> dmz \<longrightarrow> \<not> dest x \<sqsubset> dmz))"
lemmas PolicyLemmas = dmz_def internet_def intranet_def mail_def web_def lemmas PolicyLemmas = dmz_def internet_def intranet_def mail_def web_def
Internet_web_port_def Internet_mail_port_def Internet_web_port_def Internet_mail_port_def
Intranet_Internet_port_def Intranet_mail_port_def Intranet_Internet_port_def Intranet_mail_port_def
src_def dest_def src_port dest_port in_subnet_def src_def dest_def src_port dest_port in_subnet_def
end end

45
Examples/DMZ/DMZInteger.thy
View File

@ -38,10 +38,10 @@
subsection {* DMZ: Integer *} subsection {* DMZ: Integer *}
theory theory
DMZInteger DMZInteger
imports imports
"../../UPF-Firewall" "../../UPF-Firewall"
begin begin
text{* This scenario is slightly more complicated than the SimpleDMZ text{* This scenario is slightly more complicated than the SimpleDMZ
one, as we now also model specific servers within one one, as we now also model specific servers within one
network. Therefore, we cannot use anymore the modelling using network. Therefore, we cannot use anymore the modelling using
@ -71,10 +71,9 @@ The scenario is the following:
\end{labeling} \end{labeling}
*} *}
definition definition
intranet::"adr\<^sub>i\<^sub>p net" where intranet::"adr\<^sub>i\<^sub>p net" where
"intranet = {{(a,b) . (a > 1 \<and> a < 4) }}" "intranet = {{(a,b) . (a > 1 \<and> a < 4) }}"
definition definition
dmz :: "adr\<^sub>i\<^sub>p net" where dmz :: "adr\<^sub>i\<^sub>p net" where
"dmz = {{(a,b). (a > 6) \<and> (a < 11)}}" "dmz = {{(a,b). (a > 6) \<and> (a < 11)}}"
@ -88,46 +87,44 @@ definition
internet :: "adr\<^sub>i\<^sub>p net" where internet :: "adr\<^sub>i\<^sub>p net" where
"internet = {{(a,b). \<not> ( (a > 1 \<and> a < 4) \<or> (a > 6) \<and> (a < 11)) }}" "internet = {{(a,b). \<not> ( (a > 1 \<and> a < 4) \<or> (a > 6) \<and> (a < 11)) }}"
definition definition
Intranet_mail_port :: "(adr\<^sub>i\<^sub>p,'b) FWPolicy" where Intranet_mail_port :: "(adr\<^sub>i\<^sub>p,'b) FWPolicy" where
"Intranet_mail_port = (allow_from_to_ports {21::port,14} intranet mail)" "Intranet_mail_port = (allow_from_to_ports {21::port,14} intranet mail)"
definition definition
Intranet_Internet_port :: "(adr\<^sub>i\<^sub>p,'b) FWPolicy" where Intranet_Internet_port :: "(adr\<^sub>i\<^sub>p,'b) FWPolicy" where
"Intranet_Internet_port = allow_from_to_ports {80::port,90} intranet internet" "Intranet_Internet_port = allow_from_to_ports {80::port,90} intranet internet"
definition definition
Internet_web_port :: "(adr\<^sub>i\<^sub>p,'b) FWPolicy" where Internet_web_port :: "(adr\<^sub>i\<^sub>p,'b) FWPolicy" where
"Internet_web_port = (allow_from_to_ports {80::port,90} internet web)" "Internet_web_port = (allow_from_to_ports {80::port,90} internet web)"
definition definition
Internet_mail_port :: "(adr\<^sub>i\<^sub>p,'b) FWPolicy" where Internet_mail_port :: "(adr\<^sub>i\<^sub>p,'b) FWPolicy" where
"Internet_mail_port = (allow_all_from_port_to internet (21::port) dmz )" "Internet_mail_port = (allow_all_from_port_to internet (21::port) dmz )"
definition definition
policyPort :: "(adr\<^sub>i\<^sub>p, DummyContent) FWPolicy" where policyPort :: "(adr\<^sub>i\<^sub>p, DummyContent) FWPolicy" where
"policyPort = deny_all ++ "policyPort = deny_all ++
Intranet_Internet_port ++ Intranet_Internet_port ++
Intranet_mail_port ++ Intranet_mail_port ++
Internet_mail_port ++ Internet_mail_port ++
Internet_web_port" Internet_web_port"
text {*
text {* We only want to create test cases which are sent between the three main networks --- We only want to create test cases which are sent between the three main networks:
e.g. not between the mailserver and the dmz. Therefore, the constraint looks as follows. *} e.g. not between the mailserver and the dmz. Therefore, the constraint looks as follows.
*}
definition definition
not_in_same_net :: "(adr\<^sub>i\<^sub>p,DummyContent) packet \<Rightarrow> bool" where not_in_same_net :: "(adr\<^sub>i\<^sub>p,DummyContent) packet \<Rightarrow> bool" where
"not_in_same_net x = ((src x \<sqsubset> internet \<longrightarrow> \<not> dest x \<sqsubset> internet) \<and> "not_in_same_net x = ((src x \<sqsubset> internet \<longrightarrow> \<not> dest x \<sqsubset> internet) \<and>
(src x \<sqsubset> intranet \<longrightarrow> \<not> dest x \<sqsubset> intranet) \<and> (src x \<sqsubset> intranet \<longrightarrow> \<not> dest x \<sqsubset> intranet) \<and>
(src x \<sqsubset> dmz \<longrightarrow> \<not> dest x \<sqsubset> dmz))" (src x \<sqsubset> dmz \<longrightarrow> \<not> dest x \<sqsubset> dmz))"
lemmas PolicyLemmas = policyPort_def dmz_def internet_def intranet_def mail_def web_def lemmas PolicyLemmas = policyPort_def dmz_def internet_def intranet_def mail_def web_def
Intranet_Internet_port_def Intranet_mail_port_def Internet_web_port_def Intranet_Internet_port_def Intranet_mail_port_def Internet_web_port_def
Internet_mail_port_def src_def dest_def IntegerPort.src_port Internet_mail_port_def src_def dest_def IntegerPort.src_port
in_subnet_def IntegerPort.dest_port in_subnet_def IntegerPort.dest_port
end end

16
Examples/Examples.thy
View File

@ -38,13 +38,13 @@
chapter {* Examples *} chapter {* Examples *}
theory theory
Examples Examples
imports imports
"DMZ/DMZ" "DMZ/DMZ"
"VoIP/VoIP" "VoIP/VoIP"
"Transformation/Transformation" "Transformation/Transformation"
"NAT-FW/NAT-FW" "NAT-FW/NAT-FW"
"PersonalFirewall/PersonalFirewall" "PersonalFirewall/PersonalFirewall"
begin begin
end end

73
Examples/NAT-FW/NAT-FW.thy
View File

@ -38,18 +38,16 @@
section {* Example: NAT *} section {* Example: NAT *}
theory theory
"NAT-FW" "NAT-FW"
imports imports
"../../UPF-Firewall" "../../UPF-Firewall"
begin begin
definition subnet1 :: "adr\<^sub>i\<^sub>p net" where definition subnet1 :: "adr\<^sub>i\<^sub>p net" where
"subnet1 = {{(d,e). d > 1 \<and> d < 256}}" "subnet1 = {{(d,e). d > 1 \<and> d < 256}}"
definition subnet2 :: "adr\<^sub>i\<^sub>p net" where definition subnet2 :: "adr\<^sub>i\<^sub>p net" where
"subnet2 = {{(d,e). d > 500 \<and> d < 1256}}" "subnet2 = {{(d,e). d > 500 \<and> d < 1256}}"
definition definition
"accross_subnets x \<equiv> "accross_subnets x \<equiv>
((src x \<sqsubset> subnet1 \<and> (dest x \<sqsubset> subnet2)) \<or> ((src x \<sqsubset> subnet1 \<and> (dest x \<sqsubset> subnet2)) \<or>
@ -65,7 +63,6 @@ definition
nat_0 where nat_0 where
"nat_0 = (A\<^sub>f(\<lambda>x. {x}))" "nat_0 = (A\<^sub>f(\<lambda>x. {x}))"
lemmas UnfoldPolicy0 =filter_def nat_0_def lemmas UnfoldPolicy0 =filter_def nat_0_def
NATLemmas NATLemmas
ProtocolPortCombinators.ProtocolCombinators ProtocolPortCombinators.ProtocolCombinators
@ -73,220 +70,156 @@ lemmas UnfoldPolicy0 =filter_def nat_0_def
packet_defs accross_subnets_def packet_defs accross_subnets_def
subnet1_def subnet2_def subnet1_def subnet2_def
lemmas subnets = subnet1_def subnet2_def lemmas subnets = subnet1_def subnet2_def
definition Adr11 :: "int set" definition Adr11 :: "int set"
where "Adr11 = {d. d > 2 \<and> d < 3}" where "Adr11 = {d. d > 2 \<and> d < 3}"
definition Adr21 :: "int set" where definition Adr21 :: "int set" where
"Adr21 = {d. d > 502 \<and> d < 503}" "Adr21 = {d. d > 502 \<and> d < 503}"
definition nat_1 where definition nat_1 where
"nat_1 = nat_0 ++ (srcPat2pool_IntPort Adr11 Adr21)" "nat_1 = nat_0 ++ (srcPat2pool_IntPort Adr11 Adr21)"
definition policy_1 where definition policy_1 where
"policy_1 = ((\<lambda> (x,y). x) o_f "policy_1 = ((\<lambda> (x,y). x) o_f
((nat_1 \<Otimes>\<^sub>2 filter) o (\<lambda> x. (x,x))))" ((nat_1 \<Otimes>\<^sub>2 filter) o (\<lambda> x. (x,x))))"
lemmas UnfoldPolicy1 = UnfoldPolicy0 nat_1_def Adr11_def Adr21_def policy_1_def lemmas UnfoldPolicy1 = UnfoldPolicy0 nat_1_def Adr11_def Adr21_def policy_1_def
definition Adr12 :: "int set" definition Adr12 :: "int set"
where "Adr12 = {d. d > 4 \<and> d < 6}" where "Adr12 = {d. d > 4 \<and> d < 6}"
definition Adr22 :: "int set" where definition Adr22 :: "int set" where
"Adr22 = {d. d > 504 \<and> d < 506}" "Adr22 = {d. d > 504 \<and> d < 506}"
definition nat_2 where definition nat_2 where
"nat_2 = nat_1 ++ (srcPat2pool_IntPort Adr12 Adr22)" "nat_2 = nat_1 ++ (srcPat2pool_IntPort Adr12 Adr22)"
definition policy_2 where definition policy_2 where
"policy_2 = ((\<lambda> (x,y). x) o_f "policy_2 = ((\<lambda> (x,y). x) o_f
((nat_2 \<Otimes>\<^sub>2 filter) o (\<lambda> x. (x,x))))" ((nat_2 \<Otimes>\<^sub>2 filter) o (\<lambda> x. (x,x))))"
lemmas UnfoldPolicy2 = UnfoldPolicy1 nat_2_def Adr12_def Adr22_def policy_2_def lemmas UnfoldPolicy2 = UnfoldPolicy1 nat_2_def Adr12_def Adr22_def policy_2_def
definition Adr13 :: "int set" definition Adr13 :: "int set"
where "Adr13 = {d. d > 6 \<and> d < 9}" where "Adr13 = {d. d > 6 \<and> d < 9}"
definition Adr23 :: "int set" where definition Adr23 :: "int set" where
"Adr23 = {d. d > 506 \<and> d < 509}" "Adr23 = {d. d > 506 \<and> d < 509}"
definition nat_3 where definition nat_3 where
"nat_3 = nat_2 ++ (srcPat2pool_IntPort Adr13 Adr23)" "nat_3 = nat_2 ++ (srcPat2pool_IntPort Adr13 Adr23)"
definition policy_3 where definition policy_3 where
"policy_3 = ((\<lambda> (x,y). x) o_f "policy_3 = ((\<lambda> (x,y). x) o_f
((nat_3 \<Otimes>\<^sub>2 filter) o (\<lambda> x. (x,x))))" ((nat_3 \<Otimes>\<^sub>2 filter) o (\<lambda> x. (x,x))))"
lemmas UnfoldPolicy3 = UnfoldPolicy2 nat_3_def Adr13_def Adr23_def policy_3_def lemmas UnfoldPolicy3 = UnfoldPolicy2 nat_3_def Adr13_def Adr23_def policy_3_def
definition Adr14 :: "int set" definition Adr14 :: "int set"
where "Adr14 = {d. d > 8 \<and> d < 12}" where "Adr14 = {d. d > 8 \<and> d < 12}"
definition Adr24 :: "int set" where definition Adr24 :: "int set" where
"Adr24 = {d. d > 508 \<and> d < 512}" "Adr24 = {d. d > 508 \<and> d < 512}"
definition nat_4 where definition nat_4 where
"nat_4 = nat_3 ++ (srcPat2pool_IntPort Adr14 Adr24)" "nat_4 = nat_3 ++ (srcPat2pool_IntPort Adr14 Adr24)"
definition policy_4 where definition policy_4 where
"policy_4 = ((\<lambda> (x,y). x) o_f "policy_4 = ((\<lambda> (x,y). x) o_f
((nat_4 \<Otimes>\<^sub>2 filter) o (\<lambda> x. (x,x))))" ((nat_4 \<Otimes>\<^sub>2 filter) o (\<lambda> x. (x,x))))"
lemmas UnfoldPolicy4 = UnfoldPolicy3 nat_4_def Adr14_def Adr24_def policy_4_def lemmas UnfoldPolicy4 = UnfoldPolicy3 nat_4_def Adr14_def Adr24_def policy_4_def
definition Adr15 :: "int set" definition Adr15 :: "int set"
where "Adr15 = {d. d > 10 \<and> d < 15}" where "Adr15 = {d. d > 10 \<and> d < 15}"
definition Adr25 :: "int set" where definition Adr25 :: "int set" where
"Adr25 = {d. d > 510 \<and> d < 515}" "Adr25 = {d. d > 510 \<and> d < 515}"
definition nat_5 where definition nat_5 where
"nat_5 = nat_4 ++ (srcPat2pool_IntPort Adr15 Adr25)" "nat_5 = nat_4 ++ (srcPat2pool_IntPort Adr15 Adr25)"
definition policy_5 where definition policy_5 where
"policy_5 = ((\<lambda> (x,y). x) o_f "policy_5 = ((\<lambda> (x,y). x) o_f
((nat_5 \<Otimes>\<^sub>2 filter) o (\<lambda> x. (x,x))))" ((nat_5 \<Otimes>\<^sub>2 filter) o (\<lambda> x. (x,x))))"
lemmas UnfoldPolicy5 = UnfoldPolicy4 nat_5_def Adr15_def Adr25_def policy_5_def lemmas UnfoldPolicy5 = UnfoldPolicy4 nat_5_def Adr15_def Adr25_def policy_5_def
definition Adr16 :: "int set" definition Adr16 :: "int set"
where "Adr16 = {d. d > 12 \<and> d < 18}" where "Adr16 = {d. d > 12 \<and> d < 18}"
definition Adr26 :: "int set" where definition Adr26 :: "int set" where
"Adr26 = {d. d > 512 \<and> d < 518}" "Adr26 = {d. d > 512 \<and> d < 518}"
definition nat_6 where definition nat_6 where
"nat_6 = nat_5 ++ (srcPat2pool_IntPort Adr16 Adr26)" "nat_6 = nat_5 ++ (srcPat2pool_IntPort Adr16 Adr26)"
definition policy_6 where definition policy_6 where
"policy_6 = ((\<lambda> (x,y). x) o_f "policy_6 = ((\<lambda> (x,y). x) o_f
((nat_6 \<Otimes>\<^sub>2 filter) o (\<lambda> x. (x,x))))" ((nat_6 \<Otimes>\<^sub>2 filter) o (\<lambda> x. (x,x))))"
lemmas UnfoldPolicy6 = UnfoldPolicy5 nat_6_def Adr16_def Adr26_def policy_6_def lemmas UnfoldPolicy6 = UnfoldPolicy5 nat_6_def Adr16_def Adr26_def policy_6_def
definition Adr17 :: "int set" definition Adr17 :: "int set"
where "Adr17 = {d. d > 14 \<and> d < 21}" where "Adr17 = {d. d > 14 \<and> d < 21}"
definition Adr27 :: "int set" where definition Adr27 :: "int set" where
"Adr27 = {d. d > 514 \<and> d < 521}" "Adr27 = {d. d > 514 \<and> d < 521}"
definition nat_7 where definition nat_7 where
"nat_7 = nat_6 ++ (srcPat2pool_IntPort Adr17 Adr27)" "nat_7 = nat_6 ++ (srcPat2pool_IntPort Adr17 Adr27)"
definition policy_7 where definition policy_7 where
"policy_7 = ((\<lambda> (x,y). x) o_f "policy_7 = ((\<lambda> (x,y). x) o_f
((nat_7 \<Otimes>\<^sub>2 filter) o (\<lambda> x. (x,x))))" ((nat_7 \<Otimes>\<^sub>2 filter) o (\<lambda> x. (x,x))))"
lemmas UnfoldPolicy7 = UnfoldPolicy6 nat_7_def Adr17_def Adr27_def policy_7_def lemmas UnfoldPolicy7 = UnfoldPolicy6 nat_7_def Adr17_def Adr27_def policy_7_def
definition Adr18 :: "int set" definition Adr18 :: "int set"
where "Adr18 = {d. d > 16 \<and> d < 24}" where "Adr18 = {d. d > 16 \<and> d < 24}"
definition Adr28 :: "int set" where definition Adr28 :: "int set" where
"Adr28 = {d. d > 516 \<and> d < 524}" "Adr28 = {d. d > 516 \<and> d < 524}"
definition nat_8 where definition nat_8 where
"nat_8 = nat_7 ++ (srcPat2pool_IntPort Adr18 Adr28)" "nat_8 = nat_7 ++ (srcPat2pool_IntPort Adr18 Adr28)"
definition policy_8 where definition policy_8 where
"policy_8 = ((\<lambda> (x,y). x) o_f "policy_8 = ((\<lambda> (x,y). x) o_f
((nat_8 \<Otimes>\<^sub>2 filter) o (\<lambda> x. (x,x))))" ((nat_8 \<Otimes>\<^sub>2 filter) o (\<lambda> x. (x,x))))"
lemmas UnfoldPolicy8 = UnfoldPolicy7 nat_8_def Adr18_def Adr28_def policy_8_def lemmas UnfoldPolicy8 = UnfoldPolicy7 nat_8_def Adr18_def Adr28_def policy_8_def
definition Adr19 :: "int set" definition Adr19 :: "int set"
where "Adr19 = {d. d > 18 \<and> d < 27}" where "Adr19 = {d. d > 18 \<and> d < 27}"
definition Adr29 :: "int set" where definition Adr29 :: "int set" where
"Adr29 = {d. d > 518 \<and> d < 527}" "Adr29 = {d. d > 518 \<and> d < 527}"
definition nat_9 where definition nat_9 where
"nat_9 = nat_8 ++ (srcPat2pool_IntPort Adr19 Adr29)" "nat_9 = nat_8 ++ (srcPat2pool_IntPort Adr19 Adr29)"
definition policy_9 where definition policy_9 where
"policy_9 = ((\<lambda> (x,y). x) o_f "policy_9 = ((\<lambda> (x,y). x) o_f
((nat_9 \<Otimes>\<^sub>2 filter) o (\<lambda> x. (x,x))))" ((nat_9 \<Otimes>\<^sub>2 filter) o (\<lambda> x. (x,x))))"
lemmas UnfoldPolicy9 = UnfoldPolicy8 nat_9_def Adr19_def Adr29_def policy_9_def lemmas UnfoldPolicy9 = UnfoldPolicy8 nat_9_def Adr19_def Adr29_def policy_9_def
definition Adr110 :: "int set" definition Adr110 :: "int set"
where "Adr110 = {d. d > 20 \<and> d < 30}" where "Adr110 = {d. d > 20 \<and> d < 30}"
definition Adr210 :: "int set" where definition Adr210 :: "int set" where
"Adr210 = {d. d > 520 \<and> d < 530}" "Adr210 = {d. d > 520 \<and> d < 530}"
definition nat_10 where definition nat_10 where
"nat_10 = nat_9 ++ (srcPat2pool_IntPort Adr110 Adr210)" "nat_10 = nat_9 ++ (srcPat2pool_IntPort Adr110 Adr210)"
definition policy_10 where definition policy_10 where
"policy_10 = ((\<lambda> (x,y). x) o_f "policy_10 = ((\<lambda> (x,y). x) o_f
((nat_10 \<Otimes>\<^sub>2 filter) o (\<lambda> x. (x,x))))" ((nat_10 \<Otimes>\<^sub>2 filter) o (\<lambda> x. (x,x))))"
lemmas UnfoldPolicy10 = UnfoldPolicy9 nat_10_def Adr110_def Adr210_def policy_10_def lemmas UnfoldPolicy10 = UnfoldPolicy9 nat_10_def Adr110_def Adr210_def policy_10_def
end
end

7
Examples/PersonalFirewall/PersonalFirewall.thy
View File

@ -38,8 +38,9 @@
section {* Personal Firewall *} section {* Personal Firewall *}
theory theory
PersonalFirewall PersonalFirewall
imports imports
PersonalFirewallInt PersonalFirewallInt
PersonalFirewallIpv4 PersonalFirewallIpv4
PersonalFirewallDatatype
begin begin
end end

83
Examples/PersonalFirewall/PersonalFirewallDatatype.thy
View File

@ -38,71 +38,60 @@
subsection {* Personal Firewall: Datatype *} subsection {* Personal Firewall: Datatype *}
theory theory
PersonalFirewallDatatype PersonalFirewallDatatype
imports imports
FWTesting "../../UPF-Firewall"
begin begin
text{* The most basic firewall scenario; there is a personal PC on one text{*
side and the Internet on the other. There are two policies: the first The most basic firewall scenario; there is a personal PC on one side and the Internet on the
one allows all traffic from the PC to the Internet and denies all other. There are two policies: the first one allows all traffic from the PC to the Internet and
coming into the PC. The second policy only allows specific ports from denies all coming into the PC. The second policy only allows specific ports from the PC. This
the PC. This scenario comes in three variants: the first one specifies scenario comes in three variants: the first one specifies the allowed protocols directly, the
the allowed protocols directly, the second together with their second together with their respective port numbers, the third one only with the port numbers.
respective port numbers, the third one only with the port numbers. *} *}
datatype Adr = pc | internet datatype Adr = pc | internet
type_synonym DatatypeTwoNets = "Adr \<times> int" type_synonym DatatypeTwoNets = "Adr \<times> int"
instance Adr::adr .. instance Adr::adr ..
defs (overloaded)
src_port_def: "src_port (x::(DatatypeTwoNets,'b) packet) \<equiv> snd (src x)"
dest_port_def: "dest_port (x::(DatatypeTwoNets,'b) packet) \<equiv> snd (dest x)"
definition definition
PC :: "DatatypeTwoNets net" where PC :: "DatatypeTwoNets net" where
"PC = {{(a,b). a = pc}}" "PC = {{(a,b). a = pc}}"
definition definition
Internet :: "DatatypeTwoNets net" where Internet :: "DatatypeTwoNets net" where
"Internet = {{(a,b). a = internet}}" "Internet = {{(a,b). a = internet}}"
text{*
Definition of the testing constraint
*}
definition definition
not_in_same_net :: "(DatatypeTwoNets,DummyContent) packet \<Rightarrow> bool" where not_in_same_net :: "(DatatypeTwoNets,DummyContent) packet \<Rightarrow> bool" where
"not_in_same_net x = ((src x \<sqsubset> PC \<longrightarrow> dest x \<sqsubset> Internet) \<and> (src x \<sqsubset> Internet \<longrightarrow> dest x \<sqsubset> PC))" "not_in_same_net x = ((src x \<sqsubset> PC \<longrightarrow> dest x \<sqsubset> Internet) \<and> (src x \<sqsubset> Internet \<longrightarrow> dest x \<sqsubset> PC))"
text {* text {*
Definitions of the policies Definitions of the policies
In fact, the short definitions wouldn't have to be written down - they
are the automatically simplified versions of their big counterparts.
In fact, the short definitions wouldn't have to be written down - they
are the automatically simplified versions of their big counterparts.
*} *}
definition definition
strictPolicy :: "(DatatypeTwoNets,DummyContent) FWPolicy" where strictPolicy :: "(DatatypeTwoNets,DummyContent) FWPolicy" where
"strictPolicy = deny_all ++ allow_all_from_to PC Internet" "strictPolicy = deny_all ++ allow_all_from_to PC Internet"
definition definition
PortPolicy :: "(DatatypeTwoNets,'b) FWPolicy" where PortPolicy :: "(DatatypeTwoNets,'b) FWPolicy" where
"PortPolicy = deny_all ++ allow_from_ports_to {80::port,24,21} PC Internet" "PortPolicy = deny_all ++ allow_from_ports_to {80::port,24,21} PC Internet"
definition definition
PortPolicyBig :: "(DatatypeTwoNets,'b) FWPolicy" where PortPolicyBig :: "(DatatypeTwoNets,'b) FWPolicy" where
"PortPolicyBig = "PortPolicyBig =
allow_from_port_to (80::port) PC Internet \<Oplus> allow_from_port_to (80::port) PC Internet \<Oplus>
allow_from_port_to (24::port) PC Internet \<Oplus> allow_from_port_to (24::port) PC Internet \<Oplus>
allow_from_port_to (21::port) PC Internet \<Oplus> allow_from_port_to (21::port) PC Internet \<Oplus>
deny_all" deny_all"
lemmas policyLemmas = strictPolicy_def PortPolicy_def PC_def Internet_def PortPolicyBig_def src_def
lemmas policyLemmas = strictPolicy_def PortPolicy_def PC_def Internet_def PortPolicyBig_def src_def dest_def src_port_def dest_port_def
PolicyCombinators PortCombinators in_subnet_def PolicyCombinators PortCombinators in_subnet_def
end end

83
Examples/PersonalFirewall/PersonalFirewallInt.thy
View File

@ -38,76 +38,61 @@
subsection{* Personal Firewall: Integer *} subsection{* Personal Firewall: Integer *}
theory theory
PersonalFirewallInt PersonalFirewallInt
imports imports
"../../UPF-Firewall" "../../UPF-Firewall"
begin begin
text{* text{*
The most basic firewall scenario; there is a personal PC on one side and the Internet on the other. The most basic firewall scenario; there is a personal PC on one side and the Internet on the
There are two policies: the first one allows all traffic from the PC to the Internet and denies other. There are two policies: the first one allows all traffic from the PC to the Internet and
all coming into the PC. The second policy only allows specific ports from the PC. This scenario denies all coming into the PC. The second policy only allows specific ports from the PC. This
comes in three variants: the first one specifies the allowed protocols directly, the second together scenario comes in three variants: the first one specifies the allowed protocols directly, the
with their respective port numbers, the third one only with the port numbers. second together with their respective port numbers, the third one only with the port numbers.
*} *}
text{* text{*
Definitions of the subnets Definitions of the subnets
*} *}
definition definition
PC :: "(adr\<^sub>i\<^sub>p net)" where PC :: "(adr\<^sub>i\<^sub>p net)" where
"PC = {{(a,b). a = 3}}" "PC = {{(a,b). a = 3}}"
definition
Internet :: "adr\<^sub>i\<^sub>p net" where
"Internet = {{(a,b). \<not> (a = 3)}}"
definition definition
Internet :: "adr\<^sub>i\<^sub>p net" where not_in_same_net :: "(adr\<^sub>i\<^sub>p,DummyContent) packet \<Rightarrow> bool" where
"Internet = {{(a,b). \<not> (a = 3)}}" "not_in_same_net x = ((src x \<sqsubset> PC \<longrightarrow> dest x \<sqsubset> Internet) \<and> (src x \<sqsubset> Internet \<longrightarrow> dest x \<sqsubset> PC))"
text{*
Definition of the testing constraint
*}
definition
not_in_same_net :: "(adr\<^sub>i\<^sub>p,DummyContent) packet \<Rightarrow> bool" where
"not_in_same_net x = ((src x \<sqsubset> PC \<longrightarrow> dest x \<sqsubset> Internet) \<and> (src x \<sqsubset> Internet \<longrightarrow> dest x \<sqsubset> PC))"
text {* text {*
Definitions of the policies Definitions of the policies
*} *}
definition definition
strictPolicy :: "(adr\<^sub>i\<^sub>p,DummyContent) FWPolicy" where strictPolicy :: "(adr\<^sub>i\<^sub>p,DummyContent) FWPolicy" where
"strictPolicy = deny_all ++ allow_all_from_to PC Internet" "strictPolicy = deny_all ++ allow_all_from_to PC Internet"
definition definition
PortPolicy :: "(adr\<^sub>i\<^sub>p,DummyContent) FWPolicy" where PortPolicy :: "(adr\<^sub>i\<^sub>p,DummyContent) FWPolicy" where
"PortPolicy = deny_all ++ allow_from_ports_to {http,smtp,ftp} PC Internet" "PortPolicy = deny_all ++ allow_from_ports_to {http,smtp,ftp} PC Internet"
definition definition
PortPolicyBig :: "(adr\<^sub>i\<^sub>p,DummyContent) FWPolicy" where PortPolicyBig :: "(adr\<^sub>i\<^sub>p,DummyContent) FWPolicy" where
"PortPolicyBig = deny_all ++ "PortPolicyBig = deny_all ++
allow_from_port_to http PC Internet ++ allow_from_port_to http PC Internet ++
allow_from_port_to smtp PC Internet ++ allow_from_port_to smtp PC Internet ++
allow_from_port_to ftp PC Internet" allow_from_port_to ftp PC Internet"
lemmas policyLemmas = strictPolicy_def PortPolicy_def PC_def lemmas policyLemmas = strictPolicy_def PortPolicy_def PC_def
Internet_def PortPolicyBig_def src_def dest_def Internet_def PortPolicyBig_def src_def dest_def
adr\<^sub>i\<^sub>pLemmas content_def adr\<^sub>i\<^sub>pLemmas content_def
PortCombinators in_subnet_def PortPolicyBig_def id_def PortCombinators in_subnet_def PortPolicyBig_def id_def
declare Ports [simp add] declare Ports [simp add]
definition wellformed_packet::"(adr\<^sub>i\<^sub>p,DummyContent) packet \<Rightarrow> bool" where definition wellformed_packet::"(adr\<^sub>i\<^sub>p,DummyContent) packet \<Rightarrow> bool" where
"wellformed_packet p = (content p = data)" "wellformed_packet p = (content p = data)"
end
end

83
Examples/PersonalFirewall/PersonalFirewallIpv4.thy
View File

@ -38,66 +38,53 @@
subsection {* Personal Firewall IPv4 *} subsection {* Personal Firewall IPv4 *}
theory theory
PersonalFirewallIpv4 PersonalFirewallIpv4
imports imports
"../../UPF-Firewall" "../../UPF-Firewall"
begin begin
text{* text{*
The most basic firewall scenario; there is a personal PC on one side and the Internet on the
The most basic firewall scenario; there is a personal PC on one side and the Internet on the other. other. There are two policies: the first one allows all traffic from the PC to the Internet and
There are two policies: the first one allows all traffic from the PC to the Internet and denies denies all coming into the PC. The second policy only allows specific ports from the PC. This
all coming into the PC. The second policy only allows specific ports from the PC. This scenario scenario comes in three variants: the first one specifies the allowed protocols directly, the
comes in three variants: the first one specifies the allowed protocols directly, the second together second together with their respective port numbers, the third one only with the port numbers.
with their respective port numbers, the third one only with the port numbers.
*} *}
text{* text{*
Definitions of the subnets Definitions of the subnets
*} *}
definition definition
PC :: "(ipv4 net)" where PC :: "(ipv4 net)" where
"PC = {{((a,b,c,d),e). a = 1 \<and> b = 3 \<and> c = 5 \<and> d = 2}}" "PC = {{((a,b,c,d),e). a = 1 \<and> b = 3 \<and> c = 5 \<and> d = 2}}"
definition definition
Internet :: "ipv4 net" where Internet :: "ipv4 net" where
"Internet = {{((a,b,c,d),e). \<not> (a = 1 \<and> b = 3 \<and> c = 5 \<and> d = 2)}}" "Internet = {{((a,b,c,d),e). \<not> (a = 1 \<and> b = 3 \<and> c = 5 \<and> d = 2)}}"
text{*
Definition of the testing constraint
*}
definition definition
not_in_same_net :: "(ipv4,DummyContent) packet \<Rightarrow> bool" where not_in_same_net :: "(ipv4,DummyContent) packet \<Rightarrow> bool" where
"not_in_same_net x = ((src x \<sqsubset> PC \<longrightarrow> dest x \<sqsubset> Internet) \<and> (src x \<sqsubset> Internet \<longrightarrow> dest x \<sqsubset> PC))" "not_in_same_net x = ((src x \<sqsubset> PC \<longrightarrow> dest x \<sqsubset> Internet) \<and> (src x \<sqsubset> Internet \<longrightarrow> dest x \<sqsubset> PC))"
text {* text {*
Definitions of the policies Definitions of the policies
*} *}
definition definition
strictPolicy :: "(ipv4,DummyContent) FWPolicy" where strictPolicy :: "(ipv4,DummyContent) FWPolicy" where
"strictPolicy = deny_all ++ allow_all_from_to PC Internet" "strictPolicy = deny_all ++ allow_all_from_to PC Internet"
definition definition
PortPolicy :: "(ipv4,DummyContent) FWPolicy" where PortPolicy :: "(ipv4,DummyContent) FWPolicy" where
"PortPolicy = deny_all ++ allow_from_ports_to {80::port,24,21} PC Internet" "PortPolicy = deny_all ++ allow_from_ports_to {80::port,24,21} PC Internet"
definition definition
PortPolicyBig :: "(ipv4,DummyContent) FWPolicy" where PortPolicyBig :: "(ipv4,DummyContent) FWPolicy" where
"PortPolicyBig = deny_all ++ allow_from_port_to (80::port) PC Internet++ allow_from_port_to (24::port) PC Internet++ allow_from_port_to (21::port) PC Internet" "PortPolicyBig = deny_all ++ allow_from_port_to (80::port) PC Internet++ allow_from_port_to (24::port) PC Internet++ allow_from_port_to (21::port) PC Internet"
lemmas policyLemmas = strictPolicy_def PortPolicy_def PC_def lemmas policyLemmas = strictPolicy_def PortPolicy_def PC_def
Internet_def PortPolicyBig_def src_def dest_def Internet_def PortPolicyBig_def src_def dest_def
IPv4.src_port IPv4.src_port
IPv4.dest_port PolicyCombinators IPv4.dest_port PolicyCombinators
PortCombinators in_subnet_def PortPolicyBig_def PortCombinators in_subnet_def PortPolicyBig_def
end end

10
Examples/Transformation/Transformation.thy
View File

@ -36,9 +36,11 @@
*****************************************************************************) *****************************************************************************)
section {* Demonstrating Policy Transformations *} section {* Demonstrating Policy Transformations *}
theory Transformation theory
imports Transformation
Transformation01 imports
Transformation02 Transformation01
Transformation02
begin begin
end end

249
Examples/Transformation/Transformation01.thy
View File

@ -38,94 +38,82 @@
subsection {* Transformation Example 1 *} subsection {* Transformation Example 1 *}
theory theory
Transformation01 Transformation01
imports imports
"../../UPF-Firewall" "../../UPF-Firewall"
begin begin
definition definition
FWLink :: "adr\<^sub>i\<^sub>p net" where FWLink :: "adr\<^sub>i\<^sub>p net" where
"FWLink = {{(a,b). a = 1}}" "FWLink = {{(a,b). a = 1}}"
definition
any :: "adr\<^sub>i\<^sub>p net" where
"any = {{(a,b). a > 5}}"
definition
i4:: "adr\<^sub>i\<^sub>p net" where
"i4 = {{(a,b). a = 2 }}"
definition
i27:: "adr\<^sub>i\<^sub>p net" where
"i27 = {{(a,b). a = 3 }}"
definition
eth_intern:: "adr\<^sub>i\<^sub>p net" where
"eth_intern = {{(a,b). a = 4 }}"
definition
eth_private:: "adr\<^sub>i\<^sub>p net" where
"eth_private = {{(a,b). a = 5 }}"
definition definition
any :: "adr\<^sub>i\<^sub>p net" where (* Mandatory: Global *)
"any = {{(a,b). a > 5}}" MG2 :: "(adr\<^sub>i\<^sub>p net,port) Combinators" where
"MG2 = AllowPortFromTo i27 any 1 \<oplus>
definition
i4:: "adr\<^sub>i\<^sub>p net" where
"i4 = {{(a,b). a = 2 }}"
definition
i27:: "adr\<^sub>i\<^sub>p net" where
"i27 = {{(a,b). a = 3 }}"
definition
eth_intern:: "adr\<^sub>i\<^sub>p net" where
"eth_intern = {{(a,b). a = 4 }}"
definition
eth_private:: "adr\<^sub>i\<^sub>p net" where
"eth_private = {{(a,b). a = 5 }}"
definition
(* Mandatory: Global *)
MG2 :: "(adr\<^sub>i\<^sub>p net,port) Combinators" where
"MG2 = AllowPortFromTo i27 any 1 \<oplus>
AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 2 \<oplus>
AllowPortFromTo i27 any 3" AllowPortFromTo i27 any 3"
definition definition
MG3 :: "(adr\<^sub>i\<^sub>p net,port) Combinators" where MG3 :: "(adr\<^sub>i\<^sub>p net,port) Combinators" where
"MG3 = AllowPortFromTo any FWLink 1" "MG3 = AllowPortFromTo any FWLink 1"
definition definition
MG4 :: "(adr\<^sub>i\<^sub>p net,port) Combinators" where MG4 :: "(adr\<^sub>i\<^sub>p net,port) Combinators" where
"MG4 = AllowPortFromTo FWLink FWLink 4" "MG4 = AllowPortFromTo FWLink FWLink 4"
definition definition
MG7 :: "(adr\<^sub>i\<^sub>p net,port) Combinators" where MG7 :: "(adr\<^sub>i\<^sub>p net,port) Combinators" where
"MG7 = AllowPortFromTo FWLink i4 6 \<oplus> "MG7 = AllowPortFromTo FWLink i4 6 \<oplus>
AllowPortFromTo FWLink i4 7" AllowPortFromTo FWLink i4 7"
definition definition
MG8 :: "(adr\<^sub>i\<^sub>p net,port) Combinators" where MG8 :: "(adr\<^sub>i\<^sub>p net,port) Combinators" where
"MG8 = AllowPortFromTo FWLink i4 6 \<oplus> "MG8 = AllowPortFromTo FWLink i4 6 \<oplus>
AllowPortFromTo FWLink i4 7" AllowPortFromTo FWLink i4 7"
(* Default Global *) (* Default Global *)
definition
DG3:: "(adr\<^sub>i\<^sub>p net,port) Combinators" where
"DG3 = AllowPortFromTo any any 7"
definition definition
DG3:: "(adr\<^sub>i\<^sub>p net,port) Combinators" where "Policy = DenyAll \<oplus> MG8 \<oplus> MG7 \<oplus> MG4 \<oplus> MG3 \<oplus> MG2 \<oplus> DG3"
"DG3 = AllowPortFromTo any any 7"
lemmas PolicyLemmas = Policy_def
FWLink_def
any_def
i27_def
i4_def
eth_intern_def
eth_private_def
MG2_def MG3_def MG4_def MG7_def MG8_def
DG3_def
definition lemmas PolicyL = MG2_def MG3_def MG4_def MG7_def MG8_def DG3_def Policy_def
"Policy = DenyAll \<oplus> MG8 \<oplus> MG7 \<oplus> MG4 \<oplus> MG3 \<oplus> MG2 \<oplus> DG3"
lemmas PolicyLemmas = Policy_def
FWLink_def
any_def
i27_def
i4_def
eth_intern_def
eth_private_def
MG2_def MG3_def MG4_def MG7_def MG8_def
DG3_def
lemmas PolicyL = MG2_def MG3_def MG4_def MG7_def MG8_def
DG3_def Policy_def
definition definition
not_in_same_net :: "(adr\<^sub>i\<^sub>p,DummyContent) packet \<Rightarrow> bool" where not_in_same_net :: "(adr\<^sub>i\<^sub>p,DummyContent) packet \<Rightarrow> bool" where
"not_in_same_net x = (((src x \<sqsubset> i27) \<longrightarrow> ( \<not> (dest x \<sqsubset> i27))) \<and> "not_in_same_net x = (((src x \<sqsubset> i27) \<longrightarrow> ( \<not> (dest x \<sqsubset> i27))) \<and>
((src x \<sqsubset> i4) \<longrightarrow> ( \<not> (dest x \<sqsubset> i4))) \<and> ((src x \<sqsubset> i4) \<longrightarrow> ( \<not> (dest x \<sqsubset> i4))) \<and>
((src x \<sqsubset> eth_intern) \<longrightarrow> ( \<not> (dest x \<sqsubset> eth_intern))) \<and> ((src x \<sqsubset> eth_intern) \<longrightarrow> ( \<not> (dest x \<sqsubset> eth_intern))) \<and>
((src x \<sqsubset> eth_private) \<longrightarrow> ( \<not> (dest x \<sqsubset> eth_private))))" ((src x \<sqsubset> eth_private) \<longrightarrow> ( \<not> (dest x \<sqsubset> eth_private))))"
@ -140,45 +128,33 @@ lemmas fixDefs = fixElements_def NetworkCore.id_def NetworkCore.content_def
lemma sets_distinct1: "(n::int) \<noteq> m \<Longrightarrow> {(a,b). a = n} \<noteq> {(a,b). a = m}" lemma sets_distinct1: "(n::int) \<noteq> m \<Longrightarrow> {(a,b). a = n} \<noteq> {(a,b). a = m}"
apply auto by auto
done
lemma sets_distinct2: "(m::int) \<noteq> n \<Longrightarrow> {(a,b). a = n} \<noteq> {(a,b). a = m}" lemma sets_distinct2: "(m::int) \<noteq> n \<Longrightarrow> {(a,b). a = n} \<noteq> {(a,b). a = m}"
apply auto by auto
done
lemma sets_distinct3: "{((a::int),(b::int)). a = n} \<noteq> {(a,b). a > n}" lemma sets_distinct3: "{((a::int),(b::int)). a = n} \<noteq> {(a,b). a > n}"
apply auto by auto
done
lemma sets_distinct4: "{((a::int),(b::int)). a > n} \<noteq> {(a,b). a = n}" lemma sets_distinct4: "{((a::int),(b::int)). a > n} \<noteq> {(a,b). a = n}"
apply auto by auto
done
lemma aux: "\<lbrakk>a \<in> c; a \<notin> d; c = d\<rbrakk> \<Longrightarrow> False" lemma aux: "\<lbrakk>a \<in> c; a \<notin> d; c = d\<rbrakk> \<Longrightarrow> False"
apply auto by auto
done
lemma sets_distinct5: "(s::int) < g \<Longrightarrow> {(a::int, b::int). a = s} \<noteq> {(a::int, b::int). g < a}" lemma sets_distinct5: "(s::int) < g \<Longrightarrow> {(a::int, b::int). a = s} \<noteq> {(a::int, b::int). g < a}"
apply (auto simp: sets_distinct3) apply (auto simp: sets_distinct3)
apply (subgoal_tac "(s,4) \<in> {(a::int,b::int). a = (s)}") apply (subgoal_tac "(s,4) \<in> {(a::int,b::int). a = (s)}")
apply (subgoal_tac "(s,4) \<notin> {(a::int,b::int). g < a}") apply (subgoal_tac "(s,4) \<notin> {(a::int,b::int). g < a}")
apply (erule aux) apply (erule aux)
apply assumption+ apply assumption+
apply simp apply simp
by blast by blast
lemma sets_distinct6: "(s::int) < g \<Longrightarrow> {(a::int, b::int). g < a} \<noteq> {(a::int, b::int). a = s}" lemma sets_distinct6: "(s::int) < g \<Longrightarrow> {(a::int, b::int). g < a} \<noteq> {(a::int, b::int). a = s}"
apply (rule not_sym) apply (rule not_sym)
apply (rule sets_distinct5) apply (rule sets_distinct5)
by simp by simp
lemma distinctNets: "FWLink \<noteq> any \<and> FWLink \<noteq> i4 \<and> FWLink \<noteq> i27 \<and> FWLink \<noteq> eth_intern \<and> FWLink \<noteq> eth_private \<and> lemma distinctNets: "FWLink \<noteq> any \<and> FWLink \<noteq> i4 \<and> FWLink \<noteq> i27 \<and> FWLink \<noteq> eth_intern \<and> FWLink \<noteq> eth_private \<and>
any \<noteq> FWLink \<and> any \<noteq> i4 \<and> any \<noteq> i27 \<and> any \<noteq> eth_intern \<and> any \<noteq> eth_private \<and> i4 \<noteq> FWLink \<and> any \<noteq> FWLink \<and> any \<noteq> i4 \<and> any \<noteq> i27 \<and> any \<noteq> eth_intern \<and> any \<noteq> eth_private \<and> i4 \<noteq> FWLink \<and>
@ -186,83 +162,34 @@ i4 \<noteq> any \<and> i4 \<noteq> i27 \<and> i4 \<noteq> eth_intern \<and> i
i27 \<noteq> i4 \<and> i27 \<noteq> eth_intern \<and> i27 \<noteq> eth_private \<and> eth_intern \<noteq> FWLink \<and> eth_intern \<noteq> any \<and> i27 \<noteq> i4 \<and> i27 \<noteq> eth_intern \<and> i27 \<noteq> eth_private \<and> eth_intern \<noteq> FWLink \<and> eth_intern \<noteq> any \<and>
eth_intern \<noteq> i4 \<and> eth_intern \<noteq> i27 \<and> eth_intern \<noteq> eth_private \<and> eth_private \<noteq> FWLink \<and> eth_intern \<noteq> i4 \<and> eth_intern \<noteq> i27 \<and> eth_intern \<noteq> eth_private \<and> eth_private \<noteq> FWLink \<and>
eth_private \<noteq> any \<and> eth_private \<noteq> i4 \<and> eth_private \<noteq> i27 \<and> eth_private \<noteq> eth_intern" eth_private \<noteq> any \<and> eth_private \<noteq> i4 \<and> eth_private \<noteq> i27 \<and> eth_private \<noteq> eth_intern"
apply (simp add: PolicyLemmas sets_distinct1 sets_distinct2 sets_distinct3 sets_distinct4 sets_distinct5 sets_distinct6) by (simp add: PolicyLemmas sets_distinct1 sets_distinct2 sets_distinct3 sets_distinct4
done sets_distinct5 sets_distinct6)
lemma aux5: "\<lbrakk>x \<noteq> a; y\<noteq>b; (x \<noteq> y \<and> x \<noteq> b) \<or> (a \<noteq> b \<and> a \<noteq> y)\<rbrakk> \<Longrightarrow> {x,a} \<noteq> {y,b}" lemma aux5: "\<lbrakk>x \<noteq> a; y\<noteq>b; (x \<noteq> y \<and> x \<noteq> b) \<or> (a \<noteq> b \<and> a \<noteq> y)\<rbrakk> \<Longrightarrow> {x,a} \<noteq> {y,b}"
apply auto by auto
done
lemma aux2: "{a,b} = {b,a}" lemma aux2: "{a,b} = {b,a}"
apply auto by auto
done
(*
lemma noMT: "\<forall> x \<in> set (policy2list Policy). dom (C x) \<noteq> {}"
apply (simp add: PolicyLemmas)
apply (simp add: PLemmas PolicyLemmas)
by arith
*)
lemma ANDex: "allNetsDistinct (policy2list Policy)" lemma ANDex: "allNetsDistinct (policy2list Policy)"
apply (simp add: PolicyL allNetsDistinct_def distinctNets) apply (simp add: PolicyL allNetsDistinct_def distinctNets)
apply (auto simp: PLemmas PolicyLemmas netsDistinct_def sets_distinct5 sets_distinct6) by (auto simp: PLemmas PolicyLemmas netsDistinct_def sets_distinct5 sets_distinct6)
done
(*
lemma count_the_rules: "(int (length(policy2list (list2FWpolicy(normalize Policy)))) = post) \<and>
(int(length (policy2list Policy)) = pre) \<and>
(int (length((normalize Policy))) = Partitions)"
apply (insert distinctNets noMT)
apply (simp add: normalize_def PolicyL bothNets_def aux5 aux2 Nets_List_def, thin_tac "?X",thin_tac "?S")
oops
lemma normedPolicy: "normalize Policy = X"
apply (insert distinctNets noMT)
apply (simp add: normalize_def PolicyL bothNets_def aux5 aux2 Nets_List_def, thin_tac "?X",thin_tac "?S")
oops
*)
fun (sequential) numberOfRules where fun (sequential) numberOfRules where
"numberOfRules (a\<oplus>b) = numberOfRules a + numberOfRules b" "numberOfRules (a\<oplus>b) = numberOfRules a + numberOfRules b"
|"numberOfRules a = (1::int)" |"numberOfRules a = (1::int)"
fun numberOfRulesList where fun numberOfRulesList where
"numberOfRulesList (x#xs) = ((numberOfRules x)#(numberOfRulesList xs)) " "numberOfRulesList (x#xs) = ((numberOfRules x)#(numberOfRulesList xs)) "
|"numberOfRulesList [] = []" |"numberOfRulesList [] = []"
(*
lemma "numberOfRulesList (normalize Policy) = X"
apply (insert distinctNets noMT)
apply (simp add: normalize_def PolicyL bothNets_def aux5 aux2 Nets_List_def, thin_tac "?X",thin_tac "?S")
oops
*)
lemma all_in_list: "all_in_list (policy2list Policy) (Nets_List Policy)" lemma all_in_list: "all_in_list (policy2list Policy) (Nets_List Policy)"
apply (simp add: PolicyL) apply (simp add: PolicyL)
apply (unfold Nets_List_def) apply (unfold Nets_List_def)
apply (unfold bothNets_def) apply (unfold bothNets_def)
apply (insert distinctNets) apply (insert distinctNets)
apply simp by simp
done
lemmas normalizeUnfold = normalize_def Policy_def Nets_List_def bothNets_def aux aux2 bothNets_def lemmas normalizeUnfold = normalize_def Policy_def Nets_List_def bothNets_def aux aux2 bothNets_def
(* end
lemma noMT2: "\<forall> x \<in> set (policy2list Policy). dom (C x) \<noteq> {}"
apply (simp add: PLemmas normalize_def bothNets_def
PolicyLemmas aux5 aux2 Nets_List_def )
by (metis zless_add1_eq)
*)
end

219
Examples/Transformation/Transformation02.thy
View File

@ -38,123 +38,103 @@
subsection {* Transforamtion Example 2 *} subsection {* Transforamtion Example 2 *}
theory theory
Transformation02 Transformation02
imports imports
"../../UPF-Firewall" "../../UPF-Firewall"
begin begin
definition definition
FWLink :: "adr\<^sub>i\<^sub>p net" where FWLink :: "adr\<^sub>i\<^sub>p net" where
"FWLink = {{(a,b). a = 1}}" "FWLink = {{(a,b). a = 1}}"
definition definition
any :: "adr\<^sub>i\<^sub>p net" where any :: "adr\<^sub>i\<^sub>p net" where
"any = {{(a,b). a > 5}}" "any = {{(a,b). a > 5}}"
definition definition
i4_32:: "adr\<^sub>i\<^sub>p net" where i4_32:: "adr\<^sub>i\<^sub>p net" where
"i4_32 = {{(a,b). a = 2 }}" "i4_32 = {{(a,b). a = 2 }}"
definition definition
i10_32:: "adr\<^sub>i\<^sub>p net" where i10_32:: "adr\<^sub>i\<^sub>p net" where
"i10_32 = {{(a,b). a = 3 }}" "i10_32 = {{(a,b). a = 3 }}"
definition definition
eth_intern:: "adr\<^sub>i\<^sub>p net" where eth_intern:: "adr\<^sub>i\<^sub>p net" where
"eth_intern = {{(a,b). a = 4 }}" "eth_intern = {{(a,b). a = 4 }}"
definition definition
eth_private:: "adr\<^sub>i\<^sub>p net" where eth_private:: "adr\<^sub>i\<^sub>p net" where
"eth_private = {{(a,b). a = 5 }}" "eth_private = {{(a,b). a = 5 }}"
definition definition
D1a :: "(adr\<^sub>i\<^sub>p net, port) Combinators" where D1a :: "(adr\<^sub>i\<^sub>p net, port) Combinators" where
"D1a = AllowPortFromTo eth_intern any 1 \<oplus> "D1a = AllowPortFromTo eth_intern any 1 \<oplus>
AllowPortFromTo eth_intern any 2" AllowPortFromTo eth_intern any 2"
definition definition
D1b :: "(adr\<^sub>i\<^sub>p net, port) Combinators" where D1b :: "(adr\<^sub>i\<^sub>p net, port) Combinators" where
"D1b = AllowPortFromTo eth_private any 1 \<oplus> "D1b = AllowPortFromTo eth_private any 1 \<oplus>
AllowPortFromTo eth_private any 2" AllowPortFromTo eth_private any 2"
definition definition
D2a :: "(adr\<^sub>i\<^sub>p net, port) Combinators" where D2a :: "(adr\<^sub>i\<^sub>p net, port) Combinators" where
"D2a = AllowPortFromTo any i4_32 21" "D2a = AllowPortFromTo any i4_32 21"
definition definition
D2b :: "(adr\<^sub>i\<^sub>p net, port) Combinators" where D2b :: "(adr\<^sub>i\<^sub>p net, port) Combinators" where
"D2b = AllowPortFromTo any i10_32 21 \<oplus> "D2b = AllowPortFromTo any i10_32 21 \<oplus>
AllowPortFromTo any i10_32 43" AllowPortFromTo any i10_32 43"
definition definition
Policy :: "(adr\<^sub>i\<^sub>p net, port) Combinators" where Policy :: "(adr\<^sub>i\<^sub>p net, port) Combinators" where
"Policy = DenyAll \<oplus> D2b \<oplus> D2a \<oplus> D1b \<oplus> D1a" "Policy = DenyAll \<oplus> D2b \<oplus> D2a \<oplus> D1b \<oplus> D1a"
lemmas PolicyLemmas = Policy_def D1a_def D1b_def D2a_def D2b_def lemmas PolicyLemmas = Policy_def D1a_def D1b_def D2a_def D2b_def
lemmas PolicyL = Policy_def
lemmas PolicyL = Policy_def FWLink_def
FWLink_def any_def
any_def i10_32_def
i10_32_def i4_32_def
i4_32_def eth_intern_def
eth_intern_def eth_private_def
eth_private_def D1a_def D1b_def D2a_def D2b_def
D1a_def D1b_def D2a_def D2b_def
consts fixID :: id consts fixID :: id
consts fixContent :: DummyContent consts fixContent :: DummyContent
definition "fixElements p = (id p = fixID \<and> content p = fixContent)" definition "fixElements p = (id p = fixID \<and> content p = fixContent)"
lemmas fixDefs = fixElements_def NetworkCore.id_def NetworkCore.content_def lemmas fixDefs = fixElements_def NetworkCore.id_def NetworkCore.content_def
lemma sets_distinct1: "(n::int) \<noteq> m \<Longrightarrow> {(a,b). a = n} \<noteq> {(a,b). a = m}" lemma sets_distinct1: "(n::int) \<noteq> m \<Longrightarrow> {(a,b). a = n} \<noteq> {(a,b). a = m}"
apply auto by auto
done
lemma sets_distinct2: "(m::int) \<noteq> n \<Longrightarrow> {(a,b). a = n} \<noteq> {(a,b). a = m}" lemma sets_distinct2: "(m::int) \<noteq> n \<Longrightarrow> {(a,b). a = n} \<noteq> {(a,b). a = m}"
apply auto by auto
done
lemma sets_distinct3: "{((a::int),(b::int)). a = n} \<noteq> {(a,b). a > n}" lemma sets_distinct3: "{((a::int),(b::int)). a = n} \<noteq> {(a,b). a > n}"
apply auto by auto
done
lemma sets_distinct4: "{((a::int),(b::int)). a > n} \<noteq> {(a,b). a = n}" lemma sets_distinct4: "{((a::int),(b::int)). a > n} \<noteq> {(a,b). a = n}"
apply auto by auto
done
lemma aux: "\<lbrakk>a \<in> c; a \<notin> d; c = d\<rbrakk> \<Longrightarrow> False" lemma aux: "\<lbrakk>a \<in> c; a \<notin> d; c = d\<rbrakk> \<Longrightarrow> False"
apply auto by auto
done
lemma sets_distinct5: "(s::int) < g \<Longrightarrow> {(a::int, b::int). a = s} \<noteq> {(a::int, b::int). g < a}" lemma sets_distinct5: "(s::int) < g \<Longrightarrow> {(a::int, b::int). a = s} \<noteq> {(a::int, b::int). g < a}"
apply (auto simp: sets_distinct3) apply (auto simp: sets_distinct3)
apply (subgoal_tac "(s,4) \<in> {(a::int,b::int). a = (s)}") apply (subgoal_tac "(s,4) \<in> {(a::int,b::int). a = (s)}")
apply (subgoal_tac "(s,4) \<notin> {(a::int,b::int). g < a}") apply (subgoal_tac "(s,4) \<notin> {(a::int,b::int). g < a}")
apply (erule aux) apply (erule aux)
apply assumption+ apply assumption+
apply simp apply simp
by blast by blast
lemma sets_distinct6: "(s::int) < g \<Longrightarrow> {(a::int, b::int). g < a} \<noteq> {(a::int, b::int). a = s}" lemma sets_distinct6: "(s::int) < g \<Longrightarrow> {(a::int, b::int). g < a} \<noteq> {(a::int, b::int). a = s}"
apply (rule not_sym) apply (rule not_sym)
apply (rule sets_distinct5) apply (rule sets_distinct5)
by simp by simp
lemma distinctNets: "FWLink \<noteq> any \<and> FWLink \<noteq> i4_32 \<and> FWLink \<noteq> i10_32 \<and> lemma distinctNets: "FWLink \<noteq> any \<and> FWLink \<noteq> i4_32 \<and> FWLink \<noteq> i10_32 \<and>
FWLink \<noteq> eth_intern \<and> FWLink \<noteq> eth_private \<and> any \<noteq> FWLink \<and> any \<noteq> FWLink \<noteq> eth_intern \<and> FWLink \<noteq> eth_private \<and> any \<noteq> FWLink \<and> any \<noteq>
@ -165,55 +145,36 @@ eth_private \<and> i10_32 \<noteq> FWLink \<and> i10_32 \<noteq> any \<and> i10_
\<noteq> any \<and> eth_intern \<noteq> i4_32 \<and> eth_intern \<noteq> i10_32 \<and> eth_intern \<noteq> \<noteq> any \<and> eth_intern \<noteq> i4_32 \<and> eth_intern \<noteq> i10_32 \<and> eth_intern \<noteq>
eth_private \<and> eth_private \<noteq> FWLink \<and> eth_private \<noteq> any \<and> eth_private \<noteq> eth_private \<and> eth_private \<noteq> FWLink \<and> eth_private \<noteq> any \<and> eth_private \<noteq>
i4_32 \<and> eth_private \<noteq> i10_32 \<and> eth_private \<noteq> eth_intern " i4_32 \<and> eth_private \<noteq> i10_32 \<and> eth_private \<noteq> eth_intern "
apply (simp add: PolicyL sets_distinct1 sets_distinct2 sets_distinct3 by (simp add: PolicyL sets_distinct1 sets_distinct2 sets_distinct3
sets_distinct4 sets_distinct5 sets_distinct6) sets_distinct4 sets_distinct5 sets_distinct6)
done
lemma aux5: "\<lbrakk>x \<noteq> a; y\<noteq>b; (x \<noteq> y \<and> x \<noteq> b) \<or> (a \<noteq> b \<and> a \<noteq> y)\<rbrakk> \<Longrightarrow> {x,a} \<noteq> {y,b}" lemma aux5: "\<lbrakk>x \<noteq> a; y\<noteq>b; (x \<noteq> y \<and> x \<noteq> b) \<or> (a \<noteq> b \<and> a \<noteq> y)\<rbrakk> \<Longrightarrow> {x,a} \<noteq> {y,b}"
apply auto by auto
done
lemma aux2: "{a,b} = {b,a}" lemma aux2: "{a,b} = {b,a}"
apply auto by auto
done
lemma ANDex: "allNetsDistinct (policy2list Policy)" lemma ANDex: "allNetsDistinct (policy2list Policy)"
apply (simp add: PolicyLemmas allNetsDistinct_def distinctNets) apply (simp add: PolicyLemmas allNetsDistinct_def distinctNets)
apply (simp add: PolicyL) apply (simp add: PolicyL)
apply (auto simp: PLemmas PolicyL netsDistinct_def sets_distinct5 sets_distinct6 sets_distinct1 sets_distinct2) by (auto simp: PLemmas PolicyL netsDistinct_def sets_distinct5 sets_distinct6 sets_distinct1
done sets_distinct2)
fun (sequential) numberOfRules where fun (sequential) numberOfRules where
"numberOfRules (a\<oplus>b) = numberOfRules a + numberOfRules b" "numberOfRules (a\<oplus>b) = numberOfRules a + numberOfRules b"
|"numberOfRules a = (1::int)" |"numberOfRules a = (1::int)"
fun numberOfRulesList where fun numberOfRulesList where
"numberOfRulesList (x#xs) = ((numberOfRules x)#(numberOfRulesList xs)) " "numberOfRulesList (x#xs) = ((numberOfRules x)#(numberOfRulesList xs)) "
|"numberOfRulesList [] = []" |"numberOfRulesList [] = []"
lemma all_in_list: "all_in_list (policy2list Policy) (Nets_List Policy)" lemma all_in_list: "all_in_list (policy2list Policy) (Nets_List Policy)"
apply (simp add: PolicyLemmas) apply (simp add: PolicyLemmas)
apply (unfold Nets_List_def) apply (unfold Nets_List_def)
apply (unfold bothNets_def) apply (unfold bothNets_def)
apply (insert distinctNets) apply (insert distinctNets)
apply simp by simp
done
lemmas normalizeUnfold = normalize_def PolicyL Nets_List_def bothNets_def aux aux2 bothNets_def sets_distinct1 sets_distinct2 sets_distinct3 sets_distinct4 sets_distinct5 sets_distinct6 aux5 aux2 lemmas normalizeUnfold = normalize_def PolicyL Nets_List_def bothNets_def aux aux2 bothNets_def sets_distinct1 sets_distinct2 sets_distinct3 sets_distinct4 sets_distinct5 sets_distinct6 aux5 aux2
end
end

60
Examples/VoIP/VoIP.thy
View File

@ -36,17 +36,19 @@
*****************************************************************************) *****************************************************************************)
section {* Voice over IP *} section {* Voice over IP *}
theory VoIP theory
imports VoIP
"../../UPF-Firewall" imports
"../../UPF-Firewall"
begin begin
text{*
text{* In this theory we generate the test data for correct runs of In this theory we generate the test data for correct runs of the FTP protocol. As usual, we
the FTP protocol. As usual, we start with definining the networks and start with definining the networks and the policy. We use a rather simple policy which allows
the policy. We use a rather simple policy which allows only FTP only FTP connections starting from the Intranet and going to the Internet, and deny everything
connections starting from the Intranet and going to the Internet, and else.
deny everything else. *} *}
definition definition
intranet :: "adr\<^sub>i\<^sub>p net" where intranet :: "adr\<^sub>i\<^sub>p net" where
@ -60,14 +62,13 @@ definition
gatekeeper :: "adr\<^sub>i\<^sub>p net" where gatekeeper :: "adr\<^sub>i\<^sub>p net" where
"gatekeeper = {{(a,c). a =4}}" "gatekeeper = {{(a,c). a =4}}"
definition definition
voip_policy :: "(adr\<^sub>i\<^sub>p,address voip_msg) FWPolicy" where voip_policy :: "(adr\<^sub>i\<^sub>p,address voip_msg) FWPolicy" where
"voip_policy = A\<^sub>U" "voip_policy = A\<^sub>U"
text{*
text{* The next two constants check if an address is in the Intranet The next two constants check if an address is in the Intranet or in the Internet respectively.
or in the Internet respectively.*} *}
definition definition
is_in_intranet :: "address \<Rightarrow> bool" where is_in_intranet :: "address \<Rightarrow> bool" where
@ -81,9 +82,9 @@ definition
is_in_internet :: "address \<Rightarrow> bool" where is_in_internet :: "address \<Rightarrow> bool" where
"is_in_internet a = (a > 4)" "is_in_internet a = (a > 4)"
text{* text{*
The next definition is our starting state: an empty trace and the just defined policy.*} The next definition is our starting state: an empty trace and the just defined policy.
*}
definition definition
"\<sigma>_0_voip" :: "(adr\<^sub>i\<^sub>p, address voip_msg) history \<times> "\<sigma>_0_voip" :: "(adr\<^sub>i\<^sub>p, address voip_msg) history \<times>
@ -91,30 +92,25 @@ definition
where where
"\<sigma>_0_voip = ([],voip_policy)" "\<sigma>_0_voip = ([],voip_policy)"
text{*Next we state the conditions we have on our trace: a normal text{*
behaviour FTP run from the intranet to some server in the internet on Next we state the conditions we have on our trace: a normal behaviour FTP run from the intranet
port 21.*} to some server in the internet on port 21.
*}
definition "accept_voip" :: "(adr\<^sub>i\<^sub>p, address voip_msg) history \<Rightarrow> bool" where definition "accept_voip" :: "(adr\<^sub>i\<^sub>p, address voip_msg) history \<Rightarrow> bool" where
"accept_voip t = "accept_voip t = (\<exists> c s g i p1 p2. t \<in> NB_voip c s g i p1 p2 \<and> is_in_intranet c
(\<exists> c s g i p1 p2. t \<in> NB_voip c s g i p1 p2 \<and> is_in_intranet c \<and> is_in_internet s \<and> is_in_internet s
\<and> is_gatekeeper g)" \<and> is_gatekeeper g)"
fun packet_with_id where fun packet_with_id where
"packet_with_id [] i = []" "packet_with_id [] i = []"
|"packet_with_id (x#xs) i = |"packet_with_id (x#xs) i =
(if id x = i then (x#(packet_with_id xs i)) else (packet_with_id xs i))" (if id x = i then (x#(packet_with_id xs i)) else (packet_with_id xs i))"
text{*
text{*The depth of the test case generation corresponds to the maximal The depth of the test case generation corresponds to the maximal length of generated traces,
length of generated traces. 4 is the minimum to get a full FTP 4 is the minimum to get a full FTP protocol run.
protocol run. *} *}
fun ids1 where fun ids1 where
"ids1 i (x#xs) = (id x = i \<and> ids1 i xs)" "ids1 i (x#xs) = (id x = i \<and> ids1 i xs)"
@ -129,8 +125,4 @@ lemmas ST_simps = Let_def valid_SE_def unit_SE_def bind_SE_def
VOIP.NB_voip_def \<sigma>_0_voip_def PLemmas VOIP_TRPolicy_def VOIP.NB_voip_def \<sigma>_0_voip_def PLemmas VOIP_TRPolicy_def
policy2MON_def applyPolicy_def policy2MON_def applyPolicy_def
end end