Commit f9b43d47 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean
Browse files

Updated security definitions

parent b1f395e6
......@@ -81,39 +81,60 @@ The remainder of this section defines the properties we formalized and verified.
\end{enumerate}
A key note is that properties are checked not on the actual concrete model of the {\dsut}, but on an abstract model, which represents an over-approximation of the {\dsut} induced by the {\dmapper}. This is unlike in~\cite{TCP2016}, where properties where checked on a concretization of the learned model, concretization obtained by application of a reverse mapping. Building a reverse mapper is far from trivial given the {\dmapper}'s complexity. Performing model checking on an abstract model means we cannot fully translate model checking results to the concrete (unknown) model of the implementation. In particular, properties which hold for the abstract model do not necessarily hold for the implementation. Properties that don't hold however, also don't hold for the {\dsut}.
\newcommand{\dreqauth}{$hasReqAuth$}
\newcommand{\dauth}{$hasAuth$}
\newcommand{\dopchan}{$hasOpenedChannel$}
Before introducing the properties, we mention some basic predicates and conventions we use in their definition. The happy flow in SSH consists in a series of steps, the user first exchanges keys, then requests for the authentication service, followed up by supplying valid credentials and authentication, concluded by opening of a channel. Whereas the first step is complex, the subsequent steps can be captured by the simple predicates {\dreqauth} , {\dauth} and {\dopchan} respectively. The predicates are defined in terms of the output generated at a given moment, with certain values of this output indicating that the step was performed successfully. For example, \textsc{ch\_open\_success} indicates that a channel has been opened successfully. Sometimes, we also need the input that generated the output, in order to distinguish this step from a different step. In particular, requesting the authentication service is distinguished from requesting the connection service by \textsc{sr\_auth}.
\begin{center}
\begin{lstlisting}
hasReqAuth := inp=SR_AUTH & out=SR_ACCEPT
hasAuth := out=UA_PK_OK | out=UA_PW_OK
hasOpenedChannel := out=CH_OPEN_SUCCESS
\end{lstlisting}
\end{center}
Our formulation uses NuSMV syntax. We occasionally rely on past modalities operators such Once (O) and Since (S), which are uncommon, but are supported by NuSMV. We also make use of Weak Until (W) which isn't supported by NuSMV, but can be easily re-formulated in terms of Always (G) and Until (U) as:
\begin{center}
$\Psi\,W\,\Phi\, :=\, \Psi\, U\, \Phi\, | \, \Psi$
\end{center}
In the run specification, W was replaced by this re-formulation. Finally, we may define properties which we later use when defining other properties. This feature again isn't supported by NuSMV, hence the properties appear in expanded form in the run specification.
\subsection{Basic characterizing properties}
%cannot be translated. %Though in practical terms, these results are still translatable, in particular for cases where properties are not met.
In our setting, once the connection is lost, it can no longer be recovered and the {\dmapper} will itself respond with \textsc{no\_conn} to any subsequent non-Connection layer inputs sent by the {\dlearner}. This behavior is described by Property~\ref{prop:noconn}, where \emph{isConnectionInput} is a predicate which only holds if the input supplied is a Connection layer input. The reason we exclude connection inputs is due to a mapper characteristic we touched on in Section~\ref{sec:result}. The {\dmapper} maintains a buffer of opened channels and limits its size to 1. From the perspective of the {\dmapper}, a channel is open, and thus added to the buffer, whenever \textsc{ch\_open} is received from the learner, regardless if a channel was actually opened on the {\dsut}. If an attempt to open an additional channel is made, the {\dmapper} itself responds by \textsc{ch\_max} without querying the {\dsut}. Conversely, if there is no channel open (the buffer is empty) and an input operating on a channel is sent, the {\dmapper} responds by \textsc{ch\_none}, again, without querying the {\dsut}. Additionally, a channel opened on the {\dmapper} is closed and removed from the buffer on a {ch\_close} from the {\dlearner}, with a corresponding SSH CHANNEL CLOSE message being sent to the {\dsut}. We use Property~\ref{prop:channel} to describe this mapper induced behavior.
In our setting, one TCP connection with the system is made and once the connection is lost (because the system disconnects for example), it can no longer be re-established. The moment
a connection is lost is suggested by generation of the \textsc{no\_conn} output. From this moment onwards, the only outputs encountered are the \textsc{no\_conn} output (the {\dmapper} tried but failed to communicate with the {\dsut}), or outputs generated by the {\dmapper} directly, without querying the system . The latter are \textsc{ch\_max} (channel buffer is full) and \textsc{ch\_none} (channel buffer is empty). With these outputs we define Property~\ref{prop:noconn} which describes the ``one connection'' property of our setup.
\begin{property}%[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G (out=NO_CONN ->
G (!isConnectionInput(in) -> out=NO_CONN) )
G (out=NO_CONN ->
G (out=NO_CONN | out=CH_MAX | out=CH_NONE) )
\end{lstlisting}
\caption{Connection lost property.}
\caption{One connection property}
\label{prop:noconn}
\end{property}
Outputs \textsc{ch\_max} and \textsc{ch\_none} are still generated because of a characteristic we touched on in Subsection~\ref{subsec:mapper}. The {\dmapper} maintains a buffer of opened channels and limits its size to 1. From the perspective of the {\dmapper}, a channel is open, and thus added to the buffer, whenever \textsc{ch\_open} is received from the learner, regardless if a channel was actually opened on the {\dsut}. In particular, if after opening a channel via \textsc{ch\_open} an additional attempt to open a channel is made, the {\dmapper} itself responds by \textsc{ch\_max} without querying the {\dsut}. This goes on, until the {\dlearner} closes the channel by \textsc{ch\_close}, prompting removal of the channel and the sending on an actual CLOSE message to the {\dsut} (hence out!=\textsc{ch\_none}). A converse property can be formulated in a similar way for when the buffer is empty after a \textsc{ch\_close}, in which case subsequent \textsc{ch\_close} messages prompt the {\dmapper} generated {ch\_none}, until a channel is opened via \textsc{ch\_open} and an actual OPEN message is sent to the {\dsut}. Conjunction of these two behaviors forms Property~\ref{prop:channel}.
\begin{property}%[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G (inp=CH_OPEN & out!=CH_MAX ->
(inp=CH_OPEN -> out=CH_MAX)
W (inp=CH_CLOSE & out!=CH_NONE &
(isConnectionInput(in) -> out=CH_NONE)
W (inp=CH_OPEN) ) )
(G (inp=CH_OPEN) ->
X ( (inp=CH_OPEN -> out=CH_MAX)
W (inp=CH_CLOSE & out!=CH_NONE) ) ) &
(G (inp=CH_CLOSE) ->
X ( (inp=CH_CLOSE -> out=CH_NONE)
W (inp=CH_OPEN & out!=CH_MAX) ) )
\end{lstlisting}
\caption{Mapper induced property.}
\caption{Mapper induced channel property}
\label{prop:channel}
\end{property}
\subsection{Layer-critical security properties}
In SSH, upper layer services assume some notions of security, notions which are ensured by mechanisms in the lower layers. These mechanisms should have to be first engaged for the respective upper layer services to become available. As an example, authentication and connection services should only become available after exchanging and employing of kryptographic keys (key exchange) was done in the Transport layer, otherwise these services would be running over an unencrypted channel. Requests for these services should therefore not succeed unless key exchange was performed successfully.
Key exchange implies three steps which have to be performed in order but may be interleaved by other actions. Successful authentication or connection service requests should necessarily imply successful execution of the key exchange steps. We can tell a service request or a key exchange step were successful from the values of the input and output variables. For example, an authentication service request is successful if for the input \textsc{sr\_auth}, the output \textsc{sr\_accept} was received. One would expect that a connection service request would in a similar way be successful if on sending \textsc{sr\_conn}, we would also receive the output \textsc{sr\_accept}. Unfortunately, as discussed in the previous section, behavior on \textsc{sr\_conn} seems inconsistent, so in its place, we use opening a channel as means of knowing that connection Layer services were available. This is suggested by receiving a \textsc{ch\_open\_success} output to a \textsc{ch\_open} input.
Following these principles, we define the LTL specification in Property~\ref{prop:sec-trans}, where O stands for the Once-operator. This operator is a past time LTL operator which holds if its argument holds in a past time instant.
In SSH, upper layer services assume some notions of security, notions which are ensured by mechanisms in the lower layers. These mechanisms should have to be first engaged for the respective upper layer services to become available. As an example, the authentication service should only become available after exchanging and employing of kryptographic keys (key exchange) was done in the Transport layer, otherwise these services would be running over an unencrypted channel. Requests for this service should therefore not succeed unless key exchange was performed successfully.
Key exchange implies three steps which have to be performed in order but may be interleaved by other actions. Successful authentication should necessarily imply successful execution of the key exchange steps. We can tell each key exchange step were successful from the values of the input and output variables. Successful authentication request is indicated by the predicate defined earlier, {\dreqauth}. Following these principles, we define the LTL specification in Property~\ref{prop:sec-trans}, where O stands for the Once-operator. This operator is a past time LTL operator which holds if its argument holds in a past time instant.
% SR_AUTH_AUTH -> SR_AUTH
% SR_AUTH_CONN -> SR_CONN
......@@ -122,36 +143,35 @@ Following these principles, we define the LTL specification in Property~\ref{pro
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (inp=SR_AUTH & out=SR_ACCEPT) |
(inp=CH_OPEN & out=CH_OPEN_SUCCESS) ->
G ( hasReqAuth ->
O ( (inp=NEWKEYS & out=NO_RESP) &
O ( (inp=KEX30 & out=KEX31_NEWKEYS) &
O (out=KEXINIT) ) ) )
\end{lstlisting}
\caption{Transport layer security.}
\caption{Transport layer security}
\label{prop:sec-trans}
\end{property}
Apart from a secure connection, 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 \textsc{ua\_success} and \textsc{ua\_failure} respectively. Along these lines, we formulate this specification by Property~\ref{prop:sec-auth}, 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.
Apart from a secure connection, 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, captured by the predicate {\dopchan}. Provision of valid/invalid credentials is suggested by the outputs \textsc{ua\_success} and \textsc{ua\_failure} respectively. Along these lines, we formulate this specification by Property~\ref{prop:sec-auth}, 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]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (inp=CH_OPEN & out=CH_OPEN_SUCCESS) ->
(!(out=UA_FAILURE) S out=UA_SUCCESS) )
G ( hasOpenedChannel ->
out!=UA_FAILURE S out=UA_SUCCESS )
\end{lstlisting}
\caption{Authentication layer security.}
\caption{Authentication layer security}
\label{prop:sec-auth}
\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 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 can specify the properties that rekey-ing (1) should always be possible, and (2) if possible, should always preserve the state, until connection is lost. We can tell each rekey step was successful by the generated response. %There is no feasible way of describing that a state was preserved, but we can again use input and output
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. This is shown in Property~\ref{prop:rpos-pre-auth}.
In the case of the pre-authenticated state, we know we have reached this state following a successful authentication service request, indicated by the predicate {\dreqauth}. Once here, performing the inputs for rekey in succession should imply success. This is shown in Property~\ref{prop:rpos-pre-auth}.
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (inp=SR_AUTH & out=SR_ACCEPT) ->
G ( hasReqAuth ->
X (inp=KEXINIT -> out=KEXINIT &
X (inp=KEX30 -> out=KEX31_NEWKEYS &
X (inp=NEWKEYS -> out=NO_RESP) ) ) )
......@@ -164,7 +184,7 @@ Provided we perform successful finalization of a rekey, we remain in a pre-authe
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (inp=SR_AUTH & out=SR_ACCEPT) ->
G ( hasReqAuth ->
( (inp=NEWKEYS & out=NO_RESP & X inp=UA_PK_OK) ->
X out=UA_SUCCESS)
W (out=NO_CONN | out=UA_SUCCESS) )
......@@ -173,15 +193,28 @@ G ( (inp=SR_AUTH & out=SR_ACCEPT) ->
\label{prop:rper-pre-auth}
\end{property}
\textit{Perhaps this could be merged into one property?}
%\textit{Perhaps this could be merged into one property?}
\subsection{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{sr\_accept} message, until it has sent a \textsc{newkeys} message. This is translated to Property~\ref{prop:trans-kexinit}. 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.
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. A first general property can be defined for the \textsc{disconnect} output. The RFC specifies that after sending this message, a party MUST not send or receive any data\cite[p. 24]{rfc4253}. While we cannot tell what the server actually receives, we can check that the server doesn't generate any output after sending \textsc{disconnect}. After a \textsc{disconnect} message, subsequent outputs should be solely derived by the {\dmapper}. Knowing the {\dmapper} induced outputs are \textsc{no\_conn}, \textsc{ch\_max} and \textsc{ch\_none}, we formulate by Property~\ref{prop-trans-disc} to describe
expected outputs after a \textsc{disconnect}.
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( out=DISCONNECT ->
X G (out=CH_NONE | out=CH_MAX | out=NO_CONN) )
\end{lstlisting}
\caption{Only {\dmapper} outputs after DISCONNECT}
\label{prop:trans-disc}
\end{property}
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{sr\_accept} message, until it has sent a \textsc{newkeys} message. This is translated to Property~\ref{prop:trans-kexinit}. 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.
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (out=KEXINIT) ->
G ( out=KEXINIT ->
X ( (out!=SR_ACCEPT & out!=KEXINIT)
W (out=NEWKEYS | out=KEX31_NEWKEYS) ) )
\end{lstlisting}
......@@ -190,66 +223,69 @@ G ( (out=KEXINIT) ->
\label{prop:trans-kexinit}
\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{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, 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{sr\_accept}) or a disconnect(\textsc{disconnect}) which loses the connection in the next step. 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.
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{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.
% , 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 ( (inp=SR_AUTH & out!=NO_CONN & state!=s0) ->
(out=SR_ACCEPT | (out=DISCONNECT &
X G (inp=SR_AUTH -> out=NO_CONN) ) ) )
G ( (inp=SR_AUTH & state!=s0) ->
(out=SR_ACCEPT | out=DISCONNECT | out=NO_CONN ) ) )
\end{lstlisting}
\caption{Allowed outputs after SR\_ACCEPT}
\label{prop:trans-sr}
\end{property}
A general property can also be defined for the \textsc{disconnect} output. The RFC specifies that after sending this message, a party MUST not send or receive any data. While we cannot assess on what the server actually receives, we can check that the server doesn't generate any output after sending \textsc{disconnect}. All output following this \textsc{disconnect} message should be generated directly by the {\dmapper}, and never derived from {\dsut} messages. Knowing the {\dmapper} induced outputs are \textsc{no\_conn}, \textsc{ch\_max} and \textsc{ch\_none}, we formulate by Property~\ref{prop-trans-disc}.
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( out=DISCONNECT ->
X G (out=CH_NONE | out=CH_MAX | out=NO_CONN) )
\end{lstlisting}
\caption{Only {\dmapper} outputs after DISCONNECT}
\label{prop:trans-disc}
\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:auth-pre-ua} for behavior before an \textsc{ua\_success}, Property~\ref{prop:auth-post-ua} for behavior afterward, until the connection is lost.
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. Rejected requests are those using invalid credentials (\textsc{ua\_pk\_nok} and \textsc{ua\_pw\_nok}) or an unacceptable authentication method ( \textsc{ua\_none}). In case the requests succeeds (\textsc{ua\_pk\_ok} and \textsc{ua\_pw\_ok}), a \textsc{ua\_success} MUST be sent only once. While not explicitly stated, we assume this to be in a context where the authentication service had been successfully requested, hence we use the {\dreqauth} predicate. We define two properties, Property~\ref{prop:auth-pre-ua} for behavior before an \textsc{ua\_success}, Property~\ref{prop:auth-post-ua-strong} for behavior afterward.
%Indeed, before reaching this state, implementations replied with \textsc{unimplemented}.
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (inp=SR_AUTH & out=SR_ACCEPT) ->
X ( (inp=UA_PK_NOK -> out=UA_FAILURE) &
(inp=UA_PK_OK -> out=UA_SUCCESS) )
G ( hasReqAuth ->
X ( (inp=UA_PK_NOK | inp=UA_PW_NOK | inp=UA_NONE)
-> out=UA_FAILURE)
W (out=UA_SUCCESS | output=NO_CONN) )
\end{lstlisting}
\caption{UA\_SUCCESS is sent at most once}
\caption{Invalid requests prompt UA\_FAILURE }
\label{prop:auth-pre-ua}
\end{property}
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G (out=UA_SUCCESS ->
X ( ( (in =UA_PK_OK | inp=UA_PK_NOK) -> out=NO_RESP )
G ( (out=UA_SUCCESS) ->
X G (out!=UA_SUCCESS) )
\end{lstlisting}
\caption{UA\_SUCCESS is sent at most once}
\label{prop:auth-post-ua-strong}
\end{property}
In the same paragraph, it is stated that authentication requests received after a \textsc{ua\_success} SHOULD be ignored. This is a weaker statement, and it requires that all authentication messages
after a \textsc{ua\_success} output should prompt no response from the system(\textsc{no\_resp}) until the connection with the system is lost(\textsc{no\_conn}). We define $authReq$ as
a predicate which holds whenever the input is an authentication message.
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( out=UA_SUCCESS ->
X ( ( authReq-> out=NO_RESP )
W out=NO_CONN ) )
\end{lstlisting}
\caption{Silently ignore auth. requests after UA\_SUCCESS}
\caption{Silence after UA\_SUCCESS}
\label{prop:auth-post-ua}
\end{property}
\textit{Perhaps this could also be merged into one 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:conn-close}.
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. Also, this condition no longer applies once the connection is lost (\textsc{no\_conn}) or once the channel was closed. We weaken it,so it also doesn't have to hold once the rekey procedure was initiated (by input \textsc{kexinit}), as all implementations were non-responsive during the rekey procedure. Along these lines we formulate Property~\ref{prop:conn-close}.
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( ( (inp=CH_OPEN & out=CH_OPEN_SUCCESS) ->
G ( ( (inp=CH_OPEN & out=CH_OPEN_SUCCESS) ->
X (inp=CH_CLOSE -> out=CH_CLOSE &
X ( (out!=CH_CLOSE) W (out=CH_OPEN_SUCCESS) ) )
W (out=NO_CONN | inp=KEXINIT | out=CH_CLOSE) )
\end{lstlisting}
\caption{CH\_CLOSE request is followed by CH\_CLOSE response}
\caption{CH\_CLOSE response on CH\_CLOSE request}
\label{prop:conn-close}
\end{property}
......@@ -275,10 +311,11 @@ Table~\ref{tab:mcresults} presents model checking results. Crucially, all the cr
& Auth. & & & \\ \hline
Rekey & Pre-auth. & & & \\ \cline{2-5}
& Auth. & & & \\ \hline
Functional& Prop.~\ref{prop:trans-kexinit} & & & \\ \cline{2-5}
Functional& Prop.~\ref{prop:trans-disc} & & & \\ \cline{2-5}
& Prop.~\ref{prop:trans-kexinit} & & & \\ \cline{2-5}
& Prop.~\ref{prop:trans-sr} & & & \\ \cline{2-5}
& Prop.~\ref{prop:trans-disc} & & & \\ \cline{2-5}
& Prop.~\ref{prop:auth-pre-ua} & & & \\ \cline{2-5}
& Prop.~\ref{prop:auth-post-ua-strong} & & & \\ \cline{2-5}
& Prop.~\ref{prop:auth-post-ua} & & & \\ \cline{2-5}
& Prop.~\ref{prop:conn-close} & & & \\ \hline
\end{tabular}
......
Supports Markdown
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