[
[
['12','remove','hidden'],
['16','add','hl'],
['16','remove','hidden'],
['3','add','hidden'],
['18','remove','slide-up'],
['8','add','slide-down']
],
[
['16','remove','hl'],
['78','add','hl'],
['86','add','hl'],
['28','remove','slide-up'],
['18','add','slide-down']
],
[
['22','remove','hidden'],
['79','add','hl'],
['79','remove','slide-left'],
['12','add','hidden'],
['78','remove','hl'],
['78','add','slide-right'],
['86','remove','hl'],
['86','add','slide-right']
],
[
['79','remove','hl'],
['5','add','hl'],
['81','add','hl'],
['43','remove','slide-up'],
['28','add','slide-down']
],
[
['32','remove','hidden'],
['82','add','hl'],
['82','remove','slide-left'],
['83-slide','remove','slide-left'],
['22','add','hidden'],
['5','remove','hl'],
['5','add','hidden'],
['81','remove','hl'],
['81','add','slide-right']
],
[
['82','remove','hl']
],
[
['83-flip','add','flipped'],
['57','remove','slide-up'],
['43','add','slide-down']
],
[
['84','add','hl'],
['86','add','hl'],
['66','remove','slide-up'],
['57','add','slide-down']
],
[
['61','remove','hidden'],
['85','add','hl'],
['85','remove','slide-right'],
['86','add','hl'],
['86','remove','slide-right'],
['32','add','hidden'],
['84','remove','hl'],
['84','add','slide-left'],
['86','remove','hl'],
['86','add','slide-left'],
['83-slide','add','slide-left']
],
[
['85','remove','hl'],
['86','remove','hl'],
['16','add','hl'],
['79','add','hl'],
['75','remove','slide-up'],
['66','add','slide-down']
],
[
['70','remove','hidden'],
['73','add','hl'],
['73','remove','hidden'],
['78','add','hl'],
['78','remove','slide-right'],
['86','add','hl'],
['86','remove','slide-left'],
['61','add','hidden'],
['16','remove','hl'],
['16','add','hidden'],
['79','remove','hl'],
['79','add','slide-right']
],
[
['73','remove','hl'],
['78','remove','hl'],
['86','remove','hl']
]
]
The starting point of the hybrid proof is library $\lib{xor-samp-1}$.
We first introduce a new variable $X'$, which is not used anywhere. This change has no effect on the calling program.
You can check for yourself (using the algebraic properties of \xor) that $X$ and $X'$ always hold the same value. It therefore has no effect on the calling program to change a reference to $X$ into a reference to $X'$.
We want to argue that $Y$ is uniformly distributed, and we can do so by observing that $Y$ looks like an OTP ciphertext with $X$ as the key and $M$ as the plaintext. To use this fact, we first ``factor out'' the computation of $Y$ in terms of the $\lib{otp-real}$ library from \claimref{provsec.clm.otp}. Factoring out these statements leaves us with a compound library, but has no effect on the calling program.
Now we are in a situation where we can use \claimref{provsec.clm.otp} and the chain rule (\claimref{provsec.clm.chain-rule}). Replacing $\lib{otp-real}$ with $\lib{otp-rand}$ in this compound library (while keeping the other part $\lib{hyb-3-4}$ the same) has no effect on any calling program.
It has no effect on the calling program to inline a subroutine call.
Finally, we globally rename variable $X'$ to $X$. This change clearly has no effect on the calling program. The result is the library $\lib{xor-samp-2}$.
$\lib{xor-samp-1}$
$\lib{hyb-1}$
$\lib{hyb-2}$
$\lib{hyb-3-4}$
$\lib{hyb-5}$
$\lib{xor-samp-2}$
$X \gets \bits^n$
$Y $
${}:= {}$
$X \oplus M$
$\otpenc(M)$
${}\gets \bits^n$
$X' := Y \oplus M$
$X := Y \oplus M$
$\link$
$\lib{otp-real}$
$\key \gets \bits^n$
$\ctxt := \key \oplus \ptxt$
return $\ctxt$
$\lib{otp-rand}$
$\ctxt \gets \bits^n$
return $\ctxt$