\procedure{$\O{Test}(\n{ctr})$}{
\pcparse \O{unwrap}\left(\n{State}[\n{ctr}]\right) \pcas \left(\begin{array}{c}\n{U}, \n{u}, \n{V}, \n{ltk}, \n{acc}, \n{ni}, \n{nr}, \pclb\n{kmac}, \n{sid}, \n{mess}\end{array}\right)\\
\pcassert \n{acc} = \O{some}\left(\lit{true}\right) \\
\pcassert \O{unwrap}\left(\n{Fresh}[\n{ctr}]\right) \\
\pcassert \n{RevTested}[\O{unwrap}\left(\n{sid}\right)] = \O{none}\left(\O{Boolean}\right) \\
 \n{RevTested}[\O{unwrap}\left(\n{sid}\right)] \gets \O{some}\left(\lit{true}\right)\\
\pcif \n{b} \pcthen\\
\pcind\n{k} \stackrel{1}{\sample} \bin^{256}\\
\pcelse\\
\pcind \n{k} \gets \O{\n{prf}}(\n{ltk}, \n{U}, \n{V}, \O{unwrap}\left(\n{ni}\right), \O{unwrap}\left(\n{nr}\right), \lit{true})\\
 \pcreturn \n{k}\\
}
