@@ -55,7 +55,7 @@ Table~\ref{tab:experiments} describes the exact versions of the systems analyzed
{\centering{\textbf{SUT}}}&\textbf{States}&\textbf{Hypotheses }&\textbf{Mem. Q.}&\textbf{Test Q.}\\\hline%& \textbf{Tests to last Hyp.} & \textbf{Tests on last Hyp.} \\ \hline
@@ -347,8 +347,8 @@ In particular, we used {\dvauth} instead of \textit{out=UA\_SUCCESS} to suggest
& Prop.~\ref{prop:trans-kexinit}& MUST &\dt&\dt&\dt\\\cline{3-6}
& Prop.~\ref{prop:trans-sr}& MUST &\dfce{sends unimpl}* &\dfce{kex no resp}&\dt\\\cline{3-6}
& Prop.~\ref{prop:auth-pre-ua}& MUST &\dt&\dt&\dt\\\cline{3-6}
& Prop.~\ref{prop:auth-post-ua-strong}& MUST &\dt&\dt&\dfce{can recon after rekey}\\\cline{3-6}
& Prop.~\ref{prop:auth-post-ua}& SHOULD &\dfce{sends unimpl}* &\dfce{sends unimpl}* &\df\\\cline{3-6}
& Prop.~\ref{prop:auth-post-ua-strong}& MUST &\dt&\dt&\dt\\\cline{3-6}
& Prop.~\ref{prop:auth-post-ua}& SHOULD &\dfce{sends unimpl}* &\dfce{sends unimpl}* &\dt\\\cline{3-6}
& Prop.~\ref{prop:conn-close}& MUST &\dt&\dt&\dfce{sends CH\_EOF}\\\hline
\end{tabular}
\caption{Model checking results}
...
...
@@ -363,8 +363,8 @@ Property~\ref{prop:auth-post-ua}. Whether the alternative behavior adapted is ac
does leave room for interpretation of the \textsc{unimpl} message.
DropBear is the only implementation that allows rekey in both general states of the protocol. DropBear also satisfies all Transport layer specifications, however,
problematically, it violates properties of the higher layers. Upon receiving \textsc{ch\_close}, it responds by \textsc{ch\_eof} instead of \text{ch\_close}, not respecting
Property~\ref{prop:conn-close}. Moreover, the output \textsc{ua\_success} can be generated multiple times, violating both Properties ~\ref{prop:auth-post-ua-strong} and
~\ref{prop:auth-post-ua}.
problematically, it violates the property of the Connection layer. Upon receiving \textsc{ch\_close}, it responds by \textsc{ch\_eof} instead of \textsc{ch\_close}, not respecting
Property~\ref{prop:conn-close}. %Moreover, the output \textsc{ua\_success} can be generated multiple times, violating both Properties ~\ref{prop:auth-post-ua-strong} and
%~\ref{prop:auth-post-ua}.
%, though key exchange is strangely not universally permitted, while some of the functional properties described are not met.