Nice analysis by Bruno Blanchet that proves that HPKE with ML-KEM (or any other IND-CCA2 KEM) does provide IND-CCA2 security.
“Bruno models the base mode of HPKE, single shot API in CryptoVerif, and showed that if the KEM is IND-CCA2, then so is HPKE.
Since CryptoVerif is PQ-sound, that proves the security of the HPKE base mode, with the single shot API when the KEM is a post-quantum IND-CCA2 KEM.” via Karthikeyan Bhargavan on the CFRG mailing list
The post-quantum transition is causing us to abstract cryptographic protocols over Key Encapsulation Mechanisms as opposed to Diffie-Hellman-like non-interactive key exchanges.
These two papers on the binding models for KEMs are great reads on the gotchas of working with KEMs and the properties they may or may not have.
Add comment