Commit 1908d9ef authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean

Updated definitions

parent 51fc5a5b
......@@ -54,7 +54,7 @@ In the case of the pre-authenticated state, we know we have reached this state
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (input= SERVICE_REQUEST & output= SERVICE_ACCEPT) ->
( ( input = NEWKEYS & output = NO_RESP & X ( input = UA_PK_OK ) ) ->
X ( output=UA_SUCCESS) ) WU (input = DISCONNECT | output= DISCONNECT | output= UA_SUCCESS)
X ( output=UA_SUCCESS) ) W (input = DISCONNECT | output= DISCONNECT | output= UA_SUCCESS)
\end{lstlisting}
\caption{Key exchange preserves pre-authenticated state}
\label{prop:prop3}
......@@ -70,21 +70,53 @@ The RFC states in~\ref[p. 24]{rfc4254} that after sending a \textsc{kexinit} mes
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (output = KEXINIT) ->
X (output != SERVICE_ACCEPT & output != KEXINIT)
WU X (output = NEWKEYS | output = KEX31_NEWKEYS ) )
W X (output = NEWKEYS | output = KEX31_NEWKEYS ) )
\end{lstlisting}
\caption{Allowed outputs after KEXINIT}
\label{prop:prop4}
\end{property}
On the same page, it is stated 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 \textsl{service\_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, with the adjustment that we also allow the output \textsl{no\_conn}, suggesting there is no connection. Of course, if there is no connection, the server cannot possibly reply.
On the same page, it is stated 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 \textsl{service\_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, with the adjustment that we also allow the output \textsl{no\_conn}, suggesting there is no connection. Of course, if there is no connection, the server cannot possibly reply.
The RFC for the Authentication Layer states in~\ref[p. 6]{rfc2452} that if the server rejects the authentication request, it MUST respond with a \textsl{ua\_failure} message. Conversely, if the requests succeeds, an \textsl{ua\_success} MUST be sent only once. Further authentication requests received thereafter SHOULD be ignored. While not explicitly stated, we assume this to be in a context where the authentication service had been requested. Indeed, before this state, implementations replied with \textsl{unimplemented}. We define two properties, Property~\ref{prop:prop6} for behavior before an \textsl{ua\_success}, Property~\ref{prop7} for behavior afterward, until the connection is lost (suggested by the \textsl{no\_conn}).
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( X (output = UA_SUCCESS) ->
((output!=UA_SUCCESS & (input=UA_PK_NOK -> output=UA_FAILURE))
S (input=SERVICE_REQUEST_AUTH & output=SERVICE_ACCEPT) ) )
\end{lstlisting}
\caption{Implementation should send UA\_SUCCESS at most once}
\label{prop:prop6}
\end{property}
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G (output = UA_SUCCESS ->
X ( (input=UA_PK_OK | input=UA_PK_NOK) -> output=NO_RESP )
W X X(output= NO_CONN) )
\end{lstlisting}
\caption{After UA\_SUCCESS, silently ignore auth. requests}
\label{prop:prop7}
\end{property}
The Connection Layer RFC states that upon receiving a \textsl{ch\_close} message, a side should send back a \textsl{ch\_close} message, unless it has already sent this message for the channel. The channel must have been opened beforehand. Also, this condition no longer applies once the connection is lost (\textsl{no\_conn}), once a re-key procedure was initiated (by input \textsl{kexinit}) or once the channel was closed. Along those lines we formalize this with Property~\ref{prop:prop8}.
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (input= CH_OPEN & output= CH_OPEN_SUCCESS) ->
( ( input= CH_CLOSE -> output= CH_CLOSE)
W (output = NO_CONN | input = KEXINIT | output= CH_CLOSE) ) )
\end{lstlisting}
\caption{CH\_CLOSE request is followed by CH\_CLOSE response}
\label{prop:prop8}
\end{property}
The RFC for the Authentication Layer states that if the server rejects the authentication request, it MUST respond with a \textsl{ua\_failure} message. Conversely, if the requests succeeds, an \textsl{ua\_success} MUST be sent only once. Further authentication requests received thereafter SHOULD be ignored. While not explicitly stated, we assume this to be in a context where the authentication service had been requested. Indeed, outside of this state, implementations replied with \textsl{unimplemented}.
A problem was that the specification for each layer seemed to only consider messages specific to that layer. In particular, it didn't consider disconnect messages, that may be sent at any point in the protocol. For the Transport Layer, the RFC states that after sending a \textsl{kexinit} message, a party MUST not send \textsl{service\_request} or \textsl{service\_accept} messages, until it has sent a \textsl{newkeys} message. This is translated to the LTL.
%A problem was that the specification for each layer seemed to only consider messages specific to that layer. In particular, it didn't consider disconnect messages, that may be sent at any point in the protocol. For the Transport Layer, the RFC states that after sending a \textsl{kexinit} message, a party MUST not send \textsl{service\_request} or \textsl{service\_accept} messages, until it has sent a \textsl{newkeys} message. This is translated to the LTL.
On the same page, the RFC also states that in case the server rejects a service request, it should send an appropriate \textsl{disconnect} message. Moreover, in case it supports the service request, it MUST sent a \textsl{service\_accept} message. If
%On the same page, the RFC also states that in case the server rejects a service request, it should send an appropriate \textsl{disconnect} message. Moreover, in case it supports the service request, it MUST sent a \textsl{service\_accept} message. If
%The Connection Layer RFC states that upon receiving a CH_CLOSE message, a side should send back a CH\_CLOSE message, unless it has already sent this message for the channel. This of course, ignores the case when a side disconnects, in which case a CH_CLOSE would no longer have to be issued.
\subsection{Model checking results}
Table presents the model checking results. Crucially, all general security properties are met, though key exchange is strangely not universally permitted, while some of the functional properties described are not met.
Table presents the model checking results. Crucially, all the general security properties are met%, 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