Theory NetworkCore
subsection‹Packets and Networks›
theory
NetworkCore
imports
Main
begin
text‹
In networks based e.g. on TCP/IP, a message from A to B is encapsulated in \emph{packets}, which
contain the content of the message and routing information. The routing information mainly
contains its source and its destination address.
In the case of stateless packet filters, a firewall bases its decision upon this routing
information and, in the stateful case, on the content. Thus, we model a packet as a four-tuple of
the mentioned elements, together with an id field.
›
text‹The ID is an integer:›
type_synonym id = int
text‹
To enable different representations of addresses (e.g. IPv4 and IPv6, with or without ports),
we model them as an unconstrained type class and directly provide several instances:
›
class adr
type_synonym 'α src = "'α"
type_synonym 'α dest = "'α"
instance int ::adr ..
instance nat ::adr ..
instance "fun" :: (adr,adr) adr ..
instance prod :: (adr,adr) adr ..
text‹
The content is also specified with an unconstrained generic type:
›
type_synonym 'β content = "'β"
text ‹
For applications where the concrete representation of the content field does not matter (usually
the case for stateless packet filters), we provide a default type which can be used in those
cases:
›
datatype DummyContent = data
text‹Finally, a packet is:›
type_synonym ('α,'β) packet = "id × 'α src × 'α dest × 'β content"
text‹
Protocols (e.g. http) are not modelled explicitly. In the case of stateless packet filters, they
are only visible by the destination port of a packet, which are modelled as part of the address.
Additionally, stateful firewalls often determine the protocol by the content of a packet.
›
definition src :: "('α::adr,'β) packet ⇒ 'α"
where "src = fst o snd "
text‹
Port numbers (which are part of an address) are also modelled in a generic way. The integers and
the naturals are typical representations of port numbers.
›
class port
instance int ::port ..
instance nat :: port ..
instance "fun" :: (port,port) port ..
instance "prod" :: (port,port) port ..
text‹
A packet therefore has two parameters, the first being the address, the second the content. For
the sake of simplicity, we do not allow to have a different address representation format for the
source and the destination of a packet.
To access the different parts of a packet directly, we define a couple of projectors:
›
definition id :: "('α::adr,'β) packet ⇒ id"
where "id = fst"
definition dest :: "('α::adr,'β) packet ⇒ 'α dest"
where "dest = fst o snd o snd"
definition content :: "('α::adr,'β) packet ⇒ 'β content"
where "content = snd o snd o snd"
datatype protocol = tcp | udp
lemma either: "⟦a ≠ tcp;a ≠ udp⟧ ⟹ False"
by (case_tac "a",simp_all)
lemma either2[simp]: "(a ≠ tcp) = (a = udp)"
by (case_tac "a",simp_all)
lemma either3[simp]: "(a ≠ udp) = (a = tcp)"
by (case_tac "a",simp_all)
text‹
The following two constants give the source and destination port number of a packet. Address
representations using port numbers need to provide a definition for these types.
›
consts src_port :: "('α::adr,'β) packet ⇒ 'γ::port"
consts dest_port :: "('α::adr,'β) packet ⇒ 'γ::port"
consts src_protocol :: "('α::adr,'β) packet ⇒ protocol"
consts dest_protocol :: "('α::adr,'β) packet ⇒ protocol"
text‹A subnetwork (or simply a network) is a set of sets of addresses.›
type_synonym 'α net = "'α set set"
text‹The relation {in\_subnet} (‹⊏›) checks if an address is in a specific network.›
definition
in_subnet :: "'α::adr ⇒ 'α net ⇒ bool" (infixl ‹⊏› 100) where
"in_subnet a S = (∃ s ∈ S. a ∈ s)"
text‹The following lemmas will be useful later.›
lemma in_subnet:
"(a, e) ⊏ {{(x1,y). P x1 y}} = P a e"
by (simp add: in_subnet_def)
lemma src_in_subnet:
"src(q,(a,e),r,t) ⊏ {{(x1,y). P x1 y}} = P a e"
by (simp add: in_subnet_def in_subnet src_def)
lemma dest_in_subnet:
"dest (q,r,((a),e),t) ⊏ {{(x1,y). P x1 y}} = P a e"
by (simp add: in_subnet_def in_subnet dest_def)
text‹
Address models should provide a definition for the following constant, returning a network
consisting of the input address only.
›
consts subnet_of :: "'α::adr ⇒ 'α net"
lemmas packet_defs = in_subnet_def id_def content_def src_def dest_def
end