Commit 2bde7bca authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean

More updates. 0.29 scale

parent 0e7220a6
......@@ -11,7 +11,7 @@ We have adapted the setting off timing parameters to each implementation.
\begin{figure*}
\centering
\includegraphics[scale=0.27]{ssh-server_cropped}
\includegraphics[scale=0.29]{ssh-server_cropped}
\caption{Model of the OpenSSH server. {\normalfont States are collected in 3 clusters,
indicated by the rectangles, where each cluster corresponds to
one of the protocol layers.
......
......@@ -253,7 +253,8 @@ X ( (out!=SR_ACCEPT & out!=KEXINIT) W receivedNewKeys) )
\label{prop:trans-kexinit}
\end{property}
The RFC also states \cite[p. 24]{rfc4254} that if the server rejects the service request, ``it SHOULD send an appropriate SSH\_MSG\_DISCONNECT message and MUST disconnect''. Moreover, in case it supports the service request, it MUST send a \textsc{sr\_accept} message. Unfortunately, it is not evident from the specification if rejection and support are the only allowed outcomes. We assume that is the case, and formalize an LTL formula accordingly by Property~\ref{prop:trans-sr}. For any service request (\textsc{sr\_auth} or \textsc{sr\_conn}, in case we are not in the initial state, the response will be either an accept (\textsc{sr\_accept}), disconnect (\textsc{disconnect}) which loses the connection in the next step, or \textsc{no\_conn}, the output generated by the {\dmapper} after the connection is lost. We adjusted the property for the initial state since all implementations responded with \textsc{kexinit} which would easily break the property. We cannot yet explain this behavior.
%also to check for sr_conn
The RFC also states \cite[p. 24]{rfc4254} that if the server rejects the service request, ``it SHOULD send an appropriate SSH\_MSG\_DISCONNECT message and MUST disconnect''. Moreover, in case it supports the service request, it MUST send a \textsc{sr\_accept} message. Unfortunately, it is not evident from the specification if rejection and support are the only allowed outcomes. We assume that is the case, and formalize an LTL formula accordingly by Property~\ref{prop:trans-sr}. For a service request (\textsc{sr\_auth}), in case we are not in the initial state, the response will be either an accept (\textsc{sr\_accept}), disconnect (\textsc{disconnect}), or \textsc{no\_conn}, output generated by the {\dmapper} after the connection is lost. We adjusted the property for the initial state since all implementations responded with \textsc{kexinit} which would easily break the property. We cannot yet explain this behavior.
% , with the adjustment that we also allow the mapper induced output \textsc{no\_conn}, which suggests that connection was lost. Additionally, we exclude the initial state from the implication, as it is the only state where a \textsc{kexinit} is generated as a response, which seems to be the default behavior for all implementations.
\begin{property}
......@@ -274,8 +275,8 @@ The RFC for the Authentication layer states in~\cite[p. 6]{rfc4252} that if the
\begin{property}
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (hasReqAuth & !O out=UA_SUCCESS) ->
(invalidAuthReq -> (out=UA_FAILURE) )
W (out=UA_SUCCESS | endCondition ) )
(invalidAuthReq -> out=UA_FAILURE)
W (out=UA_SUCCESS | endCondition) )
\end{lstlisting}
%\caption{Invalid requests prompt UA\_FAILURE }
\label{prop:auth-pre-ua}
......@@ -301,7 +302,7 @@ In the same paragraph, it is stated that authentication requests received after
\end{property}
%\textit{Perhaps this could also be merged into one property?}
The Connection layer RFC states in \cite[p. 9]{rfc4254} that upon receiving a \textsc{ch\_close} message, a side MUST send back a \textsc{ch\_close} message, unless it had already sent this message for the channel. The channel must have been opened beforehand (\dopchan) and the property only has to hold up to when the end condition holds or the channel was closed(\textsc{ch\_close}). Along these lines we formulate Property~\ref{prop:conn-close}.
The Connection layer RFC states in \cite[p. 9]{rfc4254} that on receiving a \textsc{ch\_close} message, a side MUST send back a \textsc{ch\_close}, unless it had already sent this message for the channel. The channel must have been opened beforehand (\dopchan) and the property only has to hold until the end condition holds or the channel was closed(\textsc{ch\_close}). Along these lines we formulate Property~\ref{prop:conn-close}.
\begin{property}
\begin{lstlisting}[basicstyle=\footnotesize]
......@@ -326,7 +327,7 @@ G ( hasOpenedChannel ->
\subsection{Model checking results}
Table~\ref{tab:mcresults} presents model checking results. Crucially, the security properties hold for all three implementations. For BitVise,
because it buffered all responses during rekey (including \textsc{UA\_SUCCESS}) we had to adapt our properties slightly.
as it buffered all responses during rekey (including \textsc{UA\_SUCCESS}) we had to adapt our properties slightly.
In particular, we used {\dvauth} instead of $out=UA\_SUCCESS$ to suggest successful authentication.
%\begin{center}\small
......@@ -362,7 +363,7 @@ Property~\ref{prop:auth-post-ua}. Whether the alternative behavior adapted is ac
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
problematically, it violates properties of the higher layers. Upon receiving \textsc{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
~\ref{prop:auth-post-ua}.
......
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