Theory VOIP
subsection ‹A simple voice-over-ip model›
theory VOIP
imports StatefulCore
begin
text‹
After the FTP-Protocol which was rather simple we show the strength
of the model with a more current and especially much more
complicated example, namely Voice over IP (VoIP). VoIP is
standardized by the ITU-T under the name H.323, which can be seen as
an "umbrella standard" which aggregates standards for multimedia
conferencing over packet-based networks. H.323 poses many problems
to firewalls. These problems include:
\begin{itemize}
\item An H.323 call is made up of many different simultaneous
connections.
\item Most connections are made to dynamic ports.
\item The addresses and port numbers are exchanged within
the data stream of the next higher connection.
\item Calls can be initiated from outside the firewall.
\end{itemize}
Again we only consider a simplified VoIP scenario with the following
seven messages which are grouped into four subprotocols:
\begin{itemize}
\item Registration and Admission (H.225, port 1719): The caller
contacts its gatekeeper with a call request. The gatekeeper
either rejects or confirms the request, returning the
address of the callee in the latter case.
\begin{itemize}
\item Admission Request (ARQ)
\item Admission Reject (ARJ)
\item Admission Confirm (ACF) ‹'a›
\end{itemize}
\item Call Signaling (Q.931, port 1720) The caller and the callee
agree on the dynamic ports over which the call will take
place.
\begin{itemize}
\item Setup ‹port›
\item Connect ‹port›
\end{itemize}
\item Stream (dynamic ports). The call itself. In reality, several
connections are used here.
\item Fin (port 1720).
\end{itemize}
The two main differences to FTP are:
\begin{itemize}
\item In VoIP, we deal with three different entities: the caller,
the callee, and the gatekeeper.
\item We do not know in advance which entity will close the
connection.
\end{itemize}
We model the protocol as seen from a firewall at the caller, namely
we are not interested in the messages from the callee to its
gatekeeper. Incoming calls are not modelled either, they would
require a different set of state transitions.
›
text‹
The content of a packet now consists of one of the seven messages or
a default one. It is parameterized with the type of the address that
the gatekeeper returns.
›