[
[
['11','add','hl'],
['259','add','hl'],
['18','add','hl'],
['20','add','hl'],
['263','add','hl'],
['256','add','hl'],
['276','add','hl'],
['61','remove','slide-up'],
['29','add','slide-down']
],
[
['41','add','hl'],
['41','remove','hidden'],
['42','add','hl'],
['42','remove','hidden'],
['260','add','hl'],
['260','remove','slide-left'],
['45','add','hl'],
['45','remove','hidden'],
['281','add','hl'],
['281','remove','slide-left'],
['49','add','hl'],
['49','remove','hidden'],
['51','add','hl'],
['51','remove','hidden'],
['52','add','hl'],
['52','remove','hidden'],
['257','add','hl'],
['257','remove','slide-left'],
['3','add','hidden'],
['11','remove','hl'],
['11','add','hidden'],
['259','remove','hl'],
['259','add','slide-right'],
['18','remove','hl'],
['18','add','hidden'],
['20','remove','hl'],
['20','add','hidden'],
['263','remove','hl'],
['263','add','slide-left'],
['256','remove','hl'],
['256','add','slide-right'],
['276','remove','hl'],
['276','add','slide-right']
],
[
['41','remove','hl'],
['42','remove','hl'],
['260','remove','hl'],
['45','remove','hl'],
['281','remove','hl'],
['49','remove','hl'],
['51','remove','hl'],
['52','remove','hl'],
['257','remove','hl'],
['262','add','hl'],
['52','add','hl'],
['92','remove','slide-up'],
['61','add','slide-down']
],
[
['263','add','hl'],
['263','remove','slide-left'],
['262','remove','hl'],
['262','add','slide-right'],
['52','remove','hl'],
['52','add','hidden']
],
[
['263','remove','hl'],
['19','add','hl'],
['51','add','hl'],
['21','add','hl'],
['23','add','hl'],
['122','remove','slide-up'],
['92','add','slide-down']
],
[
['262','add','hl'],
['262','remove','slide-right'],
['256','add','hl'],
['256','remove','slide-right'],
['276','add','hl'],
['276','remove','slide-right'],
['22','remove','indent-2'],
['118','add','hl'],
['118','remove','hidden'],
['119','add','hl'],
['119','remove','hidden'],
['120','add','hl'],
['120','remove','hidden'],
['19','remove','hl'],
['19','add','hidden'],
['51','remove','hl'],
['51','add','hidden'],
['21','remove','hl'],
['21','add','hidden'],
['22','add','indent-1'],
['23','remove','hl'],
['23','add','hidden']
],
[
['262','remove','hl'],
['256','remove','hl'],
['276','remove','hl'],
['118','remove','hl'],
['119','remove','hl'],
['120','remove','hl'],
['41','add','hl'],
['42','add','hl'],
['264','add','hl'],
['155','remove','slide-up'],
['122','add','slide-down']
],
[
['265','add','hl'],
['265','remove','slide-left'],
['137','add','hl'],
['137','remove','hidden'],
['146','add','hl'],
['146','remove','hidden'],
['152','add','hl'],
['152','remove','hidden'],
['153','add','hl'],
['153','remove','hidden'],
['154','add','hl'],
['154','remove','hidden'],
['41','remove','hl'],
['41','add','hidden'],
['42','remove','hl'],
['42','add','hidden'],
['264','remove','hl'],
['264','add','slide-right']
],
[
['265','remove','hl'],
['137','remove','hl'],
['146','remove','hl'],
['152','remove','hl'],
['153','remove','hl'],
['154','remove','hl'],
['13','add','hl'],
['267','add','hl'],
['187','remove','slide-up'],
['155','add','slide-down']
],
[
['264','add','hl'],
['264','remove','slide-right'],
['259','add','hl'],
['259','remove','slide-right'],
['268','add','hl'],
['268','remove','slide-left'],
['13','remove','hl'],
['13','add','hidden'],
['267','remove','hl'],
['267','add','slide-right']
],
[
['264','remove','hl'],
['259','remove','hl'],
['268','remove','hl'],
['270','add','hl'],
['282','add','hl'],
['12','add','hl'],
['137','add','hl'],
['274','add','hl'],
['219','remove','slide-up'],
['187','add','slide-down']
],
[
['271','add','hl'],
['271','remove','slide-left'],
['216','add','hl'],
['216','remove','hidden'],
['217','add','hl'],
['217','remove','hidden'],
['270','remove','hl'],
['270','add','slide-right'],
['282','remove','hl'],
['282','add','slide-right'],
['12','remove','hl'],
['12','add','hidden'],
['137','remove','hl'],
['137','add','hidden'],
['274','remove','hl'],
['274','add','slide-left']
],
[
['271','remove','hl'],
['216','remove','hl'],
['217','remove','hl'],
['271','add','hl'],
['45','add','hl'],
['280','add','hl'],
['49','add','hl'],
['257','add','hl'],
['146','add','hl'],
['118','add','hl'],
['119','add','hl'],
['120','add','hl'],
['273','add','hl'],
['253','remove','slide-up'],
['219','add','slide-down']
],
[
['223','remove','hidden'],
['270','add','hl'],
['270','remove','slide-right'],
['282','add','hl'],
['282','remove','slide-right'],
['232','add','hl'],
['232','remove','hidden'],
['236','add','hl'],
['236','remove','hidden'],
['18','add','hl'],
['18','remove','hidden'],
['19','add','hl'],
['19','remove','hidden'],
['20','add','hl'],
['20','remove','hidden'],
['21','add','hl'],
['21','remove','hidden'],
['22','remove','indent-1'],
['23','add','hl'],
['23','remove','hidden'],
['274','add','hl'],
['274','remove','slide-left'],
['271','remove','hl'],
['271','add','slide-right'],
['45','remove','hl'],
['45','add','hidden'],
['280','remove','hl'],
['280','add','slide-right'],
['49','remove','hl'],
['49','add','hidden'],
['257','remove','hl'],
['257','add','slide-right'],
['22','add','indent-2'],
['146','remove','hl'],
['146','add','hidden'],
['118','remove','hl'],
['118','add','hidden'],
['119','remove','hl'],
['119','add','hidden'],
['120','remove','hl'],
['120','add','hidden'],
['273','remove','hl'],
['273','add','slide-right']
],
[
['270','remove','hl'],
['282','remove','hl'],
['232','remove','hl'],
['236','remove','hl'],
['18','remove','hl'],
['19','remove','hl'],
['20','remove','hl'],
['21','remove','hl'],
['23','remove','hl'],
['274','remove','hl']
]
]
The starting point of the proof is $\lib{pk-1cca-real+ro}$.
We can inline the calls to $\ro$ made in $\ccaoneenc$ and $\ccaonedec$. We can also remember the decryption of the challenge ciphertext $\ctxt^*$, as $\mathcal{D}[\ctxt^*]$, so that $\ccaonedec$ does not need to recompute it. The reason we introduce a dictionary $\mathcal{D}[\cdot]$, even though the library assigns only one position in it, is because later hybrids will use more of it.
Suppose that in some call to $\ccaonedec(\ctxt)$, we see that $\rotable[\ptxt\|S]$ is undefined; the adversary has not called the random oracle on this input. The library will return an error unless the adversary has somehow successfully anticipated the result of $\Sigma.\Enc$, with \emph{fresh randomness} $\rotable[\ptxt\|S]$. Following the reasoning described earlier, such a prediction is successful only with negligible probability at most $1/2^\secpar$, when $\Sigma$ has unique randomness. It makes a negligible difference to simply always return an error in this case.
Now $\ccaonedec()$ returns an error \emph{unless} the ciphertext has the form $\Enc(\pk,X; \ro(X))$, \emph{and} the adversary has already called $\ro(X)$. So instead of decrypting ciphertexts the usual way in $\ccaonedec()$, we can compute the associated ciphertext at the time $\ro(X)$ is called, and store its decryption for later use in $\ccaonedec()$. The change has no effect on the calling program.\FORMATTINGHACK{\pagebreak}
Modify $\ccaoneenc()$ so that, instead of using $\ro(\ptxt\|S^*)$ as randomness for $\Sigma.\Enc$, it uses a freshly sampled value $R$ unrelated to the random oracle. This changes the library's overall behavior \emph{only} in the bad event that the adversary also queries $\ro(\ptxt\|S^*)$. We can mark the change with a bad event, and later argue that it has negligible probability.\FORMATTINGHACK{\pagebreak}
Now $\ccaoneenc()$ uses randomness for $\Sigma.\Enc$ that is used for nothing else. This is exactly equivalent to calling $\Sigma.\Enc()$ the usual way (\ie, as a randomized algorithm, without externally fixing its randomness). Furthermore, the secret key of $\Sigma$ is no longer used anywhere in the library. Hence, we can apply the CPA security of $\Sigma$ to replace ciphertext $\ctxt^*$ with a uniformly chosen one. The three-hop maneuver is not shown.\FORMATTINGHACK{\pagebreak}
Now $S^*$ in $\ccaoneenc()$ is used only to trigger the bad event, and does not affect what the adversary sees. We can therefore defer the choice of $S^*$ to the end of time.
Finally, we can undo a previous change, moving decryption logic from $\ro()$ back to $\ccaonedec()$. Then the only value in $\mathcal{D}[\cdot]$ that is used is $\mathcal{D}[\ctxt^*]$, which \FORMATTINGHACK{\pagebreak}we rename simply to $\ptxt^*$. As a result, we obtain $\lib{pk-1cca-rand+ro}$, plus some end-of-time logic relating to a bad event.
$\lib{pk-1cca-real+ro}$
$\lib{pk-1cca-rand+ro}$
$(\pk,\sk) := {}$
$\Sigma.\KeyGen()$
$\Sigma.\KeyGen$
$\Sigma.\KeyGen()$
return $\pk$
if $\ctxt^*$ undefined:
$S^* \gets \bits^\secpar$
if $\rotable[\ptxt\|S^*]$ undefined:
$\rotable[\ptxt\|S^*] \gets \bits^\secpar$
$R $
${}:= {}$
$\ro(\ptxt \| S^*)$
$\rotable[\ptxt \| S^*]$
${}\gets \bits^\secpar$
$\ctxt^* $
${}:= \Sigma.\Enc(\pk, \ptxt \| S^*; R) $
${}\gets \Sigma.\C\bigr( |\ptxt| + \secpar \bigr)$
$\mathcal{D}[\ctxt^*] := \ptxt$
$B^* := \ptxt \| S^*$
$\ptxt^* := \ptxt$
return $\ctxt^*$
if $\ctxt == \ctxt^*$: return $\ptxt^*$
if $\mathcal{D}[\ctxt]$ defined: return $\mathcal{D}[\ctxt]$
$\ptxt \| S := \Sigma.\Dec(\sk,\ctxt)$
$R := \ro(\ptxt \| S)$
if
$\rotable[\ptxt\|S]$ undefined:
$\rotable[\ptxt \| S]$ undefined: return $\myerr$
$\rotable[\ptxt\|S] \gets \bits^\secpar$
if $\ctxt \ne \Sigma.\Enc(\pk,\ptxt\|S; $
$R)$:
$\rotable[\ptxt\|S])$:
$R)$:
return $\myerr$
return $\ptxt$
if $\rotable[A]$ undefined:
$\mathcal{A} := \mathcal{A} \cup \{ A \}$
$\rotable[A] \gets \bits^\secpar$
$C := \Sigma.\Enc(\pk,A; \rotable[A])$
write $\ptxt \| S := A$
$\mathcal{D}[C] := \ptxt$
return $\rotable[A]$
$S^* \gets \bits^\secpar$
$B^* := {}$
$\mathcal{D}[\ctxt^*] \| S^*$
$\ptxt^* \| S^*$
if $B^* \in \mathcal{A}$: $\badvar := \mytrue$