\procedure{$\O{Run2}(\n{state}, \n{ni})$}{
\pcparse \n{state} \pcas \left(\begin{array}{c}\n{U}, \n{v}, \n{V}, \n{ltk}, \n{acc}, \pclb\n{k}_\n{}, \n{ni}_\n{}, \pclb\n{nr}_\n{}, \n{kmac}_\n{}, \pclb\n{sid}_\n{}, \n{mess}\end{array}\right)\\
\pcassert \n{v} = \lit{true} \\
\pcassert \n{acc} = \O{none}\left(\O{Boolean}\right) \\
\pcassert \n{mess} = 0 \\
\n{nr} \stackrel{1}{\sample} \bin^{256}\\
 \n{k} \gets \O{\n{prf}}(\n{ltk}, \n{U}, \n{V}, \n{ni}, \n{nr}, \lit{true})\\
 \n{kmac} \gets \O{\n{prf}}(\n{ltk}, \n{U}, \n{V}, \n{ni}, \n{nr}, \lit{false})\\
 \n{tau} \gets \O{\n{mac}}(\n{kmac}, \n{nr}, 2)\\
 \n{sid} \gets \left(\begin{array}{c}\n{U}, \n{V}, \n{ni}, \n{nr}, \n{tau}\end{array}\right)\\
 \pcreturn \left(\begin{array}{c}\pclb\left(\begin{array}{c}\n{U}, \n{v}, \n{V}, \n{ltk}, \pclb\O{none}\left(\O{Boolean}\right), \pclb\O{some}\left(\n{k}\right), \pclb\O{some}\left(\n{ni}\right), \pclb\O{some}\left(\n{nr}\right), \pclb\O{some}\left(\n{kmac}\right), \pclb\O{some}\left(\n{sid}\right), \pclb1\end{array}\right), \pclb\left(\begin{array}{c}\n{nr}, \n{tau}\end{array}\right)\end{array}\right)\\
}
