Commit 68fb0ce3 authored by Frits Vaandrager's avatar Frits Vaandrager

minor corrections sc secur spec

parent 5f74449a
......@@ -95,11 +95,12 @@ Before introducing the properties, we mention some basic predicates and conventi
\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 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.
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 use the weak until operator W, which is not supported by NuSMV, but can be easily defined in terms of the until operator
U and globally operator G that are supported:
$p\,W\,q\, =\, p \,U\, q\, | \, G\, p$.
%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}
......@@ -134,7 +135,8 @@ Outputs \textsc{ch\_max} and \textsc{ch\_none} are still generated because of a
\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 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.
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 is the once operator. Formula $O p$ is true at time $t$ if $p$ held in at least one of the previous time steps $t' \leq t$.
% SR_AUTH_AUTH -> SR_AUTH
% SR_AUTH_CONN -> SR_CONN
......@@ -152,7 +154,8 @@ Key exchange implies three steps which have to be performed in order but may be
\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, 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.
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 indicated 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.
Formula $p S q$ is true at time $t$ if $q$ held at some time $t' \leq t$ and $p$ held in all times $t''$ such that $t' < t'' \leq t$.
\begin{property}[h]
......
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