Hybrid Sequence:
The starting point is $\lib{cca-real}$.
We can add a cache to remember the plaintexts of ciphertexts generated in $\ccaenc$.
Apply the MAC property of the PRF, in a three-hop maneuver:
\FORMATTINGHACK{\needspace{5\baselineskip}\noindent}We now argue that the three if-conditions in $\ccadec$ are exhaustive. Why? Suppose the second and third if-statements are not taken, then we must have $\prftable[\ctxt] = T$. But the library assigns to $\prftable[\ctxt] := T$ only in $\ccaenc$, where it also assigns to $\mathcal{D}[\ctxt\|T]$! So the first if-statement would have been taken this case. Knowing that the last line of $\ccadec$ is unreachable, we can remove it:\FORMATTINGHACK{\pagebreak}
Now that $\key_e$ is used only to call $\Sigma.\Enc$, we can apply CPA security. The three-hop maneuver is omitted.
It is only with negligible birthday probability that $\ctxt$ repeats in the first line of $\ccaenc$. Thus the if-statement on the next line is always taken (except with negligible probability), and its body can be made unconditional. This can be shown in a standard sequence of steps (involving either a bad event or an appeal to \lemmaref{comp.lem.birthday-lib}), which are omitted here.
Suppose $\ccaenc$ generates a ciphertext $\ctxt \| T$, and later $\ccadec$ is called with a ciphertext of the form $\ctxt \| T'$. Then $\ccadec$ will return $\myerr$ if $T \ne T'$ \FORMATTINGHACK{\pagebreak}and otherwise return $\mathcal{D}[\ctxt\|T]$. In particular, $\ccadec$ never needs to consult $\prftable[\ctxt]$. Therefore, $\ccaenc$ does not need to assign $\prftable[\ctxt]$.
Finally, we can perform several of the previous changes, this time in reverse, and obtain $\lib{cca-rand}$.
$\lib{cca-real}$
$\key_e \gets \Sigma.\K$
$\key_m \gets \bits^\secpar$
$\ccaenc$($\ptxt$):
// $\ctxt $
${}\gets \Enc(\key,\ptxt)$
$\| T \gets \C^*(|\ptxt|)$:
$\ctxt $
${}:= \Sigma.\Enc(\key_e, \ptxt)$
${}\gets \Sigma.\C(|\ptxt|)$
$T $
${}:= {}$
$F(\key_m, \ctxt)$
$\macreveal(\ctxt)$
$\prftable[\ctxt]$
$\prftable[C] \gets \bits^\secpar$
${}\gets \bits^\secpar$
return $\ctxt \| T$
$\ccadec$($\ctxt \| T$):
// $\Sigma.\Dec(\key,\ctxt)$
if
$F(\key_m, \ctxt) \ne T$: return $\myerr$
not $\macguess(\ctxt, T)$: return $\myerr$
$\prftable[\ctxt] \ne T$: return $\myerr$
$F(\key_m,\ctxt) \ne T$: return $\myerr$
return $\Dec(\key_e, \ctxt)$
$\link$
$\lib{mac-real}$
$\key \gets \bits^\secpar$
$\macguess$($X,Y$):
return $Y == F(\key,X)$
$\macreveal$($X$):
return $F(\key,X)$
$\lib{mac-ideal}$
$\macguess$($X,Y$):
if $\prftable[X]$ undefined: return $\myfalse$
return $Y == \prftable[X]$
$\macreveal$($X$):
if $\prftable[X]$ undefined: $\prftable[X] \gets \bits^\secpar$
return $\prftable[X]$