[
[
['136','add','hl'],
['138','add','hl'],
['140','add','hl'],
['17','remove','slide-up'],
['2','add','slide-down']
],
[
['24','add','hl'],
['24','remove','hidden'],
['25','add','hl'],
['25','remove','hidden'],
['26','add','hl'],
['26','remove','hidden'],
['27','add','hl'],
['27','remove','hidden'],
['28','add','hl'],
['28','remove','hidden'],
['4','add','hidden'],
['136','remove','hl'],
['136','add','slide-left'],
['138','remove','hl'],
['138','add','slide-right'],
['140','remove','hl'],
['140','add','slide-left']
],
[
['24','remove','hl'],
['25','remove','hl'],
['26','remove','hl'],
['27','remove','hl'],
['28','remove','hl'],
['25','add','hl'],
['135','add','hl'],
['36','remove','slide-up'],
['17','add','slide-down']
],
[
['136','add','hl'],
['136','remove','slide-left'],
['137-slide','remove','slide-left'],
['25','remove','hl'],
['25','add','hidden'],
['135','remove','hl'],
['135','add','slide-right']
],
[
['136','remove','hl']
],
[
['137-flip','add','flipped'],
['36','add','slide-down']
],
[
['136','add','hl']
],
[
['91','add','hl'],
['91','remove','hidden'],
['92','add','hl'],
['92','remove','hidden'],
['138','add','hl'],
['138','remove','slide-right'],
['136','remove','hl'],
['136','add','slide-left'],
['137-slide','add','slide-left']
],
[
['91','remove','hl'],
['92','remove','hl'],
['138','remove','hl'],
['91','add','hl'],
['92','add','hl'],
['139','add','hl'],
['102','remove','slide-up']
],
[
['140','add','hl'],
['140','remove','slide-left'],
['91','remove','hl'],
['91','add','hidden'],
['92','remove','hl'],
['92','add','hidden'],
['139','remove','hl'],
['139','add','slide-right']
],
[
['140','remove','hl'],
['142','add','hl'],
['24','add','hl'],
['26','add','hl'],
['27','add','hl'],
['28','add','hl'],
['120','remove','slide-up'],
['102','add','slide-down']
],
[
['122','remove','hidden'],
['143','add','hl'],
['143','remove','slide-left'],
['139','add','hl'],
['139','remove','slide-right'],
['135','add','hl'],
['135','remove','slide-right'],
['136','add','hl'],
['136','remove','slide-left'],
['142','remove','hl'],
['142','add','slide-right'],
['24','remove','hl'],
['24','add','hidden'],
['26','remove','hl'],
['26','add','hidden'],
['27','remove','hl'],
['27','add','hidden'],
['28','remove','hl'],
['28','add','hidden']
],
[
['143','remove','hl'],
['139','remove','hl'],
['135','remove','hl'],
['136','remove','hl']
]
]
The starting point is $\L_h$.
We can create a separate branch of the if-statement to isolate the adversary's $(h+1)$th call to $\prgsamp$. This allows us to give a name $\seed^*$ to the PRG's seed in this call. \FORMATTINGHACK{\pagebreak}
We can apply the PRF-security of $F$ to the $(h+1)$th call to $\prgsamp$. This is a three-hop maneuver that replaces calls to $F(\seed^*,\cdot)$ with a lazy random dictionary.
The condition ``if $\prftable[i]$ undefined'' is always true, because $i$ takes on distinct values. We can therefore make the body of the if-statement unconditional:
\FORMATTINGHACK{\needspace{3\baselineskip}} Now the ``if'' and ``else if'' branches behave identically: They uniformly sample a $km$-bit string. Unifying them into one branch results in $\L_{h+1}$, which completes the proof.
$\L_h$
$\L_{h+1}$
$count := count + 1$
$Y \gets \bits^{km}$
return $Y$
else if $count == h+1$:
$\seed^* \gets \bits^\secpar$
for $i = 0$ to $k-1$:
if $\prftable[i]$ undefined:
$\prftable[i] \gets \bits^\secpar$
$X_i $
${}:= {}$
$F(\seed^*, i)$
$\prfquery(i)$
$\prftable[i]$
${}\gets \bits^\secpar$
return $X_0 \| \cdots \| X_{k-1}$
else:
$\seed \gets \bits^\secpar$
for $i = 0$ to $k-1$:
$X_i := F(\seed, i)$
return $X_0 \| \cdots \| X_{k-1}$
$\link$
$\lib{prf-real}$
$\key \gets \bits^\secpar$
return $F(\key,X)$
$\lib{prf-rand}$
if $\prftable[X]$ undefined:
$\prftable[X] \gets \bits^\secpar$
return $\prftable[X]$