\procedure{$\O{NewSession}(\n{U}, \n{u}, \n{V}, \n{kid})$}{
\pcassert (\n{LTK}[\n{kid}] \neq \bot) \\
 \n{ctr}_\n{} \gets (\n{ctr}_\n{} + 1)\\
 \n{ltk} \gets \n{LTK}[\n{kid}]\\
 \n{State}[\n{ctr}_\n{}] \gets \left(\begin{array}{c}\n{U}, \n{u}, \n{V}, \n{ltk}, \bot, \bot, \bot, \bot, \pclb\bot, \bot, 0\end{array}\right)\\
 \n{Fresh}[\n{ctr}_\n{}] \gets \n{H}[\n{kid}]\\
 \pcreturn \n{ctr}_\n{}\\
}
