Kyber-CCA-KEM - Deterministic implicit rejection

Let me assume that you want to use the following decapsulation algorithm:

1. On input $sk$ and $c$:
2. let $m' = \mathrm{Dec}(sk,c)$
3. if $m' = \bot$ or $\mathrm{Enc}(pk,m';G(m')) \neq c$, then return $H(sk,c)$
4. else return $H(m',c)$

The explicit-rejection version of the Fujisaki-Okamoto transform, where the decapsulation algorithm returns $\bot$ in step 3, is secure in the (Q)ROM. (See Hövelmanns, Hülsing, and Majenz (ASIACRYPT 2022) and Ge, Shan, and Xue (CRYPTO 2023).) Thus, the variant where the decapsulation algorithm returns $F(pk,c)$ for some fixed $F$ independent from $sk$ is also secure. But, if it involves sk as $H(sk,c)$, this value 'leaks' $sk$. We need to argue if it is secure or not.

Fortunately, this variant using $H(sk,c)$ is directly treated in Chen, Lu, Jia, and Li (ISC 2022). Since Kyber's key pair (pk,sk) is (almost surely) one-to-one, we can use their theorem and the variant is secure in the QROM.

NOTE: I didn't check their proof in detail. Additional Note: Kyber might modify their FO transform according to the discussion in the PQC mailing list.