\korg supports three general attacker models: an attacker that can drop, replay, or reordering messages on a channel. Additionally, \korg supports user-defined attacker that insert arbitrary messages onto a channel. In this section we discuss the various details that go into each attacker model.

\subsection{Dropping Attacker Model}%
\label{sub:Dropping Attacker}

The first and most simple general attacker model \korg supports is an attacker that can \textit{drop} messages from a channel. The user specifies a "drop limit" value that limits the number of packets the attacker can drop from the channel. Note, a higher drop limit will increase the search space of possible attacks, thereby increasing execution time.

The dropper attacker model gadget \korg synthesizes works as follows. The gadget will nondeterministically choose to observe a message on a channel. Then, if the drop limit variable is not zero, it will consume the message. An example is shown in Figure \ref{lst:korg_drop}.



\subsection{Replaying Attacker Model}%
\label{sub:Replay Attacker}
The second attacker model \korg supports is an attacker that can observe and \textit{replay} messages back onto a channel. Similarly to the drop limit for the dropping attacker model, the user can specify a "replay limit" that caps the number of messages the attacker can replay back onto the specified channel. 

The dropper attacker model gadget \korg synthesizes works as follows. The gadget has two states, \textsc{Consume} and \textsc{Replay}. The gadget starts in the \textsc{Consume} state and nondeterministically reads (but not consumes) messages on the target channel, sending them into a local storage buffer. Once the gadget read the number of messages on the channel equivalent to the defined replay limit, its state changes to \textsc{Replay}. In the \textsc{Replay} state, the gadget nondeterministically selects messages from its storage buffer to replay onto the channel until out of messages. An example is shown in Figure \ref{lst:korg_replay}.


\subsection{Reordering Attacker Model}%
\label{sub:reordering Attacker}
Lastly, \korg supports an attacker model such that an attacker can \textit{reorder} messages on a channel. Like the drop and replay attacker models, the user can specify a "reordering limit" that caps the number of messages that can be reorderingd by the attacker on the specified channel.

The reordering attacker model gadget \korg synthesizes works as follows. The gadget has three states, \textsc{Init}, \textsc{Consume}, and \textsc{Replay}. The gadget begins in the \textsc{Init} state, where it arbitrarily chooses a message to start consuming by transitioning to the \textsc{Consume} state. When in the \textsc{Consume} state, the gadget consumes all messages that appear on the channel, filling up a local buffer, until hitting the defined reordering limit. Once this limit is hit, the gadget transitions into the \textsc{Replay} state. In the \textsc{Replay} state, the gadget nondeterministically selects messages from its storage buffer to replay onto the channel until out of messages. An example is shown in Figure \ref{lst:korg_reordering}.



\subsection{Custom Attacker Models}%
\label{sub:Custom Attacker Models}
While the drop, replay, and reordering attacker models as previously described have complex gadgets that \korg synthesizes with respect to a user-specified channel, \korg also supports the synthesis of gadgets with respect to user-defined inputs and outputs. The user defines an \textit{IO-file} denoting the specific input and output messages the attacker is capable of sending, and \korg generates a gadget capable of synthesizing attacks with respect to the user's specification. An example I/O file is given in Figure \ref{lst:io-file}, and the generated gadget is given in \ref{lst:io-file-synth}.


