\procedure{$\O{Run4}(\n{state}, \n{msg})$}{
\pcparse \n{state} \pcas \left(\begin{array}{c}\n{U}, \n{v}, \n{V}, \n{ltk}, \n{acc}, \n{k}, \pclb\n{ni}_\n{}, \n{nr}, \n{kmac}, \n{sid}, \pclb\n{mess}\end{array}\right)\\
\pcassert \n{v} = \lit{true} \\
\pcassert \n{acc} = \bot \\
\pcassert \n{mess} = 1 \\
\pcparse \n{msg} \pcas \left(\begin{array}{c}\n{ni}, \n{tau}\end{array}\right)\\
\pcif \left(\begin{array}{c}\phantom{ \wedge }\O{\n{mac}}(\n{kmac}, \n{ni}, 3) = \n{tau}\pclb \wedge \n{ni} = \n{ni}_\n{}\end{array}\right) \pcthen\\
\pcind \n{acc} \gets \lit{true}\\
\pcind \n{tau}_\n{} \gets \O{\n{mac}}(\n{kmac}, \n{zeron}, 4)\\
\pcind \pcreturn \left(\begin{array}{c}\pclb\left(\begin{array}{c}\n{U}, \n{v}, \n{V}, \n{ltk}, \n{acc}, \n{k}, \pclb\n{ni}_\n{}, \n{nr}, \n{kmac}, \n{sid}, 2\end{array}\right), \pclb\left(\begin{array}{c}\n{tau}_\n{}\end{array}\right)\end{array}\right)\\
\pcelse\\
\pcind \n{acc} \gets \lit{false}\\
\pcind \pcreturn \left(\begin{array}{c}\pclb\left(\begin{array}{c}\n{U}, \n{v}, \n{V}, \n{ltk}, \n{acc}, \n{k}, \pclb\n{ni}_\n{}, \n{nr}, \n{kmac}, \n{sid}, 2\end{array}\right), \pclb\left(\begin{array}{c}\n{zeron}\end{array}\right)\end{array}\right)\\
}
