\procedure{$\O{NewSession}(\n{U}, \n{u}, \n{V}, \n{kid})$}{
 \n{ctr}_\n{} \gets (\n{ctr}_\n{} + 1)\\
\n{hon} \stackrel{\mathsf{\tiny{invoke}}}{\gets} \O{Hon}(\n{kid}) \pccomment{Pkg: Prf} \\
 \n{State}[\n{ctr}_\n{}] \gets \left(\begin{array}{c}\n{U}, \n{u}, \n{V}, \n{kid}, \bot, \bot, \bot, \bot, \pclb\bot, 0\end{array}\right)\\
 \n{Fresh}[\n{ctr}_\n{}] \gets \n{hon}\\
 \pcreturn \n{ctr}_\n{}\\
}
