diff --git a/Examples/DMZ/DMZ.thy b/Examples/DMZ/DMZ.thy index f16951d..d804cee 100644 --- a/Examples/DMZ/DMZ.thy +++ b/Examples/DMZ/DMZ.thy @@ -38,38 +38,9 @@ section {* A Simple DMZ Setup *} theory DMZ -imports - DMZDatatype - DMZInteger + imports + DMZDatatype + DMZInteger 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 diff --git a/Examples/DMZ/DMZDatatype.thy b/Examples/DMZ/DMZDatatype.thy index fc5e885..26a5e14 100644 --- a/Examples/DMZ/DMZDatatype.thy +++ b/Examples/DMZ/DMZDatatype.thy @@ -38,83 +38,81 @@ subsection {* DMZ Datatype *} theory DMZDatatype -imports + imports "../../UPF-Firewall" 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 -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). - -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. *} - - + 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 instance Adr::adr .. type_synonym port = int type_synonym Networks = "Adr \ port" - definition intranet::"Networks net" where - "intranet = {{(a,b). a= Intranet}}" + "intranet = {{(a,b). a= Intranet}}" definition dmz :: "Networks net" where - "dmz = {{(a,b). a= DMZ}}" + "dmz = {{(a,b). a= DMZ}}" definition mail :: "Networks net" where - "mail = {{(a,b). a=Mail}}" + "mail = {{(a,b). a=Mail}}" definition web :: "Networks net" where - "web = {{(a,b). a=Web}}" + "web = {{(a,b). a=Web}}" definition internet :: "Networks net" where - "internet = {{(a,b). a= Internet}}" - + "internet = {{(a,b). a= Internet}}" + definition Intranet_mail_port :: "(Networks ,DummyContent) FWPolicy" where "Intranet_mail_port = (allow_from_ports_to {21::port,14} intranet mail)" - + definition Intranet_Internet_port :: "(Networks,DummyContent) FWPolicy" where "Intranet_Internet_port = allow_from_ports_to {80::port,90} intranet internet" - + definition Internet_web_port :: "(Networks,DummyContent) FWPolicy" where "Internet_web_port = (allow_from_ports_to {80::port,90} internet web)" - + definition Internet_mail_port :: "(Networks,DummyContent) FWPolicy" where "Internet_mail_port = (allow_all_from_port_to internet (21::port) dmz)" - + definition policyPort :: "(Networks, DummyContent) FWPolicy" where - "policyPort = deny_all ++ + "policyPort = deny_all ++ Intranet_Internet_port ++ Intranet_mail_port ++ Internet_mail_port ++ Internet_web_port" - -text {* 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. *} +text {* + 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. \ +*} definition - not_in_same_net :: "(Networks,DummyContent) packet \ bool" where - "not_in_same_net x = ((src x \ internet \ \ dest x \ internet) \ + not_in_same_net :: "(Networks,DummyContent) packet \ bool" where + "not_in_same_net x = ((src x \ internet \ \ dest x \ internet) \ (src x \ intranet \ \ dest x \ intranet) \ (src x \ dmz \ \ dest x \ dmz))" - + lemmas PolicyLemmas = dmz_def internet_def intranet_def mail_def web_def - Internet_web_port_def Internet_mail_port_def - Intranet_Internet_port_def Intranet_mail_port_def - src_def dest_def src_port dest_port in_subnet_def - - + Internet_web_port_def Internet_mail_port_def + Intranet_Internet_port_def Intranet_mail_port_def + src_def dest_def src_port dest_port in_subnet_def + + end diff --git a/Examples/DMZ/DMZInteger.thy b/Examples/DMZ/DMZInteger.thy index dc4e087..b78e1a3 100644 --- a/Examples/DMZ/DMZInteger.thy +++ b/Examples/DMZ/DMZInteger.thy @@ -38,10 +38,10 @@ subsection {* DMZ: Integer *} theory DMZInteger -imports - "../../UPF-Firewall" + imports + "../../UPF-Firewall" 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 @@ -71,10 +71,9 @@ The scenario is the following: \end{labeling} *} - definition - intranet::"adr\<^sub>i\<^sub>p net" where - "intranet = {{(a,b) . (a > 1 \ a < 4) }}" + intranet::"adr\<^sub>i\<^sub>p net" where + "intranet = {{(a,b) . (a > 1 \ a < 4) }}" definition dmz :: "adr\<^sub>i\<^sub>p net" where "dmz = {{(a,b). (a > 6) \ (a < 11)}}" @@ -88,46 +87,44 @@ definition internet :: "adr\<^sub>i\<^sub>p net" where "internet = {{(a,b). \ ( (a > 1 \ a < 4) \ (a > 6) \ (a < 11)) }}" - definition Intranet_mail_port :: "(adr\<^sub>i\<^sub>p,'b) FWPolicy" where "Intranet_mail_port = (allow_from_to_ports {21::port,14} intranet mail)" - + definition Intranet_Internet_port :: "(adr\<^sub>i\<^sub>p,'b) FWPolicy" where "Intranet_Internet_port = allow_from_to_ports {80::port,90} intranet internet" - + definition Internet_web_port :: "(adr\<^sub>i\<^sub>p,'b) FWPolicy" where "Internet_web_port = (allow_from_to_ports {80::port,90} internet web)" - + definition Internet_mail_port :: "(adr\<^sub>i\<^sub>p,'b) FWPolicy" where "Internet_mail_port = (allow_all_from_port_to internet (21::port) dmz )" - - definition policyPort :: "(adr\<^sub>i\<^sub>p, DummyContent) FWPolicy" where - "policyPort = deny_all ++ + "policyPort = deny_all ++ Intranet_Internet_port ++ Intranet_mail_port ++ Internet_mail_port ++ Internet_web_port" - -text {* 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. *} - +text {* + 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. +*} + definition - not_in_same_net :: "(adr\<^sub>i\<^sub>p,DummyContent) packet \ bool" where - "not_in_same_net x = ((src x \ internet \ \ dest x \ internet) \ + not_in_same_net :: "(adr\<^sub>i\<^sub>p,DummyContent) packet \ bool" where + "not_in_same_net x = ((src x \ internet \ \ dest x \ internet) \ (src x \ intranet \ \ dest x \ intranet) \ (src x \ dmz \ \ dest x \ dmz))" - + 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 - Internet_mail_port_def src_def dest_def IntegerPort.src_port - in_subnet_def IntegerPort.dest_port - + Intranet_Internet_port_def Intranet_mail_port_def Internet_web_port_def + Internet_mail_port_def src_def dest_def IntegerPort.src_port + in_subnet_def IntegerPort.dest_port + end diff --git a/Examples/Examples.thy b/Examples/Examples.thy index 9e7b0ae..68d0893 100644 --- a/Examples/Examples.thy +++ b/Examples/Examples.thy @@ -38,13 +38,13 @@ chapter {* Examples *} theory Examples -imports - "DMZ/DMZ" - "VoIP/VoIP" - "Transformation/Transformation" - "NAT-FW/NAT-FW" - "PersonalFirewall/PersonalFirewall" + imports + "DMZ/DMZ" + "VoIP/VoIP" + "Transformation/Transformation" + "NAT-FW/NAT-FW" + "PersonalFirewall/PersonalFirewall" begin - + end - + diff --git a/Examples/NAT-FW/NAT-FW.thy b/Examples/NAT-FW/NAT-FW.thy index 522f78f..7d48110 100644 --- a/Examples/NAT-FW/NAT-FW.thy +++ b/Examples/NAT-FW/NAT-FW.thy @@ -38,18 +38,16 @@ section {* Example: NAT *} theory "NAT-FW" -imports - "../../UPF-Firewall" + imports + "../../UPF-Firewall" begin - definition subnet1 :: "adr\<^sub>i\<^sub>p net" where "subnet1 = {{(d,e). d > 1 \ d < 256}}" definition subnet2 :: "adr\<^sub>i\<^sub>p net" where "subnet2 = {{(d,e). d > 500 \ d < 1256}}" - definition "accross_subnets x \ ((src x \ subnet1 \ (dest x \ subnet2)) \ @@ -65,7 +63,6 @@ definition nat_0 where "nat_0 = (A\<^sub>f(\x. {x}))" - lemmas UnfoldPolicy0 =filter_def nat_0_def NATLemmas ProtocolPortCombinators.ProtocolCombinators @@ -73,220 +70,156 @@ lemmas UnfoldPolicy0 =filter_def nat_0_def packet_defs accross_subnets_def subnet1_def subnet2_def - lemmas subnets = subnet1_def subnet2_def - - - - definition Adr11 :: "int set" where "Adr11 = {d. d > 2 \ d < 3}" definition Adr21 :: "int set" where "Adr21 = {d. d > 502 \ d < 503}" - definition nat_1 where "nat_1 = nat_0 ++ (srcPat2pool_IntPort Adr11 Adr21)" - definition policy_1 where "policy_1 = ((\ (x,y). x) o_f ((nat_1 \\<^sub>2 filter) o (\ x. (x,x))))" - lemmas UnfoldPolicy1 = UnfoldPolicy0 nat_1_def Adr11_def Adr21_def policy_1_def - - - definition Adr12 :: "int set" where "Adr12 = {d. d > 4 \ d < 6}" definition Adr22 :: "int set" where "Adr22 = {d. d > 504 \ d < 506}" - definition nat_2 where "nat_2 = nat_1 ++ (srcPat2pool_IntPort Adr12 Adr22)" - definition policy_2 where "policy_2 = ((\ (x,y). x) o_f ((nat_2 \\<^sub>2 filter) o (\ x. (x,x))))" - lemmas UnfoldPolicy2 = UnfoldPolicy1 nat_2_def Adr12_def Adr22_def policy_2_def - - - definition Adr13 :: "int set" where "Adr13 = {d. d > 6 \ d < 9}" definition Adr23 :: "int set" where "Adr23 = {d. d > 506 \ d < 509}" - definition nat_3 where "nat_3 = nat_2 ++ (srcPat2pool_IntPort Adr13 Adr23)" - definition policy_3 where "policy_3 = ((\ (x,y). x) o_f ((nat_3 \\<^sub>2 filter) o (\ x. (x,x))))" - lemmas UnfoldPolicy3 = UnfoldPolicy2 nat_3_def Adr13_def Adr23_def policy_3_def - - - definition Adr14 :: "int set" where "Adr14 = {d. d > 8 \ d < 12}" definition Adr24 :: "int set" where "Adr24 = {d. d > 508 \ d < 512}" - definition nat_4 where "nat_4 = nat_3 ++ (srcPat2pool_IntPort Adr14 Adr24)" - definition policy_4 where "policy_4 = ((\ (x,y). x) o_f ((nat_4 \\<^sub>2 filter) o (\ x. (x,x))))" - lemmas UnfoldPolicy4 = UnfoldPolicy3 nat_4_def Adr14_def Adr24_def policy_4_def - - - definition Adr15 :: "int set" where "Adr15 = {d. d > 10 \ d < 15}" definition Adr25 :: "int set" where "Adr25 = {d. d > 510 \ d < 515}" - definition nat_5 where "nat_5 = nat_4 ++ (srcPat2pool_IntPort Adr15 Adr25)" - definition policy_5 where "policy_5 = ((\ (x,y). x) o_f ((nat_5 \\<^sub>2 filter) o (\ x. (x,x))))" - lemmas UnfoldPolicy5 = UnfoldPolicy4 nat_5_def Adr15_def Adr25_def policy_5_def - - - definition Adr16 :: "int set" where "Adr16 = {d. d > 12 \ d < 18}" definition Adr26 :: "int set" where "Adr26 = {d. d > 512 \ d < 518}" - definition nat_6 where "nat_6 = nat_5 ++ (srcPat2pool_IntPort Adr16 Adr26)" - definition policy_6 where "policy_6 = ((\ (x,y). x) o_f ((nat_6 \\<^sub>2 filter) o (\ x. (x,x))))" - lemmas UnfoldPolicy6 = UnfoldPolicy5 nat_6_def Adr16_def Adr26_def policy_6_def - - - definition Adr17 :: "int set" where "Adr17 = {d. d > 14 \ d < 21}" definition Adr27 :: "int set" where "Adr27 = {d. d > 514 \ d < 521}" - definition nat_7 where "nat_7 = nat_6 ++ (srcPat2pool_IntPort Adr17 Adr27)" - definition policy_7 where "policy_7 = ((\ (x,y). x) o_f ((nat_7 \\<^sub>2 filter) o (\ x. (x,x))))" - lemmas UnfoldPolicy7 = UnfoldPolicy6 nat_7_def Adr17_def Adr27_def policy_7_def - - - definition Adr18 :: "int set" where "Adr18 = {d. d > 16 \ d < 24}" definition Adr28 :: "int set" where "Adr28 = {d. d > 516 \ d < 524}" - definition nat_8 where "nat_8 = nat_7 ++ (srcPat2pool_IntPort Adr18 Adr28)" - definition policy_8 where "policy_8 = ((\ (x,y). x) o_f ((nat_8 \\<^sub>2 filter) o (\ x. (x,x))))" - lemmas UnfoldPolicy8 = UnfoldPolicy7 nat_8_def Adr18_def Adr28_def policy_8_def - - - definition Adr19 :: "int set" where "Adr19 = {d. d > 18 \ d < 27}" definition Adr29 :: "int set" where "Adr29 = {d. d > 518 \ d < 527}" - definition nat_9 where "nat_9 = nat_8 ++ (srcPat2pool_IntPort Adr19 Adr29)" - definition policy_9 where "policy_9 = ((\ (x,y). x) o_f ((nat_9 \\<^sub>2 filter) o (\ x. (x,x))))" - lemmas UnfoldPolicy9 = UnfoldPolicy8 nat_9_def Adr19_def Adr29_def policy_9_def - - - definition Adr110 :: "int set" where "Adr110 = {d. d > 20 \ d < 30}" definition Adr210 :: "int set" where "Adr210 = {d. d > 520 \ d < 530}" - definition nat_10 where "nat_10 = nat_9 ++ (srcPat2pool_IntPort Adr110 Adr210)" - definition policy_10 where "policy_10 = ((\ (x,y). x) o_f ((nat_10 \\<^sub>2 filter) o (\ x. (x,x))))" - lemmas UnfoldPolicy10 = UnfoldPolicy9 nat_10_def Adr110_def Adr210_def policy_10_def - - -end +end \ No newline at end of file diff --git a/Examples/PersonalFirewall/PersonalFirewall.thy b/Examples/PersonalFirewall/PersonalFirewall.thy index ba98c54..b4b5db6 100644 --- a/Examples/PersonalFirewall/PersonalFirewall.thy +++ b/Examples/PersonalFirewall/PersonalFirewall.thy @@ -38,8 +38,9 @@ section {* Personal Firewall *} theory PersonalFirewall -imports - PersonalFirewallInt - PersonalFirewallIpv4 + imports + PersonalFirewallInt + PersonalFirewallIpv4 + PersonalFirewallDatatype begin end diff --git a/Examples/PersonalFirewall/PersonalFirewallDatatype.thy b/Examples/PersonalFirewall/PersonalFirewallDatatype.thy index 2563a22..62fd5a2 100644 --- a/Examples/PersonalFirewall/PersonalFirewallDatatype.thy +++ b/Examples/PersonalFirewall/PersonalFirewallDatatype.thy @@ -38,71 +38,60 @@ subsection {* Personal Firewall: Datatype *} theory PersonalFirewallDatatype -imports - FWTesting + imports + "../../UPF-Firewall" begin -text{* The most basic firewall scenario; there is a personal PC on one -side and the Internet on the other. There are two policies: the first -one allows all traffic from the PC to the Internet and denies all -coming into the PC. The second policy only allows specific ports from -the PC. This scenario comes in three variants: the first one specifies -the allowed protocols directly, the second together with their -respective port numbers, the third one only with the port numbers. *} +text{* + The most basic firewall scenario; there is a personal PC on one side and the Internet on the + other. There are two policies: the first one allows all traffic from the PC to the Internet and + denies all coming into the PC. The second policy only allows specific ports from the PC. This + scenario comes in three variants: the first one specifies the allowed protocols directly, the + second together with their respective port numbers, the third one only with the port numbers. +*} datatype Adr = pc | internet - + type_synonym DatatypeTwoNets = "Adr \ int" - + instance Adr::adr .. - -defs (overloaded) - src_port_def: "src_port (x::(DatatypeTwoNets,'b) packet) \ snd (src x)" - dest_port_def: "dest_port (x::(DatatypeTwoNets,'b) packet) \ snd (dest x)" - + definition - PC :: "DatatypeTwoNets net" where -"PC = {{(a,b). a = pc}}" - + PC :: "DatatypeTwoNets net" where + "PC = {{(a,b). a = pc}}" + definition - Internet :: "DatatypeTwoNets net" where -"Internet = {{(a,b). a = internet}}" - - -text{* -Definition of the testing constraint -*} - + Internet :: "DatatypeTwoNets net" where + "Internet = {{(a,b). a = internet}}" + definition - not_in_same_net :: "(DatatypeTwoNets,DummyContent) packet \ bool" where -"not_in_same_net x = ((src x \ PC \ dest x \ Internet) \ (src x \ Internet \ dest x \ PC))" - + not_in_same_net :: "(DatatypeTwoNets,DummyContent) packet \ bool" where + "not_in_same_net x = ((src x \ PC \ dest x \ Internet) \ (src x \ Internet \ dest x \ PC))" + text {* -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. + 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. *} definition - strictPolicy :: "(DatatypeTwoNets,DummyContent) FWPolicy" where -"strictPolicy = deny_all ++ allow_all_from_to PC Internet" - + strictPolicy :: "(DatatypeTwoNets,DummyContent) FWPolicy" where + "strictPolicy = deny_all ++ allow_all_from_to PC Internet" + definition - PortPolicy :: "(DatatypeTwoNets,'b) FWPolicy" where -"PortPolicy = deny_all ++ allow_from_ports_to {80::port,24,21} PC Internet" - + PortPolicy :: "(DatatypeTwoNets,'b) FWPolicy" where + "PortPolicy = deny_all ++ allow_from_ports_to {80::port,24,21} PC Internet" + definition - PortPolicyBig :: "(DatatypeTwoNets,'b) FWPolicy" where -"PortPolicyBig = + PortPolicyBig :: "(DatatypeTwoNets,'b) FWPolicy" where + "PortPolicyBig = allow_from_port_to (80::port) PC Internet \ allow_from_port_to (24::port) PC Internet \ allow_from_port_to (21::port) PC Internet \ deny_all" - - -lemmas policyLemmas = strictPolicy_def PortPolicy_def PC_def Internet_def PortPolicyBig_def src_def dest_def src_port_def dest_port_def + +lemmas policyLemmas = strictPolicy_def PortPolicy_def PC_def Internet_def PortPolicyBig_def src_def PolicyCombinators PortCombinators in_subnet_def - -end + +end \ No newline at end of file diff --git a/Examples/PersonalFirewall/PersonalFirewallInt.thy b/Examples/PersonalFirewall/PersonalFirewallInt.thy index e9231b5..d3de5ae 100644 --- a/Examples/PersonalFirewall/PersonalFirewallInt.thy +++ b/Examples/PersonalFirewall/PersonalFirewallInt.thy @@ -38,76 +38,61 @@ subsection{* Personal Firewall: Integer *} theory PersonalFirewallInt -imports - "../../UPF-Firewall" + imports + "../../UPF-Firewall" begin text{* -The most basic firewall scenario; there is a personal PC on one side and the Internet on the other. -There are two policies: the first one allows all traffic from the PC to the Internet and denies -all coming into the PC. The second policy only allows specific ports from the PC. This scenario -comes in three variants: the first one specifies the allowed protocols directly, the second together -with their respective port numbers, the third one only with the port numbers. + The most basic firewall scenario; there is a personal PC on one side and the Internet on the + other. There are two policies: the first one allows all traffic from the PC to the Internet and + denies all coming into the PC. The second policy only allows specific ports from the PC. This + scenario comes in three variants: the first one specifies the allowed protocols directly, the + second together with their respective port numbers, the third one only with the port numbers. *} - - text{* -Definitions of the subnets + Definitions of the subnets *} definition - PC :: "(adr\<^sub>i\<^sub>p net)" where -"PC = {{(a,b). a = 3}}" + PC :: "(adr\<^sub>i\<^sub>p net)" where + "PC = {{(a,b). a = 3}}" + +definition + Internet :: "adr\<^sub>i\<^sub>p net" where + "Internet = {{(a,b). \ (a = 3)}}" definition - Internet :: "adr\<^sub>i\<^sub>p net" where -"Internet = {{(a,b). \ (a = 3)}}" - - - -text{* -Definition of the testing constraint -*} - - - -definition - not_in_same_net :: "(adr\<^sub>i\<^sub>p,DummyContent) packet \ bool" where -"not_in_same_net x = ((src x \ PC \ dest x \ Internet) \ (src x \ Internet \ dest x \ PC))" - + not_in_same_net :: "(adr\<^sub>i\<^sub>p,DummyContent) packet \ bool" where + "not_in_same_net x = ((src x \ PC \ dest x \ Internet) \ (src x \ Internet \ dest x \ PC))" + text {* -Definitions of the policies + Definitions of the policies *} - - definition - strictPolicy :: "(adr\<^sub>i\<^sub>p,DummyContent) FWPolicy" where -"strictPolicy = deny_all ++ allow_all_from_to PC Internet" + strictPolicy :: "(adr\<^sub>i\<^sub>p,DummyContent) FWPolicy" where + "strictPolicy = deny_all ++ allow_all_from_to PC Internet" definition - PortPolicy :: "(adr\<^sub>i\<^sub>p,DummyContent) FWPolicy" where -"PortPolicy = deny_all ++ allow_from_ports_to {http,smtp,ftp} PC Internet" - + PortPolicy :: "(adr\<^sub>i\<^sub>p,DummyContent) FWPolicy" where + "PortPolicy = deny_all ++ allow_from_ports_to {http,smtp,ftp} PC Internet" + definition - PortPolicyBig :: "(adr\<^sub>i\<^sub>p,DummyContent) FWPolicy" where -"PortPolicyBig = deny_all ++ + PortPolicyBig :: "(adr\<^sub>i\<^sub>p,DummyContent) FWPolicy" where + "PortPolicyBig = deny_all ++ allow_from_port_to http PC Internet ++ allow_from_port_to smtp PC Internet ++ allow_from_port_to ftp PC Internet" - - + lemmas policyLemmas = strictPolicy_def PortPolicy_def PC_def - Internet_def PortPolicyBig_def src_def dest_def - adr\<^sub>i\<^sub>pLemmas content_def - PortCombinators in_subnet_def PortPolicyBig_def id_def - - + Internet_def PortPolicyBig_def src_def dest_def + adr\<^sub>i\<^sub>pLemmas content_def + PortCombinators in_subnet_def PortPolicyBig_def id_def + declare Ports [simp add] - + definition wellformed_packet::"(adr\<^sub>i\<^sub>p,DummyContent) packet \ bool" where - "wellformed_packet p = (content p = data)" - - -end + "wellformed_packet p = (content p = data)" + +end \ No newline at end of file diff --git a/Examples/PersonalFirewall/PersonalFirewallIpv4.thy b/Examples/PersonalFirewall/PersonalFirewallIpv4.thy index 6ac6de2..f1f5c0d 100644 --- a/Examples/PersonalFirewall/PersonalFirewallIpv4.thy +++ b/Examples/PersonalFirewall/PersonalFirewallIpv4.thy @@ -38,66 +38,53 @@ subsection {* Personal Firewall IPv4 *} theory PersonalFirewallIpv4 -imports - "../../UPF-Firewall" + imports + "../../UPF-Firewall" begin - - + text{* - -The most basic firewall scenario; there is a personal PC on one side and the Internet on the other. -There are two policies: the first one allows all traffic from the PC to the Internet and denies -all coming into the PC. The second policy only allows specific ports from the PC. This scenario -comes in three variants: the first one specifies the allowed protocols directly, the second together -with their respective port numbers, the third one only with the port numbers. - + The most basic firewall scenario; there is a personal PC on one side and the Internet on the + other. There are two policies: the first one allows all traffic from the PC to the Internet and + denies all coming into the PC. The second policy only allows specific ports from the PC. This + scenario comes in three variants: the first one specifies the allowed protocols directly, the + second together with their respective port numbers, the third one only with the port numbers. *} - - + text{* -Definitions of the subnets + Definitions of the subnets *} - + definition - PC :: "(ipv4 net)" where -"PC = {{((a,b,c,d),e). a = 1 \ b = 3 \ c = 5 \ d = 2}}" - + PC :: "(ipv4 net)" where + "PC = {{((a,b,c,d),e). a = 1 \ b = 3 \ c = 5 \ d = 2}}" + definition - Internet :: "ipv4 net" where -"Internet = {{((a,b,c,d),e). \ (a = 1 \ b = 3 \ c = 5 \ d = 2)}}" - - -text{* -Definition of the testing constraint -*} - + Internet :: "ipv4 net" where + "Internet = {{((a,b,c,d),e). \ (a = 1 \ b = 3 \ c = 5 \ d = 2)}}" + definition - not_in_same_net :: "(ipv4,DummyContent) packet \ bool" where -"not_in_same_net x = ((src x \ PC \ dest x \ Internet) \ (src x \ Internet \ dest x \ PC))" - + not_in_same_net :: "(ipv4,DummyContent) packet \ bool" where + "not_in_same_net x = ((src x \ PC \ dest x \ Internet) \ (src x \ Internet \ dest x \ PC))" + text {* -Definitions of the policies + Definitions of the policies *} - definition - strictPolicy :: "(ipv4,DummyContent) FWPolicy" where -"strictPolicy = deny_all ++ allow_all_from_to PC Internet" - + strictPolicy :: "(ipv4,DummyContent) FWPolicy" where + "strictPolicy = deny_all ++ allow_all_from_to PC Internet" + definition - PortPolicy :: "(ipv4,DummyContent) FWPolicy" where -"PortPolicy = deny_all ++ allow_from_ports_to {80::port,24,21} PC Internet" - + PortPolicy :: "(ipv4,DummyContent) FWPolicy" where + "PortPolicy = deny_all ++ allow_from_ports_to {80::port,24,21} PC Internet" + definition - 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 :: "(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" + lemmas policyLemmas = strictPolicy_def PortPolicy_def PC_def - Internet_def PortPolicyBig_def src_def dest_def - IPv4.src_port - IPv4.dest_port PolicyCombinators - PortCombinators in_subnet_def PortPolicyBig_def - - - + Internet_def PortPolicyBig_def src_def dest_def + IPv4.src_port + IPv4.dest_port PolicyCombinators + PortCombinators in_subnet_def PortPolicyBig_def + end diff --git a/Examples/Transformation/Transformation.thy b/Examples/Transformation/Transformation.thy index 0f6eac4..5c3093e 100644 --- a/Examples/Transformation/Transformation.thy +++ b/Examples/Transformation/Transformation.thy @@ -36,9 +36,11 @@ *****************************************************************************) section {* Demonstrating Policy Transformations *} -theory Transformation -imports - Transformation01 - Transformation02 +theory + Transformation + imports + Transformation01 + Transformation02 begin end + \ No newline at end of file diff --git a/Examples/Transformation/Transformation01.thy b/Examples/Transformation/Transformation01.thy index 07d29bd..224df2f 100644 --- a/Examples/Transformation/Transformation01.thy +++ b/Examples/Transformation/Transformation01.thy @@ -38,94 +38,82 @@ subsection {* Transformation Example 1 *} theory Transformation01 -imports - "../../UPF-Firewall" + imports + "../../UPF-Firewall" begin definition - FWLink :: "adr\<^sub>i\<^sub>p net" where -"FWLink = {{(a,b). a = 1}}" + FWLink :: "adr\<^sub>i\<^sub>p net" where + "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 - 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 -(* Mandatory: Global *) - - MG2 :: "(adr\<^sub>i\<^sub>p net,port) Combinators" where -"MG2 = AllowPortFromTo i27 any 1 \ + (* Mandatory: Global *) + MG2 :: "(adr\<^sub>i\<^sub>p net,port) Combinators" where + "MG2 = AllowPortFromTo i27 any 1 \ AllowPortFromTo i27 any 2 \ AllowPortFromTo i27 any 3" - + definition - MG3 :: "(adr\<^sub>i\<^sub>p net,port) Combinators" where -"MG3 = AllowPortFromTo any FWLink 1" - + MG3 :: "(adr\<^sub>i\<^sub>p net,port) Combinators" where + "MG3 = AllowPortFromTo any FWLink 1" + definition - MG4 :: "(adr\<^sub>i\<^sub>p net,port) Combinators" where -"MG4 = AllowPortFromTo FWLink FWLink 4" - + MG4 :: "(adr\<^sub>i\<^sub>p net,port) Combinators" where + "MG4 = AllowPortFromTo FWLink FWLink 4" + definition - MG7 :: "(adr\<^sub>i\<^sub>p net,port) Combinators" where -"MG7 = AllowPortFromTo FWLink i4 6 \ + MG7 :: "(adr\<^sub>i\<^sub>p net,port) Combinators" where + "MG7 = AllowPortFromTo FWLink i4 6 \ AllowPortFromTo FWLink i4 7" - + definition - MG8 :: "(adr\<^sub>i\<^sub>p net,port) Combinators" where -"MG8 = AllowPortFromTo FWLink i4 6 \ + MG8 :: "(adr\<^sub>i\<^sub>p net,port) Combinators" where + "MG8 = AllowPortFromTo FWLink i4 6 \ 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 - DG3:: "(adr\<^sub>i\<^sub>p net,port) Combinators" where -"DG3 = AllowPortFromTo any any 7" + "Policy = DenyAll \ MG8 \ MG7 \ MG4 \ MG3 \ MG2 \ 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 -definition -"Policy = DenyAll \ MG8 \ MG7 \ MG4 \ MG3 \ MG2 \ 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 +lemmas PolicyL = MG2_def MG3_def MG4_def MG7_def MG8_def DG3_def Policy_def definition - not_in_same_net :: "(adr\<^sub>i\<^sub>p,DummyContent) packet \ bool" where -"not_in_same_net x = (((src x \ i27) \ ( \ (dest x \ i27))) \ + not_in_same_net :: "(adr\<^sub>i\<^sub>p,DummyContent) packet \ bool" where + "not_in_same_net x = (((src x \ i27) \ ( \ (dest x \ i27))) \ ((src x \ i4) \ ( \ (dest x \ i4))) \ ((src x \ eth_intern) \ ( \ (dest x \ eth_intern))) \ ((src x \ eth_private) \ ( \ (dest x \ eth_private))))" @@ -140,45 +128,33 @@ lemmas fixDefs = fixElements_def NetworkCore.id_def NetworkCore.content_def lemma sets_distinct1: "(n::int) \ m \ {(a,b). a = n} \ {(a,b). a = m}" -apply auto -done + by auto lemma sets_distinct2: "(m::int) \ n \ {(a,b). a = n} \ {(a,b). a = m}" -apply auto -done - - + by auto lemma sets_distinct3: "{((a::int),(b::int)). a = n} \ {(a,b). a > n}" -apply auto -done - + by auto lemma sets_distinct4: "{((a::int),(b::int)). a > n} \ {(a,b). a = n}" -apply auto -done - + by auto lemma aux: "\a \ c; a \ d; c = d\ \ False" -apply auto -done - - + by auto + lemma sets_distinct5: "(s::int) < g \ {(a::int, b::int). a = s} \ {(a::int, b::int). g < a}" -apply (auto simp: sets_distinct3) -apply (subgoal_tac "(s,4) \ {(a::int,b::int). a = (s)}") -apply (subgoal_tac "(s,4) \ {(a::int,b::int). g < a}") -apply (erule aux) -apply assumption+ -apply simp -by blast - + apply (auto simp: sets_distinct3) + apply (subgoal_tac "(s,4) \ {(a::int,b::int). a = (s)}") + apply (subgoal_tac "(s,4) \ {(a::int,b::int). g < a}") + apply (erule aux) + apply assumption+ + apply simp + by blast lemma sets_distinct6: "(s::int) < g \ {(a::int, b::int). g < a} \ {(a::int, b::int). a = s}" -apply (rule not_sym) -apply (rule sets_distinct5) -by simp - + apply (rule not_sym) + apply (rule sets_distinct5) + by simp lemma distinctNets: "FWLink \ any \ FWLink \ i4 \ FWLink \ i27 \ FWLink \ eth_intern \ FWLink \ eth_private \ any \ FWLink \ any \ i4 \ any \ i27 \ any \ eth_intern \ any \ eth_private \ i4 \ FWLink \ @@ -186,83 +162,34 @@ i4 \ any \ i4 \ i27 \ i4 \ eth_intern \ i i27 \ i4 \ i27 \ eth_intern \ i27 \ eth_private \ eth_intern \ FWLink \ eth_intern \ any \ eth_intern \ i4 \ eth_intern \ i27 \ eth_intern \ eth_private \ eth_private \ FWLink \ eth_private \ any \ eth_private \ i4 \ eth_private \ i27 \ eth_private \ eth_intern" -apply (simp add: PolicyLemmas sets_distinct1 sets_distinct2 sets_distinct3 sets_distinct4 sets_distinct5 sets_distinct6) -done - - + by (simp add: PolicyLemmas sets_distinct1 sets_distinct2 sets_distinct3 sets_distinct4 + sets_distinct5 sets_distinct6) lemma aux5: "\x \ a; y\b; (x \ y \ x \ b) \ (a \ b \ a \ y)\ \ {x,a} \ {y,b}" - apply auto -done - + by auto lemma aux2: "{a,b} = {b,a}" - apply auto -done - -(* -lemma noMT: "\ x \ set (policy2list Policy). dom (C x) \ {}" -apply (simp add: PolicyLemmas) -apply (simp add: PLemmas PolicyLemmas) -by arith -*) - + by auto lemma ANDex: "allNetsDistinct (policy2list Policy)" -apply (simp add: PolicyL allNetsDistinct_def distinctNets) -apply (auto simp: PLemmas PolicyLemmas netsDistinct_def sets_distinct5 sets_distinct6) -done - -(* -lemma count_the_rules: "(int (length(policy2list (list2FWpolicy(normalize Policy)))) = post) \ -(int(length (policy2list Policy)) = pre) \ - (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 -*) - + apply (simp add: PolicyL allNetsDistinct_def distinctNets) + by (auto simp: PLemmas PolicyLemmas netsDistinct_def sets_distinct5 sets_distinct6) + fun (sequential) numberOfRules where - "numberOfRules (a\b) = numberOfRules a + numberOfRules b" - |"numberOfRules a = (1::int)" - - - + "numberOfRules (a\b) = numberOfRules a + numberOfRules b" +|"numberOfRules a = (1::int)" fun numberOfRulesList where "numberOfRulesList (x#xs) = ((numberOfRules x)#(numberOfRulesList xs)) " |"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)" -apply (simp add: PolicyL) -apply (unfold Nets_List_def) -apply (unfold bothNets_def) -apply (insert distinctNets) -apply simp -done + apply (simp add: PolicyL) + apply (unfold Nets_List_def) + apply (unfold bothNets_def) + apply (insert distinctNets) + by simp lemmas normalizeUnfold = normalize_def Policy_def Nets_List_def bothNets_def aux aux2 bothNets_def -(* -lemma noMT2: "\ x \ set (policy2list Policy). dom (C x) \ {}" -apply (simp add: PLemmas normalize_def bothNets_def - PolicyLemmas aux5 aux2 Nets_List_def ) -by (metis zless_add1_eq) -*) - - -end +end \ No newline at end of file diff --git a/Examples/Transformation/Transformation02.thy b/Examples/Transformation/Transformation02.thy index 3362158..1517bdc 100644 --- a/Examples/Transformation/Transformation02.thy +++ b/Examples/Transformation/Transformation02.thy @@ -38,123 +38,103 @@ subsection {* Transforamtion Example 2 *} theory Transformation02 -imports - "../../UPF-Firewall" + imports + "../../UPF-Firewall" begin - + definition - FWLink :: "adr\<^sub>i\<^sub>p net" where -"FWLink = {{(a,b). a = 1}}" - + FWLink :: "adr\<^sub>i\<^sub>p net" where + "FWLink = {{(a,b). a = 1}}" + definition - any :: "adr\<^sub>i\<^sub>p net" where -"any = {{(a,b). a > 5}}" - + any :: "adr\<^sub>i\<^sub>p net" where + "any = {{(a,b). a > 5}}" + definition - i4_32:: "adr\<^sub>i\<^sub>p net" where -"i4_32 = {{(a,b). a = 2 }}" - + i4_32:: "adr\<^sub>i\<^sub>p net" where + "i4_32 = {{(a,b). a = 2 }}" + definition - i10_32:: "adr\<^sub>i\<^sub>p net" where -"i10_32 = {{(a,b). a = 3 }}" - + i10_32:: "adr\<^sub>i\<^sub>p net" where + "i10_32 = {{(a,b). a = 3 }}" + definition - eth_intern:: "adr\<^sub>i\<^sub>p net" where -"eth_intern = {{(a,b). a = 4 }}" - + 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 }}" - - - + eth_private:: "adr\<^sub>i\<^sub>p net" where + "eth_private = {{(a,b). a = 5 }}" + definition - D1a :: "(adr\<^sub>i\<^sub>p net, port) Combinators" where -"D1a = AllowPortFromTo eth_intern any 1 \ + D1a :: "(adr\<^sub>i\<^sub>p net, port) Combinators" where + "D1a = AllowPortFromTo eth_intern any 1 \ AllowPortFromTo eth_intern any 2" - - + definition - D1b :: "(adr\<^sub>i\<^sub>p net, port) Combinators" where -"D1b = AllowPortFromTo eth_private any 1 \ + D1b :: "(adr\<^sub>i\<^sub>p net, port) Combinators" where + "D1b = AllowPortFromTo eth_private any 1 \ AllowPortFromTo eth_private any 2" - + definition - D2a :: "(adr\<^sub>i\<^sub>p net, port) Combinators" where -"D2a = AllowPortFromTo any i4_32 21" - - + D2a :: "(adr\<^sub>i\<^sub>p net, port) Combinators" where + "D2a = AllowPortFromTo any i4_32 21" + definition - D2b :: "(adr\<^sub>i\<^sub>p net, port) Combinators" where -"D2b = AllowPortFromTo any i10_32 21 \ + D2b :: "(adr\<^sub>i\<^sub>p net, port) Combinators" where + "D2b = AllowPortFromTo any i10_32 21 \ AllowPortFromTo any i10_32 43" - - - + definition - Policy :: "(adr\<^sub>i\<^sub>p net, port) Combinators" where -"Policy = DenyAll \ D2b \ D2a \ D1b \ D1a" - + Policy :: "(adr\<^sub>i\<^sub>p net, port) Combinators" where + "Policy = DenyAll \ D2b \ D2a \ D1b \ D1a" + lemmas PolicyLemmas = Policy_def D1a_def D1b_def D2a_def D2b_def - - - lemmas PolicyL = Policy_def - FWLink_def - any_def - i10_32_def - i4_32_def - eth_intern_def - eth_private_def - D1a_def D1b_def D2a_def D2b_def + +lemmas PolicyL = Policy_def + FWLink_def + any_def + i10_32_def + i4_32_def + eth_intern_def + eth_private_def + D1a_def D1b_def D2a_def D2b_def consts fixID :: id consts fixContent :: DummyContent - + definition "fixElements p = (id p = fixID \ content p = fixContent)" - + lemmas fixDefs = fixElements_def NetworkCore.id_def NetworkCore.content_def - - lemma sets_distinct1: "(n::int) \ m \ {(a,b). a = n} \ {(a,b). a = m}" -apply auto -done + by auto lemma sets_distinct2: "(m::int) \ n \ {(a,b). a = n} \ {(a,b). a = m}" -apply auto -done - - + by auto lemma sets_distinct3: "{((a::int),(b::int)). a = n} \ {(a,b). a > n}" -apply auto -done - - + by auto + lemma sets_distinct4: "{((a::int),(b::int)). a > n} \ {(a,b). a = n}" -apply auto -done - - + by auto + lemma aux: "\a \ c; a \ d; c = d\ \ False" -apply auto -done - + by auto lemma sets_distinct5: "(s::int) < g \ {(a::int, b::int). a = s} \ {(a::int, b::int). g < a}" -apply (auto simp: sets_distinct3) -apply (subgoal_tac "(s,4) \ {(a::int,b::int). a = (s)}") -apply (subgoal_tac "(s,4) \ {(a::int,b::int). g < a}") -apply (erule aux) -apply assumption+ -apply simp -by blast - + apply (auto simp: sets_distinct3) + apply (subgoal_tac "(s,4) \ {(a::int,b::int). a = (s)}") + apply (subgoal_tac "(s,4) \ {(a::int,b::int). g < a}") + apply (erule aux) + apply assumption+ + apply simp + by blast + lemma sets_distinct6: "(s::int) < g \ {(a::int, b::int). g < a} \ {(a::int, b::int). a = s}" -apply (rule not_sym) -apply (rule sets_distinct5) -by simp - + apply (rule not_sym) + apply (rule sets_distinct5) + by simp lemma distinctNets: "FWLink \ any \ FWLink \ i4_32 \ FWLink \ i10_32 \ FWLink \ eth_intern \ FWLink \ eth_private \ any \ FWLink \ any \ @@ -165,55 +145,36 @@ eth_private \ i10_32 \ FWLink \ i10_32 \ any \ i10_ \ any \ eth_intern \ i4_32 \ eth_intern \ i10_32 \ eth_intern \ eth_private \ eth_private \ FWLink \ eth_private \ any \ eth_private \ i4_32 \ eth_private \ i10_32 \ eth_private \ eth_intern " -apply (simp add: PolicyL sets_distinct1 sets_distinct2 sets_distinct3 - sets_distinct4 sets_distinct5 sets_distinct6) -done - - - + by (simp add: PolicyL sets_distinct1 sets_distinct2 sets_distinct3 + sets_distinct4 sets_distinct5 sets_distinct6) + lemma aux5: "\x \ a; y\b; (x \ y \ x \ b) \ (a \ b \ a \ y)\ \ {x,a} \ {y,b}" - apply auto -done - - + by auto + lemma aux2: "{a,b} = {b,a}" - apply auto -done - - - - + by auto + lemma ANDex: "allNetsDistinct (policy2list Policy)" -apply (simp add: PolicyLemmas allNetsDistinct_def distinctNets) -apply (simp add: PolicyL) -apply (auto simp: PLemmas PolicyL netsDistinct_def sets_distinct5 sets_distinct6 sets_distinct1 sets_distinct2) -done - + apply (simp add: PolicyLemmas allNetsDistinct_def distinctNets) + apply (simp add: PolicyL) + by (auto simp: PLemmas PolicyL netsDistinct_def sets_distinct5 sets_distinct6 sets_distinct1 + sets_distinct2) + fun (sequential) numberOfRules where - "numberOfRules (a\b) = numberOfRules a + numberOfRules b" - |"numberOfRules a = (1::int)" - - - - + "numberOfRules (a\b) = numberOfRules a + numberOfRules b" +|"numberOfRules a = (1::int)" + fun numberOfRulesList where - "numberOfRulesList (x#xs) = ((numberOfRules x)#(numberOfRulesList xs)) " - |"numberOfRulesList [] = []" - - - + "numberOfRulesList (x#xs) = ((numberOfRules x)#(numberOfRulesList xs)) " +|"numberOfRulesList [] = []" + lemma all_in_list: "all_in_list (policy2list Policy) (Nets_List Policy)" -apply (simp add: PolicyLemmas) -apply (unfold Nets_List_def) -apply (unfold bothNets_def) -apply (insert distinctNets) -apply simp -done - - + apply (simp add: PolicyLemmas) + apply (unfold Nets_List_def) + apply (unfold bothNets_def) + apply (insert distinctNets) + by simp + 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 \ No newline at end of file diff --git a/Examples/VoIP/VoIP.thy b/Examples/VoIP/VoIP.thy index 586b29a..907ab3c 100644 --- a/Examples/VoIP/VoIP.thy +++ b/Examples/VoIP/VoIP.thy @@ -36,17 +36,19 @@ *****************************************************************************) section {* Voice over IP *} -theory VoIP -imports - "../../UPF-Firewall" +theory + VoIP + imports + "../../UPF-Firewall" begin + - -text{* In this theory we generate the test data for correct runs of -the FTP protocol. As usual, we start with definining the networks and -the policy. We use a rather simple policy which allows only FTP -connections starting from the Intranet and going to the Internet, and -deny everything else. *} +text{* + In this theory we generate the test data for correct runs of the FTP protocol. As usual, we + start with definining the networks and the policy. We use a rather simple policy which allows + only FTP connections starting from the Intranet and going to the Internet, and deny everything + else. +*} definition intranet :: "adr\<^sub>i\<^sub>p net" where @@ -60,14 +62,13 @@ definition gatekeeper :: "adr\<^sub>i\<^sub>p net" where "gatekeeper = {{(a,c). a =4}}" - definition voip_policy :: "(adr\<^sub>i\<^sub>p,address voip_msg) FWPolicy" where "voip_policy = A\<^sub>U" - -text{* The next two constants check if an address is in the Intranet -or in the Internet respectively.*} +text{* + The next two constants check if an address is in the Intranet or in the Internet respectively. +*} definition is_in_intranet :: "address \ bool" where @@ -81,9 +82,9 @@ definition is_in_internet :: "address \ bool" where "is_in_internet a = (a > 4)" - 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 "\_0_voip" :: "(adr\<^sub>i\<^sub>p, address voip_msg) history \ @@ -91,30 +92,25 @@ definition where "\_0_voip = ([],voip_policy)" -text{*Next we state the conditions we have on our trace: a normal -behaviour FTP run from the intranet to some server in the internet on -port 21.*} +text{* + Next we state the conditions we have on our trace: a normal behaviour FTP run from the intranet + to some server in the internet on port 21. +*} definition "accept_voip" :: "(adr\<^sub>i\<^sub>p, address voip_msg) history \ bool" where - "accept_voip t = - (\ c s g i p1 p2. t \ NB_voip c s g i p1 p2 \ is_in_intranet c \ is_in_internet s + "accept_voip t = (\ c s g i p1 p2. t \ NB_voip c s g i p1 p2 \ is_in_intranet c + \ is_in_internet s \ is_gatekeeper g)" - - fun packet_with_id where "packet_with_id [] i = []" |"packet_with_id (x#xs) i = (if id x = i then (x#(packet_with_id xs i)) else (packet_with_id xs i))" - -text{*The depth of the test case generation corresponds to the maximal -length of generated traces. 4 is the minimum to get a full FTP -protocol run. *} - - - - +text{* + The depth of the test case generation corresponds to the maximal length of generated traces, + 4 is the minimum to get a full FTP protocol run. +*} fun ids1 where "ids1 i (x#xs) = (id x = i \ 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 \_0_voip_def PLemmas VOIP_TRPolicy_def policy2MON_def applyPolicy_def - - - - end