caption The starting point is $\lib{kem-1cca-real+ro}$

lib \lib{kem-1cca-real+ro}
    // $\KeyGen$:
    \sk \gets \Z_n
    \pk := g^{\sk}

    // $(\ctxt^*, \ptxt^*) := \Encaps(\pk)$:
    r^* \gets \Z_n
    \ctxt^* := g^{r^*}
    \ptxt^* := \ro( \ctxt^*, \pk^{r^*} )

    proc \ccaonepk()
        return $\pk$

    proc \ccaoneenc()
        return $(\ctxt^*, \ptxt^*)$

    proc \ccaonedec(\ctxt)
        // $\Decaps(\sk,\ctxt)$:
        return $\ro( \ctxt, \ctxt^{\sk} )$

    // random oracle expecting two group elements:
    proc \ro(A,B)
        if $\rotable[A,B]$ undefined:
            \rotable[A,B] \gets \bits^n
        return $\rotable[A,B]$
end


\equiv

lib \lib{kem-1cca-real+ro}
    \sk \gets \Z_n
    \pk := g^{\sk}

    r^* \gets \Z_n
    \ctxt^* := g^{r^*}
    \ptxt^* := \ro( \ctxt^*, \pk^{r^*} )

    proc \ccaonepk()
        return $\pk$

    proc \ccaoneenc()
        return $(\ctxt^*, \ptxt^*)$

    proc \ccaonedec(\ctxt)
        return $\ro( \ctxt, \ctxt^{\sk} )$

    proc \ro(A,B)
        if $\rotable[A,B]$ undefined:
            \rotable[A,B] \gets \bits^n
        return $\rotable[A,B]$
end



\equiv

caption Inline first call to $\ro$; the result is always chosen uniformly since it is the first call.

lib 
    \sk \gets \Z_n
    \pk := g^{\sk}

    r^* \gets \Z_n
    \ctxt^* := g^{r^*}
    \ptxt^* \gets \bits^n
    \rotable[\ctxt^*, \pk^{r^*}] := \ptxt^*    

    proc \ccaonepk()
        return $\pk$

    proc \ccaoneenc()
        return $(\ctxt^*, \ptxt^*)$

    proc \ccaonedec(\ctxt)
        return $\ro( \ctxt, \ctxt^{\sk} )$

    proc \ro(A,B)
        if $\rotable[A,B]$ undefined:
            \rotable[A,B] \gets \bits^n
        return $\rotable[A,B]$
end


\equiv

caption 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]$.

lib 
    \sk \gets \Z_n
    \pk := g^{\sk}

    r^* \gets \Z_n
    \ctxt^* := g^{r^*}
    \ptxt^* \gets \bits^n

    proc \ccaonepk()
        return $\pk$

    proc \ccaoneenc()
        return $(\ctxt^*, \ptxt^*)$

    proc \ccaonedec(\ctxt)
        return $\ro( \ctxt, \ctxt^{\sk} )$

    proc \ro(A,B)
        if $(A,B) == (\ctxt^*, \pk^{r^*})$:
            return $\ptxt^*$
        else if $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]$
end



\equiv
caption 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^*})$.

lib 
    \sk \gets \Z_n
    \pk := g^{\sk}

    r^* \gets \Z_n
    \ctxt^* := g^{r^*}
    \ptxt^* \gets \bits^n

    proc \ccaonepk()
        return $\pk$

    proc \ccaoneenc()
        return $(\ctxt^*, \ptxt^*)$

    proc \ccaonedec(\ctxt)
        if $\ctxt == \ctxt^*$: return $\ptxt^*$
        if $U[\ctxt]$ undefined:
            U[\ctxt] \gets \bits^n
        return $U[\ctxt]$

    proc \ro(A,B)
        if $(A,B) == (\ctxt^*, \pk^{r^*})$:
            return $\ptxt^*$
        else if $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]$
end



\equiv

caption Apply gap CDH: $\sk$ becomes $x$; $\pk$ becomes $g^x$; $r^*$ becomes $y$; and $\ctxt^*$ becomes $g^y$.

lib 
    (\pk,\ctxt^*) := \subname{gapcdh.get}()
    \ptxt^* \gets \bits^n

    proc \ccaonepk()
        return $\pk$

    proc \ccaoneenc()
        return $(\ctxt^*, \ptxt^*)$

    proc \ccaonedec(\ctxt)
        if $\ctxt == \ctxt^*$: return $\ptxt^*$:
        if $U[\ctxt]$ undefined:
            U[\ctxt] \gets \bits^n
        return $U[\ctxt]$

    proc \ro(A,B)
        if $A == \ctxt^*$ and $\subname{gapcdh.test}(B)$:
            return $\ptxt^*$
        else if $\subname{gapcdh.ddh}(A,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]$
end


lib \lib{gapcdh-real}
    x \gets \Z_n
    y \gets \Z_n
    Y := g^y

    proc gapcdh.get()
        return $(g^x, g^y)$

    proc gapcdh.ddh(S,T)
        return $S^x == T$

    proc gapcdh.test(Z)
        return $Z == g^{xy}$
end

\indist


lib 
    (\pk,\ctxt^*) := \subname{gapcdh.get}()
    \ptxt^* \gets \bits^n

    proc \ccaonepk()
        return $\pk$

    proc \ccaoneenc()
        return $(\ctxt^*, \ptxt^*)$

    proc \ccaonedec(\ctxt)
        if $\ctxt == \ctxt^*$: return $\ptxt^*$:
        if $U[\ctxt]$ undefined:
            U[\ctxt] \gets \bits^n
        return $U[\ctxt]$

    proc \ro(A,B)
        if $A == \ctxt^*$ and $\subname{gapcdh.test}(B)$:
            return $\ptxt^*$
        else if $\subname{gapcdh.ddh}(A,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]$
end
lib \lib{gapcdh-fake}
    x \gets \Z_n
    Y \gets \G

    proc gapcdh.get()
        return $(g^x, Y)$

    proc gapcdh.ddh(S,T)
        return $S^x == T$

    proc gapcdh.test(Z)
        return $\myfalse$
end



\equiv

lib 
    \sk \gets \Z_n
    \pk := g^{\sk}
    
    \ctxt^* \gets \G
    \ptxt^* \gets \bits^n

    proc \ccaonepk()
        return $\pk$

    proc \ccaoneenc()
        return $(\ctxt^*, \ptxt^*)$

    proc \ccaonedec(\ctxt)
        if $\ctxt == \ctxt^*$: return $\ptxt^*$
        if $U[\ctxt]$ undefined:
            U[\ctxt] \gets \bits^n
        return $U[\ctxt]$

    proc \ro(A,B)
        if $A == \ctxt^*$ and $\myfalse$:
            return $\ptxt^*$
        else if $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]$
end



\equiv
caption Remove unreachable case in $\ro$

lib 
    \sk \gets \Z_n
    \pk := g^{\sk}
    
    \ctxt^* \gets \G
    \ptxt^* \gets \bits^n

    proc \ccaonepk()
        return $\pk$

    proc \ccaoneenc()
        return $(\ctxt^*, \ptxt^*)$

    proc \ccaonedec(\ctxt)
        if $\ctxt == \ctxt^*$: return $\ptxt^*$
        if $U[\ctxt]$ undefined:
            U[\ctxt] \gets \bits^n
        return $U[\ctxt]$

    proc \ro(A,B)
        if $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]$
end



\equiv
caption 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 \lib{kem-1cca-rand+ro}
    // $\KeyGen$:
    \sk \gets \Z_n
    \pk := g^{\sk}
    
    \ctxt^* \gets \G
    \ptxt^* \gets \bits^n

    proc \ccaonepk()
        return $\pk$

    proc \ccaoneenc()
        return $(\ctxt^*, \ptxt^*)$

    proc \ccaonedec(\ctxt)
        if $\ctxt == \ctxt^*$: return $\ptxt^*$
        // $\Decaps(\sk,\ctxt)$:
        return $\ro(\ctxt, \ctxt^{\sk})$

    proc \ro(A,B)
        if $\rotable[A,B]$ undefined:
            \rotable[A,B] \gets \bits^n
        return $\rotable[A,B]$
end