lib \lib{cpa-real}
    \key \gets \bits^\secpar

    proc \cpaenc(\ptxt)
        // $R\|S \gets \Enc(\key,\ptxt)$
        R \gets \bits^\secpar
        Y := F(\key,R)
        S := Y \oplus \ptxt
        return $R\|S$
end

caption The starting point is $\lib{cpa-real}$.

\equiv

lib
    proc \cpaenc(\ptxt) R \gets \bits^\secpar
        R \gets \bits^\secpar
        Y := \prfquery(R)
        S := Y \oplus \ptxt
        return $R\|S$
end
lib \lib{prf-real}
    \key \gets \bits^\secpar

    proc \prfquery(X)
        return $F(\key,X)$
end

caption We can apply the security of the PRF in a standard three-hop maneuver:


\indist

lib
    proc \cpaenc(\ptxt)
        R \gets \bits^\secpar
        Y := \prfquery(R)
        S := Y \oplus \ptxt
        return $R\|S$
end
lib \lib{prf-rand}
    proc \prfquery(X)
        if $\prftable[X]$ undefined:
            \prftable[X] \gets \bits^n
        return $\prftable[X]$
end


\equiv

lib
    proc \cpaenc(\ptxt)
        R \gets \bits^\secpar
        if $\prftable[R]$ undefined:
            \prftable[R] \gets \bits^n
        S := \prftable[R] \oplus \ptxt
        return $R\|S$
end

\equiv

caption Sampling $R$ uniformly is indistinguishable from sampling without replacement.

lib
    proc \cpaenc(\ptxt)
        R := \bdaysamp()
        if $\prftable[R]$ undefined:
            \prftable[R] \gets \bits^n
        S := \prftable[R] \oplus \ptxt
        return $R\|S$
end
lib \lib{samp-rand}
    proc \bdaysamp()
        R \gets \bits^\secpar
        return $R$
end

\indist


lib
    proc \cpaenc(\ptxt)
        R := \bdaysamp()
        if $\prftable[R]$ undefined:
            \prftable[R] \gets \bits^n
        S := \prftable[R] \oplus \ptxt
        return $R\|S$
end
lib \lib{samp-uniq}
    proc \bdaysamp()
        R \gets \bits^\secpar \setminus \mathcal{R}
        \mathcal{R} := \mathcal{R} \cup \{ R \}
        return $R$
end


\equiv

lib
    proc \cpaenc(\ptxt)
        R \gets \bits^\secpar \setminus \mathcal{R}
        \mathcal{R} := \mathcal{R} \cup \{R\}
        if $\prftable[R]$ undefined:
            \prftable[R] \gets \bits^n
        S := \prftable[R] \oplus \ptxt
        return $R\|S$
end

\equiv

caption In this hybrid, the $R$ values can never repeat, so the if-statement is always taken. Thus, we can make its body unconditional.

lib
    proc \cpaenc(\ptxt)
        R \gets \bits^\secpar \setminus \mathcal{R}
        \mathcal{R} := \mathcal{R} \cup \{R\}
        \prftable[R] \gets \bits^n
        S := \prftable[R] \oplus \ptxt
        return $R\|S$
end

\equiv

caption Each value of $\prftable[R]$ is sampled uniformly and used only in a single \xor expression. As a result, $S$ is a OTP encryption of $\ptxt$, with $\prftable[R]$ playing the role of the key. 


lib
    proc \cpaenc(\ptxt)
        R \gets \bits^\secpar \setminus \mathcal{R}
        \mathcal{R} := \mathcal{R} \cup \{R\}
        S := \otpenc(\ptxt)
        return $R\|S$
end
lib \lib{otp-real}
    proc \otpenc(\ptxt)
        \key \gets \bits^n
        \ctxt := \key \oplus \ptxt
        return $\ctxt$
end

\equiv

lib
    proc \cpaenc(\ptxt)
        R \gets \bits^\secpar \setminus \mathcal{R}
        \mathcal{R} := \mathcal{R} \cup \{R\}
        S := \otpenc(\ptxt)
        return $R\|S$
end
lib \lib{otp-rand}
    proc \otpenc(\ptxt)
        R \gets \bits^n
        return $R$
end


\equiv

lib
    proc \cpaenc(\ptxt)
        R \gets \bits^\secpar \setminus \mathcal{R}
        \mathcal{R} := \mathcal{R} \cup \{R\}
        S \gets \bits^n
        return $R\|S$
end


\indist

caption Finally, we can revert $R$ so that it is sampled uniformly (with replacement).  The result is $\lib{cpa-rand}$, which completes the proof.

lib \lib{cpa-rand}
    proc \cpaenc(\ptxt)
        R \gets \bits^\secpar
        S \gets \bits^n

        return $R\|S$
end