diff --git a/learning_results.tex b/learning_results.tex index 068b73ddc6b5bd259f10d8f0aa606d5aefee0c58..593c358ebd19f59193d335a88cb6d7ece602b3d3 100644 --- a/learning_results.tex +++ b/learning_results.tex @@ -11,7 +11,7 @@ We have adapted the setting off timing parameters to each implementation. \begin{figure*} \centering - \includegraphics[scale=0.29]{ssh-server_cropped} + \includegraphics[scale=0.297]{ssh-server_cropped} \caption{Model of the OpenSSH server. {\normalfont States are collected in 3 clusters, indicated by the rectangles, where each cluster corresponds to one of the protocol layers. diff --git a/security_definitions.tex b/security_definitions.tex index 3ccbafd0b9f3d6a2a2078b0e875605f08142e5c7..38546788f397da054ddd6de7a86244aed5dc23d4 100644 --- a/security_definitions.tex +++ b/security_definitions.tex @@ -326,8 +326,8 @@ G ( hasOpenedChannel -> \subsection{Model checking results} -Table~\ref{tab:mcresults} presents model checking results. Crucially, the security properties hold for all three implementations. For BitVise, -as it buffered all responses during rekey (including \textsc{UA\_SUCCESS}) we had to adapt our properties slightly. +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}). In particular, we used {\dvauth} instead of $out=UA\_SUCCESS$ to suggest successful authentication. %\begin{center}\small