Commit 388d280e authored by Frits Vaandrager's avatar Frits Vaandrager

minor edits sec prop section

parent 685a8267
......@@ -199,7 +199,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 unclear, 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 does not 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]
......@@ -207,12 +207,12 @@ expected outputs after a \textsc{disconnect}.
G ( out=DISCONNECT ->
X G (out=CH_NONE | out=CH_MAX | out=NO_CONN) )
\end{lstlisting}
\caption{Only {\dmapper} outputs after DISCONNECT}
\caption{No output 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.
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 output \textsc{kex31\_newkeys} means that the {\dsut} sends a \textsc{kex31} followed by a \textsc{newkeys}.
\begin{property}[h]
......@@ -226,13 +226,13 @@ The RFC states in~\cite[p. 24]{rfc4254} that after sending a \textsc{kexinit} me
\label{prop:trans-kexinit}
\end{property}
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.
The RFC also states \cite[p. 24]{rfc4254} 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.
% , 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.
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (inp=SR_AUTH & state!=s0) ->
(out=SR_ACCEPT | out=DISCONNECT | out=NO_CONN ) ) )
(out=SR_ACCEPT | out=DISCONNECT | out=NO_CONN )))
\end{lstlisting}
\caption{Allowed outputs after SR\_ACCEPT}
\label{prop:trans-sr}
......
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