Commit 351f97fe authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean

Some minor and defo final edits. Alles klaar

parent c8884d15
...@@ -7,7 +7,7 @@ systems. BitVise is a well-known proprietary Windows-only SSH implementation. ...@@ -7,7 +7,7 @@ systems. BitVise is a well-known proprietary Windows-only SSH implementation.
In our experimental setup, {\dlearner} and {\dmapper} ran inside a Linux Virtual Machine. OpenSSH and DropBear were In our experimental setup, {\dlearner} and {\dmapper} ran inside a Linux Virtual Machine. OpenSSH and DropBear were
learned over a localhost connection, whereas BitVise was learned over a virtual connection with the Windows host machine. learned over a localhost connection, whereas BitVise was learned over a virtual connection with the Windows host machine.
We have adapted the setting off timing parameters to each implementation. We have adapted the setting of timing parameters to each implementation.
\begin{figure*} \begin{figure*}
\centering \centering
...@@ -67,14 +67,13 @@ responses for higher layer inputs sent during key re-exchange, and would deliver ...@@ -67,14 +67,13 @@ responses for higher layer inputs sent during key re-exchange, and would deliver
a major contributor to the number of states. For each state where rekeying a major contributor to the number of states. For each state where rekeying
is possible, the sequence of transitions constituting the complete is possible, the sequence of transitions constituting the complete
rekeying process should lead back to that state. This rekeying process should lead back to that state. This
leads to two additional rekeying states for each state where rekeying leads to two additional rekeying states for every state allowing rekey. Many states were also added due to {\dmapper} generated outputs such as \textsc{ch\_none} or \textsc{ch\_max}, outputs which signal that no channel is open or that the maximum number of channels have been opened.
is possible. Many states were also added due to {\dmapper} generated outputs such as \textsc{ch\_none} or \textsc{ch\_max}, outputs which signal that no channel is open or that the maximum number of channels have been opened.
Figure~\ref{fig:sshserver} shows the model learned for OpenSSH, with some edits to improve readability. The happy flow, in green, is fully explored in the model and mostly matches our earlier description of it\footnote{The only exception is in the Transport layer, where unlike in our happy flow definition, the server is the first to send the \textsc{newkeys} message. This is also accepted behavior, as the protocol does not specify which side should send \textsc{newkeys} first.}. Also explored is what happens when a rekeying sequence is attempted. We notice that rekeying is only allowed in states of the Connection layer. Strangely, for these states, rekeying is not state preserving, as the generated output on receiving a \textsc{sr\_auth}, \textsc{sr\_conn} or \textsc{kex30} changes from \textsc{unimpl} to \textsc{no\_resp}. This leads to two sub-clusters of states, one before the first rekey, the other afterward. In all other states, the first step of a Figure~\ref{fig:sshserver} shows the model learned for OpenSSH, with some edits to improve readability. The happy flow, in green, is fully explored in the model and mostly matches our earlier description of it\footnote{The only exception is in the Transport layer, where unlike in our happy flow definition, the server is the first to send the \textsc{newkeys} message. This is also accepted behavior, as the protocol does not specify which side should send \textsc{newkeys} first.}. Also explored is what happens when a rekeying sequence is attempted. We notice that rekeying is only allowed in states of the Connection layer. Strangely, for these states, rekeying is not state preserving, as the generated output on receiving a \textsc{sr\_auth}, \textsc{sr\_conn} or \textsc{kex30} changes from \textsc{unimpl} to \textsc{no\_resp}. This leads to two sub-clusters of states, one before the first rekey, the other afterward. In all other states, the first step of a
rekeying (\textsc{kexinit}) yields (\textsc{unimpl}), while the last step (\textsc{newkeys}) causes the system to disconnect. rekeying (\textsc{kexinit}) yields (\textsc{unimpl}), while the last step (\textsc{newkeys}) causes the system to disconnect.
We were puzzled by how systems reacted to \textsc{sr\_conn}, the request for services of the Connection layer. These services can be accessed once the user had authenticated, without the need of a prior service request. That in itself was not strange, as authentication messages already mention that connection services should start after authentication \footnote{This is a technical detail, the message format of authentication messages requires a field which says the service started after authentication. The only option is to start Connection layer services. }. We were puzzled by how systems reacted to \textsc{sr\_conn}, the request for services of the Connection layer. These services can be accessed once the user had authenticated, without the need of a prior service request. That in itself was not strange, as authentication messages already mention that connection services should start after authentication \footnote{This is a technical detail, the message format of authentication messages requires a field which says the service started after authentication. The only option is to start Connection layer services. }.
Unexpected was that an explicit request either lead to \textsc{unimpl}/\textsc{no\_resp} with no state change, as in the case of OpenSSH, or termination of the connection, as in the case of BitVise. The latter was particularly strange, as in theory, once authenticated, the user should always have access to the service, and not be disconnected on requesting this service. Only DropBear seems to respond positively (\textsc{sr\_accept}) to \textsc{sr\_conn} after authentication. Unexpected was that an explicit request either lead to \textsc{unimpl}/\textsc{no\_resp} with no state change, as in the case of OpenSSH, or termination of the connection, as in the case of BitVise. The latter was particularly strange, as in theory, once authenticated, the user should always have access to the service, and not be disconnected when requesting this service. Only DropBear seems to respond positively (\textsc{sr\_accept}) to \textsc{sr\_conn} after authentication.
We also notice the intricate authentication behavior: We also notice the intricate authentication behavior:
after an unsuccessful authentication attempt the only authentication method still allowed is password authentication. Finally, only BitVise allowed multiple terminals to be requested over the same channel. As depicted in the model, OpenSSH abruptly terminates on requesting a second terminal. DropBear exhibits a similar behavior. after an unsuccessful authentication attempt the only authentication method still allowed is password authentication. Finally, only BitVise allowed multiple terminals to be requested over the same channel. As depicted in the model, OpenSSH abruptly terminates on requesting a second terminal. DropBear exhibits a similar behavior.
......
...@@ -70,7 +70,7 @@ convey its own parameter preferences before key exchange can proceed. Also inclu ...@@ -70,7 +70,7 @@ convey its own parameter preferences before key exchange can proceed. Also inclu
\textbf{Message} & \textbf{Description} \\ \textbf{Message} & \textbf{Description} \\
\textsc{disconnect} & Terminates the current connection~\cite[p. 23]{rfc4253} \\ \textsc{disconnect} & Terminates the current connection~\cite[p. 23]{rfc4253} \\
\textsc{ignore} & Has no intended effect~\cite[p. 24]{rfc4253} \\ \textsc{ignore} & Has no intended effect~\cite[p. 24]{rfc4253} \\
\textsc{unimpl} & Intended response to an unimplemented message~\cite[p. 25]{rfc4253} \\ \textsc{unimpl} & Intended response to unrecognized messages~\cite[p. 25]{rfc4253} \\
\textsc{debug} & Provides other party with debug information~\cite[p. 25]{rfc4253} \\ \textsc{debug} & Provides other party with debug information~\cite[p. 25]{rfc4253} \\
\textsc{kexinit}* & Sends parameter preferences~\cite[p. 17]{rfc4253} \\ \textsc{kexinit}* & Sends parameter preferences~\cite[p. 17]{rfc4253} \\
%\textsc{guessinit}* & A \textsc{kexinit} after which a guessed \textsc{kex30} follows~\cite[p. 19]{rfc4253} \\ %\textsc{guessinit}* & A \textsc{kexinit} after which a guessed \textsc{kex30} follows~\cite[p. 19]{rfc4253} \\
...@@ -92,10 +92,10 @@ The Authentication layer defines one single client message type in the form of t ...@@ -92,10 +92,10 @@ The Authentication layer defines one single client message type in the form of t
\begin{tabular}{ll} \begin{tabular}{ll}
\textbf{Message} & \textbf{Description} \\ \textbf{Message} & \textbf{Description} \\
\textsc{ua\_none} & Authenticates with the ``none'' method~\cite[p. 7]{rfc4252} \\ \textsc{ua\_none} & Authenticates with the ``none'' method~\cite[p. 7]{rfc4252} \\
\textsc{ua\_pk\_ok}* & Provides a valid name/key combination~\cite[p. 8]{rfc4252} \\ \textsc{ua\_pk\_ok}* & Provides a valid name/key pair~\cite[p. 8]{rfc4252} \\
\textsc{ua\_pk\_nok}* & Provides an invalid name/key combination~\cite[p. 8]{rfc4252} \\ \textsc{ua\_pk\_nok}* & Provides an invalid name/key pair~\cite[p. 8]{rfc4252} \\
\textsc{ua\_pw\_ok} & Provides a valid name/password combination~\cite[p. 10]{rfc4252} \\ \textsc{ua\_pw\_ok} & Provides a valid name/password pair~\cite[p. 10]{rfc4252} \\
\textsc{ua\_pw\_nok} & Provides an invalid name/password combination~\cite[p. 10]{rfc4252} \\ \textsc{ua\_pw\_nok} & Provides an invalid name/password pair~\cite[p. 10]{rfc4252} \\
\end{tabular} \end{tabular}
\caption{Authentication layer inputs} \caption{Authentication layer inputs}
\vspace{-7mm} \vspace{-7mm}
...@@ -134,7 +134,7 @@ The restricted alphabet only supports the most general channel management inputs ...@@ -134,7 +134,7 @@ The restricted alphabet only supports the most general channel management inputs
The {\dmapper} must provide a translation between abstract messages The {\dmapper} must provide a translation between abstract messages
and well-formed SSH messages: it has to translate abstract inputs and well-formed SSH messages: it has to translate abstract inputs
listed in tables~\ref{trans-alphabet}-\ref{conn-alphabet} to actual listed in Tables~\ref{trans-alphabet}-\ref{conn-alphabet} to actual
SSH packets, and translate the SSH packets received in answer SSH packets, and translate the SSH packets received in answer
to our abstract outputs. to our abstract outputs.
...@@ -178,8 +178,7 @@ with a randomly generated channel identifier, on a \textsc{ch\_close}, it remove ...@@ -178,8 +178,7 @@ with a randomly generated channel identifier, on a \textsc{ch\_close}, it remove
(if there was any). The buffer size, or the maximum number of opened channels, is limited to one. Initially the buffer is empty. Lastly, the {\dmapper} also stores the sequence number of the last received message from the {\dsut}. This number is then used when constructing \textsc{unimpl} inputs. (if there was any). The buffer size, or the maximum number of opened channels, is limited to one. Initially the buffer is empty. Lastly, the {\dmapper} also stores the sequence number of the last received message from the {\dsut}. This number is then used when constructing \textsc{unimpl} inputs.
In the following cases, inputs are answered by the {\dmapper} directly In the following cases, inputs are answered by the {\dmapper} directly
instead of being sent to the {\dsut} to find out its response: (1) on receiving a \textsc{ch\_open} input instead of being sent to the {\dsut} to find out its response: (1) on receiving a \textsc{ch\_open} input if the buffer has reached the size limit, the {\dmapper} directly responds with \textsc{ch\_max}; (2)
and the buffer has reached the size limit, the {\dmapper} directly responds with \textsc{ch\_max}; (2)
on receiving any input operating on a channel (all Connection layer inputs other than \textsc{ch\_open}) when the buffer is empty, the on receiving any input operating on a channel (all Connection layer inputs other than \textsc{ch\_open}) when the buffer is empty, the
{\dmapper} directly responds with \textsc{ch\_none}; (3) if connection with the {\dsut} was terminated, the {\dmapper} {\dmapper} directly responds with \textsc{ch\_none}; (3) if connection with the {\dsut} was terminated, the {\dmapper}
responds with a \textsc{no\_conn} message, as sending further messages to the {\dsut} is pointless in that case. responds with a \textsc{no\_conn} message, as sending further messages to the {\dsut} is pointless in that case.
...@@ -241,7 +240,7 @@ in an SQLite database and verifies if a new observation is different ...@@ -241,7 +240,7 @@ in an SQLite database and verifies if a new observation is different
to one cached from a previous protocol run. If so, it raises to one cached from a previous protocol run. If so, it raises
a warning, which then needs to be manually investigated. a warning, which then needs to be manually investigated.
An added benefit of this cache is that is allows the {\dmapper} to An added benefit of this cache is that it allows the {\dmapper} to
supply answer to some inputs without actually sending them to the supply answer to some inputs without actually sending them to the
{\dsut}. This sped up learning a lot when we had to restart {\dsut}. This sped up learning a lot when we had to restart
experiments: any new experiment on the same {\dsut} could start where experiments: any new experiment on the same {\dsut} could start where
...@@ -250,7 +249,7 @@ was an important benefit, as experiments could take several days. ...@@ -250,7 +249,7 @@ was an important benefit, as experiments could take several days.
%A subsequent identical learning run can quickly resume from where the previous one was ended, as the cache from the previous run is used to quickly respond to all queries up to the point the previous run ended. %A subsequent identical learning run can quickly resume from where the previous one was ended, as the cache from the previous run is used to quickly respond to all queries up to the point the previous run ended.
Another practical problem beside non-determinism is that an SSH server Another practical problem besides non-determinism is that an SSH server
may produce a sequence of outputs in response to a single input. This may produce a sequence of outputs in response to a single input. This
means it is not behaving as a Mealy machines, which allows for means it is not behaving as a Mealy machines, which allows for
only one output. Dealing with this is simple: the {\dmapper} only one output. Dealing with this is simple: the {\dmapper}
......
...@@ -49,7 +49,7 @@ Initially, the {\dlearner} only knows the input alphabet $I$ and output alphabet ...@@ -49,7 +49,7 @@ Initially, the {\dlearner} only knows the input alphabet $I$ and output alphabet
The task of the {\dlearner} is to learn $\M$ via two types of queries: The task of the {\dlearner} is to learn $\M$ via two types of queries:
\begin{itemize} \begin{itemize}
\item \item
With a \emph{membership query}, the learner asks what the response is to an input sequence $\sigma \in I^{\ast}$. With a \emph{membership query}, the {\dlearner} asks what the response is to an input sequence $\sigma \in I^{\ast}$.
The teacher answers with the output sequence in $A_{\M}(\sigma)$. The teacher answers with the output sequence in $A_{\M}(\sigma)$.
\item \item
With an \emph{equivalence query}, the {\dlearner} asks whether a hypothesized Mealy machine $\CH$ is correct, that is, With an \emph{equivalence query}, the {\dlearner} asks whether a hypothesized Mealy machine $\CH$ is correct, that is,
......
...@@ -9,7 +9,7 @@ ...@@ -9,7 +9,7 @@
%Hence it makes sense to (1) formalize specification so as to eliminate ambiguity, and (2) use model checking to verify the %specifications automatically. To these ends, we use the NuSMV model checker \cite{NuSMV2} to verify security properties for the %learned models, properties which we formalize using LTL formulas. %Hence it makes sense to (1) formalize specification so as to eliminate ambiguity, and (2) use model checking to verify the %specifications automatically. To these ends, we use the NuSMV model checker \cite{NuSMV2} to verify security properties for the %learned models, properties which we formalize using LTL formulas.
A NuSMV model is specified via a set of finite variables together with a transition-function that describes 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 given specification is not true. We generate NuSMV models automatically from the learned models. Generation proceeds by first defining a NuSMV file with three variables, corresponding to inputs, outputs and states. The transition-function is then extracted from the learned model and appended to this file. A NuSMV model is specified via a set of finite variables together with a transition-function that describes 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 given specification is not true. We generate NuSMV models automatically from the learned models. Generation proceeds by first defining a NuSMV file with three variables, corresponding to inputs, outputs and states. The transition-function is then extracted from the learned model and appended to this file.
This function updates the output and state variables for a given valuation of the input variable and the current state. Figure~\ref{fig:nusmvex} gives an example of a Mealy machine and it's associated NuSMV model. This function updates the output and state variables for a given valuation of the input variable and the current state. Figure~\ref{fig:nusmvex} gives an example of a Mealy machine and its associated NuSMV model.
%\parbox{\columnwidth}{ %\parbox{\columnwidth}{
% \parbox{0.5\columnwidth}{ % \parbox{0.5\columnwidth}{
...@@ -102,7 +102,7 @@ A key note is that properties are checked not on the actual concrete model of th ...@@ -102,7 +102,7 @@ A key note is that properties are checked not on the actual concrete model of th
escapeinside={(*}{*)},% escapeinside={(*}{*)},%
} }
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} , {\dvauth} 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}. 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 to authenticate, concluded by opening of a channel. Whereas the first step is complex, the subsequent steps can be captured by the simple predicates {\dreqauth}, {\dvauth} 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, so as 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}.
To these predicates, we add predicates for valid, invalid and all authentication methods, a predicate for the receipt of \textsc{newkeys} from the server, and receipt of \textsc{kexinit}, which can also be seen as initiation of key (re-) exchange. These latter predicates have to be tweaked in accordance with the input alphabet used and with the output the {\dsut} generated (\textsc{kexinit} could be sent in different packaging, either alone, or joined by a different message). Their formulations correspond to the OpenSSH setting. Finally, by {\dconnlost} we define a predicate suggesting that connection was lost, and by {\dend}, the end condition for most higher layer properties. To these predicates, we add predicates for valid, invalid and all authentication methods, a predicate for the receipt of \textsc{newkeys} from the server, and receipt of \textsc{kexinit}, which can also be seen as initiation of key (re-) exchange. These latter predicates have to be tweaked in accordance with the input alphabet used and with the output the {\dsut} generated (\textsc{kexinit} could be sent in different packaging, either alone, or joined by a different message). Their formulations correspond to the OpenSSH setting. Finally, by {\dconnlost} we define a predicate suggesting that connection was lost, and by {\dend}, the end condition for most higher layer properties.
\begin{center} \begin{center}
\begin{lstlisting}[basicstyle=\footnotesize] \begin{lstlisting}[basicstyle=\footnotesize]
...@@ -144,7 +144,7 @@ a connection is lost is marked by generation of the \textsc{no\_conn} output. F ...@@ -144,7 +144,7 @@ a connection is lost is marked by generation of the \textsc{no\_conn} output. F
\label{prop:noconn} \label{prop:noconn}
\end{property} \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 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}. 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 open 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{property}%[h]
\begin{lstlisting}[basicstyle=\footnotesize] \begin{lstlisting}[basicstyle=\footnotesize]
...@@ -162,7 +162,7 @@ Outputs \textsc{ch\_max} and \textsc{ch\_none} are still generated because of a ...@@ -162,7 +162,7 @@ Outputs \textsc{ch\_max} and \textsc{ch\_none} are still generated because of a
\subsection{Security properties} \subsection{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. 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 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$. Key exchange implies three steps which have to be performed in order but may be interleaved by other actions. Successful authentication necessarily implies 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_AUTH -> SR_AUTH
...@@ -181,7 +181,7 @@ Key exchange implies three steps which have to be performed in order but may be ...@@ -181,7 +181,7 @@ Key exchange implies three steps which have to be performed in order but may be
\label{prop:sec-trans} \label{prop:sec-trans}
\end{property} \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 has been 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. 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 as a state where a channel has been 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$. 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$.
...@@ -302,7 +302,7 @@ In the same paragraph, it is stated that authentication requests received after ...@@ -302,7 +302,7 @@ In the same paragraph, it is stated that authentication requests received after
\end{property} \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 in \cite[p. 9]{rfc4254} that on receiving a \textsc{ch\_close} message, a side MUST send back a \textsc{ch\_close}, unless it had already sent this message for the channel. The channel must have been opened beforehand (\dopchan) and the property only has to hold until the end condition holds or the channel was closed(\textsc{ch\_close}). Along these lines we formulate Property~\ref{prop:conn-close}. The Connection layer RFC states in \cite[p. 9]{rfc4254} that on receiving a \textsc{ch\_close} message, a side MUST send back a \textsc{ch\_close}, unless it had already sent this message for the channel. The channel must have been opened beforehand (\dopchan) and the property only has to hold until the end condition holds or the channel was closed(\textit{out=CH\_CLOSE}). We formulate Property~\ref{prop:conn-close} accordingly.
\begin{property} \begin{property}
\begin{lstlisting}[basicstyle=\footnotesize] \begin{lstlisting}[basicstyle=\footnotesize]
...@@ -328,7 +328,7 @@ G ( hasOpenedChannel -> ...@@ -328,7 +328,7 @@ G ( hasOpenedChannel ->
\subsection{Model checking results} \subsection{Model checking results}
Table~\ref{tab:mcresults} presents model checking results. Crucially, the security properties hold for all three implementations. We had to slightly adapt our properties for BitVise Table~\ref{tab:mcresults} presents model checking results. Crucially, the security properties hold for all three implementations. We had to slightly adapt our properties for BitVise
as it buffered all responses during rekey (incl. \textsc{UA\_SUCCESS}). as it buffered all responses during rekey (incl. \textsc{UA\_SUCCESS}).
In particular, we used {\dvauth} instead of $out=UA\_SUCCESS$ to suggest successful authentication. In particular, we used {\dvauth} instead of \textit{out=UA\_SUCCESS} to suggest successful authentication.
%\begin{center}\small %\begin{center}\small
% \centering % \centering
......
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