\procedure{$\O{Test}(\n{ctr})$}{
\pcparse \n{State}[\n{ctr}] \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} = \lit{true} \\
\pcassert \n{Fresh}[\n{ctr}] \\
\pcassert \n{RevTested}[\n{sid}] = \bot \\
 \n{RevTested}[\n{sid}] \gets \lit{true}\\
\pcif \n{b} \pcthen\\
\pcind\n{k} \stackrel{id4}{\sample} \bin^{256}\\
\pcelse\\
\pcind\n{k} \stackrel{\mathsf{\tiny{invoke}}}{\gets} \O{Eval}(\n{ltk}, \n{U}, \n{V}, \n{ni}, \n{nr}, \lit{true}) \pccomment{Pkg: Prf} \\
 \pcreturn \n{k}\\
}
