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

Added all LTL

parent 1908d9ef
......@@ -5,7 +5,9 @@
We use the NuSMV model checker to verify security properties. NuSMV is a model checker where a state of a model is specified as a set of finite variables, and a transition-function which makes changes on these variables. Specifications in temporal logic, such as CTL and LTL, can be checked for truth on specified models. NuSMV provides a counterexample if a certain specification is not true. NuSMV models are generated automatically from the learned models. Generation proceeds by first defining in an empty NuSMV file three variables, corresponding to inputs, outputs and states. The transition-function is then extracted from the learned model and appended to the file. This function updates the output and state variable for given valuations of the input variable. Below we give an example of a Mealy machine and it's associated NuSMV model.
In this section, we define the properties that we formalized and verified with the NuSMV model checker. We group these properties into three categories:
The remainder of this section defines the properties we formalized and verified. We group these properties into three categories:
\begin{enumerate}
......@@ -14,11 +16,13 @@ In this section, we define the properties that we formalized and verified with t
\item \textit{other functional properties}, which are extracted from the SHOULD's and the MUST's of the RFC specifications
\end{enumerate}
A key note is that the properties describe not only the {\dsut}, but the {\dsut} and {\dmapper} assemble. Properties had to be adjusted so they with consideration of the {\dmapper}'s behavior. In particular, once connection with the server is lost it cannot be recovered and the {\dmapper} will itself respond with \textsc{no\_conn} responses. These have to be accounted for in the properties specified.
\subsection{General security properties}
Both the Transport and the Authentication Layers can be said to provide notions of security, which secure access to services of the Connection Layer. For each of these layers, we define general security properties that reflect successful implementation of these notions.
%Each upper SSH layer assumes a notion of security is provided by the layer bellow. The Authentication Layer assumes integrity and confidentiality is provided by the Transport Layer, the Connection Layer the same assumptions, plus it also assumes authentication was successful. We define a general property for each upper layer on the basis of successful implementation of these security notions.
The security property for the Transport layer is defined as follows: ``We consider a transport layer state machine secure if there is no path from the initial state to the point where the authentication service is invoked without exchanging and employing cryptographic keys.''\cite{Verleg2016} In other words, authentication request cannot succeed if key exchange wasn't performed successfully. Key exchange implies performing three steps. These steps have to be performed in order but may be interleaved by other actions. A successful authentication request should necessarily imply successful execution of the key exchange steps. We can tell an authentication request or a key exchange step was successful from the values of the input and output variables. For example, an authentication request is successful if for the input SERVICE\_REQUEST\_AUTH, the output SERVICE\_ACCEPT was received. Following these principles, we define the LTL specification in Property~\ref{prop:prop1}. O stands for the Once-operator, a past time LTL operator, which is true if its argument is true in a past time instant.
The security property for the Transport layer is defined as follows: ``We consider a transport layer state machine secure if there is no path from the initial state to the point where the authentication service is invoked without exchanging and employing cryptographic keys.''\cite{Verleg2016} In other words, authentication request cannot succeed if key exchange wasn't performed successfully. Key exchange implies performing three steps. These steps have to be performed in order but may be interleaved by other actions. A successful authentication request should necessarily imply successful execution of the key exchange steps. We can tell an authentication request or a key exchange step was successful from the values of the input and output variables. For example, an authentication request is successful if for the input \textsc{service\_request\_auth}, the output \textsc{service\_accept} was received. Following these principles, we define the LTL specification in Property~\ref{prop:prop1}. O stands for the Once-operator, a past time LTL operator, which is true if its argument is true in a past time instant.
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
......@@ -33,7 +37,7 @@ G ( (input=SERVICE_REQUEST_AUTH & output=SERVICE_ACCEPT) ->
In a similar way, we say that the Authentication Layer is secure ``if there is no path from the unauthenticated state to the authenticated state without providing the correct credentials.''\cite{Verleg2016}
Since we have no method to directly determine if the model is in an authenticated state, we consider the authenticated state to be a state where opening a channel can be done successfully.
Since opening a channel should only be possible after user authentication, this should show if we are in an authenticated state. The specification then is rather simple: Always, if a channel is opened successfully, has there not been a failure in user authentication since a successful user authentication. Opening a channel successfully in the model is straightforward, a request to open a channel is sent to the server, and a success message is received back. Checking whether there has been a success or failure in user authentication is done by checking if the server ever sends the UA\_FAILURE or UA\_SUCCESS packets. Additional checks if the user actually made a user authentication request could potentially be added. The resulting LTL is shown in Property~\ref{prop:prop2}. This LTL uses the Since-operator (S) which holds if its first argument holds for every state since its second argument holds. Note that the second argument has to hold somewhere in the path for the Since operator to hold.
Since opening a channel should only be possible after user authentication, this should show if we are in an authenticated state. The specification then is rather simple: Always, if a channel is opened successfully, has there not been a failure in user authentication since a successful user authentication. Opening a channel successfully in the model is straightforward, a request to open a channel is sent to the server, and a success message is received back. Checking whether there has been a success or failure in user authentication is done by checking if the server ever sends the \textsc{ua\_failure} or \textsc{ua\_success} packets. Additional checks if the user actually made a user authentication request could potentially be added. The resulting LTL is shown in Property~\ref{prop:prop2}. This LTL uses the Since-operator (S) which holds if its first argument holds for every state since its second argument holds. Note that the second argument has to hold somewhere in the path for the Since operator to hold.
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
......@@ -45,16 +49,16 @@ G ( (input= CH_OPEN & output= CH_OPEN_SUCCESS) ->
\end{property}
\subsection{Key exchange properties}
Important properties are that re-exchanging keys 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 map to multiple states in the learned models. For each state, we specify the properties that performing key exchange (1) should always be allowed from that state, and (2) when allowed, should always preserve the state, until specific inputs or outputs are encountered that necessarily change it. An example of such inputs or outputs are those corresponding to a \emph{disconnect} action from either side. 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 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 map to multiple states in the learned models. For each state, we specify the properties that performing key exchange (1) should always be allowed from that state, and (2) when allowed, should always preserve the state, until specific inputs or outputs are encountered that necessarily change it. An example of such inputs or outputs are those corresponding to a \emph{disconnect} action from either side. 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 key re-exchange in succession should imply success. Provided we perform successful finalization of a re-key, we remain in a pre-authenticated state until we exit this state on a \textsc{disconnect} from either side, or via a successful authentication (\textsc{ua\_success}. The latter is described in Property~\ref{prop:prop3}. Note that, we can tell of being in a pre-authenticated state, if authenticating with a valid public key implies success. WU 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 key re-exchange in succession should imply success. Provided we perform successful finalization of a re-key, we remain in a pre-authenticated state until we exit this state, either through a \textsc{disconnect} from either side, or via successful authentication (\textsc{ua\_success}). The latter is described in Property~\ref{prop:prop3}. Note that, we can tell of being 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 ( (input= SERVICE_REQUEST & output= SERVICE_ACCEPT) ->
( ( input = NEWKEYS & output = NO_RESP & X ( input = UA_PK_OK ) ) ->
X ( output=UA_SUCCESS) ) W (input = DISCONNECT | output= DISCONNECT | output= UA_SUCCESS)
( ( input = NEWKEYS & output = NO_RESP
& X ( input = UA_PK_OK ) ) -> X ( output=UA_SUCCESS) )
W (input = DISCONNECT | output= DISCONNECT | output= UA_SUCCESS)
\end{lstlisting}
\caption{Key exchange preserves pre-authenticated state}
\label{prop:prop3}
......@@ -63,7 +67,7 @@ G ( (input= SERVICE_REQUEST & output= SERVICE_ACCEPT) ->
\subsection{Other functional properties}
We have also formalized and checked properties drawn from the RFC specifications. We found the specification vague, which sometimes meant we had to make certain assumptions in order to formalize properly.
The RFC states in~\ref[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}.
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}.
\begin{property}[h]
......@@ -76,9 +80,19 @@ G ( (output = 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 \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.
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (input= SERVICE_REQUEST_AUTH & output!= SERVICE_ACCEPT & state != s0)
-> (output = DISCONNECT | output = NO_CONN) ))
\end{lstlisting}
\caption{Allowed outputs after SERVICE\_ACCEPT}
\label{prop:prop5}
\end{property}
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}).
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. 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 reaching this state, implementations replied with \textsc{unimplemented}. 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 (suggested by the \textsc{no\_conn}).
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( X (output = UA_SUCCESS) ->
......@@ -99,7 +113,7 @@ G (output = UA_SUCCESS ->
\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}.
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 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 (\textsc{no\_conn}), once a re-key procedure was initiated (by input \textsc{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]
......@@ -112,11 +126,13 @@ G ( (input= CH_OPEN & output= CH_OPEN_SUCCESS) ->
\end{property}
%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 \textsc{kexinit} message, a party MUST not send \textsc{service\_request} or \textsc{service\_accept} messages, until it has sent a \textsc{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 \textsc{disconnect} message. Moreover, in case it supports the service request, it MUST sent a \textsc{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 the 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