Table~\ref{tab:mcresults} presents model checking results. Crucially, the security properties hold for all three implementations. For BitVise,
as it buffered all responses during rekey (including \textsc{UA\_SUCCESS}) we had to adapt our properties slightly.
Table~\ref{tab:mcresults} presents model checking results. Crucially, the security properties hold for all three implementations. We had to slightly adapt our properties for BitVise
as it buffered all responses during rekey (incl. \textsc{UA\_SUCCESS}).
In particular, we used {\dvauth} instead of $out=UA\_SUCCESS$ to suggest successful authentication.