\section{Model}
\subsection{Basic Functions}
The netwok model relies on three types of entities (at present, as we model more complex functionality we might get to
other things):

\begin{itemize}
\item $node$: These are network elements including endhosts, switches (when modelled), middleboxes, etc. In the rest of
the document identifiers $e, e_1, e_2, \ldots$ are assumed to be $node$s.
\item $address$: Addresses assigned to nodes. In the rest of the document identifiers $a, b, a_1, a_2\ldots$ are assumed
to be $address$es
\item $packet$: Packets. We currently model them as tuples with the following fields:
\begin{itemize}
\item $src$: $src\in address$.
\item $dest$: $dest\in address$.
\item $origin$: $origin\in node$. This is a pseudofield in the packet tracking its true origin (which is important for
answering questions about isolation).
\item $body$: $body\in \mathbb{N}$. Payload 
\item $seq$: $seq\in \mathbb{N}$. Sequence number.
\item $options$: IP Options: represented as integer.
\item $src_port$: Source port
\item $dest_port$: Destination port
\end{itemize}
For the rest of the document identifiers $p, p_1,\ldots$ represent packets.
\item $etype = \left\{R, S\right\}$ The event type, this is used to record times at which packets are received and sent. $R$ represents
the event of a node receiving a packet, while $S$ represents a node sending a packet. Event type variables are represented as $E$ below.
\item $time \subset \mathbb{N}$: Time/ordering information for an event, represented by the variable $\tau$.
\item Events: Events are represented by the tuple $\left( e, p, E \right)$ and represent the act of packet $p$ either being received at or
sent from node $e$.
\end{itemize}

We also create a few basic functions to model relationships between these types and also network functionality. These
are:
\begin{itemize}
\item $hostHasAddr: e, a \rightarrow boolean$: True if $node$ $e$ is assigned address $a$.
\item $addrToHost: a \rightarrow e$: Returns $node$ $e$ associated with address $a$. (Note this implies that the address
to node mapping is onto).
\item $send: e_1, e_2, p \rightarrow boolean$ True if $e_1$ sent $e_2$ packet $p$.
\item $recv: e_1, e_2, p \rightarrow boolean$ True if $e_2$ received packet $p$ from $e_1$.
\item $etime: e, p, E \rightarrow \tau$ The time at which event $\left( e, p, E \right)$ occurs.
\item $failed: e, \tau \rightarrow boolean$ True if $e$ is failed at time $\tau$
\end{itemize}

Given these functions and types we layer them on to produce the test network. We go bottom up starting with the network:

\subsection{Network Layer}
\subsubsection{Basic Conditions}
These are basic conditions we assume for the entire network:
\begin{itemize}
\item $\forall e_1, e_2, p:\ recv(e_1, e_2, p) \iff send(e_1, e_2, p)$: No packet loss
\item Don't consider loopback packets, we have really no control over them.
\begin{align*}
\forall e_1, e_2, p:& send(e_1, e_2, p) \Rightarrow e_1 \neq e_2\\
\forall e_1, e_2, p:& recv(e_1, e_2. p) \Rightarrow e_1 \neq e_2\\
\forall e_1, e_2, p:& send(e_1, e_2, p) \Rightarrow p.src \neq p.dest\\
\end{align*}
\item And a set of rules for time:
\begin{itemize}
\item Record the event that a packet is received and make sure packets are not received before being sent:
\begin{align*}
    \forall e_1, e_2, p:& recv(e_1, e_2, p)\Rightarrow etime(e_2, p, R) > 0 \land etime(e_2, p, R) > etime(e_1, p, S)
\end{align*}
\item Record the event that packet is sent. Make sure packets are received after being sent (yes this is redundant given above)
\begin{align*}
    \forall e_1, e_2, p:& send(e_1, e_2, p)\Rightarrow etime(e_1, p, S) > 0 \land etime(e_2, p, R) > etime(e_1, p, S)
\end{align*}
\item Make sure there are no other causes of receive events
\begin{align*}
    \forall e_1, p:& \neg(\exists e_2:\ recv(e_2, e_1, p)) \implies etime(e_1, p, R) = 0
\end{align*}
\item There are similarly no other causes for send events
\begin{align*}
    \forall e_1, p:& \neg(\exists e_2:\ send(e_1, e_2, p)) \implies etime(e_1, p, S) = 0
\end{align*}
\item No sends or receives when failed
\end{itemize}
\end{itemize}

\subsection{End Hosts}
End hosts are just nodes with a couple of extra constraints. For endhost $e$:
\begin{itemize}
\item $\forall e_i, p:\ send(e, e_i, p) \Rightarrow hostHasAddr(e, p.src)$: An end host does not forward packets on anyone
elses behalf. Note that this prevents host spoofing. One could obviously turn this off, but...
\item $\forall e_i, p:\ send(e, e_i, p) \Rightarrow p.origin = e$ Track origin correctly.
\end{itemize}

\subsection{Stateless Firewall}
Stateless firewalls just implement ACLs based on packet source and destination. ACLs are specified as a table $A \subset
address\times address = \left\{(a, b)\right\}$ which specifies the set of addresses that are denied (it is equally easy
to build one based on allowed addresses). Given a firewall $f$ and a table $A$, the firewall model says:

\begin{itemize}
\item The correct sending condition from equation~\ref{eq:sanesend}.
\item $\forall e_1, p:\ send(f, e_1, p) \Rightarrow \exists e_2 recv(e_2, f, p)$: The firewall does not invent packets.
\item $\forall e, p:\ send(f, e, p) \Rightarrow (p.src, p.dest) \not \in A \land (p.dest, p.src) \not \in A$ Sending the packet is not disallowed by an
ACL.
\end{itemize}

\subsection{Stateful Firewall}
Stateful firewally can cache previous decisions. In particular this means we don't need to have ACLs that are symmetric
(one side can punch a hole through the firewall). Cached rules are modeled as a function: $cached: a_1, a_2 \rightarrow
boolean$ which is true when packets with either source $a_1$ and destination $a_2$ or source $a_2$ and destination $a_1$
are allowed through the firewall. We also track the time at which a rule gets cached using a separate function $ctime:
a_1, a_2 \rightarrow \tau$ which models the time at which rules allowing traffic between $a_1$ and $a_2$ get cached.
(This also allows us to potentially model expiration times).

The logical model for a stateful firewall $f$ with ACL table $A$ is:

\begin{itemize}
\item The correct sending condition from equation~\ref{eq:sanesend}.
\item ACL based constraint for caching
    \begin{align*}
        \forall a, x, b, y:\ cached(a, x, b, y) \iff \\
        \ \exists e, p:\ recv(e, f, p)\\
        \ \ \land p.src = a\\
        \ \ \land p.src\_port = x\\
        \ \ \land p.dest = b\\
        \ \ \land p.dest\_port = y\\
        \ \ \land ctime(a, x, b, y) = etime(f, p, R)\\
        \ \ \land \lnot \left(a, b\right) \in A
    \end{align*}
\item Do not invent packets
     \begin{align*}
         \forall e, p:\ send(f, e, p) \implies\\
         \ \exists e_2:\ recv(e_2, f, p)\\
         \ \ \left(\nexists e_3:\ e_3 \neq e \land send(f, e_3, p)\right)\\
         \ \ etime(f, p, R) < etime(f, p, S)
     \end{align*}
\item Actual sends
        \begin{align*}
            \forall e, p:\ send(f, e, p) \implies\\
            \ (cached(p.src, p.src\_port, p.dest, p.dest\_port) \land\\
             \  \     ctime(p.src, p.src\_port, p.dest, p.dest\_port) \leq\\
             \ \ \    etime(f, p, R))
             \ \lor (cached(p.dest, p.dest\_port, p.src, p.src\_port) \land\\
             \  \     ctime(p.dest, p.dest\_port, p.src, p.src\_port) \leq\\
             \ \ \    etime(f, p, R))
        \end{align*}
\end{itemize}

\subsection{Web Proxy}
Web proxies modify packet headers (and were our original source of violations). Given a web proxy $w$ we model it as
follows:
\begin{itemize}
\item $\forall e, p:\ send(w, e, p) \implies hostHasAddr(w, p.src)$ Send all packets so source address belongs to the
proxy, thus allowing caching.
\item $\forall e_1, p_1:\ send(w, e, p) \implies \exists e_2, p_2:\ recv(e_2, w, p_2) \land p_2.origin = p.origin \land
p_2.dest = p.dest \land hostHasAddr(p_2.origin, p_2.src) \land etime(w, p_1, S) \geq etime(w, p_1, R)$ rules for what
packets a webproxy sends. These are actually somewhat incomplete (we are not accounting for responses here). The
reason is that currently I model all endhosts as endhosts instead of as servers and client, which would make this
somewhat more reasonable.
\end{itemize}

\subsection{Compression Box}
First we define a couple of global functions (actually we can define many of them they are just a kind of algorithm)
$compress$ and $uncompress$. Compression box is represented by $c$.

\begin{itemize}
    \item $\forall x, y \in \mathbb{Z}: compress(x) = y \implies uncompress(y) = x$
    \item 
        \begin{align*}
            \forall e_1, p_1:\ send(c, e_1, p_1) \implies\\
            \ \exists e_2, p_2:&\  recv(e_2, c, p_2)\\
                               &\land PacketHeaderEqual(p_1, p_2)\\
                               &\land p_1.body = compress(p_2.body)\\
                               &\land \left(\nexists e_3:\ e_3 \neq e_1 \land send(c, e_3, p_1)\right)\\
                               &\land etime(c, p_1, S) > etime(c, p_2, R)
        \end{align*}
\end{itemize}

