Commit 5b286f87 authored by Erik Poll's avatar Erik Poll
Browse files
parents 7ce02209 84355219
\section{Introduction}\label{introduction}
SSH is security protocols that is widely to interact securely with
SSH is a security protocols that is widely to interact securely with
remote machines. SSH -- or more precisely, the transport layer
protocol of SSH -- has been subjected to security analysis
\cite{Williams2011Analysis}, incl.\ analyses that revealed
......
DEFINE isDisconnected := (out=NO_CONN | out=CH_MAX | out=CH_NONE);
DEFINE hasReqAuth := (inp=SR_AUTH & out=SR_ACCEPT);
DEFINE hasOpenedChannel := (out=CH_OPEN_SUCCESS);
DEFINE hasAuth := (out=UA_PK_OK | out=UA_PW_OK);
DEFINE authReq := (inp=UA_PK_OK | inp=UA_PW_OK | inp=UA_PK_NOK | inp=UA_PW_NOK | inp=UA_NONE);
-- General Properties
-- Once a connection is lost, it is lost for good
LTLSPEC NAME gen_one_conn := G (out=NO_CONN ->
G isDisconnected)
-- Cyclic behavior induced by CH_OPEN and CH_CLOSE
LTLSPEC NAME gen_cyclic := (G (inp=CH_OPEN) ->
X ( (inp=CH_OPEN -> out=CH_MAX) U (inp=CH_CLOSE & out!=CH_NONE) | G (inp=CH_OPEN -> out=CH_MAX) ) ) &
(G (inp=CH_CLOSE) ->
X ( (inp=CH_CLOSE -> out=CH_NONE) U (inp=CH_OPEN & out!=CH_MAX) | G (inp=CH_CLOSE -> out=CH_NONE) ) )
-- Security Properties
-- Transport Layer Security
LTLSPEC NAME trans_sec := G ( (inp=SR_AUTH & out=SR_ACCEPT) ->
LTLSPEC NAME trans_sec := G ( hasReqAuth ->
O ( (inp=NEWKEYS & out=NO_RESP) &
O ( (inp=KEX30 & out=KEX31_NEWKEYS) &
O (out=KEXINIT) ) ) )
-- Authentication Layer Security
LTLSPEC NAME auth_sec := G ( (inp=CH_OPEN & out=CH_OPEN_SUCCESS) ->
LTLSPEC NAME auth_sec := G ( hasOpenedChannel ->
( out!=UA_FAILURE S out=UA_SUCCESS) )
-- Rekey Properties
-- Authenticated rekey is possible
LTLSPEC NAME auth_rekey_pos := G ( ( ( inp=CH_CLOSE & out=CH_CLOSE) | (inp=CH_OPEN & out=CH_OPEN_SUCCESS) | ( out=UA_SUCCESS) ) ->
( X (inp=KEXINIT -> out=KEXINIT & X (inp=KEX30 -> out=KEX31_NEWKEYS & X (inp=NEWKEYS -> out=NO_RESP) ) ) ) )
-- Authenticated state is preserved
LTLSPEC NAME auth_rekey_pres := G ( ( ( inp=CH_CLOSE & out=CH_CLOSE) | (inp=CH_OPEN & out=CH_OPEN_SUCCESS) | (inp=SR_AUTH & out=SR_ACCEPT) ) ->
( ( inp=NEWKEYS & out=NO_RESP & X ( inp=CH_OPEN ) ) -> X ( out=CH_OPEN_SUCCESS | out=CH_MAX) ) U (out=NO_CONN) |
( G ( ( inp=NEWKEYS & out=NO_RESP & X ( inp=CH_OPEN ) ) -> X ( out=CH_OPEN_SUCCESS | out=CH_MAX) )
& G ! (out=NO_CONN) ) )
-- Pre-auth rekey is possible
LTLSPEC NAME pre-auth_rekey_pos := G ( (inp=SR_AUTH & out=SR_ACCEPT) ->
( X (inp=KEXINIT -> out=KEXINIT & X ( inp=KEX30 -> out=KEX31_NEWKEYS & X (inp=NEWKEYS -> out=NO_RESP) ) ) ) )
-- Functional Properties
---- Preauth state is preserved
LTLSPEC G ( (inp=SR_AUTH & out=SR_ACCEPT) ->
( ( inp=NEWKEYS & out=NO_RESP & X ( inp=UA_PK_OK ) ) -> X ( out=UA_SUCCESS) ) U (out=NO_CONN | out=UA_SUCCESS) |
( G ( ( inp=NEWKEYS & out=NO_RESP & X ( inp=UA_PK_OK ) ) -> X ( out=UA_SUCCESS) )
& G ! (out=DISCONNECT | out=UA_SUCCESS) ) )
-- Pre-auth state is preserved
LTLSPEC NAME pre-auth_rekey_pres := G ( (inp=SR_AUTH & out=SR_ACCEPT) ->
( ( inp=NEWKEYS & out=NO_RESP & X ( inp=UA_PK_OK ) ) -> X ( out=UA_SUCCESS) ) U (out=NO_CONN | out=UA_SUCCESS) |
( G ( ( inp=NEWKEYS & out=NO_RESP & X ( inp=UA_PK_OK ) ) -> X ( out=UA_SUCCESS) )
& G ! (out=NO_CONN | out=UA_SUCCESS) ) )
-- Server sends DISCONNECT:
-- The sender MUST NOT send or receive any data after this message, and
-- the recipient MUST NOT accept any data after receiving this message.
LTLSPEC NAME trans_disc := G (out=DISCONNECT ->
X G (isDisconnected) )
-- Functional Properties
---- After sending a KEXINIT, the other side should not send another KEXINIT or SR_ACCEPT until it has sent NEWKEYS
LTLSPEC NAME trans_kexinit := G ( (out=KEXINIT) ->
X ( ( (out!=SR_ACCEPT & out!=KEXINIT) U (out=NEWKEYS | out=KEX31_NEWKEYS ) |
G (out!=SR_ACCEPT & out!=KEXINIT) & G ! (out=NEWKEYS | out=KEX31_NEWKEYS ) ) ) )
G (out!=SR_ACCEPT & out!=KEXINIT) ) ) )
-- If the server rejects the service request, it SHOULD send an
-- appropriate SSH_MSG_DISCONNECT message and MUST disconnect.
LTLSPEC NAME trans_sr := G ( (inp=SR_AUTH & out!=NO_CONN & state!=s0) ->
(out=SR_ACCEPT | (out=DISCONNECT & X G(inp=SR_AUTH -> out=NO_CONN) ) ) )
(out=SR_ACCEPT | out=DISCONNECT ) )
-- If the server rejects the authentication request, it MUST respond
-- with the following: SSH_MSG_USERAUTH_FAILURE. *It may also disconnect on failed unauth attempts
LTLSPEC NAME auth_ua_pre := G ( (inp=SR_AUTH & out=SR_ACCEPT) ->
( (inp=UA_PK_NOK -> out=UA_FAILURE) & (inp=UA_PK_OK -> out=UA_SUCCESS) ) U (out=UA_SUCCESS | out=NO_CONN | out=DISCONNECT) |
(G ( (inp=UA_PK_NOK -> out=UA_FAILURE) & (inp=UA_PK_OK -> out=UA_SUCCESS) ) & G !(out=UA_SUCCESS | out=NO_CONN | out=DISCONNECT) ) )
LTLSPEC NAME auth_ua_pre := G ( hasReqAuth ->
(inp=UA_PK_NOK | inp=UA_PW_NOK | inp=UA_NONE -> out=UA_FAILURE ) U (out=UA_SUCCESS | out=NO_CONN | out=DISCONNECT) |
G (inp=UA_PK_NOK | inp=UA_PW_NOK | inp=UA_NONE -> out=UA_FAILURE ) )
-- SSH_MSG_USERAUTH_SUCCESS MUST be sent only once. When
-- SSH_MSG_USERAUTH_SUCCESS has been sent, any further authentication
-- requests received after that SHOULD be silently ignored. *openssh sends UNIMPL, is that bad?
-- SSH_MSG_USERAUTH_SUCCESS MUST be sent only once.
LTLSPEC NAME auth_ua_post := G ( (out=UA_SUCCESS) ->
X ( (inp=UA_PK_OK | inp=UA_PK_NOK) -> out=NO_RESP) U (out=NO_CONN) |
(G X ( (inp=UA_PK_OK | inp=UA_PK_NOK) -> out=NO_RESP) & G !(out=NO_CONN) ) )
X G (out!=UA_SUCCESS) )
-- When SSH_MSG_USERAUTH_SUCCESS has been sent, any further authentication
-- requests received after that SHOULD be silently ignored. *openssh sends UNIMPL, is that bad?
LTLSPEC NAME auth_ua_post_strong := G (out=UA_SUCCESS ->
X ( ( authReq -> out=NO_RESP | out=NO_CONN) ) )
-- Upon receiving this message, a party MUST
-- send back an SSH_MSG_CHANNEL_CLOSE unless it has already sent this
......@@ -71,6 +70,6 @@ LTLSPEC NAME auth_ua_post := G ( (out=UA_SUCCESS) ->
-- party when it has both sent and received SSH_MSG_CHANNEL_CLOSE, and
-- the party may then reuse the channel number.
-- Had to add NEWKEYS and KEXINIT ins, strangely KEXINIT closes
LTLSPEC NAME conn_close := G ( (inp=CH_OPEN & out=CH_OPEN_SUCCESS) ->
LTLSPEC NAME conn_close := G ( hasOpenedChannel ->
( ( ( (inp=CH_CLOSE) -> (out=CH_CLOSE)) U (out=NO_CONN | inp=KEXINIT | out=CH_CLOSE) ) |
( G ( (inp=CH_CLOSE) -> (out=CH_CLOSE)) & G ! (out=NO_CONN | inp=KEXINIT | out=CH_CLOSE) ) ) )
\ No newline at end of file
( G ( (inp=CH_CLOSE) -> (out=CH_CLOSE)) ) ) )
\ No newline at end of file
......@@ -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 ->
......
......@@ -450,6 +450,20 @@ machine learning algorithms},
year = {2015}
}
@incollection{deRuiter16OpenSSL,
author="de Ruiter, Joeri",
editor="Brumley, Billy Bob and R{\"o}ning, Juha",
title="A Tale of the OpenSSL State Machine: A Large-Scale Black-Box Analysis",
bookTitle="Secure IT Systems: 21st Nordic Conference, NordSec 2016, Oulu, Finland, November 2-4, 2016. Proceedings",
series = "Lecture Notes in Computer Science",
year="2016",
publisher="Springer International Publishing",
pages="169--184",
volume="10014",
isbn="978-3-319-47560-8",
doi="10.1007/978-3-319-47560-8_11",
}
@techreport{Poll_rigorous_2011,
author = {Poll, Erik and Schubert, Aleksy},
citeulike-article-id = {13778664},
......
\section{The Secure Shell Protocol} \label{sec:ssh}
The Secure Shell Protocol (or SSH) is a protocol used for secure remote login and other secure network services over an insecure network. It is an application layer protocol running on top of TCP, which provides reliable data transfer, but does not provide any form of connection security. The initial version of SSH was superseded by a second version (SSHv2), as the former was found to contain design flaws~\cite{FutoranskyAttack} which could not be fixed without losing backwards compatibility. This work focuses on SSHv2.
The Secure Shell Protocol (or SSH) is a protocol used for secure remote login and other secure network services over an insecure network. It runs as an application layer protocol on top of TCP, which provides reliable data transfer, but does not provide any form of connection security. The initial version of SSH was superseded by a second version (SSHv2), after the former was found to contain design flaws which could not be fixed without losing backwards compatibility~\cite{FutoranskyAttack}. This work focuses on SSHv2.
SSHv2 follows a client-server paradigm. The protocol consists of three layers (Figure~\ref{fig:sshcomponents}):
\begin{enumerate}
\item The \textit{transport layer protocol} (RFC 4253~\cite{rfc4253}) forms the basis for any communication between a client and a server. It provides confidentiality, integrity and server authentication as well as optional compression.
\item The \textit{user authentication protocol} (RFC 4252~\cite{rfc4252}) is used to authenticate the client to the server.
\item The \textit{connection protocol} (RFC 4254~\cite{rfc4254}) allows the encrypted channel to be multiplexed in different channels. These channels enable a user to run multiple processes, such as terminal emulation or file transfer, over a single SSH connection.
\item The \textit{connection protocol} (RFC 4254~\cite{rfc4254}) allows the encrypted channel to be multiplexed in different channels. These channels enable a user to run multiple applications, such as terminal emulation or file transfer, over a single SSH connection.
\end{enumerate}
Each layer has its own specific messages. The SSH protocol is interesting in that outer layers do not encapsulate inner layers. This means that different layers can interact. Hence, it makes sense to analyze SSH as a whole, instead of analyzing its constituent layers independently. We review each layer, outlining the relevant messages which are later used in learning, and characterising the so-called \textit{happy flow} that a normal protocol
run follows.
At a high level, a typical SSH protocol run uses the three constituent protocols in the order given above: after the client establishes a TCP connection with the server, (1) the two sides use the transport layer protocol to negotiate key exchange and encryption algorithms, and use these to establish session keys which are then used to secure further communication; (2) the client uses the user authentication protocol to authenticate to the server; (3) the client uses the connection protocol to accesses services on the server, for example the terminal service.
At a high level, a typical SSH protocol run uses the three constituent protocols in the order given above: after the client establishes a TCP connection with the server, (1) the two sides use the transport layer protocol to negotiate key exchange and encryption algorithms, and use these to establish session keys, which are then used to secure further communication; (2) the client uses the user authentication protocol to authenticate to the server; (3) the client uses the connection protocol to access services on the server, for example the terminal service.
%Different layers are identified by their message numbers. These message numbers will form the basis of the state fuzzing. The SSH protocol is especially interesting because outer layers do not encapsulate inner layers. This means that different layers can interact. One could argue that this is a less systematic approach, in which a programmer is more likely to make state machine-related errors.
......@@ -24,7 +24,9 @@ At a high level, a typical SSH protocol run uses the three constituent protocols
\end{figure}
\subsection{Transport layer}\label{ssh-run-trans}
SSH runs over TCP, and provides end-to-end confidentialty and integrity using pseudo-random session keys. Once a TCP connection has been established with the server, these session keys are securely negotiated as part of a \textsl{key exchange} method, the first step of the protocol. Key exchange begins by the two sides exchanging their preferences for the key exchange algorithm used, as well as encryption, compression and hashing algorithms. Preferences are sent with a \textsc{kexinit} message. Subsequently, key exchange using the negotiated algorithm takes place. Following this algorithm, one-time session keys for encryption and hashing are generated by each side, together with an identifier for the session. Diffie-Hellman is the main key exchange algorithm, and the only one required for support by the RFC. Under the Diffie-Hellman scheme, \textsc{kex30} and \textsc{kex31} are exchanged and new session keys are produced. These keys are used from the moment the \textsc{newkeys} command has been issued by both parties. A subsequent \textsc{sr\_auth} requests the authentication service. The happy flow thus consists of the succession of the three steps comprising key exchange, followed up by a successful authentication service request. The sequence is shown in Figure~\ref{fig:hf-trans}.
SSH runs over TCP, and provides end-to-end confidentiality and integrity using session keys. Once a TCP connection has been established with the server, these session keys are securely negotiated using a \textsl{key exchange} algorithm, the first step of the protocol. The key exchange begins by the two sides exchanging their preferences for the key exchange algorithm to be used, as well as encryption, compression and hashing algorithms. Preferences are sent with a \textsc{kexinit} message.
%TODO How is the algorithm picked?
Subsequently, key exchange using the negotiated algorithm takes place. Following this algorithm, one-time session keys for encryption and hashing are generated by each side, together with an identifier for the session. The main key exchange algorithm is Diffie-Hellman, which is also the only one required by the RFC. For the Diffie-Hellman scheme, \textsc{kex30} and \textsc{kex31} are exchanged to establish fresh session keys. These keys are used from the moment the \textsc{newkeys} command has been issued by both parties. A subsequent \textsc{sr\_auth} requests the authentication service. The happy flow thus consists of the succession of the three steps comprising key exchange, followed up by a successful authentication service request. The sequence is shown in Figure~\ref{fig:hf-trans}.
\begin{figure}[!hb]
\includegraphics[scale=0.285]{hf-trans.pdf}
......@@ -32,7 +34,7 @@ SSH runs over TCP, and provides end-to-end confidentialty and integrity using ps
\label{fig:hf-trans}
\end{figure}
\textsl{Key re-exchange}~\cite[p. 23]{rfc4253}, or \textsl{rekeying}, is a near identical process, with the difference being that instead of taking place at the beginning, it takes place once session keys are already in place. The purpose is to renew session keys so as to foil potential replay attacks~\cite[p. 17]{rfc4251}. It follows the same steps as key exchange. Messages exchanged as part of it are encrypted using the old set of keys, messages exchanged afterward are encrypted using the new keys. A fundamental property of rekeying is that it should preserve the state; that is, after the rekeying procedure is complemeted, the protocol should be in the same state as
\textsl{Key re-exchange}~\cite[p. 23]{rfc4253}, or \textsl{rekeying}, is a near identical process, with the difference being that instead of taking place at the beginning, it takes place once session keys are already in place. The purpose is to renew session keys so as to foil potential replay attacks~\cite[p. 17]{rfc4251}. It follows the same steps as key exchange. Messages exchanged as part of it are encrypted using the old set of keys, messages exchanged afterwards are encrypted using the new keys. A fundamental property of rekeying is that it should preserve the state; that is, after the rekeying procedure is completed, the protocol should be in the same state as
it was before the rekeying started, with as only difference that new keys are now in use. %Some implementations are known not support rekeying in certain states of the protocol.
%We consider an 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.
......@@ -40,7 +42,8 @@ it was before the rekeying started, with as only difference that new keys are no
\subsection{Authentication layer}\label{ssh-run-auth}
Once a secure tunnl has been established, the client can authenticate. For this RFC 4252~\cite{rfc4252} defines four authentication methods (password, public-key, host-based and none). The authentication request includes a user name, service name and authentication data, which consists of both the authentication method as well as the data needed to perform the actual authentication, such the password or public key. The happy flow for this layer, as shown in Figure~\ref{fig:hf-auth}, is simply a single protocol step that results in a successful authentication. The messages \textsc{ua\_pw\_ok} and \textsc{ua\_pk\_ok} achieve this for respectively password or public key authentication. Figure~\ref{fig:hf-auth} presents the case for password authentication.
Once a secure tunnel has been established, the client can authenticate. For this, four authentication methods are defined in RFC 4252~\cite{rfc4252}: password, public-key, host-based and none. The authentication request includes a user name, service name and authentication data, which consists of both the authentication method as well as the data needed to perform the actual authentication, such as the password or public key. The happy flow for this layer, as shown in Figure~\ref{fig:hf-auth}, is simply a single protocol step that results in a successful authentication. The messages \textsc{ua\_pw\_ok} and \textsc{ua\_pk\_ok} achieve this for respectively password and public key authentication (see Figure~\ref{fig:hf-auth}).
%Figure~\ref{fig:hf-auth} presents the case for password authentication.
%We consider a user authentication layer state machine secure if there is no path from the unauthenticated state to the authenticated state without providing correct credentials.
\begin{figure}[!ht]
......@@ -52,7 +55,7 @@ Once a secure tunnl has been established, the client can authenticate. For this
\subsection{Connection layer}\label{ssh-run-conn}
Successful authentication makes services of the Connection layer available. The Connection layer enables the user to open and close channels of various types, with each type providing access to specific services. Of the various services available, we focus on the remote terminal over a session channel, a classica use of SSH. The happy flow consists of opening a session channel, \textsc{ch\_open}, requesting a ``pseudo terminal'' \textsc{ch\_request\_pty}, sending and managing data via the messages \textsc{ch\_send\_data}, \textsc{ch\_window\_adjust}, \textsc{ch\_send\_eof}, and eventually closing the channel via \textsc{ch\_close}, as depicted in Figure~\ref{fig:hf-conn}.
Successful authentication makes services of the connection layer available. The connection layer enables the user to open and close channels of various types, with each type providing access to specific services. Of the various services available, we focus on the remote terminal over a session channel, a classical use of SSH. The happy flow consists of opening a session channel, \textsc{ch\_open}, requesting a ``pseudo terminal'' \textsc{ch\_request\_pty}, sending and managing data via the messages \textsc{ch\_send\_data}, \textsc{ch\_window\_adjust}, \textsc{ch\_send\_eof}, and eventually closing the channel via \textsc{ch\_close}, as depicted in Figure~\ref{fig:hf-conn}.
\marginpar{\tiny Erik: to match this text, the figure should include a cycle
for \textsc{ch\_send\_data}, \textsc{ch\_window\_adjust}, \textsc{ch\_send\_eof}??}
......
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