\procedure{$\O{Run1}(\n{state})$}{
\pcparse \n{state} \pcas \left(\begin{array}{c}\n{U}, \n{u}, \n{V}, \n{ltk}, \n{acc}, \n{k}, \pclb\n{ni}_\n{}, \n{nr}, \n{kmac}, \n{sid}, \pclb\n{mess}\end{array}\right)\\
\pcassert \n{u} = \lit{false} \\
\pcassert \n{acc} = \O{none}\left(\O{Boolean}\right) \\
\pcassert \n{mess} = 0 \\
\n{ni} \stackrel{id2}{\sample} \bin^{256}\\
 \pcreturn \left(\begin{array}{c}\pclb\left(\begin{array}{c}\n{U}, \n{u}, \n{V}, \n{ltk}, \pclb\O{none}\left(\O{Boolean}\right), \pclb\n{k}, \pclb\O{some}\left(\n{ni}\right), \pclb\n{nr}, \n{kmac}, \n{sid}, 1\end{array}\right), \pclb\left(\begin{array}{c}\n{ni}\end{array}\right)\end{array}\right)\\
}
