\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 \O{some}\left(\left(\begin{array}{c}\n{U}, \n{u}, \n{V}, \n{kid}, \pclb\O{none}\left(\O{Boolean}\right), \pclb\O{none}\left(\bin^{256}\right), \pclb\O{none}\left(\bin^{256}\right), \pclb\O{none}\left(\bin^{256}\right), \pclb\O{none}\left(\O{Tuple[..]}\right), \pclb0\end{array}\right)\right)\\
 \n{Fresh}[\n{ctr}_\n{}] \gets \O{some}\left(\n{hon}\right)\\
 \pcreturn \n{ctr}_\n{}\\
}
