\korg supports three general attacker models: an attacker that can drop, replay, or rearrange 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.

\begin{figure}[h]
\begin{lstlisting}[caption={Example dropping attacker model gadget}, label={lst:spin-model}]
chan cn = [8] of { int, int, int }; 

active proctype attacker_drop() {
int b_0, b_1, b_2;
byte lim = 3; // drop limit
MAIN:
  do
  :: cn ? [b_0, b_1, b_2] -> atomic {
    if
    :: lim == 0 -> goto BREAK;
    :: else ->
       cn ? b_0, b_1, b_2; // consume message on the channel
       lim = lim - 1;
       goto MAIN;
    fi
    }
  od
BREAK:
}
\end{lstlisting}
\end{figure}

\subsection{Replaying Attacker Model}%
\label{sub:Replay Attacker}
The second attacker model \korg supports is an attacker that can observe and 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. 

\jg{todo: describe impl more}

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

\subsection{Custom Attacker Models}%
\label{sub:Custom Attacker Models}
While the drop, replay, and rearrange 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.  
