[
[
['5','add','hl'],
['9','add','hl'],
['21','add','hl'],
['24','add','hl'],
['2','add','slide-down']
],
[
['5','remove','hl'],
['5','add','hidden'],
['9','remove','hl'],
['9','add','hidden'],
['21','remove','hl'],
['21','add','hidden'],
['24','remove','hl'],
['24','add','hidden']
],
[
['321','add','hl'],
['55','remove','slide-up']
],
[
['322','add','hl'],
['322','remove','slide-left'],
['63','add','hl'],
['63','remove','hidden'],
['4','add','hidden'],
['321','remove','hl'],
['321','add','slide-right']
],
[
['322','remove','hl'],
['63','remove','hl'],
['63','add','hl'],
['331','add','hl'],
['337','add','hl'],
['340','add','hl'],
['328','add','hl'],
['80','remove','slide-up'],
['55','add','slide-down']
],
[
['99','add','hl'],
['99','remove','hidden'],
['100','add','hl'],
['100','remove','hidden'],
['101','add','hl'],
['101','remove','hidden'],
['102','add','hl'],
['102','remove','hidden'],
['103','add','hl'],
['103','remove','hidden'],
['104','add','hl'],
['104','remove','hidden'],
['105','add','hl'],
['105','remove','hidden'],
['26','remove','indent-1'],
['27','remove','indent-2'],
['28','remove','indent-1'],
['63','remove','hl'],
['63','add','hidden'],
['331','remove','hl'],
['331','add','slide-left'],
['337','remove','hl'],
['337','add','slide-right'],
['340','remove','hl'],
['340','add','slide-left'],
['328','remove','hl'],
['328','add','slide-left'],
['26','add','indent-2'],
['27','add','indent-3'],
['28','add','indent-2']
],
[
['99','remove','hl'],
['100','remove','hl'],
['101','remove','hl'],
['102','remove','hl'],
['103','remove','hl'],
['104','remove','hl'],
['105','remove','hl'],
['333','add','hl'],
['324','add','hl'],
['111','remove','slide-up'],
['80','add','slide-down']
],
[
['127','add','hl'],
['127','remove','hidden'],
['128','add','hl'],
['128','remove','hidden'],
['129','add','hl'],
['129','remove','hidden'],
['325','add','hl'],
['325','remove','slide-left'],
['333','remove','hl'],
['333','add','slide-left'],
['324','remove','hl'],
['324','add','slide-right']
],
[
['127','remove','hl'],
['128','remove','hl'],
['129','remove','hl'],
['325','remove','hl'],
['6','add','hl'],
['7','add','hl'],
['8','add','hl'],
['10','add','hl'],
['11','add','hl'],
['330','add','hl'],
['327','add','hl'],
['335','add','hl'],
['145','remove','slide-up'],
['111','add','slide-down']
],
[
['147','add','hl'],
['147','remove','hidden'],
['333','add','hl'],
['333','remove','slide-left'],
['331','add','hl'],
['331','remove','slide-left'],
['328','add','hl'],
['328','remove','slide-left'],
['334-slide','remove','slide-left'],
['6','remove','hl'],
['6','add','hidden'],
['7','remove','hl'],
['7','add','hidden'],
['8','remove','hl'],
['8','add','hidden'],
['10','remove','hl'],
['10','add','hidden'],
['11','remove','hl'],
['11','add','hidden'],
['330','remove','hl'],
['330','add','slide-right'],
['327','remove','hl'],
['327','add','slide-right'],
['335','remove','hl'],
['335','add','slide-right']
],
[
['147','remove','hl'],
['333','remove','hl'],
['331','remove','hl'],
['328','remove','hl']
],
[
['334-flip','add','flipped'],
['145','add','slide-down']
],
[
['147','add','hl'],
['333','add','hl'],
['336','add','hl'],
['328','add','hl']
],
[
['6','add','hl'],
['6','remove','hidden'],
['7','add','hl'],
['7','remove','hidden'],
['8','add','hl'],
['8','remove','hidden'],
['235','add','hl'],
['235','remove','hidden'],
['337','add','hl'],
['337','remove','slide-right'],
['327','add','hl'],
['327','remove','slide-right'],
['335','add','hl'],
['335','remove','slide-right'],
['147','remove','hl'],
['147','add','hidden'],
['333','remove','hl'],
['333','add','slide-left'],
['336','remove','hl'],
['336','add','slide-left'],
['328','remove','hl'],
['328','add','slide-left'],
['334-slide','add','slide-left']
],
[
['6','remove','hl'],
['7','remove','hl'],
['8','remove','hl'],
['235','remove','hl'],
['337','remove','hl'],
['327','remove','hl'],
['335','remove','hl'],
['333','add','hl'],
['331','add','hl'],
['100','add','hl'],
['101','add','hl'],
['263','remove','slide-up']
],
[
['333','add','hl'],
['333','remove','slide-left'],
['340','add','hl'],
['340','remove','slide-left'],
['328','add','hl'],
['328','remove','slide-left'],
['333','remove','hl'],
['333','add','slide-right'],
['331','remove','hl'],
['331','add','slide-right'],
['100','remove','hl'],
['100','add','hidden'],
['101','remove','hl'],
['101','add','hidden']
],
[
['333','remove','hl'],
['340','remove','hl'],
['328','remove','hl'],
['128','add','hl'],
['129','add','hl'],
['325','add','hl'],
['99','add','hl'],
['102','add','hl'],
['103','add','hl'],
['104','add','hl'],
['105','add','hl'],
['294','remove','slide-up'],
['263','add','slide-down']
],
[
['296','remove','hidden'],
['5','add','hl'],
['5','remove','hidden'],
['312','add','hl'],
['312','remove','hidden'],
['341','add','hl'],
['341','remove','slide-left'],
['330','add','hl'],
['330','remove','slide-right'],
['331','add','hl'],
['331','remove','slide-right'],
['336','add','hl'],
['336','remove','slide-left'],
['26','remove','indent-2'],
['27','remove','indent-3'],
['28','remove','indent-2'],
['128','remove','hl'],
['128','add','hidden'],
['129','remove','hl'],
['129','add','hidden'],
['325','remove','hl'],
['325','add','slide-right'],
['99','remove','hl'],
['99','add','hidden'],
['102','remove','hl'],
['102','add','hidden'],
['103','remove','hl'],
['103','add','hidden'],
['104','remove','hl'],
['104','add','hidden'],
['105','remove','hl'],
['105','add','hidden'],
['26','add','indent-1'],
['27','add','indent-2'],
['28','add','indent-1']
],
[
['5','remove','hl'],
['312','remove','hl'],
['341','remove','hl'],
['330','remove','hl'],
['331','remove','hl'],
['336','remove','hl']
]
]
The starting point is $\lib{kem-1cca-real+ro}$
Inline first call to $\ro$; the result is always chosen uniformly since it is the first call.
Replace every expression of the form $\rotable[\ctxt^*, \pk^{r^*}]$ with $\ptxt^*$. Similarly, introduce a new associative array $U[\cdot]$ and replace every expression of the form $\rotable[A,A^{\sk}]$ with $U[A]$.
Inline the call to $\ro$ made in $\ccaonedec$. Note that $\ccaonedec$ always calls $\ro$ with an input of the form $(A,A^{\sk})$, and this includes the case that $A = \ctxt^*$, where we have $(A,A^{\sk}) = (\ctxt^*,\pk^{r^*})$.
Apply gap CDH: $\sk$ becomes $x$; $\pk$ becomes $g^x$; $r^*$ becomes $y$; and $\ctxt^*$ becomes $g^y$.
Remove unreachable case in $\ro$
Rewrite expressions of the form $U[A]$ as $U[A,A^{\sk}]$, and rewrite $\ccaonedec$ in terms of a call to $\ro$ as before. The result is $\lib{kem-1cca-rand+ro}$, which completes the proof.
$\lib{kem-1cca-real+ro}$
$\lib{kem-1cca-rand+ro}$
$\sk \gets \Z_n$
$\pk := g^{\sk}$
$r^* \gets \Z_n$
$\ctxt^* := g^{r^*}$
$(\pk,\ctxt^*) := \subname{gapcdh.get}()$
$\ctxt^* \gets \G$
$\ptxt^* $
${}:= \ro( \ctxt^*, \pk^{r^*} )$
${}\gets \bits^n$
$\rotable[\ctxt^*, \pk^{r^*}] := \ptxt^* $
return $\pk$
return $(\ctxt^*, \ptxt^*)$
if $\ctxt == \ctxt^*$: return $\ptxt^*$
if $U[\ctxt]$ undefined:
$U[\ctxt] \gets \bits^n$
return
$\ro( \ctxt, \ctxt^{\sk} )$
$U[\ctxt]$
$\ro(\ctxt, \ctxt^{\sk})$
if
$(A,B) == (\ctxt^*, \pk^{r^*})$:
$A == \ctxt^*$ and
$\subname{gapcdh.test}(B)$:
$\myfalse$:
$A^{\sk} == B$:
return $\ptxt^*$
else if
$A^{\sk} == B$:
$\subname{gapcdh.ddh}(A,B)$:
$A^{\sk} == B$:
if $U[A]$ undefined:
$U[A] \gets \bits^n$
return $U[A]$
else:
if $\rotable[A,B]$ undefined:
$\rotable[A,B] \gets \bits^n$
return $\rotable[A,B]$
$\link$
$\lib{gapcdh-real}$
$x \gets \Z_n$
$y \gets \Z_n$
$Y := g^y$
return $(g^x, g^y)$
return $S^x == T$
return $Z == g^{xy}$
$\lib{gapcdh-fake}$
$x \gets \Z_n$
$Y \gets \G$
return $(g^x, Y)$
return $S^x == T$
return $\myfalse$