Commit fb7b522f authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean

10 is the magic number

parent 99cccefb
......@@ -32,20 +32,24 @@ This function updates the output and state variables for a given valuation of th
%\lstset{showspaces=true}
\begin{figure}[h]
\centering
%\begin{subfigure}
\begin{tikzpicture}[scale=0.1,>=stealth',shorten >=1pt,auto,node distance=2.5cm]
\node[initial,state] (q0) {$q_0$};
\node[state] (q1) [right of=q0] {$q_1$};
\path[->] (q0) edge node {BEGIN/OK} (q1);
\path[->] (q0) edge [loop above] node {MSG/NOK} (q0);
\path[->] (q1) edge [loop above] node {BEGIN/OK} (q1);
\path[->] (q1) edge [loop right] node {MSG/ACK} (q1);
\end{tikzpicture}
%\end{subfigure}
\\
\begin{figure}[htbp]
\begin{tabular}{p{0.17\textwidth}p{0.17\textwidth}}
\begin{minipage}{.17\textwidth}
\centering
\begin{tikzpicture}[scale=0.1,>=stealth',shorten >=1pt,auto,node distance=2.5cm]
\footnotesize
\node[initial,state] (q0) {$q_0$};
\node[state] (q1) [below of=q0] {$q_1$};
\path[->] (q0) edge node {BEGIN/OK} (q1);
\path[->] (q0) edge [loop above] node {MSG/NOK} (q0);
\path[->] (q1) edge [loop right] node {BEGIN/OK} (q1);
\path[->] (q1) edge [loop below] node {MSG/ACK} (q1);
\end{tikzpicture}
\end{minipage}
&
\begin{minipage}{.17\textwidth}
\tiny
\begin{lstlisting}
MODULE main
......@@ -67,12 +71,12 @@ This function updates the output and state variables for a given valuation of th
state = q1 & inp = MSG: ACK;
esac;
\end{lstlisting}
\caption{Mealy machine + associated NuSMV code}
\label{fig:nusmvex}
\end{minipage}
\end{tabular}
\caption{Mealy machine + associated NuSMV code}
\label{fig:nusmvex}
\end{figure}
The remainder of this section defines the properties we formalized and verified. We group these properties into four categories:
\begin{enumerate}
......@@ -242,8 +246,7 @@ The RFC states in~\cite[p. 24]{rfc4254} that after sending a \textsc{kexinit} me
\begin{property}
\begin{lstlisting}[basicstyle=\footnotesize]
G ( out=KEXINIT ->
X ( (out!=SR_ACCEPT & out!=KEXINIT)
W receivedNewKeys ) )
X ( (out!=SR_ACCEPT & out!=KEXINIT) W receivedNewKeys) )
\end{lstlisting}
%\caption{Disallowed outputs after KEXINIT}
%\captionsetup{font=small}
......@@ -333,7 +336,7 @@ In particular, we used {\dvauth} instead of $out=UA\_SUCCESS$ to suggest success
\small
\begin{tabular}{| l | l | c | c |c | c |}
\hline
& & & \multicolumn{3}{c|}{\emph{SSH Implementation}}\\ \cline{4-6}
% & & & \multicolumn{3}{c|}{\emph{SSH Implementation}}\\ \cline{4-6}
& Property & Key word &\tiny{OpenSSH} & \tiny{Bitvise} & \tiny{DropBear} \\ \hline
Security & Trans. & & \dt & \dt & \dt \\ \cline{3-6}
& Auth. & & \dt & \dt & \dt \\ \hline
......@@ -361,6 +364,6 @@ does leave room for interpretation of the \textsc{unimpl} message.
DropBear is the only implementation that allows rekey in both general states of the protocol. DropBear also satisfies all transport layer specifications, however,
problematically, it violates properties of the higher layers. Upon receiving \text{ch\_close}, it responds by \textsc{ch\_eof} instead of \text{ch\_close}, not respecting
Property~\ref{prop:conn-close}. Moreover, the output \textsc{ua\_success} can be generated multiple times, violating both Properties ~\ref{prop:auth-post-ua-strong} and
(implicitly) ~\ref{prop:auth-post-ua}.
~\ref{prop:auth-post-ua}.
%, though key exchange is strangely not universally permitted, while some of the functional properties described are not met.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment