Commit 7d54b2dc authored by Erik Poll's avatar Erik Poll
Browse files

.

parent fda79915
......@@ -53,8 +53,7 @@ their rules were tied to routines in the code, so had to be slightly adapted
to fit the different implementations. In contrast, our properties are
defined at an abstract level so do not need such tailoring. Moreover,
our black box approach approach means we can analyse any implemention
of SSH, not just C implementations. \marginpar{\tiny @Paul: do these
properties bear any resemblance of your LTL properties}
of SSH, not just C implementations.
Formal models of SSH in the form of state machines have been used
before, namely for a manual code review of OpenSSH
......
......@@ -12,10 +12,10 @@ Certain arrangements had to be made including the setting of timing parameters t
\begin{figure*}
\centering
\includegraphics[scale=0.30]{ssh-server}
\caption{OpenSSH server. States are collected in 3 clusters,
\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.
We eliminate redundant states and information induced by the {\dmapper}, as well as states present in successful rekey sequences. Wherever rekey was permitted, we replaced the rekey states and transitions by a single \textsl{REKEY SEQUENCE} transition. We also factor out edges common to states within a cluster. We replace common disconnecting edges, by one edge from the cluster to the disconnect state. Common self loop edges are colored, and the actual i/o information only appears on one edge. Transitions with similar start and end states are joined together on the same edge. Transition labels are kept short by regular expressions(UA\_* stands for all inputs starting with UA\_) or by factoring out common start strings. Green edges highlight the happy flow. }
We eliminate redundant states and information induced by the {\dmapper}, as well as states present in successful rekey sequences. Wherever rekey was permitted, we replaced the rekey states and transitions by a single \textsl{REKEY SEQUENCE} transition. We also factor out edges common to states within a cluster. We replace common disconnecting edges, by one edge from the cluster to the disconnect state. Common self loop edges are colored, and the actual i/o information only appears on one edge. Transitions with similar start and end states are joined together on the same edge. Transition labels are kept short by regular expressions(UA\_* stands for all inputs starting with UA\_) or by factoring out common start strings. Green edges highlight the happy flow. }}
\label{fig:sshserver}
\end{figure*}
......
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