[
[
['5','add','hl'],
['6','add','hl'],
['98','add','hl'],
['95','add','hl'],
['14','remove','slide-up'],
['2','add','slide-down']
],
[
['17','add','hl'],
['17','remove','hidden'],
['99','add','hl'],
['99','remove','slide-left'],
['21','add','hl'],
['21','remove','hidden'],
['96','add','hl'],
['96','remove','slide-left'],
['4','add','hidden'],
['5','remove','hl'],
['5','add','hidden'],
['6','remove','hl'],
['6','add','hidden'],
['98','remove','hl'],
['98','add','slide-right'],
['95','remove','hl'],
['95','add','slide-right']
],
[
['17','remove','hl'],
['99','remove','hl'],
['21','remove','hl'],
['96','remove','hl'],
['102','add','hl'],
['25','remove','slide-up'],
['14','add','slide-down']
],
[
['29','add','hl'],
['29','remove','hidden'],
['30','add','hl'],
['30','remove','hidden'],
['34','add','hl'],
['34','remove','hidden'],
['102','remove','hl'],
['102','add','slide-left']
],
[
['29','remove','hl'],
['30','remove','hl'],
['34','remove','hl']
],
[
['45','add','hl'],
['45','remove','hidden'],
['39','remove','slide-up'],
['25','add','slide-down']
],
[
['45','remove','hl'],
['17','add','hl'],
['101','add','hl'],
['30','add','hl'],
['54','remove','slide-up'],
['39','add','slide-down']
],
[
['102','add','hl'],
['102','remove','slide-left'],
['58','add','hl'],
['58','remove','hidden'],
['59','add','hl'],
['59','remove','hidden'],
['60','add','hl'],
['60','remove','hidden'],
['62','add','hl'],
['62','remove','hidden'],
['69','add','hl'],
['69','remove','hidden'],
['70','add','hl'],
['70','remove','hidden'],
['71','add','hl'],
['71','remove','hidden'],
['72','add','hl'],
['72','remove','hidden'],
['73','add','hl'],
['73','remove','hidden'],
['17','remove','hl'],
['17','add','hidden'],
['101','remove','hl'],
['101','add','slide-right'],
['30','remove','hl'],
['30','add','hidden']
],
[
['102','remove','hl'],
['58','remove','hl'],
['59','remove','hl'],
['60','remove','hl'],
['62','remove','hl'],
['69','remove','hl'],
['70','remove','hl'],
['71','remove','hl'],
['72','remove','hl'],
['73','remove','hl'],
['104','add','hl'],
['29','add','hl'],
['59','add','hl'],
['62','add','hl'],
['34','add','hl'],
['76','remove','slide-up'],
['54','add','slide-down']
],
[
['17','add','hl'],
['17','remove','hidden'],
['101','add','hl'],
['101','remove','slide-right'],
['104','remove','hl'],
['104','add','slide-right'],
['29','remove','hl'],
['29','add','hidden'],
['59','remove','hl'],
['59','add','hidden'],
['62','remove','hl'],
['62','add','hidden'],
['34','remove','hl'],
['34','add','hidden']
],
[
['17','remove','hl'],
['101','remove','hl']
]
]
The starting point is $\lib{mac-real}$.
We replace the PRF with a lazy random dictionary $\prftable[\cdot]$. The standard three-hop maneuver is not shown.
We can keep track of which values of $X$ have had their $\prftable[X]$ value revealed, in the set $\mathcal{R}$. We define a bad event when the caller guesses $\prftable[X]$ before it has been revealed. Neither of these changes affects the library's outputs; they are purely internal bookkeeping.
\FORMATTINGHACK{\needspace{3\baselineskip}\noindent}We can change the library's behavior after the bad event is triggered. The change is indistinguishable, assuming we later show that the bad event has negligible probability.
In the current hybrid we sample $\prftable[X]$ as soon as it is needed, whether for $\macguess$ or $\macreveal$. Then we trigger the bad event as early guesses arrive. An equivalent approach is to keep track of early guesses, sample $\prftable[X]$ only in $\macreveal$ (or at the end of time if $\macreveal$ is never called for $X$), and trigger the bad event then, when $\prftable[X]$ is sampled.
\FORMATTINGHACK{\needspace{3\baselineskip}\noindent}$X \in \mathcal{R}$ if and only if $\prftable[X]$ is defined. Thus, we can do away with $\mathcal{R}$ and change the condition ``if $X \not\in \mathcal{R}$'' to ``if $\prftable[X]$ undefined.'' The second if-statement in $\macguess$ is unreachable and can be removed.
$\lib{mac-real}$
$\key \gets \bits^\secpar$
if $\prftable[X]$ undefined:
$\prftable[X] \gets \bits^\secpar$
if $X \not\in {}$
$\mathcal{R}$ and $Y == \prftable[X]$:
$\mathcal{R}$:
$\badvar := \mytrue$
$\textsf{early}[X] := \textsf{early}[X] \cup \{Y\}$
$\mathcal{G} := \mathcal{G} \cup \{X\}$
return $\myfalse$
if $\prftable[X]$ undefined: $\prftable[X] \gets \bits^\secpar$
return $Y == {}$
$F(\key,X)$
$\prftable[X]$
$\mathcal{R} := \mathcal{R} \cup \{X\}$
if $\prftable[X]$ undefined: $\prftable[X] \gets \bits^\secpar$
return
$F(\key,X)$
$\prftable[X]$
for each $X \in \mathcal{G}$:
if $\prftable[X]$ undefined: $\prftable[X] \gets \bits^\secpar$
if $\prftable[X] \in \textsf{early}[X]$: $\badvar := \mytrue$