learning_setup.tex 27.8 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
\section{Learning setup} \label{sec:setup}
%This chapter will cover the setup used to infer the state machines. We provide a general setup outline in Section~\ref{components}. The tested SSH servers are described in Section~\ref{suts}, which were queried with the alphabet described in Section~\ref{alphabet}. Section~\ref{setup-handling} will cover the challenging SUT behaviour faced when implementing the mapper, and the adaptations that were made to overcome these challenges. Section~\ref{layers-individual} will discuss the relation between state machines for individual layers and the state machine of the complete SSH protocol. The conventions on visualisation of the inferred state machines are described in Section~\ref{visualisation}.

%Throughout this chapter, an individual SSH message to a SUT is denoted as a \textit{query}. A \textit{trace} is a sequence of multiple queries, starting from a SUT's initial state. Message names in this chapter are usually self-explanatory, but a mapping to the official RFC names is provided in Appendix~\ref{appendixa}.

%\section{Components}\label{components}

The learning setup consists of three components: a \emph{learner}, \emph{mapper} and the SUT. The {\dlearner} generates abstract inputs, representing SSH messages. The {\dmapper} transforms these messages into well-formed SSH packets and sends them to the {\dsut}. The {\dsut} sends response packets back to the {\dmapper}, which in turn, translates these packets to abstract outputs. The {\dmapper} then sends the abstract outputs back to the learner. 


The learner uses LearnLib ~\cite{LearnLib2009}, a Java library implementing $L^{\ast}$ based algorithms for learning Mealy machines. The {\dmapper} is based on Paramiko, an open source SSH implementation written in Python\footnote{Paramiko is available at \url{http://www.paramiko.org/}}. We opted for Paramiko because its code is relatively well structured and documented. The {\dsut} can be any existing implementation of a SSH server. The {\dlearner} communicates with the {\dmapper} over sockets. A graphical representation of our setup is shown in Figure~\ref{fig:components}.
\begin{figure}
  \noindent\makebox[\textwidth]{\includegraphics[width=1.1\textwidth]{example-components.pdf}}
  \caption{The setup consists of a learner, mapper and SUT.}
  \label{fig:components}
\end{figure}

%figure

\subsection{The learning alphabet}
The learning alphabet comprises of input/output messages by which the {\dlearner} interfaces with the {\dmapper}. Section~\ref{sec:ssh} outlines essential inputs, while Table X provides a summary
of all messages available at each layer.

\subsection{The mapper}
The {\dmapper} must provide translation between abstract message representations and well-formed SSH messages. For this purpose, the {\dmapper} maintains update various state elements.
An example 

\subsection{Compacting SSH into a Mealy machine}
The 

is  also written in Java, and interprets and inverts a mapper. The network adapter is a Python program based on Scapy \cite{Scapy}, Pcapy \cite{Pcapy}, and Impacket \cite{Impacket}. 
It uses Scapy to craft TCP packets, and Scapy together with a Pcapy and Impacket based sniffer to intercept responses.

In order to infer state machines, the learner needs to query the SUT. We use LearnLib\footnote{More information on LearnLib is available at \url{http://learnlib.de/}}, a Java library for automata learning, as a basis for our learner. The L* algorithm implemented in LearnLib can only handle abstract messages, and can neither output nor process actual SSH network traffic. The mapper translates abstract message representations to well-formed SSH messages. 

Drafting a mapper proved to be non-trivial. Because the mapper needs to participate in an SSH session, it should be able to engage in processes such as key exchange and authentication, and has to support features such as encryption and compression. For this thesis, an open source SSH implementation was used as a starting point for the implementation of the mapper. We used the Python-written Paramiko package\footnote{Paramiko is available at \url{http://www.paramiko.org/}} because its code is relatively well-structured. 

The convenience of using existing code comes at a cost. Since Paramiko features a state machine of its own, normal execution of the Paramiko code will result in messages being sent, received, interpreted and rejected without an explicit order to do so. We therefore altered the package so that it only sends queries when explicitly told to by the learner, and accepts all response messages. The message numbers as defined by the RFC~\cite{rfc4250} are used to map response messages to an abstract representation that the learner can interpret. 

Although all messages are accepted and returned to the learner, the mapper still needs a minimal state machine of its own. The mapper state will only be changed if necessary for participation in the protocol's execution. In other words: the mapper only processes and records the contents of a SUT's response when strictly needed. For example, when a SUT sends an \textsc{discon} or \textsc{debug} message, the mapper does nothing but return the abstract representation to the leaner. Keeping the mapper's message interpretation to a minimum allows the learner to interpret the SUT's state machine without the mapper cluttering the results. Some response message, however, do need to be interpreted by the mapper in order to participate in the SSH protocol. These messages can be found in Table~\ref{table:state}. The mapper's own state consists of the information saved upon receiving these messages.

The mapper communicates with the leaner over a socket connection and implements a simple protocol. It interprets abstract message representations (for example, ``\textsc{kexinit}") as well as a special reset command, which is used to revert the SUT to the initial state. This is effectively done by terminating the connection to the SUT and initializing a new one. 
\begin{table}[!ht]
\centering
\begin{tabular}{ll}
\textbf{Message} & \textbf{Influence on mapper state} \\
\textsc{kexinit} & Saves SUT's parameter preferences\tablefootnote{The parameters that must be supported according to the RFCs to ensure interoperability are used if no \textsc{kexinit} has been received.}. \\
\textsc{kex31} & Saves the exchange hash resulting from key exchange. \\
\textsc{newkeys} & Takes in use new keys for all outgoing messages\tablefootnote{Silently ignored when key exchange has not yet been completed.}. \\
\textsc{ch\_accept} & Saves the channel identifier, used in some queries\tablefootnote{Zero is used if no \textsc{ch\_accept} has been received.}. \\
\textit{any} & Saves the sequence number, used for the \textsc{unimpl} query\tablefootnote{Zero is used if no message has been received.}. \\
\end{tabular}
\caption{State-changing responses implemented by the mapper. These combinedly result in the mapper's state.}
\label{table:state}
\end{table}

As soon as the learner builds a state machine hypothesis, it uses the equivalence oracle to check the hypothesis' adequateness. We used a random-walk algorithm, which uses 2000 randomly constructed traces containing ten to fifteen queries each. Although this does not guarantee model correctness (no oracle can be absolutely conclusive in a black-box testing setup), it gives us reasonable confidence that the model is correct. More complex state machines will need other algorithms\footnote{An overview of LearnLib's equivalence oracles can be found on \\ \url{https://learnlib.github.io/learnlib/maven-site/0.9.1/apidocs/de/learnlib/eqtests/basic/package-summary.html}} or parameters to find counterexamples, but we deem these parameters adequate for the state machines found in Chapter~\ref{results}. 

\section{SUTs}\label{suts}
Six SSH servers have been tested. They can be found in Table~\ref{tested-suts}. Unfortunately, no recent figures are available on their market share. There is little doubt, however, that OpenSSH is the market leader. The OpenSSH project reported\footnote{Data are available on \url{http://www.openssh.com/usage/graphs.html}} over 80\% market share for their server in 2008 and it has been the default server on many UNIX-based operating systems for years. DropBear is an alternative to OpenSSH and was designed to be a drop-in replacement for low resource systems. It is the server of choice for routers running OpenWRT. Bitvise and PowerShell are Windows-only clients, with the latter providing Window's PowerShell as emulated terminal. The company of SSH's founding father Tatu Ylönen markets Tectia, which is available on various platforms. Cisco's high-end networking hardware ships with their IOS operating system, which has a build-in proprietary SSH client.


\begin{table}[!hb]
\centering
\begin{tabular}{lllll}
\textbf{Name} & \textbf{Developer}          & \textbf{Version} & \textbf{Platform} & \textbf{License} \\
OpenSSH       & OpenBSD Project         & 6.9p1-2          & UNIX-based        & BSD              \\
DropBear      & Matt Johnston               & 2014.65-1        & UNIX-based        & MIT              \\
Bitvise       & Bitvise                     & 6.45             & Windows           & Proprietary      \\
PowerShell    & N Software                  & 6.0.5732         & Windows           & Proprietary      \\
Tectia        & SSH Comm. Sec. & 6.4.12.353       & Various    & Proprietary      \\
CiscoSSH      & Cisco                       & 1.25          & Cisco IOS         & Proprietary     
\end{tabular}
\caption{The SSH implementations tested in this thesis.}
\label{tested-suts}
\end{table}
\clearpage
In our setup, we ran OpenSSH and DropBear on the same operating system as the mapper. CiscoSSH ran on a Catalyst 3550 switch, and other SUTs were executed in a virtual machine. Of course, SUTs can run on any system as long as it accepts incoming connections from the mapper. However, querying over localhost is preferable because it reduces timing differences. 

In their default configuration, all of the SUTs support (only) SSH version~2. Furthermore, all SUTs support our alphabet defined in Section~\ref{alphabet}, with the exception of CiscoSSH, which does not support public key authentication\footnote{IOS supports public key authentication since version 15, while the Catalyst switch runs on IOS 12.2(46)SE.}. 

\begin{figure}[!ht]
  \begin{center}
    \includegraphics[width=0.95\textwidth]{imgs/3550.jpg}
    \caption{The Catalyst 3550 used for testing.}
    \label{fig:catalyst}
  \end{center}
\end{figure}

\section{Alphabet}\label{alphabet}
Learning time tends to grow rapidly as the input alphabet grows. It is therefore important to focus on messages for which interesting state-changing behaviour can be expected. As a general principle, we therefore chose not to query protocol messages that are not intended to be sent from a client to a server\footnote{Applying this principle to the RFC's messages results in not including \textsc{service\_accept}, \textsc{ua\_accept}, \textsc{ua\_failure}, \textsc{ua\_banner}, \textsc{ua\_pk\_ok}, \textsc{ua\_pw\_changereq}, \textsc{ch\_success} and \textsc{ch\_failure} in our alphabet.}. 

Applying this ``outgoing only'' principle to the transport layer results in the messages of Table~\ref{trans-alphabet}\footnote{A mapping to the official RFC names is provided in Appendix~\ref{appendixa}.}. The only message that is out of the ordinary is \textsc{guessinit}. This is a special instance of \textsc{kexinit} for which \texttt{first\_kex\_packet\_follows} is enabled~\cite[p. 17]{rfc4253}. Our mapper can only handle correct key guesses, so the wrong-guess procedure as described in ~\cite[p. 19]{rfc4253} was not supported. When needed, SUTs were configured to make this guess work by altering their cipher preferences. The SSH version and comment string (described in Section~\ref{ssh-run-trans}) was not queried because it does not follow the binary packet protocol.

\begin{table}[!ht]
\centering
\begin{tabular}{ll}
\textbf{Message} & \textbf{Description} \\
\textsc{discon} & Terminates the current connection~\cite[p. 23]{rfc4253} \\
\textsc{ignore} & Has no intended effect~\cite[p. 24]{rfc4253} \\
\textsc{unimpl} & Intended response to an unimplemented message~\cite[p. 25]{rfc4253} \\
\textsc{debug} & Provides other party with debug information~\cite[p. 25]{rfc4253} \\
\textsc{kexinit} & Sends parameter preferences~\cite[p. 17]{rfc4253} \\
\textsc{guessinit} & A \textsc{kexinit} after which a guessed \textsc{kex30} follows~\cite[p. 19]{rfc4253} \\
\textsc{kex30} & Initializes the Diffie-Hellman key exchange~\cite[p. 21]{rfc4253} \\
\textsc{newkeys} & Requests to take new keys into use~\cite[p. 21]{rfc4253} \\
\textsc{sr\_auth} & Requests the authentication protocol~\cite[p. 23]{rfc4253} \\
\textsc{sr\_conn} & Requests the connection protocol~\cite[p. 23]{rfc4253}
\end{tabular}
\caption{Alphabet used to query the transport layer.}
\label{trans-alphabet}
\end{table}

For the user authentication layer, applying our ``outgoing only'' principle results in just one message: the authentication request~\cite[p. 4]{rfc4252}. Its parameters contain all information needed for authentication. As stated in Section~\ref{ssh-run-auth}, four authentication methods exist: none, password, public key and host-based. Our mapper supports all methods except the host-based authentication because various SUTs lack support for this feature. As shown in Table~\ref{auth-alphabet}, both the public key as well as the password method have a \textsc{ok} and \textsc{nok} variant which provides respectively correct and incorrect credentials. 

\begin{table}[!ht]
\centering
\begin{tabular}{ll}
\textbf{Message} & \textbf{Description} \\
\textsc{ua\_none} & Authenticates with the ``none'' method~\cite[p. 7]{rfc4252} \\
\textsc{ua\_pk\_ok} & Provides a valid name/key combination~\cite[p. 8]{rfc4252} \\
\textsc{ua\_pk\_nok} & Provides an invalid name/key combination~\cite[p. 8]{rfc4252} \\
\textsc{ua\_pw\_ok} & Provides a valid name/password combination~\cite[p. 10]{rfc4252} \\
\textsc{ua\_pw\_nok} & Provides an invalid name/password combination~\cite[p. 10]{rfc4252} \\
\end{tabular}
\caption{Alphabet used to query the user authentication layer.}
\label{auth-alphabet}
\end{table}

The connection protocol allows the client to request different processes over a single channel. Our mapper only implements requesting terminal emulation because availability of other processes depends heavily on a SUTs configuration. Moreover, little security-relevant information is expected to be gained by thoroughly testing other process requests. Combining this premise with the aforementioned ``outgoing only'' principle resulted in the alphabet of Table~\ref{conn-alphabet}. 

\begin{table}[!ht]
\centering
\begin{tabular}{ll}
\textbf{Message} & \textbf{Description} \\
\textsc{ch\_open} & Opens a new channel~\cite[p. 5]{rfc4254} \\
\textsc{ch\_close} & Closes a channel~\cite[p. 9]{rfc4254} \\
\textsc{ch\_eof} & Indicates that no more data will be sent~\cite[p. 9]{rfc4254} \\
\textsc{ch\_data} & Sends data over the channel~\cite[p. 7]{rfc4254} \\
\textsc{ch\_edata} & Sends typed data over the channel~\cite[p. 8]{rfc4254} \\
\textsc{ch\_window\_adjust} & Adjusts the window size~\cite[p. 7]{rfc4254} \\
\textsc{ch\_request\_pty} & Requests terminal emulation~\cite[p. 11]{rfc4254} \\
\end{tabular}
\caption{Alphabet used to query the connection layer.}
\label{conn-alphabet}
\end{table}

\section{Challenging SUT behaviour}\label{setup-handling}
Creating a mapper proved to be difficult, with three types of SUT behaviour being especially challenging. We will elaborate on how our mapper handles issues with regard to non-determination, receiving multiple responses and non-termination. 

\subsection{Non-determinism}\label{challenging-nondeterminism}
The learner expects that the a SUT behaves deterministically. In reality, however, the SSH protocol and its implementations exhibit non-deterministic behaviour. Sources of this behaviour can be divided into three categories:

\begin{enumerate}
\item SSH's \textit{protocol design} is inherently non-deterministic. Firstly, because underspecification leads to multiple options for developers, from which one can be selected in a non-deterministic manner. Secondly, because non-deterministic behaviour directly results from the specifications. An example of the latter is allowing to insert \textsc{debug} and \textsc{ignore} messages at any given time.

\item \textit{Response timing} is a source of non-determinism as well. If a SUT does not reply within a predefined time-out, the mapper assumes that no response will follow. If the time-out is of similar order of magnitude as the SUTs response time, timing variances will cause some queries to result in a response while others do not. In general, we want the time-out to be significantly higher than the average response time\footnote{Note that if the time-out is lower than the response time, the SUT behaves deterministically but the resulting model will note adequately describe the SUT's state machine.}. 

\item Other \textit{timing-related quirks} can cause non-deterministic behaviour as well. Some SUTs behave unexpectedly when a new query is received shortly after the previous one. For example, a trace in which a valid user authentication is performed within five milliseconds after an authentication request on DropBear can cause the authentication to (wrongly) fail.  
\end{enumerate}

With regard to the \textit{protocol design}: although the protocol allows for quite some non-deterministic constructs in theory, most SUTs seem to behave deterministically when it comes to what message they send. Tectia and Bitvise sometimes send seemingly random \textsc{ignore} and \textsc{debug} messages, but these could be easily filtered without influencing the structure of the state machine. 

With regard to the \textit{timing}: timing issues proved to be difficult to tackle. To detect non-determinism, the learner has been extended with a SQLite-based trace and response log. For any (sub)trace, the learner checks if the SUT's response matches earlier responses. In case of non-determinism, an exception is thrown and manual investigation is needed. This manual investigation typically leads to changing the delays and time-outs. For debugging purposes, the mapper also accepts complete traces as input. For example, the command ``20 \textsc{kexinit kex30 newkeys} reset" repeats the key exchange 20 times, so that variances in responses can be easily spotted. Because responses to some queries (such as authentication requests) need substantially more time, the mapper allows the time-out to be set based on the type of query. 

\subsection{Multiple responses}\label{challenging-multiple}

In a Mealy machine, an input from a given state leads to a single output. In practise, however, a SUT might respond with more than one message. For example, Tectia sends three messages (\textsc{ignore}, \textsc{ua\_banner} and \textsc{ua\_success}) in response to a single successful authentication request. If our mapper would only read the first message, other messages would appear as if they are responses to subsequent queries. 

The mapper has been altered to successfully deal with multiple response-behaviour. The abstract representation returned to the learner is the concatenation of all responses received within the message time-out period. The response to the aforementioned authentication query on Tectia will thus be presented to the learner as \textsc{ignore+ua\_banner+ua\_success}. By using this method, we make sure that there are no subsequent messages in the socket pipeline when querying for new responses. 

Waiting for multiple responses comes at a cost. Whereas a single response-approach allows to return the message to the learner as soon as a response is received, our altered mapper has to wait for subsequent messages. The waiting times quickly accumulate and result in a significantly slower learning process. To speed up learning, the learner has been altered so that it can query the trace and response log mentioned in Section~\ref{challenging-nondeterminism}. If a cached trace is available, the mapper need not be queried. This did not only improve learning speed, it also provides a way to store learned traces to quickly resume the learning process later on.

An important observation has to be made with regard to the asynchronous nature of message exchange in SSH~\cite{Poll2011Rigorous}. Neither the client nor the server needs to wait for a certain timeslot in order to transmit. Moreover, there is no requirement to receive and process queued messages before transmitting new ones. This results in a protocol in which, for example, both the server and the client can have the impression that they sent their version number before receiving the version number of their counterpart. This is an inherent property of the SSH protocol, and receiving multiple responses does not change this behaviour. This did not prove to be a major limitation in our setup, since this behaviour does not alter the structure of inferred state machines. 

\subsection{Non-termination}\label{challenging-nontermination}

Mealy machines are unable to adequately model buffers in a protocol. Automata such as register machines are able to effectively model buffers, but are not supported by L*. Buffers should therefore be removed at the mapper-level. 

We have encountered buffers in two occasions. Firstly, some implementations buffer certain responses, such as the \textsc{accept} message, when in key re-exchange. As soon as rekeying completes, these queued messages are released all at once. This leads to a \textsc{newkeys} message (indicating rekeying has completed), directly followed by all buffered messages. Buffer-behaviour can also be observed when opening and closing channels, since a SUT can close only as many channels as have previously been opened. 

Buffers are hard to detect since LearnLib does not release intermediate results while building a state machine hypothesis. In other words, an observer has no way to know whether the learner is expanding on a buffer and will consequentially never terminate. To detect this behaviour, we let the learner regularly extract and display the response alphabet size from the trace and response log. 

The multiple responses resulting from buffers are concatenated into one message as described in Section~\ref{challenging-multiple}. An example of such a message is \textsc{newkeys+accept+accept+accept}. Consequently, the response alphabet will quickly grow. As soon as this happens, the mapper gives a warning and the learning process can be halted to investigate the buffer.

Generic countermeasures were also added to correct buffering behaviour. If a response is identical to the one received before within the same message time-out, an asterisk is appended. Subsequent identical messages are discarded. The \textsc{newkeys+accept+accept+accept} response will thus be returned to the learner as \textsc{newkeys+accept*}. From the learners perspective, this effectively removes the buffer. 

A SUT can only close as many channels as previously have been opened, which faces the learner with a buffer as well. We therefore restricted the number of simultaneously open channels to one. The mapper returns a custom response \textsc{ch\_max} for every subsequent \textsc{ch\_open}. These \textsc{ch\_max} messages are filtered from the state machine representation.

\section{Inferring individual layers}\label{layers-individual}
Initially, the setup was used to infer a state machine in which all three layers (transport, user authentication and connection) of the SSH protocol were combined. There are multiple reasons as to why this has proven to be infeasible. 

Firstly, the number of states tends to grow quickly when combining all layers. Given the timing restrictions we had to keep in mind to prevent non-determinism, inferring and validating the combined state machines could easily end up taking days. This would not have been an insurmountable problem if the implementations behaved fully Mealy machine-compliant but, as described in Section~\ref{challenging-nontermination}, in many cases they do not. Unexpected buffers in the protocol's implementation become increasingly difficult to detect and prevent as different layers start interacting.

The lack of choke points between protocol layers makes SSH an especially difficult protocol to infer. This means that there is no point after which it can be safely assumed that previously ran layers will no longer interact. Rekeying poses the most notable example, in which a sequence of three transport layer messages could be sent at any given time during execution of a higher layer. 

In one of our earlier attempts to infer a combined state machine, our setup was able to detect rekeying, but unable to detect that rekeying preserves the state in the higher layers. A schematic overview of this behaviour is shown in Figure~\ref{fig:rekey-correct-incorrect}. A model in which the state is not preserved after rekeying is erroneous, since it implies that the server has no information on authentication and channels any more as soon as rekeying completes.

Although a human observer will easily notice the rekeying pattern (\textsc{kexinit}; \textsc{kex30}; \textsc{newkeys}), LearnLib's L* cannot recognize nor anticipate on the repetition of such patterns. It is trivial to see that this behaviour results in an exploding number of states as soon as the number of higher-layer states increases.
In order to still make some observations on the security-wise interesting rekey operation, we add a \textsc{rekey} to the user authentication and connection alphabet. This operations implements the messages \textsc{kexinit}; \textsc{kex30}; \textsc{newkeys} as an atomic operation. By performing an entire rekey procedure at once, we can deduce when rekeying succeeds and whether this correctly preserves state.

\begin{figure}[!ht]
  \noindent\makebox[\textwidth]{\includegraphics[width=0.75\textwidth]{imgs/example-rekey.pdf}}
  \caption{State machines showing state preserving (left) and non-state preserving (right) rekeying. A adequate model should correctly preserve state.}
  \label{fig:rekey-correct-incorrect}
\end{figure}

One could wonder what the combined state machine for the three different layers would look like. On secure implementations, the transport and user authentication layer need to complete before the connection layer starts. It will thus not be a parallel composition of three layers running independently, as would be the case when, for example, three different OSI-layers would be considered. The key re-exchange, however, causes the protocol to not be entirely sequential either. Without providing an airtight formal definition, the combined state machine $SM_{ssh}$ would look something like:\\

$SM_{ssh} = SM_{trans}; (SM_{trans} \times SM_{auth}); (SM_{trans} \times SM_{conn})$

\section{State machine visualisation}\label{visualisation}
As soon as our setup finishes learning, it outputs the state machine as a GraphViz\footnote{More information on GraphViz is available at \url{http://www.graphviz.org/}} file. Various alterations are applied to improve readability while keeping the machines unequivocal. State machines in various stages of this visualisation process have been attached in Appendix~\ref{appendixb} for the interested reader.

A slightly altered version of Python's Pydot\footnote{Pydot is available at \url{https://pypi.python.org/pypi/pydot}} package is used to merge labels of edges that span between the same nodes. Subsequently, \textsc{other} and \textsc{any} representations are added in order to merge queries that result in similar responses. To keep the machine unambiguous, a node can have at most one outgoing edge with an \textsc{other} label. If no confusion is possible, the \textsc{any/no\_conn} label will be omitted. 

Queries using the \textsc{ignore} and \textsc{debug} message are removed from the representations because they never resulted in a state change. The same applies to the \textsc{unimpl} message on all SUTs except DropBear and Tectia. Green edges were added to denote each layer's happy flow\footnote{Happy flows are defined in Section~\ref{ssh-run}.}.