\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{ni}_\n{}, \n{nr}_\n{}, \pclb\n{kmac}_\n{}, \pclb\n{sid}_\n{}, \n{mess}\end{array}\right)\\
\pcassert \n{v} = \lit{true} \\
\pcassert \n{acc} = \bot \\
\pcassert \n{mess} = 0 \\
\n{nr} \stackrel{1}{\sample} \bin^{256}\\
\n{kmac} \stackrel{\mathsf{\tiny{invoke}}}{\gets} \O{Eval}(\n{ltk}, \n{U}, \n{V}, \n{ni}, \n{nr}, \lit{false}) \pccomment{Pkg: Prf} \\
 \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}, \bot, \n{ni}, \n{nr}, \pclb\n{kmac}, \n{sid}, 1\end{array}\right), \pclb\left(\begin{array}{c}\n{nr}, \n{tau}\end{array}\right)\end{array}\right)\\
}
