\procedure{$\O{Eval}(\n{h}, \n{a}, \n{aa}, \n{c}, \n{d}, \n{e})$}{
\pcassert (\n{LTK}[\n{h}] \neq \bot) \\
\pcif \left(\n{H}[\n{h}] = \lit{false} \vee \neg \n{b}\right) \pcthen\\
\pcind \n{k} \gets \n{LTK}[\n{h}]\\
\pcind \pcreturn \O{\n{prf}}(\n{k}, \n{a}, \n{aa}, \n{c}, \n{d}, \n{e})\\
\pcif \n{PRF}[\left(\begin{array}{c}\n{h}, \n{a}, \n{aa}, \n{c}, \n{d}, \n{e}\end{array}\right)] = \bot \pcthen\\
\pcind\n{temp} \stackrel{id5}{\sample} \bin^{256}\\
\pcind \n{PRF}[\left(\begin{array}{c}\n{h}, \n{a}, \n{aa}, \n{c}, \n{d}, \n{e}\end{array}\right)] \gets \n{temp}\\
\pcind \pcreturn \n{temp}\\
 \n{y} \gets \n{PRF}[\left(\begin{array}{c}\n{h}, \n{a}, \n{aa}, \n{c}, \n{d}, \n{e}\end{array}\right)]\\
 \pcreturn \n{y}\\
}
