Commit 8443a6ec authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean

Updated security definitions

parent 40274912
......@@ -99,7 +99,7 @@ Our formulation uses NuSMV syntax. We occasionally rely on past modalities opera
\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.
In the actual 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}
......@@ -116,7 +116,7 @@ a connection is lost is suggested by generation of the \textsc{no\_conn} output.
\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}.
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 continues 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 \textsc{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]
......@@ -132,7 +132,7 @@ Outputs \textsc{ch\_max} and \textsc{ch\_none} are still generated because of a
\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, 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.
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 the service 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.
......@@ -196,7 +196,7 @@ Provided we perform successful finalization of a rekey, we remain in a pre-authe
%\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. 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
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]
......@@ -262,8 +262,7 @@ The RFC for the Authentication layer states in~\cite[p. 6]{rfc4252} that if the
\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.
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}). The formulation of this statement shown in Property~\ref{prop:auth-post-ua}. The property uses $authReq$, a predicate which holds iff the input is an authentication message.
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( out=UA_SUCCESS ->
......
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