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

Checked style.

This commit is contained in:
Achim D. Brucker 2016-12-27 23:43:47 +00:00
parent 2f0da5f6ba
commit e0dac8a3ab
15 changed files with 127 additions and 134 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
PacketFilter/DatatypeAddress.thy
View File

@ -38,8 +38,8 @@
subsection {* Datatype Addresses *}
theory
DatatypeAddress
imports
NetworkCore
imports
NetworkCore
begin
text{*
@ -58,5 +58,5 @@ definition
definition
internet::"DatatypeAddress net" where
"internet = {{internet_adr}}"
end

10
PacketFilter/DatatypePort.thy
View File

@ -36,8 +36,10 @@
*****************************************************************************)
subsection {* Datatype Addresses with Ports *}
theory DatatypePort
imports NetworkCore
theory
DatatypePort
imports
NetworkCore
begin
text{*
@ -67,7 +69,7 @@ definition
overloading src_port_datatype \<equiv> "src_port :: ('\<alpha>::adr,'\<beta>) packet \<Rightarrow> '\<gamma>::port"
begin
definition
"src_port_datatype (x::(DatatypePort,'\<beta>) packet) \<equiv> (snd o fst o snd) x"
"src_port_datatype (x::(DatatypePort,'\<beta>) packet) \<equiv> (snd o fst o snd) x"
end
overloading dest_port_datatype \<equiv> "dest_port :: ('\<alpha>::adr,'\<beta>) packet \<Rightarrow> '\<gamma>::port"
@ -87,7 +89,7 @@ lemma src_port : "src_port ((a,x,d,e)::(DatatypePort,'\<beta>) packet) = snd x"
lemma dest_port : "dest_port ((a,d,x,e)::(DatatypePort,'\<beta>) packet) = snd x"
by (simp add: dest_port_datatype_def in_subnet)
lemmas DatatypePortLemmas = src_port dest_port src_port_datatype_def dest_port_datatype_def
end

8
PacketFilter/IPv4.thy
View File

@ -38,8 +38,8 @@
subsection {* Formalizing IPv4 Addresses *}
theory
IPv4
imports
NetworkCore
imports
NetworkCore
begin
text{*
A theory describing IPv4 addresses with ports. The host address is a four-tuple of Integers,
@ -58,7 +58,7 @@ type_synonym
overloading src_port_ipv4 \<equiv> "src_port :: ('\<alpha>::adr,'\<beta>) packet \<Rightarrow> '\<gamma>::port"
begin
definition
"src_port_ipv4 (x::(ipv4,'\<beta>) packet) \<equiv> (snd o fst o snd) x"
"src_port_ipv4 (x::(ipv4,'\<beta>) packet) \<equiv> (snd o fst o snd) x"
end
overloading dest_port_ipv4 \<equiv> "dest_port :: ('\<alpha>::adr,'\<beta>) packet \<Rightarrow> '\<gamma>::port"
@ -74,7 +74,7 @@ definition
end
definition subnet_of_ip :: "ipv4_ip \<Rightarrow> ipv4 net"
where "subnet_of_ip ip = {{(a,b). (a = ip)}}"
where "subnet_of_ip ip = {{(a,b). (a = ip)}}"
lemma src_port: "src_port (a,(x::ipv4),d,e) = snd x"
by (simp add: src_port_ipv4_def in_subnet)

11
PacketFilter/IPv4_TCPUDP.thy
View File

@ -36,8 +36,9 @@
*****************************************************************************)
subsection {* IPv4 with Ports and Protocols *}
theory IPv4_TCPUDP
imports IPv4
theory
IPv4_TCPUDP
imports IPv4
begin
type_synonym
@ -48,7 +49,7 @@ instance protocol :: adr ..
overloading src_port_ipv4_TCPUDP \<equiv> "src_port :: ('\<alpha>::adr,'\<beta>) packet \<Rightarrow> '\<gamma>::port"
begin
definition
"src_port_ipv4_TCPUDP (x::(ipv4_TCPUDP,'\<beta>) packet) \<equiv> (fst o snd o fst o snd) x"
"src_port_ipv4_TCPUDP (x::(ipv4_TCPUDP,'\<beta>) packet) \<equiv> (fst o snd o fst o snd) x"
end
overloading dest_port_ipv4_TCPUDP \<equiv> "dest_port :: ('\<alpha>::adr,'\<beta>) packet \<Rightarrow> '\<gamma>::port"
@ -70,7 +71,7 @@ definition
end
definition subnet_of_ip :: "ipv4_ip \<Rightarrow> ipv4_TCPUDP net"
where "subnet_of_ip ip = {{(a,b). (a = ip)}}"
where "subnet_of_ip ip = {{(a,b). (a = ip)}}"
lemma src_port: "src_port (a,(x::ipv4_TCPUDP),d,e) = fst (snd x)"
by (simp add: src_port_ipv4_TCPUDP_def in_subnet)
@ -79,5 +80,5 @@ lemma dest_port: "dest_port (a,d,(x::ipv4_TCPUDP),e) = fst (snd x)"
by (simp add: dest_port_ipv4_TCPUDP_def in_subnet)
lemmas Ipv4_TCPUDPLemmas = src_port dest_port src_port_ipv4_TCPUDP_def dest_port_ipv4_TCPUDP_def
dest_protocol_ipv4_TCPUDP_def subnet_of_ipv4_TCPUDP_def
dest_protocol_ipv4_TCPUDP_def subnet_of_ipv4_TCPUDP_def
end

10
PacketFilter/IntegerAddress.thy
View File

@ -36,13 +36,15 @@
*****************************************************************************)
subsection {* Integer Addresses *}
theory IntegerAddress
imports NetworkCore
theory
IntegerAddress
imports
NetworkCore
begin
text{* A theory where addresses are modelled as Integers.*}
type_synonym
adr\<^sub>i = "int"
adr\<^sub>i = "int"
end

6
PacketFilter/IntegerPort.thy
View File

@ -38,8 +38,8 @@
subsection{* Integer Addresses with Ports *}
theory
IntegerPort
imports
NetworkCore
imports
NetworkCore
begin
text{*
@ -59,7 +59,7 @@ type_synonym
overloading src_port_int \<equiv> "src_port :: ('\<alpha>::adr,'\<beta>) packet \<Rightarrow> '\<gamma>::port"
begin
definition
"src_port_int (x::(adr\<^sub>i\<^sub>p,'\<beta>) packet) \<equiv> (snd o fst o snd) x"
"src_port_int (x::(adr\<^sub>i\<^sub>p,'\<beta>) packet) \<equiv> (snd o fst o snd) x"
end
overloading dest_port_int \<equiv> "dest_port :: ('\<alpha>::adr,'\<beta>) packet \<Rightarrow> '\<gamma>::port"

16
PacketFilter/IntegerPort_TCPUDP.thy
View File

@ -38,8 +38,8 @@
subsection {* Integer Addresses with Ports and Protocols *}
theory
IntegerPort_TCPUDP
imports
NetworkCore
imports
NetworkCore
begin
text{* A theory describing addresses which are modelled as a pair of Integers - the first being
@ -59,7 +59,7 @@ instance protocol :: adr ..
overloading src_port_int_TCPUDP \<equiv> "src_port :: ('\<alpha>::adr,'\<beta>) packet \<Rightarrow> '\<gamma>::port"
begin
definition
"src_port_int_TCPUDP (x::(adr\<^sub>i\<^sub>p\<^sub>p,'\<beta>) packet) \<equiv> (fst o snd o fst o snd) x"
"src_port_int_TCPUDP (x::(adr\<^sub>i\<^sub>p\<^sub>p,'\<beta>) packet) \<equiv> (fst o snd o fst o snd) x"
end
overloading dest_port_int_TCPUDP \<equiv> "dest_port :: ('\<alpha>::adr,'\<beta>) packet \<Rightarrow> '\<gamma>::port"
@ -94,18 +94,16 @@ lemma dest_port: "dest_port (a,d,x::adr\<^sub>i\<^sub>p\<^sub>p,e) = fst (snd x)
text {* Common test constraints: *}
definition port_positive :: "(adr\<^sub>i\<^sub>p\<^sub>p,'b) packet \<Rightarrow> bool" where
"port_positive x = (dest_port x > (0::port))"
"port_positive x = (dest_port x > (0::port))"
definition fix_values :: "(adr\<^sub>i\<^sub>p\<^sub>p,DummyContent) packet \<Rightarrow> bool" where
"fix_values x = (src_port x = (1::port) \<and> src_protocol x = udp \<and> content x = data \<and> id x = 1)"
"fix_values x = (src_port x = (1::port) \<and> src_protocol x = udp \<and> content x = data \<and> id x = 1)"
lemmas adr\<^sub>i\<^sub>p\<^sub>pLemmas = src_port dest_port src_port_int_TCPUDP_def dest_port_int_TCPUDP_def
src_protocol_int_TCPUDP_def dest_protocol_int_TCPUDP_def
subnet_of_int_TCPUDP_def
src_protocol_int_TCPUDP_def dest_protocol_int_TCPUDP_def subnet_of_int_TCPUDP_def
lemmas adr\<^sub>i\<^sub>p\<^sub>pTestConstraints = port_positive_def fix_values_def
end

20
PacketFilter/NetworkCore.thy
View File

@ -38,8 +38,8 @@
subsection{* Packets and Networks *}
theory
NetworkCore
imports
Main
imports
Main
begin
text{*
@ -94,7 +94,7 @@ text{*
*}
definition src :: "('\<alpha>::adr,'\<beta>) packet \<Rightarrow> '\<alpha>"
where "src = fst o snd "
where "src = fst o snd "
text{*
Port numbers (which are part of an address) are also modelled in a generic way. The integers and
@ -116,24 +116,24 @@ text{*
To access the different parts of a packet directly, we define a couple of projectors:
*}
definition id :: "('\<alpha>::adr,'\<beta>) packet \<Rightarrow> id"
where "id = fst"
where "id = fst"
definition dest :: "('\<alpha>::adr,'\<beta>) packet \<Rightarrow> '\<alpha> dest"
where "dest = fst o snd o snd"
where "dest = fst o snd o snd"
definition content :: "('\<alpha>::adr,'\<beta>) packet \<Rightarrow> '\<beta> content"
where "content = snd o snd o snd"
where "content = snd o snd o snd"
datatype protocol = tcp | udp
lemma either: "\<lbrakk>a \<noteq> tcp;a \<noteq> udp\<rbrakk> \<Longrightarrow> False"
by (case_tac a,simp_all)
by (case_tac a,simp_all)
lemma either2[simp]: "(a \<noteq> tcp) = (a = udp)"
by (case_tac a,simp_all)
by (case_tac a,simp_all)
lemma either3[simp]: "(a \<noteq> udp) = (a = tcp)"
by (case_tac a,simp_all)
by (case_tac a,simp_all)
text{*
The following two constants give the source and destination port number of a packet. Address
@ -164,7 +164,7 @@ lemma in_subnet:
lemma src_in_subnet:
"src(q,(a,e),r,t) \<sqsubset> {{(x1,y). P x1 y}} = P a e"
by (simp add: in_subnet_def in_subnet src_def)
by (simp add: in_subnet_def in_subnet src_def)
lemma dest_in_subnet:
"dest (q,r,((a),e),t) \<sqsubset> {{(x1,y). P x1 y}} = P a e"

18
PacketFilter/NetworkModels.thy
View File

@ -36,18 +36,18 @@
*****************************************************************************)
section{* Network Models *}
theory
theory
NetworkModels
imports
DatatypeAddress
DatatypePort
imports
DatatypeAddress
DatatypePort
IntegerAddress
IntegerPort
IntegerPort_TCPUDP
IntegerAddress
IntegerPort
IntegerPort_TCPUDP
IPv4
IPv4_TCPUDP
IPv4
IPv4_TCPUDP
begin
text{*

8
PacketFilter/PacketFilter.thy
View File

@ -37,9 +37,9 @@
subsection {* Network Policies: Packet Filter *}
theory
PacketFilter
imports
NetworkModels
ProtocolPortCombinators
Ports
imports
NetworkModels
ProtocolPortCombinators
Ports
begin
end

15
PacketFilter/PolicyCombinators.thy
View File

@ -36,9 +36,10 @@
*****************************************************************************)
subsection {* Policy Combinators *}
theory PolicyCombinators
imports
PolicyCore
theory
PolicyCombinators
imports
PolicyCore
begin
text{* In order to ease the specification of a concrete policy, we
@ -69,8 +70,7 @@ definition
definition
deny_all_from_to :: "'\<alpha>::adr net \<Rightarrow> '\<alpha>::adr net \<Rightarrow> (('\<alpha>,'\<beta>) packet \<mapsto> unit)" where
"deny_all_from_to src_net dest_net =
{pa. src pa \<sqsubset> src_net \<and> dest pa \<sqsubset> dest_net} \<triangleleft> D\<^sub>U"
"deny_all_from_to src_net dest_net = {pa. src pa \<sqsubset> src_net \<and> dest pa \<sqsubset> dest_net} \<triangleleft> D\<^sub>U"
text{* All these combinators and the default rules are put into one
@ -81,6 +81,5 @@ text{* All these combinators and the default rules are put into one
lemmas PolicyCombinators = allow_all_from_def deny_all_from_def
allow_all_to_def deny_all_to_def allow_all_from_to_def
deny_all_from_to_def UPFDefs
end
end

4
PacketFilter/PolicyCore.thy
View File

@ -38,8 +38,8 @@
subsection {* Policy Core *}
theory
PolicyCore
imports NetworkCore
"$AFP/UPF/UPF"
imports NetworkCore
"$AFP/UPF/UPF"
begin

66
PacketFilter/PortCombinators.thy
View File

@ -36,8 +36,10 @@
*****************************************************************************)
subsection {* Policy Combinators with Ports *}
theory PortCombinators
imports PolicyCombinators
theory
PortCombinators
imports
PolicyCombinators
begin
text{*
@ -54,38 +56,34 @@ text{*
definition
allow_all_from_port :: "'\<alpha>::adr net \<Rightarrow> ('\<gamma>::port) \<Rightarrow> (('\<alpha>,'\<beta>) packet \<mapsto> unit)" where
"allow_all_from_port src_net s_port =
{pa. src_port pa = s_port} \<triangleleft> allow_all_from src_net"
"allow_all_from_port src_net s_port = {pa. src_port pa = s_port} \<triangleleft> allow_all_from src_net"
definition
deny_all_from_port :: "'\<alpha>::adr net \<Rightarrow> '\<gamma>::port \<Rightarrow> (('\<alpha>,'\<beta>) packet \<mapsto> unit)" where
"deny_all_from_port src_net s_port =
{pa. src_port pa = s_port} \<triangleleft> deny_all_from src_net "
"deny_all_from_port src_net s_port = {pa. src_port pa = s_port} \<triangleleft> deny_all_from src_net "
definition
allow_all_to_port :: "'\<alpha>::adr net \<Rightarrow> '\<gamma>::port \<Rightarrow> (('\<alpha>,'\<beta>) packet \<mapsto> unit)" where
"allow_all_to_port dest_net d_port =
{pa. dest_port pa = d_port} \<triangleleft> allow_all_to dest_net"
"allow_all_to_port dest_net d_port = {pa. dest_port pa = d_port} \<triangleleft> allow_all_to dest_net"
definition
deny_all_to_port :: "'\<alpha>::adr net \<Rightarrow> '\<gamma>::port \<Rightarrow> (('\<alpha>,'\<beta>) packet \<mapsto> unit)" where
"deny_all_to_port dest_net d_port =
{pa. dest_port pa = d_port} \<triangleleft> deny_all_to dest_net"
"deny_all_to_port dest_net d_port = {pa. dest_port pa = d_port} \<triangleleft> deny_all_to dest_net"
definition
allow_all_from_port_to:: "'\<alpha>::adr net \<Rightarrow> '\<gamma>::port \<Rightarrow> '\<alpha>::adr net \<Rightarrow> (('\<alpha>,'\<beta>) packet \<mapsto> unit)"
where
"allow_all_from_port_to src_net s_port dest_net
allow_all_from_port_to:: "'\<alpha>::adr net \<Rightarrow> '\<gamma>::port \<Rightarrow> '\<alpha>::adr net \<Rightarrow> (('\<alpha>,'\<beta>) packet \<mapsto> unit)"
where
"allow_all_from_port_to src_net s_port dest_net
= {pa. src_port pa = s_port} \<triangleleft> allow_all_from_to src_net dest_net"
definition
deny_all_from_port_to::"'\<alpha>::adr net \<Rightarrow> '\<gamma>::port \<Rightarrow> '\<alpha>::adr net \<Rightarrow> (('\<alpha>,'\<beta>) packet \<mapsto> unit)"
deny_all_from_port_to::"'\<alpha>::adr net \<Rightarrow> '\<gamma>::port \<Rightarrow> '\<alpha>::adr net \<Rightarrow> (('\<alpha>,'\<beta>) packet \<mapsto> unit)"
where
"deny_all_from_port_to src_net s_port dest_net
"deny_all_from_port_to src_net s_port dest_net
= {pa. src_port pa = s_port} \<triangleleft> deny_all_from_to src_net dest_net "
definition
allow_all_from_port_to_port::"'\<alpha>::adr net \<Rightarrow> '\<gamma>::port \<Rightarrow> '\<alpha>::adr net \<Rightarrow> '\<gamma>::port \<Rightarrow>
allow_all_from_port_to_port::"'\<alpha>::adr net \<Rightarrow> '\<gamma>::port \<Rightarrow> '\<alpha>::adr net \<Rightarrow> '\<gamma>::port \<Rightarrow>
(('\<alpha>,'\<beta>) packet \<mapsto> unit)" where
"allow_all_from_port_to_port src_net s_port dest_net d_port =
{pa. dest_port pa = d_port} \<triangleleft> allow_all_from_port_to src_net s_port dest_net"
@ -105,30 +103,31 @@ definition
definition
deny_all_from_to_port :: "'\<alpha>::adr net \<Rightarrow> '\<alpha>::adr net \<Rightarrow> '\<gamma>::port \<Rightarrow>
(('\<alpha>,'\<beta>) packet \<mapsto> unit)" where
"deny_all_from_to_port src_net dest_net d_port = {pa. dest_port pa = d_port} \<triangleleft> deny_all_from_to src_net dest_net"
"deny_all_from_to_port src_net dest_net d_port =
{pa. dest_port pa = d_port} \<triangleleft> deny_all_from_to src_net dest_net"
definition
allow_from_port_to :: "'\<gamma>::port \<Rightarrow> '\<alpha>::adr net \<Rightarrow> '\<alpha>::adr net \<Rightarrow> (('\<alpha>,'\<beta>) packet \<mapsto> unit)"
where
"allow_from_port_to port src_net dest_net =
where
"allow_from_port_to port src_net dest_net =
{pa. src_port pa = port} \<triangleleft> allow_all_from_to src_net dest_net"
definition
deny_from_port_to :: "'\<gamma>::port \<Rightarrow> '\<alpha>::adr net \<Rightarrow> '\<alpha>::adr net \<Rightarrow> (('\<alpha>,'\<beta>) packet \<mapsto> unit)"
where
"deny_from_port_to port src_net dest_net =
where
"deny_from_port_to port src_net dest_net =
{pa. src_port pa = port} \<triangleleft> deny_all_from_to src_net dest_net"
definition
allow_from_to_port :: "'\<gamma>::port \<Rightarrow> '\<alpha>::adr net \<Rightarrow> '\<alpha>::adr net \<Rightarrow> (('\<alpha>,'\<beta>) packet \<mapsto> unit)"
where
"allow_from_to_port port src_net dest_net =
where
"allow_from_to_port port src_net dest_net =
{pa. dest_port pa = port} \<triangleleft> allow_all_from_to src_net dest_net"
definition
deny_from_to_port :: "'\<gamma>::port \<Rightarrow> '\<alpha>::adr net \<Rightarrow> '\<alpha>::adr net \<Rightarrow> (('\<alpha>,'\<beta>) packet \<mapsto> unit)"
where
"deny_from_to_port port src_net dest_net =
where
"deny_from_to_port port src_net dest_net =
{pa. dest_port pa = port} \<triangleleft> deny_all_from_to src_net dest_net"
definition
@ -137,7 +136,6 @@ definition
"allow_from_ports_to ports src_net dest_net =
{pa. src_port pa \<in> ports} \<triangleleft> allow_all_from_to src_net dest_net"
definition
allow_from_to_ports :: "'\<gamma>::port set \<Rightarrow> '\<alpha>::adr net \<Rightarrow> '\<alpha>::adr net \<Rightarrow>
(('\<alpha>,'\<beta>) packet \<mapsto> unit)" where
@ -150,17 +148,16 @@ definition
"deny_from_ports_to ports src_net dest_net =
{pa. src_port pa \<in> ports} \<triangleleft> deny_all_from_to src_net dest_net"
definition
deny_from_to_ports :: "'\<gamma>::port set \<Rightarrow> '\<alpha>::adr net \<Rightarrow> '\<alpha>::adr net \<Rightarrow>
(('\<alpha>,'\<beta>) packet \<mapsto> unit)" where
"deny_from_to_ports ports src_net dest_net =
{pa. dest_port pa \<in> ports} \<triangleleft> deny_all_from_to src_net dest_net"
definition
allow_all_from_port_tos:: "'\<alpha>::adr net \<Rightarrow> ('\<gamma>::port) set \<Rightarrow> '\<alpha>::adr net \<Rightarrow> (('\<alpha>,'\<beta>) packet \<mapsto> unit)"
where
"allow_all_from_port_tos src_net s_port dest_net
allow_all_from_port_tos:: "'\<alpha>::adr net \<Rightarrow> ('\<gamma>::port) set \<Rightarrow> '\<alpha>::adr net \<Rightarrow> (('\<alpha>,'\<beta>) packet \<mapsto> unit)"
where
"allow_all_from_port_tos src_net s_port dest_net
= {pa. dest_port pa \<in> s_port} \<triangleleft> allow_all_from_to src_net dest_net"
text{*
@ -177,7 +174,6 @@ lemmas PortCombinatorsCore =
allow_from_port_to_def allow_from_to_port_def deny_from_to_port_def
deny_from_port_to_def allow_all_from_port_tos_def
lemmas PortCombinators =
PortCombinatorsCore PolicyCombinators
lemmas PortCombinators = PortCombinatorsCore PolicyCombinators
end
end

17
PacketFilter/Ports.thy
View File

@ -37,7 +37,8 @@
subsection {* Ports *}
theory Ports
imports Main
imports
Main
begin
text{*
@ -48,28 +49,26 @@ text{*
definition http::int where "http = 80"
lemma http1: "x \<noteq> 80 \<Longrightarrow> x \<noteq> http"
by (simp add: http_def)
by (simp add: http_def)
lemma http2: "x \<noteq> 80 \<Longrightarrow> http \<noteq> x"
by (simp add: http_def)
by (simp add: http_def)
definition smtp::int where "smtp = 25"
lemma smtp1: "x \<noteq> 25 \<Longrightarrow> x \<noteq> smtp"
by (simp add: smtp_def)
by (simp add: smtp_def)
lemma smtp2: "x \<noteq> 25 \<Longrightarrow> smtp \<noteq> x"
by (simp add: smtp_def)
by (simp add: smtp_def)
definition ftp::int where "ftp = 21"
lemma ftp1: "x \<noteq> 21 \<Longrightarrow> x \<noteq> ftp"
by (simp add: ftp_def)
by (simp add: ftp_def)
lemma ftp2: "x \<noteq> 21 \<Longrightarrow> ftp \<noteq> x"
by (simp add: ftp_def)
by (simp add: ftp_def)
text{* And so on for all desired port numbers. *}

46
PacketFilter/ProtocolPortCombinators.thy
View File

@ -37,8 +37,10 @@
subsection {* Policy Combinators with Ports and Protocols *}
theory ProtocolPortCombinators
imports PortCombinators
theory
ProtocolPortCombinators
imports
PortCombinators
begin
text{*
@ -74,19 +76,19 @@ definition
{pa. dest_protocol pa = p} \<triangleleft> deny_all_to_port dest_net d_port"
definition
allow_all_from_port_to_prot:: "protocol =>'\<alpha>::adr net \<Rightarrow> '\<gamma>::port \<Rightarrow> '\<alpha>::adr net \<Rightarrow> (('\<alpha>,'\<beta>) packet \<mapsto> unit)"
where
"allow_all_from_port_to_prot p src_net s_port dest_net =
allow_all_from_port_to_prot:: "protocol =>'\<alpha>::adr net \<Rightarrow> '\<gamma>::port \<Rightarrow> '\<alpha>::adr net \<Rightarrow> (('\<alpha>,'\<beta>) packet \<mapsto> unit)"
where
"allow_all_from_port_to_prot p src_net s_port dest_net =
{pa. dest_protocol pa = p} \<triangleleft> allow_all_from_port_to src_net s_port dest_net"
definition
deny_all_from_port_to_prot::"protocol \<Rightarrow> '\<alpha>::adr net \<Rightarrow> '\<gamma>::port \<Rightarrow> '\<alpha>::adr net \<Rightarrow> (('\<alpha>,'\<beta>) packet \<mapsto> unit)"
deny_all_from_port_to_prot::"protocol \<Rightarrow> '\<alpha>::adr net \<Rightarrow> '\<gamma>::port \<Rightarrow> '\<alpha>::adr net \<Rightarrow> (('\<alpha>,'\<beta>) packet \<mapsto> unit)"
where
"deny_all_from_port_to_prot p src_net s_port dest_net =
"deny_all_from_port_to_prot p src_net s_port dest_net =
{pa. dest_protocol pa = p} \<triangleleft> deny_all_from_port_to src_net s_port dest_net"
definition
allow_all_from_port_to_port_prot::"protocol \<Rightarrow> '\<alpha>::adr net \<Rightarrow> '\<gamma>::port \<Rightarrow> '\<alpha>::adr net \<Rightarrow> '\<gamma>::port \<Rightarrow>
allow_all_from_port_to_port_prot::"protocol \<Rightarrow> '\<alpha>::adr net \<Rightarrow> '\<gamma>::port \<Rightarrow> '\<alpha>::adr net \<Rightarrow> '\<gamma>::port \<Rightarrow>
(('\<alpha>,'\<beta>) packet \<mapsto> unit)" where
"allow_all_from_port_to_port_prot p src_net s_port dest_net d_port =
{pa. dest_protocol pa = p} \<triangleleft> allow_all_from_port_to_port src_net s_port dest_net d_port "
@ -111,26 +113,26 @@ definition
definition
allow_from_port_to_prot :: "protocol =>'\<gamma>::port \<Rightarrow> '\<alpha>::adr net \<Rightarrow> '\<alpha>::adr net \<Rightarrow> (('\<alpha>,'\<beta>) packet \<mapsto> unit)"
where
"allow_from_port_to_prot p port src_net dest_net =
where
"allow_from_port_to_prot p port src_net dest_net =
{pa. dest_protocol pa = p} \<triangleleft> allow_from_port_to port src_net dest_net"
definition
deny_from_port_to_prot :: "protocol =>'\<gamma>::port \<Rightarrow> '\<alpha>::adr net \<Rightarrow> '\<alpha>::adr net \<Rightarrow> (('\<alpha>,'\<beta>) packet \<mapsto> unit)"
where
"deny_from_port_to_prot p port src_net dest_net =
where
"deny_from_port_to_prot p port src_net dest_net =
{pa. dest_protocol pa = p} \<triangleleft> deny_from_port_to port src_net dest_net"
definition
allow_from_to_port_prot :: "protocol =>'\<gamma>::port \<Rightarrow> '\<alpha>::adr net \<Rightarrow> '\<alpha>::adr net \<Rightarrow> (('\<alpha>,'\<beta>) packet \<mapsto> unit)"
where
"allow_from_to_port_prot p port src_net dest_net =
where
"allow_from_to_port_prot p port src_net dest_net =
{pa. dest_protocol pa = p} \<triangleleft> allow_from_to_port port src_net dest_net"
definition
deny_from_to_port_prot :: "protocol =>'\<gamma>::port \<Rightarrow> '\<alpha>::adr net \<Rightarrow> '\<alpha>::adr net \<Rightarrow> (('\<alpha>,'\<beta>) packet \<mapsto> unit)"
where
"deny_from_to_port_prot p port src_net dest_net =
where
"deny_from_to_port_prot p port src_net dest_net =
{pa. dest_protocol pa = p} \<triangleleft> deny_from_to_port port src_net dest_net"
definition
@ -139,7 +141,6 @@ definition
"allow_from_ports_to_prot p ports src_net dest_net =
{pa. dest_protocol pa = p} \<triangleleft> allow_from_ports_to ports src_net dest_net"
definition
allow_from_to_ports_prot :: "protocol =>'\<gamma>::port set \<Rightarrow> '\<alpha>::adr net \<Rightarrow> '\<alpha>::adr net \<Rightarrow>
(('\<alpha>,'\<beta>) packet \<mapsto> unit)" where
@ -152,16 +153,13 @@ definition
"deny_from_ports_to_prot p ports src_net dest_net =
{pa. dest_protocol pa = p} \<triangleleft> deny_from_ports_to ports src_net dest_net"
definition
deny_from_to_ports_prot :: "protocol =>'\<gamma>::port set \<Rightarrow> '\<alpha>::adr net \<Rightarrow> '\<alpha>::adr net \<Rightarrow>
(('\<alpha>,'\<beta>) packet \<mapsto> unit)" where
"deny_from_to_ports_prot p ports src_net dest_net =
{pa. dest_protocol pa = p} \<triangleleft> deny_from_to_ports ports src_net dest_net"
text{* As before, we put all the rules into one lemma
to ease writing later. *}
text{* As before, we put all the rules into one lemma to ease writing later. *}
lemmas ProtocolCombinatorsCore =
allow_all_from_port_prot_def deny_all_from_port_prot_def allow_all_to_port_prot_def
@ -173,8 +171,6 @@ lemmas ProtocolCombinatorsCore =
allow_from_port_to_prot_def allow_from_to_port_prot_def deny_from_to_port_prot_def
deny_from_port_to_prot_def
lemmas ProtocolCombinators = PortCombinators.PortCombinators
ProtocolCombinatorsCore
lemmas ProtocolCombinators = PortCombinators.PortCombinators ProtocolCombinatorsCore
end
end