[CFRG] Re: RG Last Call on draft-irtf-cfrg-hybrid-kems-12 and draft-irtf-cfrg-concrete-hybrid-kems-04

[Douglas Stebila <[e-mail]>]

Dear CFRG,

We have built ProofFrog models of the four hybrid KEM frameworks (CG, CK, UG, UK) in the draft, in both the seeded and the expanded decapsulation key format, and developed 57 machine-checked proofs of correctness, IND-CCA security, and the binding notions.  This message gives five comments for the research group last call.

A longer preliminary report, with details on the modelling, results, and suggested draft text for each comment, is at:

  https://github.com/ProofFrog/examples/blob/main/applications/cfrg-hybrid-kems/REPORT-CFRG-20260722.md

The models and proofs themselves are at:

  https://github.com/ProofFrog/examples/tree/main/applications/cfrg-hybrid-kems


Main conclusions
----------------

We did not find any attacks, and most of the claims made in the draft are supported by our analysis.  For some binding properties that the draft states as holding in the standard model, we were able to give proofs only in the random oracle model.  We support publication once the claims identified in comment 1 below are clarified.  The changes we suggest are to the security considerations text rather than to the constructions.

Our analysis was done against draft -10, but we have checked applicability to draft -12.


What we checked
---------------

For each of the four hybrid frameworks, in both the seeded and the expanded decapsulation key format, we proved:
- correctness;
- IND-CCA under each of the two complementary assumptions, that is, one proof assuming the post-quantum component is secure and one assuming the traditional component is;
- binding: LEAK-BIND-K-CT and LEAK-BIND-K-PK, and, in some cases, HON-BIND-K-CT and HON-BIND-K-PK.

This yields 57 proofs, with each file stating the assumptions used for the result to go through.  Most proofs are in the standard model, but 4 of the 16 IND-CCA proofs and 6 of the 30 binding proofs are in the random oracle model; the latter six are the subject of comment 1.


Comments
--------

1. LEAK binding for CG-seeded and CK-seeded is not established in the standard model.  (Draft -12 Sections 5.2, 6.4.2, 6.4.1)

Every LEAK-BIND result in our suite holds in the standard model except for CG and CK in the seeded format, where we were able to obtain it only by modelling the seed-expansion PRG as a programmable random oracle.  A LEAK-BIND adversary is given the honestly generated decapsulation key, which in the seeded format is the seed itself, so PRG security cannot be invoked; UG and UK are unaffected because their binding argument reduces directly to a KDF collision without relying on an underlying binding assumption.

Draft -12 Section 5.2 makes the seeded format the primary definition of the decapsulation key, so the format the draft prefers is the one for which our results are weaker.  The final sentence of the closing paragraph of Section 6.4.1 extends its PRG argument to the binding sketches of Section 6.4.2, which for CG and CK in the seeded format is precisely the step we were unable to take.

We did not find an attack and we do not claim the property fails.  Our suggestion is to limit that sentence to the IND-CCA analyses, and to state the CG and CK binding sketches as random oracle model results for the seeded format.


2. The traditional branches of UG and CG depend on a variant of SDH over shared-secret encodings, not group elements.  (Draft -12 Sections 4.2, 6.1.3, 6.2.1)

Draft -12 Section 6.2.1 requires that the strong Diffie-Hellman problem be hard in Group_T, but our UG and CG traditional-branch proofs do not reduce to that assumption.  They reduce to a variant in which both the adversary's target and its decision oracle range over shared-secret encodings rather than over group elements.  Because Section 4.2 does not require ElementToSharedSecret to be injective, and gives the two-to-one X-coordinate map as its example, neither the target nor the oracle carries over directly; we are not aware of a reduction in either direction between the two assumptions.  We recommend that Sections 6.1.3 and 6.2.1 refer to the variant explicitly.


3. The seed-based analyses repeatedly assume that GenerateKeyPair is equivalent to DeriveKeyPair on a random seed.  (Draft -12 Sections 6.4.1, 5.2, 4.1, 6.2)

Draft -12 Section 6.4.1 argues that component key pairs derived from a single seed are indistinguishable from independently generated ones.  PRG security gives independent uniform seeds, but the key pairs still come from DeriveKeyPair applied to those seeds, whereas the analyses in the literature assume GenerateKeyPair; the argument needs the two to give the same distribution.  Draft -12 Section 5.2 states that equivalence for the hybrid, but Section 4.1 does not state it for the components.

The same step is needed in every seeded analysis, the IND-CCA ones included.  The property holds by definition for the KEMs the draft targets, ML-KEM among them, but it does not follow from the Section 4.1 interface alone.  We suggest listing this condition among the other component requirements in Section 6.2.


4. Draft -12 discusses rejection handling but does not apply it in the pseudocode or the CG and CK binding arguments.  (Draft -12 Sections 4.1, 4.2, 5.3 to 5.6, 6.4.2)

Draft -12 Section 4.1 states that decapsulation may return an error, and Section 4.2 that the hybrid returns an error when Group_T.Exp does.  The decapsulation pseudocode in Sections 5.3 to 5.6 nonetheless computes a shared secret unconditionally, with no check that the component decapsulations succeeded, whereas three of the four analyses the draft cites do include such a check.  Stating explicit-rejection versions of that pseudocode separately would resolve the discrepancy.

The preamble to Section 6.4.2 separately argues that the collision arguments are unaffected by how rejection is signalled.  For UG and UK that argument terminates in a KDF collision and is easy to follow, but for CG and CK it does not terminate there: it continues into a reduction to binding of the post-quantum component, which is where rejection behaviour seems most likely to matter.  Since we did not model explicit rejection, we can offer no conclusion either way, and it would be worth giving that argument explicitly for those two frameworks.


5. Indifferentiability of the KDF is not needed for most of the results.  (Draft -12 Sections 6.1.5, 6.2.1)

Draft -12 Section 6.1.5 requires the KDF to be indifferentiable from a random oracle, even to a quantum attacker, while Section 6.2.1 notes that some analyses need only a PRF-style assumption and says the draft ignores this for simplicity.  Our results make that alternative concrete: of the 8 IND-CCA results, one per framework and branch, 6 assume only that the KDF is a pseudorandom function, the exceptions being the traditional branches of UG and CG, which do model it as a random oracle.  Every binding result assumes only collision resistance of the KDF.

We suggest recording in Section 6.2.1 which assumptions suffice for which results; this would let an instantiation justify a KDF that is not known to be indifferentiable, and Section 6.1.5 could then note that indifferentiability is required only where a proof models the KDF as a random oracle.


Scope of the analysis
---------------------

  - Everything is generic over the component KEM and the nominal group; we don't prove anything about or depend on specifics of ML-KEM, X25519, P-256 or any other concrete choice.
  - We model only implicitly rejecting KEMs.  Draft -12 Section 4.2 allows a hybrid over groups such as P-256 or ristretto255 where some byte strings do not decode and thus lead to explicit rejection, so our binding results for UG and CG do not cover those instantiations.
  - ProofFrog does not distinguish classical from quantum adversaries, and our random-oracle-model results do not carry over to the QROM.
  - We do not prove MAL-BIND.
  - ProofFrog is a research prototype rather than a verified proof assistant.  We re-check some proofs in EasyCrypt where we can, and 28 of the 57 are currently accepted there, but those EasyCrypt models and proofs have not been reviewed by an EasyCrypt expert.
  - We used an LLM coding agent extensively, including in authoring the proofs and the ProofFrog engine itself.  Every proof is machine-checked regardless of how it was drafted, but that only helps if the checker is correct, and the ProofFrog checker is itself partly agent-authored.

The report expands on each of these.


  Report:  https://github.com/ProofFrog/examples/blob/main/applications/cfrg-hybrid-kems/REPORT-CFRG-20260722.md
  Models:  https://github.com/ProofFrog/examples/tree/main/applications/cfrg-hybrid-kems


Douglas Stebila and Camryn Steckel
University of Waterloo

P.S. Sorry this comes so close to the end of the last call.





> On Jul 8, 2026, at 6:24 AM, Nick Sullivan <[e-mail]> wrote:
> 
> Dear CFRG,
> 
> This message starts a two-week RG Last Call on two related documents. The last
> call ends on Wednesday July 22, 2026:
> 
>   Hybrid PQ/T Key Encapsulation Mechanisms (generic constructions)
>   draft-irtf-cfrg-hybrid-kems-12
>   https://www.ietf.org/archive/id/draft-irtf-cfrg-hybrid-kems-12.html
> 
>   Concrete Hybrid PQ/T Key Encapsulation Mechanisms
>   draft-irtf-cfrg-concrete-hybrid-kems-04
>   https://www.ietf.org/archive/id/draft-irtf-cfrg-concrete-hybrid-kems-04.html
> 
> Both are intended as Informational RFCs. Please reply on-list with your position
> on each document: ready to publish as-is, ready with specific changes, or not
> ready, together with the technical reasons. This feedback will help the chairs
> judge whether the documents are ready for IRSG review and publication.
> 
> The scope and approach of this work were settled when the group adopted it well
> over a year ago, and both drafts have developed on the list in the open since
> then. This last call is about whether the text is technically correct and
> complete, so please ground any objection in a specific problem with the
> documents. Detailed comments are best filed as issues on the repositories
> (https://github.com/cfrg/draft-irtf-cfrg-hybrid-kems,
> https://github.com/cfrg/draft-irtf-cfrg-concrete-hybrid-kems) positions belong
> here on the list.
> 
> Both documents were reviewed by the CFRG Crypto Review Panel ahead of this last
> call. The reviews are on the CFRG and crypto-panel lists:
> 
>   Thomas Pornin (NCC Group), 3 June 2026, reviewed the generic framework with a
>   focus on the constructions and reductions, and concluded that it describes a
>   secure construction, with editorial and technical comments now reflected in -12.
> 
>   Virendra Kumar (Qualcomm), 8 June 2026, reviewed the generic framework for
>   clarity, with notational comments now reflected in -12.
> 
>   Russ Housley (Vigil Security), 2 June 2026, reviewed both drafts and found the
>   constructions and instantiations as specified.
> 
> The current revisions incorporate changes proposed by the panel's comments.
> 
> Thank you,
> Nick, for the CFRG chairs
> _______________________________________________
> CFRG mailing list -- [e-mail]
> To unsubscribe send an email to [e-mail]