\subsection{Full Korg Soundness and Completeness Proofs}%
\label{sub:korg_proofs}

\setcounter{theorem}{0} 
\begin{theorem}
  A process, as defined in Hippel et al., always directly corresponds to a Büchi automata.
\end{theorem}

\begin{proof}
  \jg{highly standard equivalence argument}
  
\end{proof}

\begin{theorem}
  Checking whether there exists an attacker under a given threat model, the R-$\exists$ASP problem as proposed in Hippel et al., is equivalent to B\"uchi Automata language inclusion (which is in turn solved by the \spin model checker).
\end{theorem}

\begin{proof}
  \jg{arguing the equivalence of buchi automata intersection and process composition}
  
\end{proof}

\begin{theorem}
Checking whether there exists an attacker for a given threat model, the R-$\exists$ASP problem as proposed in Hippel et al., is PSPACE-complete.
\end{theorem}

\begin{proof}
  \jg{cite lower bounds for natural proof systems}
  
\end{proof}

\subsection{Preventing Korg Livelocks}%
\label{sub:Preventing Korg Livelocks}
In general, there are two types of LTL properties: safety, and liveness. Informally, safety properties state "a bad thing never happens," and liveness properties state "a good thing always happens." 
Therefore, safety properties can be violated by finite traces, while liveness properties require infinite traces to be violated. 
When evaluating a \korg attacker model gadget against a \promela model and a liveness property, it is crucial to ensure the gadget has no cyclic behavior. If a \korg gadget has cyclic behavior in any way, it'll trivially violate the liveness 
property and produce a garbage attack trace. To prevent this, we make the following considerations.

First, we design our \korg gadgets such that they never arbitrarily send and consume messages to a single channel. Second, we allow \korg gadgets, 
which are always processing messages on channels, to arbitrarily "skip" messages on a channel if need be. To demonstrate the latter, consider the extension of the drop attacker model gadget in Figure \ref{lst:drop_passer}. We implement message skipping by arbitrarily stopping and waiting after observing a message on a channel; once the channel is observed changing lengths, the message is considered skipped and future messages can be consumed.

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

active proctype attacker_drop() {
int b_0, b_1, b_2, blocker;
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
    }
  // pass over a message on a channel as needed
  :: cn ? [b_0, b_1, b_2] -> atomic {
    // wait for the channel to change lengths
    // then, once it does, go to MAIN
    blocker = len(cn);
    do
    :: blocker != len(cn) -> goto MAIN;
    od
    }
  :: goto BREAK;
  od
BREAK:
}
\end{lstlisting}
\end{figure}


