security_definitions.tex 23.5 KB
Newer Older
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
1
\section{Security specifications} \label{sec:specs}
2

Paul Fiterau Brostean's avatar
updates  
Paul Fiterau Brostean committed
3 4
\newfloat{property}{thp}{lop}
\floatname{property}{Property}
5

6
The size models of the models makes them difficult to manually inspect and verify against specifications. Manual analysis is further complicated by the ambiguity present in textual specifications.
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
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 to verify security properties for the learned models, properties which we formalize using LTL formulas.  
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
8

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
9 10
NuSMV is a model checker where a model is specified as a set of finite variables, and a transition-function which makes 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. NuSMV models are generated automatically from the learned models. Generation proceeds by first defining in an empty NuSMV file three variables, corresponding to inputs, outputs and states. The transition-function is then extracted from the learned model and appended to the 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.
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
11

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32
%\parbox{\columnwidth}{
%  \parbox{0.5\columnwidth}{
%\begin{tikzpicture}[>=stealth',shorten >=1pt,auto,node distance=2.8cm]
%  \node[initial,state] (q0)      {$q_0$};
%  \node[state]         (q1) [right of=q0]  {$q_1$};
%
%  \path[->]          (q0)  	edge  						   node {INIT/OK} (q1);
%	\path[->]          (q0)  	edge  [loop above]   node {MSG/NOK} (q0);
%	\path[->]          (q1)  	edge  [loop above]   node {INIT/OK} (q1);
%  \path[->]          (q1)  	edge  [loop right] 	 node {MSG/ACK} (q1);
%\end{tikzpicture}	
%}
%\parbox{0.5\columnwidth}{
%\begin{verbatim}
%
%\end{verbatim}
%}
%}

%\lstset{showspaces=true}

Erik Poll's avatar
shit  
Erik Poll committed
33
\begin{figure}[h]
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
34 35 36 37 38 39 40 41 42 43 44 45 46 47 48
\centering
%\begin{subfigure}
\begin{tikzpicture}[>=stealth',shorten >=1pt,auto,node distance=2.8cm]
  \node[initial,state] (q0)      {$q_0$};
  \node[state]         (q1) [right of=q0]  {$q_1$};

  \path[->]          (q0)  	edge  						   node {INIT/OK} (q1);
	\path[->]          (q0)  	edge  [loop above]   node {MSG/NOK} (q0);
	\path[->]          (q1)  	edge  [loop above]   node {INIT/OK} (q1);
  \path[->]          (q1)  	edge  [loop right] 	 node {MSG/ACK} (q1);
\end{tikzpicture}
%\end{subfigure}
\\
\small
\begin{lstlisting}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
49 50
	MODULE main 
		VAR state : {q0, q1};
Frits Vaandrager's avatar
Frits Vaandrager committed
51
		inp : {BEGIN, MSG};
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
52 53 54
		out : {OK, NOK, ACK};
		ASSIGN
		init(state) := q0;
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
55
		next(state) := case
Frits Vaandrager's avatar
Frits Vaandrager committed
56
			state = q0 & inp = BEGIN: q1;
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
57
			state = q0 & inp = MSG: q0; 
Frits Vaandrager's avatar
Frits Vaandrager committed
58
			state = q1 & inp = BEGIN: q1;
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
59
			state = q1 & inp = MSG: q1; 
Frits Vaandrager's avatar
Frits Vaandrager committed
60 61 62 63 64
	    esac;
		out := case
			state = q0 & inp = BEGIN: OK;
			state = q0 & inp = MSG: NOK;
			state = q1 & inp = BEGIN: OK;
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
65 66
			state = q1 & inp = MSG: ACK;
		esac;
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
67 68 69 70 71
\end{lstlisting}

\caption{A Mealy Machine and its associated NuSMV model}
\label{fig:nusmvex}
\end{figure}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
72

Erik Poll's avatar
shit  
Erik Poll committed
73

74
The remainder of this section defines the properties we formalized and verified. We group these properties into four categories: 
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
75

Paul Fiterau Brostean's avatar
updates  
Paul Fiterau Brostean committed
76
\begin{enumerate}
77
\item \textit{basic characterizing properties}, properties which characterize the {\dmapper} and {\dsut} assembly at a basic level. These hold for all systems.
78 79
\item \textit{layer-critical security properties}, these are properties fundamental to achieving the main security goal of the respective layer.
\item \textit{key re-exchange properties}, that is properties regarding the key re-exchange operation (after the initial key exchange was done).
80
\item \textit{functional properties}, which are extracted from the SHOULD's and the MUST's of the RFC specifications. They may have a security impact.
Paul Fiterau Brostean's avatar
updates  
Paul Fiterau Brostean committed
81
\end{enumerate}
82

83
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}. 
84 85 86 87 88 89 90

\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}
91
\begin{lstlisting}[basicstyle=\footnotesize]
92 93 94 95 96 97 98 99 100 101 102 103
	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.

104
\subsection{Basic characterizing properties}
105

106
 %cannot be translated. %Though in practical terms, these results are still translatable, in particular for cases where properties are not met. 
107 108
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.
109 110 111

\begin{property}%[h]
\begin{lstlisting}[basicstyle=\footnotesize]
112 113
	G (out=NO_CONN -> 
		G (out=NO_CONN | out=CH_MAX | out=CH_NONE) )
114
\end{lstlisting}
115
\caption{One connection property}
116 117
\label{prop:noconn}
\end{property}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
118

119 120
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}.

121 122
\begin{property}%[h]
\begin{lstlisting}[basicstyle=\footnotesize]
123 124 125 126 127 128
	(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) ) ) 
129
\end{lstlisting}
130
\caption{Mapper induced channel property}
131 132
\label{prop:channel}
\end{property}
133

134
\subsection{Layer-critical security properties} 
135
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.
136

137
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. 
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
138

139 140 141
% SR_AUTH_AUTH -> SR_AUTH
% SR_AUTH_CONN -> SR_CONN
% SR_ACCEPT -> SR_ACCEPT
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
142 143


Paul Fiterau Brostean's avatar
updates  
Paul Fiterau Brostean committed
144
\begin{property}[h]
145
\begin{lstlisting}[basicstyle=\footnotesize]
146 147 148 149
	G ( hasReqAuth -> 
			O ( (inp=NEWKEYS & out=NO_RESP) & 
				O ( (inp=KEX30 & out=KEX31_NEWKEYS) & 
					O (out=KEXINIT) ) ) )
150
\end{lstlisting}
151
\caption{Transport layer security}
152
\label{prop:sec-trans}
Paul Fiterau Brostean's avatar
updates  
Paul Fiterau Brostean committed
153
\end{property}
154

155
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.
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
156

157

Paul Fiterau Brostean's avatar
updates  
Paul Fiterau Brostean committed
158
\begin{property}[h]
159
\begin{lstlisting}[basicstyle=\footnotesize]
160 161
	G ( hasOpenedChannel ->
		out!=UA_FAILURE S out=UA_SUCCESS )
162
\end{lstlisting}
163
\caption{Authentication layer security}
164
\label{prop:sec-auth}
Paul Fiterau Brostean's avatar
updates  
Paul Fiterau Brostean committed
165
\end{property}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
166

167
\subsection{Key re-exchange properties}
168 169
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. 
Paul Fiterau Brostean's avatar
updated  
Paul Fiterau Brostean committed
170

171
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}.
Paul Fiterau Brostean's avatar
updated  
Paul Fiterau Brostean committed
172 173
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
174 175 176 177
	G ( hasReqAuth -> 
		X (inp=KEXINIT -> out=KEXINIT & 
			X (inp=KEX30 -> out=KEX31_NEWKEYS & 
				X (inp=NEWKEYS -> out=NO_RESP) ) ) ) 
Paul Fiterau Brostean's avatar
updated  
Paul Fiterau Brostean committed
178
\end{lstlisting}
179 180
\caption{Rekey possible in pre-auth. state}
\label{prop:rpos-pre-auth}
Paul Fiterau Brostean's avatar
updated  
Paul Fiterau Brostean committed
181 182
\end{property}

183
Provided we perform successful finalization of a rekey, we remain in a pre-authenticated state until we exit this state, either by losing the connection (suggested by the \textsc{no\_conn} ) or by successful authentication (\textsc{ua\_success}). The latter is described in Property~\ref{prop:rper-pre-auth}. Note that, we can tell we are in a pre-authenticated state if authenticating with a valid public key results in success. W represents the Weak Until operator.
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
184 185 186

\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
187 188 189 190
	G ( hasReqAuth ->
		( (inp=NEWKEYS & out=NO_RESP & X inp=UA_PK_OK) -> 
			X out=UA_SUCCESS) 
		W (out=NO_CONN | out=UA_SUCCESS) )
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
191
\end{lstlisting}
Paul Fiterau Brostean's avatar
updated  
Paul Fiterau Brostean committed
192
\caption{Key exchange preserves pre-auth. state}
193
\label{prop:rper-pre-auth}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
194
\end{property}
195

196
%\textit{Perhaps this could be merged into one property?}
197

198
\subsection{Functional properties}
199 200 201 202 203 204 205 206 207 208 209 210 211 212
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.
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
213 214 215 216


\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
217 218 219
	G ( out=KEXINIT -> 
		X ( (out!=SR_ACCEPT & out!=KEXINIT) 
			W (out=NEWKEYS | out=KEX31_NEWKEYS) )	)
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
220
\end{lstlisting}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
221 222
\caption{Disallowed outputs after KEXINIT}
\captionsetup{font=small}
223
\label{prop:trans-kexinit}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
224 225
\end{property}

226
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.
Paul Fiterau Brostean's avatar
updated  
Paul Fiterau Brostean committed
227
% , 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.
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
228 229 230

\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
231 232
	G ( (inp=SR_AUTH & state!=s0) ->
		(out=SR_ACCEPT | out=DISCONNECT | out=NO_CONN ) ) )
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
233
\end{lstlisting}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
234
\caption{Allowed outputs after SR\_ACCEPT}
235
\label{prop:trans-sr}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
236 237
\end{property}

238

239 240 241 242 243

%\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. 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}. 
244 245
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
246 247 248 249
	G ( hasReqAuth  -> 
		X ( (inp=UA_PK_NOK | inp=UA_PW_NOK | inp=UA_NONE) 
			-> out=UA_FAILURE)
		W (out=UA_SUCCESS | output=NO_CONN) )
250
\end{lstlisting}
251 252
\caption{Invalid requests prompt UA\_FAILURE }
\label{prop:auth-pre-ua}
253 254
\end{property}

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
255 256
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
257 258
	G ( (out=UA_SUCCESS) ->
		X G (out!=UA_SUCCESS) )
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
259
\end{lstlisting}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
260
\caption{UA\_SUCCESS is sent at most once}
261
\label{prop:auth-post-ua-strong}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
262 263
\end{property}

264 265 266
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.
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
267 268
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
269 270 271
	G ( out=UA_SUCCESS -> 
		X ( ( authReq-> out=NO_RESP ) 
			W out=NO_CONN ) )
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
272
\end{lstlisting}
273 274

\caption{Silence after UA\_SUCCESS}
275
\label{prop:auth-post-ua}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
276
\end{property}
277
%\textit{Perhaps this could also be merged into one property?}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
278

279
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}. 
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
280 281 282

\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
283 284 285 286
	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) ) 
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
287
\end{lstlisting}
288
\caption{CH\_CLOSE response on CH\_CLOSE request}
289
\label{prop:conn-close}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
290
\end{property}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
291 292


293
%A problem was that the specification for each layer seemed to only consider messages specific to that layer. In particular, it didn't consider disconnect messages, that may be sent at any point in the protocol. For the Transport Layer, the RFC states that after sending a \textsc{kexinit} message, a party MUST not send \textsc{service\_request} or \textsc{sr\_accept} messages, until it has sent a \textsc{newkeys} message. This is translated to the LTL.
294

295
%On the same page, the RFC also states that in case the server rejects a service request, it should send an appropriate \textsc{disconnect} message. Moreover, in case it supports the service request, it MUST sent a \textsc{sr\_accept} message. If
296

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
297
%The Connection Layer RFC states that upon receiving a CH_CLOSE message, a side should send back a CH\_CLOSE message, unless it has already sent this message for the channel. This of course, ignores the case when a side disconnects, in which case a CH_CLOSE would no longer have to be issued. 
298 299

\subsection{Model checking results}
300 301
Table~\ref{tab:mcresults} presents model checking results. Crucially, all the critical security properties hold. 
%\begin{center}\small
302
%	\centering
Paul Fiterau Brostean's avatar
updated  
Paul Fiterau Brostean committed
303
\begin{table}
304 305
	\centering
	\small
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
306
	\begin{tabular}{| r | r | c |c | c |}
307
		\hline 
308 309 310 311 312 313
		          &   					 																	& 		\multicolumn{3}{c|}{\emph{SSH Implementation}}\\ \cline{3-5} 					
							&   Property 	 																	& OpenSSH	 & Bitvise	& Dropbear \\ \hline 
		Critical  &   Trans. 		 																	&          & 				 & 				 \\ \cline{2-5}
		    			&   Auth.      																	&  				 & 				 & 				 \\ \hline 
		Rekey 		&   Pre-auth.  																	&  				 &         &          \\ \cline{2-5}
		    			&   Auth.      																	&  				 &         &          \\ \hline 
314 315
		Functional&   Prop.~\ref{prop:trans-disc}							   	&  				 &         &          \\ \cline{2-5} 
							&   Prop.~\ref{prop:trans-kexinit}					   	&  				 &         &          \\ \cline{2-5} 
316 317
		    			&   Prop.~\ref{prop:trans-sr}										&  				 &         &          \\ \cline{2-5}
		    			&   Prop.~\ref{prop:auth-pre-ua} 								&  				 &         &          \\ \cline{2-5}
318
							&   Prop.~\ref{prop:auth-post-ua-strong}				&  				 &         &          \\ \cline{2-5}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
319
							&   Prop.~\ref{prop:auth-post-ua} 							&  				 &         &          \\ \cline{2-5}
320
		    			&   Prop.~\ref{prop:conn-close}  								&  				 &         &          \\ \hline 		
321
	\end{tabular}
Paul Fiterau Brostean's avatar
updated  
Paul Fiterau Brostean committed
322
	\caption{Model checking results}
323 324 325
	\label{tab:mcresults}
\end{table}
%\end{center}
326 327


Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
328 329

%, though key exchange is strangely not universally permitted, while some of the functional properties described are not met.