dekker.one
An Uppaal analysis of the connection setup of the TCP protocol.
Added Abstract
+5
-7
+5
-7
Report/GDN.tex
+5
-7
Report/GDN.tex
···
45
45
\large
46
46
\textsc{Jip J. Dekker} \\[2mm]
47
47
\normalsize Radboud University Nijmegen \\
48
-
\normalsize 4122100
48
+
\normalsize s4122100
49
49
\vspace{-5mm}
50
50
\and
51
51
\large
52
52
\textsc{Ben Br\"ucker} \\[2mm]
53
53
\normalsize Radboud University Nijmegen \\
54
-
\normalsize 0413291
54
+
\normalsize s0413291
55
55
\vspace{-5mm}
56
56
}
57
57
\date{}
···
64
64
65
65
\twocolumn[\begin{@twocolumnfalse}
66
66
\maketitle
67
-
\begin{abstract}
68
-
\noindent Abstract Abstract Abstract Abstract Abstract Abstract Abstract Abstract Abstract Abstract Abstract Abstract Abstract Abstract Abstract Abstract Abstract Abstract Abstract Abstract Abstract Abstract Abstract Abstract Abstract Abstract Abstract Abstract
69
-
\end{abstract}
67
+
\begin{abstract}
68
+
\noindent In this report we will discuss our model in Uppaal of the 3-way handshake as used in the TCP protocol. We will give an overview of the handshake itself and provide meaningful observation about specific aspects of this protocol. Furthermore we will discuss the specifics of our model and comment on some of the decisions we made designing the model. In conclusion we will submit our model to verification and model checking using the Uppaal query language, proving basic basic functionality and guaranteeing connection setup.
69
+
\end{abstract}
70
70
\end{@twocolumnfalse}]
71
71
72
72
\thispagestyle{fancy}
73
-
74
-
\lettrine[nindent=0em,lines=3]{I} ntroduction Introduction Introduction Introduction Introduction Introduction Introduction Introduction Introduction Introduction Introduction Introduction Introduction Introduction Introduction Introduction Introduction .
75
73
76
74
\section{Modeling the TCP handshake}
77
75
We will now discuss how we modeled the TCP handshake, defined in Rfc793 ``Transmission Control Protocol'', as an Uppaal model. We will start by giving a short overview this TCP handshake. For more information please check Rfc793.