[
[
['136','add','hl'],
['8','add','hl'],
['142','add','hl'],
['143','add','hl'],
['144','add','hl'],
['147','add','hl'],
['158','add','hl'],
['133','add','hl'],
['14','remove','slide-up'],
['2','add','slide-down']
],
[
['137','add','hl'],
['137','remove','slide-left'],
['148','add','hl'],
['148','remove','slide-right'],
['20','add','hl'],
['20','remove','hidden'],
['21','add','hl'],
['21','remove','hidden'],
['134','add','hl'],
['134','remove','slide-left'],
['4','add','hidden'],
['136','remove','hl'],
['136','add','slide-right'],
['8','remove','hl'],
['8','add','hidden'],
['142','remove','hl'],
['142','add','slide-left'],
['143','remove','hl'],
['143','add','slide-left'],
['144','remove','hl'],
['144','add','slide-left'],
['147','remove','hl'],
['147','add','slide-right'],
['158','remove','hl'],
['158','add','slide-left'],
['133','remove','hl'],
['133','add','slide-right']
],
[
['137','remove','hl'],
['148','remove','hl'],
['20','remove','hl'],
['21','remove','hl'],
['134','remove','hl'],
['154','add','hl'],
['141','add','hl'],
['21','add','hl'],
['138','add','hl'],
['151','add','hl'],
['26','remove','slide-up'],
['14','add','slide-down']
],
[
['32','add','hl'],
['32','remove','hidden'],
['20','remove','indent-1'],
['142','add','hl'],
['142','remove','slide-left'],
['34','add','hl'],
['34','remove','hidden'],
['35','add','hl'],
['35','remove','hidden'],
['139','add','hl'],
['139','remove','slide-left'],
['37','add','hl'],
['37','remove','hidden'],
['154','remove','hl'],
['154','add','slide-left'],
['20','add','indent-2'],
['141','remove','hl'],
['141','add','slide-right'],
['21','remove','hl'],
['21','add','hidden'],
['138','remove','hl'],
['138','add','slide-right'],
['151','remove','hl'],
['151','add','slide-left']
],
[
['32','remove','hl'],
['142','remove','hl'],
['34','remove','hl'],
['35','remove','hl'],
['139','remove','hl'],
['37','remove','hl'],
['9','add','hl'],
['142','add','hl'],
['35','add','hl'],
['41','remove','slide-up'],
['26','add','slide-down']
],
[
['143','add','hl'],
['143','remove','slide-left'],
['49','add','hl'],
['49','remove','hidden'],
['9','remove','hl'],
['9','add','hidden'],
['142','remove','hl'],
['142','add','slide-right'],
['35','remove','hl'],
['35','add','hidden']
],
[
['143','remove','hl'],
['49','remove','hl'],
['137','add','hl'],
['148','add','hl'],
['143','add','hl'],
['55','remove','slide-up'],
['41','add','slide-down']
],
[
['145','add','hl'],
['145','remove','slide-left'],
['144','add','hl'],
['144','remove','slide-left'],
['146-slide','remove','slide-left'],
['137','remove','hl'],
['137','add','slide-right'],
['148','remove','hl'],
['148','add','slide-right'],
['143','remove','hl'],
['143','add','slide-right']
],
[
['145','remove','hl'],
['144','remove','hl']
],
[
['146-flip','add','flipped'],
['55','add','slide-down']
],
[
['145','add','hl'],
['144','add','hl']
],
[
['137','add','hl'],
['137','remove','slide-right'],
['148','add','hl'],
['148','remove','slide-right'],
['147','add','hl'],
['147','remove','slide-right'],
['145','remove','hl'],
['145','add','slide-left'],
['144','remove','hl'],
['144','add','slide-left'],
['146-slide','add','slide-left']
],
[
['137','remove','hl'],
['148','remove','hl'],
['147','remove','hl'],
['5','add','hl'],
['6','add','hl'],
['153','add','hl'],
['49','add','hl'],
['150','add','hl'],
['113','remove','slide-up']
],
[
['136','add','hl'],
['136','remove','slide-right'],
['145','add','hl'],
['145','remove','slide-left'],
['154','add','hl'],
['154','remove','slide-left'],
['151','add','hl'],
['151','remove','slide-left'],
['5','remove','hl'],
['5','add','hidden'],
['6','remove','hl'],
['6','add','hidden'],
['153','remove','hl'],
['153','add','slide-right'],
['49','remove','hl'],
['49','add','hidden'],
['150','remove','hl'],
['150','add','slide-right']
],
[
['136','remove','hl'],
['145','remove','hl'],
['154','remove','hl'],
['151','remove','hl'],
['32','add','hl'],
['147','add','hl'],
['34','add','hl'],
['10','add','hl'],
['37','add','hl'],
['156','add','hl'],
['124','remove','slide-up'],
['113','add','slide-down']
],
[
['126','remove','hidden'],
['153','add','hl'],
['153','remove','slide-right'],
['20','remove','indent-2'],
['158','add','hl'],
['158','remove','slide-left'],
['138','add','hl'],
['138','remove','slide-right'],
['133','add','hl'],
['133','remove','slide-right'],
['150','add','hl'],
['150','remove','slide-right'],
['129','add','hl'],
['129','remove','hidden'],
['157','add','hl'],
['157','remove','slide-left'],
['32','remove','hl'],
['32','add','hidden'],
['20','add','indent-1'],
['147','remove','hl'],
['147','add','slide-right'],
['34','remove','hl'],
['34','add','hidden'],
['10','remove','hl'],
['10','add','hidden'],
['37','remove','hl'],
['37','add','hidden'],
['156','remove','hl'],
['156','add','slide-right']
],
[
['153','remove','hl'],
['158','remove','hl'],
['138','remove','hl'],
['133','remove','hl'],
['150','remove','hl'],
['129','remove','hl'],
['157','remove','hl']
]
]
The starting point is $\lib{prf-real}$.
Since $F$ is a secure PRF, we may replace it with a lazy random dictionary. The standard three-hop maneuver is not shown.
The library uses a dictionary data structure, and one way to implement a dictionary is as a simple list of pairs $(Y,Z)$. To read from the dictionary at position $Y$, simply scan the list to find a record with the correct $Y$. To modify the dictionary, append a new record to the list. This is not a very efficient way to implement a dictionary, but it is correct nonetheless. In this proof it is convenient to store not only $Y$ and $Z$ but also $X$ in each record.
Each record $(X,Y,Z)$ in $\mathcal{D}$ satisfies $Y = H^*(\key_1,X)$. So instead of comparing $Y'$ and $Y$, the library can compare $H^*(\key_1,X')$ and $H^*(\key_1,X)$ with the same effect.
Now the library implements a dictionary in terms of hash comparisons, so we can apply the CRHF security of $H^*$ in a three-hop maneuver.
The $Y$-values, and therefore $\key_1$, are no longer being used. They can be removed.
The resulting library is an (inefficient) implementation of a lazy random dictionary, but this time indexed by $X$ values rather than their hashes. In other words, it is $\lib{prf-rand}$.\FORMATTINGHACK{\pagebreak}
$\lib{prf-real}$
$\key_1 $
$\| \key_2 \gets \bits^{2\secpar}$
${}\gets \bits^\secpar$
${}:= \crhfgetsalt()$
${}\gets \bits^\secpar$
$\lib{prf-rand}$
$Y := H^*(\key_1, X)$
for each
$(X',Y',Z') \in \mathcal{D}$:
$(X',Z') \in \mathcal{D}$:
if
$\prftable[Y]$ undefined:
$Y' == Y$:
$H^*(\key_1,X') == H^*(\key_1,X)$:
$\crhfcmp(X',X)$:
$X' == X$:
$\prftable[X]$ undefined:
$\prftable[Y] \gets \bits^n$
return $Z'$
$Y := H^*(\key_1, X)$
$Z $
${}:= {}$
$F(\key_2, Y)$
$\prftable[Y]$
${}\gets \bits^n$
$\mathcal{D} := \mathcal{D} \cup {}$
$\{ (X,Y,Z) \}$
$\{ (X,Z) \}$
$\prftable[X] \gets \bits^n$
$\link$
$\lib{crhf-real}$
$\salt \gets \bits^\secpar$
return $\salt$
return $H^*(\salt,X) == H^*(\salt,X')$
$\lib{crhf-ideal}$
$\salt \gets \bits^\secpar$
return $\salt$
return $X == X'$