Commit 1bcdb8db authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean

updated

parent 9be6fcdb
......@@ -41,7 +41,7 @@ G ( (in =SERVICE_REQUEST_AUTH & out =SERVICE_ACCEPT) |
\label{prop:prop1}
\end{property}
Apart from a secure connection, the connection layer services also assume that the client behind the connection was authenticated. This is ensured by the Authentication layer by means of an authentication mechanism, which only succeeds, and thus authenticates the client, if valid credentials are provided. For the implementation to be secure, there should be no path from an unauthenticated to an authenticated state without the provision of valid credentials. We consider an authenticated state, a state where a channel can be opened successfully. Provision of valid/invalid credentials is suggested by the outputs \textsl{ua\_success} and \textsl{ua\_failure} respectively. Along these lines, we formulate this specification by Property~\ref{prop:prop2}, where S stands for the Since-operator. This operator holds if its first argument holds up to the moment its second argument holds, with the mention that the second argument also has to hold somewhere along the path.
Apart from a secure connection, the connection layer services also assume that the client behind the connection was authenticated. This is ensured by the Authentication layer by means of an authentication mechanism, which only succeeds, and thus authenticates the client, if valid credentials are provided. For the implementation to be secure, there should be no path from an unauthenticated to an authenticated state without the provision of valid credentials. We consider an authenticated state, a state where a channel can be opened successfully. Provision of valid/invalid credentials is suggested by the outputs \textsl{ua\_success} and \textsl{ua\_failure} respectively. Along these lines, we formulate this specification by Property~\ref{prop:prop2}, where S stands for the Since-operator. This operator holds if its first argument holds up to the moment its second argument holds, with the mention that the second argument has to hold somewhere along the path.
\begin{property}[h]
......@@ -54,21 +54,35 @@ G ( (in= CH_OPEN & out= CH_OPEN_SUCCESS) ->
\end{property}
\subsection{Key re-exchange properties}
Important properties are that re-exchanging keys (or rekey-ing) is allowed in all states of the protocol, and its successful execution doesn't change the protocol state\cite[p. 24]{rfc4254}. We consider 2 general protocol states, pre-authenticated (after a successful authentication request, before authentication) and authenticated. These may map to multiple states in the learned models. For each state, we specify the properties that rekey-ing (1) should always be allowed from that state, and (2) when allowed, should always preserve the state, until the connection is lost. We can tell we are in one of these states from the input/output transition leading up to it. These properties are useful in characterizing the various implementations. In~\cite{Verleg2016} we note great variance on satisfaction of these properties.
Important properties are that re-exchanging keys (or rekey-ing) is allowed in all states of the protocol, and its successful execution doesn't change the protocol state\cite[p. 24]{rfc4254}. We consider 2 general protocol states, pre-authenticated (after a successful authentication request, before authentication) and authenticated. These may map to multiple states in the learned models. For each state, we specify the properties that rekey-ing (1) should always be allowed from that state, and (2) when allowed, should always preserve the state, until connection is lost. We can tell we are in one of these states from the input/output transition leading up to it. These properties are useful in characterizing the various implementations. In~\cite{Verleg2016} we note great variance on satisfaction of these properties.
In the case of the pre-authenticated state, we know we have reached this state following a successful authentication service request. Once here, performing the inputs for rekey in succession should imply success. Provided we perform successful finalization of a rekey, we remain in a pre-authenticated state until we exit this state, either by losing the connection (suggested by the \textsc{no\_conn} ) or via successful authentication (\textsc{ua\_success}). The latter is described in Property~\ref{prop:prop3}. Note that, we can tell we are in a pre-authenticated state if authenticating with a valid public key results in success. W represents the Weak Until operator.
In the case of the pre-authenticated state, we know we have reached this state following a successful authentication service request. Once here, performing the inputs for rekey in succession should imply success. This is shown in Property~\ref{prop:prop25}.
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (in=SERVICE_REQUEST_AUTH & out=SERVICE_ACCEPT) ->
X (in = KEXINIT -> out = KEXINIT &
X ( in = KEX30 -> out= KEX31_NEWKEYS &
X (in = NEWKEYS -> out=NO_RESP ) ) ) )
\end{lstlisting}
\caption{Key exchange possible in pre-auth. state}
\label{prop:prop25}
\end{property}
Provided we perform successful finalization of a rekey, we remain in a pre-authenticated state until we exit this state, either by losing the connection (suggested by the \textsc{no\_conn} ) or via successful authentication (\textsc{ua\_success}). The latter is described in Property~\ref{prop:prop3}. Note that, we can tell we are in a pre-authenticated state if authenticating with a valid public key results in success. W represents the Weak Until operator.
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (in = SERVICE_REQUEST & out = SERVICE_ACCEPT) ->
( ( in = NEWKEYS & out = NO_RESP
& X ( in = UA_PK_OK ) ) -> X ( out =UA_SUCCESS) )
W (out = NO_CONN | out = UA_SUCCESS)
( ( in = NEWKEYS & out = NO_RESP
& X ( in = UA_PK_OK ) ) -> X ( out =UA_SUCCESS) )
W (out = NO_CONN | out = UA_SUCCESS)
\end{lstlisting}
\caption{Key exchange preserves pre-authenticated state}
\caption{Key exchange preserves pre-auth. state}
\label{prop:prop3}
\end{property}
\textit{Perhaps this could be merged into one property?}
\subsection{Basic functional properties}
We have also formalized and checked properties drawn from the RFC specifications. We found parts of the specification vague, which sometimes meant that we had to give our own interpretation before we could formalize. The RFC states in~\cite[p. 24]{rfc4254} that after sending a \textsc{kexinit} message, a party MUST not send another \textsc{kexinit}, or a \textsc{service\_accept} message, until it has sent a \textsc{newkeys} message. This is translated to Property~\ref{prop:prop4}. Note that \textsc{kex31\_newkeys} suggests that the {\dsut} sends a \textsc{kex31}, followed by a \textsc{newkeys}, so it depicts a case where \textsc{newkeys} was sent.
......@@ -85,25 +99,32 @@ G ( (out = 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 \textsc{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 by Property~\ref{prop:prop5} , 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.
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 \textsc{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 by Property~\ref{prop:prop5}. For any service request, in case connection wasn't lost (\textsc{no\_conn}) or we are not in the initial state, the response will either be
an accept(\textsc{service\_accept}) or a disconnect(\textsc{disconnect}) which loses the connection. 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}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (in = SERVICE_REQUEST_AUTH & out != SERVICE_ACCEPT & state != s0)
-> (out = DISCONNECT | out = NO_CONN) ))
G ( (in = SERVICE_REQUEST_AUTH
& out != NO_CONN
& state != s0)
-> (out = SERVICE_ACCEPT | (out = DISCONNECT &
X G (in = SERVICE_REQUEST -> out = NO_CONN) ) ) )
\end{lstlisting}
\caption{Allowed outputs after SERVICE\_ACCEPT}
\label{prop:prop5}
\end{property}
%\textit{Could strengthen this so we check that it disconnects (DISCONNECT) after the first rejected service request}
The RFC for the Authentication Layer states in~\cite[p. 6]{rfc4252} that if the server rejects the authentication request, it MUST respond with a \textsc{ua\_failure} message. Conversely, if the requests succeeds, a \textsc{ua\_success} MUST be sent only once. 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 successfully requested. We define two properties, Property~\ref{prop:prop6} for behavior before an \textsc{ua\_success}, Property~\ref{prop:prop7} for behavior afterward, until the connection is lost.
%Indeed, before reaching this state, implementations replied with \textsc{unimplemented}.
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( X (out = UA_SUCCESS) ->
((out !=UA_SUCCESS & (in =UA_PK_NOK -> out =UA_FAILURE))
S (in =SERVICE_REQUEST_AUTH & out =SERVICE_ACCEPT) ) )
G ( (in=SERVICE_REQUEST_AUTH & out=SERVICE_ACCEPT) ->
X ( (in = UA_PK_NOK -> out = UA_FAILURE) &
(in = UA_PK_OK -> out = UA_SUCCESS) )
W ( out = UA_SUCCESS | output = NO_CONN) )
\end{lstlisting}
\caption{UA\_SUCCESS is sent at most once}
\label{prop:prop6}
......@@ -118,14 +139,16 @@ G (out = UA_SUCCESS ->
\caption{Silently ignore auth. requests after UA\_SUCCESS}
\label{prop:prop7}
\end{property}
\textit{Perhaps this could also be merged into one property?}
The Connection Layer RFC states that upon receiving a \textsc{ch\_close} message, a side should send back a \textsc{ch\_close} message, unless it had 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 (\textsc{no\_conn}), once a re-key procedure was initiated (by input \textsc{kexinit}) or once the channel was closed. Along those lines we formulate Property~\ref{prop:prop8}.
The Connection Layer RFC states that upon receiving a \textsc{ch\_close} message, a side SHOULD send back a \textsc{ch\_close} message, unless it had 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 (\textsc{no\_conn}), once a re-key procedure was initiated (by input \textsc{kexinit}) or once the channel was closed. Along those lines we formulate Property~\ref{prop:prop8}.
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (in = CH_OPEN & out = CH_OPEN_SUCCESS) ->
( ( in = CH_CLOSE -> out = CH_CLOSE)
W (out = NO_CONN | in = KEXINIT | out = CH_CLOSE) ) )
G ( ( (in = CH_OPEN & out = CH_OPEN_SUCCESS) ->
X (in = CH_CLOSE -> out = CH_CLOSE &
X ( (out != CH_CLOSE) W (out = CH_OPEN_SUCCESS) ) )
W (out = NO_CONN | in = KEXINIT | out = CH_CLOSE) )
\end{lstlisting}
\caption{CH\_CLOSE request is followed by CH\_CLOSE response}
\label{prop:prop8}
......@@ -142,9 +165,10 @@ G ( (in = CH_OPEN & out = CH_OPEN_SUCCESS) ->
Table~\ref{tab:mcresults} presents the model checking results. Crucially, all the critical security properties hold.
\begin{center}\small
% \centering
\begin{table}
\begin{tabular}{| r | r | ccc |}
\hline
& & \multicolumn{3}{c}{\emph{SSH Implementation}}\\ \cline{3-5}
& & \multicolumn{3}{c|}{\emph{SSH Implementation}}\\ \cline{3-5}
& Property & OpenSSH & Bitvise & Dropbear \\ \hline
Critical & Trans. & & & \\ \cline{2-5}
& Auth. & & & \\ \hline
......@@ -155,8 +179,9 @@ Table~\ref{tab:mcresults} presents the model checking results. Crucially, all th
& Prop. 7 & & & \\ \cline{2-5}
& Prop. 8 & & & \\ \hline
\end{tabular}
\caption{Model checking results}
\label{tab:mcresults}
\caption{Model checking results}
\end{table}
\end{center}
......
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