\procedure{$\O{NewSession}(\n{U}, \n{u}, \n{V}, \n{kid})$}{
\pcassert (\n{LTK}[\n{kid}] \neq \O{none}\left(\bin^{256}\right)) \\
 \n{ctr}_\n{} \gets (\n{ctr}_\n{} + 1)\\
 \n{ltk} \gets \O{unwrap}\left(\n{LTK}[\n{kid}]\right)\\
 \n{State}[\n{ctr}_\n{}] \gets \O{some}\left(\left(\begin{array}{c}\n{U}, \n{u}, \n{V}, \n{ltk}, \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(\bin^{256}\right), \pclb\O{none}\left(\O{Tuple[..]}\right), \pclb0\end{array}\right)\right)\\
 \n{Fresh}[\n{ctr}_\n{}] \gets \n{H}[\n{kid}]\\
 \pcreturn \n{ctr}_\n{}\\
}
