[
[
['4','add','hl'],
['5','add','hl'],
['7','add','hl'],
['149','add','hl'],
['27','remove','slide-up'],
['12','add','slide-down']
],
[
['150','add','hl'],
['150','remove','slide-left'],
['151-slide','remove','slide-left'],
['3','add','hidden'],
['4','remove','hl'],
['4','add','hidden'],
['5','remove','hl'],
['5','add','hidden'],
['7','remove','hl'],
['7','add','hidden'],
['149','remove','hl'],
['149','add','slide-right']
],
[
['150','remove','hl']
],
[
['151-flip','add','flipped'],
['27','add','slide-down']
],
[
['9','add','hl'],
['153','add','hl']
],
[
['149','add','hl'],
['149','remove','slide-right'],
['47','add','hl'],
['47','remove','hidden'],
['48','remove','indent-1'],
['48','add','hl'],
['48','remove','hidden'],
['154','add','hl'],
['154','remove','slide-right'],
['9','remove','hl'],
['9','add','hidden'],
['48','add','indent-2'],
['153','remove','hl'],
['153','add','slide-left'],
['151-slide','add','slide-left']
],
[
['149','remove','hl'],
['47','remove','hl'],
['48','remove','hl'],
['154','remove','hl'],
['156','add','hl'],
['159','add','hl'],
['53','remove','slide-up']
],
[
['157','add','hl'],
['157','remove','slide-left'],
['158-slide','remove','slide-left'],
['156','remove','hl'],
['156','add','slide-right'],
['159','remove','hl'],
['159','add','slide-right']
],
[
['157','remove','hl']
],
[
['158-flip','add','flipped'],
['53','add','slide-down']
],
[
['157','add','hl'],
['165','add','hl']
],
[
['159','add','hl'],
['159','remove','slide-right'],
['164','add','hl'],
['164','remove','slide-right'],
['86','add','hl'],
['86','remove','hidden'],
['157','remove','hl'],
['157','add','slide-left'],
['165','remove','hl'],
['165','add','slide-left'],
['158-slide','add','slide-left']
],
[
['159','remove','hl'],
['164','remove','hl'],
['86','remove','hl'],
['165','add','hl'],
['47','add','hl'],
['93','remove','slide-up']
],
[
['165','add','hl'],
['165','remove','slide-left'],
['48','remove','indent-2'],
['165','remove','hl'],
['165','add','slide-right'],
['47','remove','hl'],
['47','add','hidden'],
['48','add','indent-1']
],
[
['165','remove','hl'],
['48','add','hl'],
['154','add','hl'],
['103','remove','slide-up'],
['93','add','slide-down']
],
[
['160','add','hl'],
['160','remove','slide-left'],
['161-slide','remove','slide-left'],
['48','remove','hl'],
['48','add','hidden'],
['154','remove','hl'],
['154','add','slide-right']
],
[
['160','remove','hl']
],
[
['161-flip','add','flipped'],
['103','add','slide-down']
],
[
['165','add','hl'],
['162','add','hl']
],
[
['165','add','hl'],
['165','remove','slide-right'],
['163','add','hl'],
['163','remove','slide-right'],
['165','remove','hl'],
['165','add','slide-left'],
['162','remove','hl'],
['162','add','slide-left'],
['161-slide','add','slide-left']
],
[
['165','remove','hl'],
['163','remove','hl'],
['164','add','hl'],
['86','add','hl'],
['139','remove','slide-up']
],
[
['141','remove','hidden'],
['156','add','hl'],
['156','remove','slide-right'],
['165','add','hl'],
['165','remove','slide-left'],
['145','add','hl'],
['145','remove','hidden'],
['164','remove','hl'],
['164','add','slide-right'],
['86','remove','hl'],
['86','add','hidden']
],
[
['156','remove','hl'],
['165','remove','hl'],
['145','remove','hl']
]
]
The starting point is $\lib{cpa-real}$.
We can apply the security of the PRF in a standard three-hop maneuver:
Sampling $R$ uniformly is indistinguishable from sampling without replacement.
In this hybrid, the $R$ values can never repeat, so the if-statement is always taken. Thus, we can make its body unconditional.
Each value of $\prftable[R]$ is sampled uniformly and used only in a single \xor expression. As a result, $S$ is a OTP encryption of $\ptxt$, with $\prftable[R]$ playing the role of the key.
Finally, we can revert $R$ so that it is sampled uniformly (with replacement). The result is $\lib{cpa-rand}$, which completes the proof.
$\lib{cpa-real}$
$\key \gets \bits^\secpar$
$\lib{cpa-rand}$
$R $
${}\gets \bits^\secpar$
${}:= \bdaysamp()$
${}\gets \bits^\secpar$
${} \setminus \mathcal{R}$
$$
$Y := {}$
$F(\key,R)$
$\prfquery(R)$
$\mathcal{R} := \mathcal{R} \cup \{R\}$
if $\prftable[R]$ undefined:
$\prftable[R] \gets \bits^n$
$S $
${}:= {}$
$Y \oplus \ptxt$
$\prftable[R] \oplus \ptxt$
$\otpenc(\ptxt)$
${}\gets \bits^n$
return $R\|S$
$\link$
$\lib{prf-real}$
$\key \gets \bits^\secpar$
return $F(\key,X)$
$\lib{prf-rand}$
if $\prftable[X]$ undefined:
$\prftable[X] \gets \bits^n$
return $\prftable[X]$
$\link$
$\lib{samp-rand}$
$R \gets \bits^\secpar$
return $R$
$\lib{samp-uniq}$
$R \gets \bits^\secpar \setminus \mathcal{R}$
$\mathcal{R} := \mathcal{R} \cup \{ R \}$
return $R$
$\link$
$\lib{otp-real}$
$\key \gets \bits^n$
$\ctxt := \key \oplus \ptxt$
return $\ctxt$
$\lib{otp-rand}$
$R \gets \bits^n$
return $R$