[
[
['8','add','hl'],
['233','add','hl'],
['20','add','hl'],
['244','add','hl'],
['230','add','hl'],
['263','add','hl'],
['29','remove','slide-up'],
['2','add','slide-down']
],
[
['234','add','hl'],
['234','remove','slide-left'],
['45','add','hl'],
['45','remove','hidden'],
['46','add','hl'],
['46','remove','hidden'],
['231','add','hl'],
['231','remove','slide-left'],
['4','add','hidden'],
['8','remove','hl'],
['8','add','hidden'],
['233','remove','hl'],
['233','add','slide-right'],
['20','remove','hl'],
['20','add','hidden'],
['244','remove','hl'],
['244','add','slide-left'],
['230','remove','hl'],
['230','add','slide-right'],
['263','remove','hl'],
['263','add','slide-right']
],
[
['234','remove','hl'],
['45','remove','hl'],
['46','remove','hl'],
['231','remove','hl'],
['234','add','hl'],
['243','add','hl'],
['46','add','hl'],
['231','add','hl'],
['239','add','hl'],
['25','add','hl'],
['236','add','hl'],
['260','add','hl'],
['55','remove','slide-up'],
['29','add','slide-down']
],
[
['245','add','hl'],
['245','remove','slide-left'],
['244','add','hl'],
['244','remove','slide-left'],
['72','add','hl'],
['72','remove','hidden'],
['241','add','hl'],
['241','remove','slide-left'],
['240','add','hl'],
['240','remove','slide-left'],
['77','add','hl'],
['77','remove','hidden'],
['237','add','hl'],
['237','remove','slide-left'],
['234','remove','hl'],
['234','add','slide-right'],
['243','remove','hl'],
['243','add','slide-right'],
['46','remove','hl'],
['46','add','hidden'],
['231','remove','hl'],
['231','add','slide-right'],
['239','remove','hl'],
['239','add','slide-right'],
['25','remove','hl'],
['25','add','hidden'],
['236','remove','hl'],
['236','add','slide-right'],
['260','remove','hl'],
['260','add','slide-right']
],
[
['245','remove','hl'],
['244','remove','hl'],
['72','remove','hl'],
['241','remove','hl'],
['240','remove','hl'],
['77','remove','hl'],
['237','remove','hl'],
['9','add','hl'],
['249','add','hl'],
['246','add','hl'],
['253','add','hl'],
['258','add','hl'],
['262','add','hl'],
['81','remove','slide-up'],
['55','add','slide-down']
],
[
['250','add','hl'],
['250','remove','slide-left'],
['247','add','hl'],
['247','remove','slide-left'],
['96','add','hl'],
['96','remove','hidden'],
['102','add','hl'],
['102','remove','hidden'],
['9','remove','hl'],
['9','add','hidden'],
['249','remove','hl'],
['249','add','slide-right'],
['246','remove','hl'],
['246','add','slide-right'],
['253','remove','hl'],
['253','add','slide-left'],
['258','remove','hl'],
['258','add','slide-right'],
['262','remove','hl'],
['262','add','slide-left']
],
[
['250','remove','hl'],
['247','remove','hl'],
['96','remove','hl'],
['102','remove','hl'],
['255','add','hl'],
['259','add','hl'],
['10','add','hl'],
['252','add','hl'],
['108','remove','slide-up'],
['81','add','slide-down']
],
[
['256','add','hl'],
['256','remove','slide-left'],
['249','add','hl'],
['249','remove','slide-right'],
['253','add','hl'],
['253','remove','slide-left'],
['257-slide','remove','slide-left'],
['255','remove','hl'],
['255','add','slide-right'],
['259','remove','hl'],
['259','add','slide-right'],
['10','remove','hl'],
['10','add','hidden'],
['252','remove','hl'],
['252','add','slide-right']
],
[
['256','remove','hl'],
['249','remove','hl'],
['253','remove','hl']
],
[
['257-flip','add','flipped'],
['108','add','slide-down']
],
[
['256','add','hl'],
['249','add','hl'],
['263','add','hl'],
['253','add','hl'],
['260','add','hl']
],
[
['255','add','hl'],
['255','remove','slide-right'],
['259','add','hl'],
['259','remove','slide-right'],
['10','add','hl'],
['10','remove','hidden'],
['263','add','hl'],
['263','remove','slide-right'],
['258','add','hl'],
['258','remove','slide-right'],
['260','add','hl'],
['260','remove','slide-right'],
['256','remove','hl'],
['256','add','slide-left'],
['249','remove','hl'],
['249','add','slide-right'],
['263','remove','hl'],
['263','add','slide-left'],
['253','remove','hl'],
['253','add','slide-left'],
['260','remove','hl'],
['260','add','slide-left'],
['257-slide','add','slide-left']
],
[
['255','remove','hl'],
['259','remove','hl'],
['10','remove','hl'],
['263','remove','hl'],
['258','remove','hl'],
['260','remove','hl'],
['45','add','hl'],
['72','add','hl'],
['241','add','hl'],
['258','add','hl'],
['24','add','hl'],
['77','add','hl'],
['237','add','hl'],
['205','remove','slide-up']
],
[
['207','remove','hidden'],
['243','add','hl'],
['243','remove','slide-right'],
['230','add','hl'],
['230','remove','slide-right'],
['263','add','hl'],
['263','remove','slide-left'],
['262','add','hl'],
['262','remove','slide-left'],
['239','add','hl'],
['239','remove','slide-right'],
['25','add','hl'],
['25','remove','hidden'],
['236','add','hl'],
['236','remove','slide-right'],
['260','add','hl'],
['260','remove','slide-left'],
['45','remove','hl'],
['45','add','hidden'],
['72','remove','hl'],
['72','add','hidden'],
['241','remove','hl'],
['241','add','slide-right'],
['258','remove','hl'],
['258','add','slide-right'],
['24','remove','hl'],
['24','add','hidden'],
['77','remove','hl'],
['77','add','hidden'],
['237','remove','hl'],
['237','add','slide-right']
],
[
['243','remove','hl'],
['230','remove','hl'],
['263','remove','hl'],
['262','remove','hl'],
['239','remove','hl'],
['25','remove','hl'],
['236','remove','hl'],
['260','remove','hl']
]
]
The starting point of the hybrid proof is $\lib{kem-1cca-real+ro}$.
We can inline all of the calls to $\ro$. The call to $\ro$ that determines $\ptxt^*$ is the first, so its result is always sampled uniformly.
Now we can perform the renaming suggested above. Whatever was previously stored in $\rotable[A]$ is now stored in $\mathcal{D}[A^e]$. Thus, $\rotable[\ctxt^d]$ becomes $\mathcal{D}[\ctxt]$.
We can carve out an exception for the challenge ciphertext $\ctxt^*$, so that $\mathcal{D}[\ctxt^*]$ is never used. Additionally, now the value $R^*$ is used only to compute $\ctxt^*$. Since $R^*$ is uniform, and exponentiation-by-$e$ is a 1-to-1 function, the resulting distribution on $\ctxt^*$ is uniform.\FORMATTINGHACK{\pagebreak}
The special case in $\ro(A)$ is triggered when the calling program provides an $e$-th root of $\ctxt^*$. Since $d$ is no longer used anywhere in the library, we can apply the RSA assumption to argue that this special case never happens.
We can remove the unreachable if-statement and also revert the previous change, replacing $\mathcal{D}[A^e]$ with $\rotable[A]$. The result is $\lib{kem-1cca-rand+ro}$.
$\lib{kem-1cca-real+ro}$
$\lib{kem-1cca-rand+ro}$
$(\nmod,e, {}$
$d) := \RSA.\KeyGen()$
$\ctxt^*) \gets \rsachallenge()$
$d) := \RSA.\KeyGen()$
$\pk := (\nmod,e)$
$R^* \gets \Z_\nmod$
$\ctxt^* $
${}:= (R^*)^e \pct \nmod$
${}\gets \Z_\nmod$
$\ptxt^* $
${}:= {}$
$\ro(R^*)$
$\rotable[R^*] \gets \bits^\secpar$
$\mathcal{D}[\ctxt^*] \gets \bits^\secpar$
${}\gets \bits^\secpar$
return $\pk$
return $(\ctxt^*, \ptxt^*)$
if $\ctxt == \ctxt^*$: return $\ptxt^*$
if
$\rotable[\ctxt^d \pct \nmod]$ undefined:
$\mathcal{D}[\ctxt]$ undefined:
$\rotable[\ctxt^d \pct \nmod] \gets \bits^\secpar$
$\mathcal{D}[\ctxt] \gets \bits^\secpar$
return
$\ro(\ctxt^d \pct \nmod)$
$\rotable[\ctxt^d \pct \nmod]$
$\mathcal{D}[\ctxt]$
$\ro(\ctxt^d \pct \nmod)$
if
$A^e \equiv_\nmod \ctxt^*$: return $\ptxt^*$
$\rsacheck(A)$: return $\ptxt^*$
$\myfalse$: return $\ptxt^*$
$\rotable[A]$ undefined:
if
$\rotable[A]$ undefined:
$\mathcal{D}[A^e \pct \nmod]$ undefined:
$\rotable[A] \gets \bits^\secpar$
$\mathcal{D}[A^e \pct \nmod] \gets \bits^\secpar$
return
$\rotable[A]$
$\mathcal{D}[A^e \pct \nmod]$
$\rotable[A]$
$\link$
$\lib{rsa-real}$
$(\nmod,e, d) := \RSA.\KeyGen()$
$Y \gets \Z_\nmod$
return $(\nmod,e,Y)$
return $Y \equiv_\nmod X^e$
$\lib{rsa-ideal}$
$(\nmod,e, d) := \RSA.\KeyGen()$
$Y \gets \Z_\nmod$
return $(\nmod,e,Y)$
return $\myfalse$