[
[
['10','add','hl'],
['46','add','hl'],
['29','remove','slide-up'],
['15','add','slide-down']
],
[
['47','add','hl'],
['47','remove','slide-left'],
['3','add','hidden'],
['10','remove','hl'],
['10','add','hidden'],
['46','remove','hl'],
['46','add','slide-right']
],
[
['47','remove','hl'],
['11','add','hl'],
['49','add','hl'],
['43','remove','slide-up'],
['29','add','slide-down']
],
[
['33','remove','hidden'],
['50','add','hl'],
['50','remove','slide-left'],
['11','remove','hl'],
['11','add','hidden'],
['49','remove','hl'],
['49','add','slide-right']
],
[
['50','remove','hl']
]
]
Starting with $\lib{pk-cpa-real}$,
we can immediately apply the CPA-security of $\Sigma_{\text{pke}}$. The simple three-hop maneuver is not shown.
With the ephemeral key $\key$ no longer used except to encrypt $\ptxt$, we can apply the one-time secrecy property. Again, the three-hop maneuver is not shown, and the result is $\lib{pk-cpa-rand}$, completing the proof.
$\lib{pk-cpa-real}$
$\lib{pk-cpa-rand}$
$(\pk,\sk) \gets \Sigma_{\text{pke}}.\KeyGen$
return $\pk$
$\key \gets \Sigma_{\text{ske}}.\K$
$\ctxt_{\text{pke}} $
${}:= \Sigma_{\text{pke}}.\Enc(\pk,\key)$
${}\gets \Sigma_{\text{pke}}.\C$
$\ctxt_{\text{ske}} $
${}:= \Sigma_{\text{ske}}.\Enc(\key,\ptxt)$
${}\gets \Sigma_{\text{ske}}.\C( |\ptxt| )$
return $(\ctxt_{\text{pke}}, \ctxt_{\text{ske}})$