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

["D. J. Bernstein" <[e-mail]>]

Neil Madden writes:
> Unlike some other commentators on this thread, I don't object to
> defining some generic constructions for C2PRI KEMs if there is a
> sufficient justification. If I was writing a library to implement
> this, I would use the type system to (try to) ensure constructions are
> used appropriately, something like:
>   type KEM ...
>   type C2PRIKEM extends KEM ...
>   def CK(trad: KEM, pq: C2PRIKEM) -> KEM
>   def UK(trad: KEM, pq: KEM) -> KEM

The above is an example of what I meant by "simple (but again nowhere
near universal) type discipline"; and type-checking tools for it are an
example of what I meant by "test mechanisms that enforce these security
requirements"---where I also noted that we're "nowhere near universal
deployment" of such test mechanisms.

For me, the real-world mess of different software-engineering practices
feeds into the analysis of the security consequences of protocol-level
designs. For example, some programmers leap at every opportunity to put
information into types while other programmers are allergic to this and
many more are somewhere in the middle. Many libraries will end up with
just a "KEM" concept (or maybe lump that further into a "group" concept)
without any tests that stop programmers from plugging a non-"C2PRI" KEM
into "CK". The main way for such tests to happen would be for the
library-architecture designers to notice and act upon the "C2PRI"
warnings in the spec; this certainly isn't a reliable mechanism. The
plugging mechanism will then be exposed to more programmers than the
architecture designers, and many of those programmers also won't notice
the "C2PRI" warnings in the spec.

Let me also point out that most type efforts simply give up when they
have to cross library boundaries. Look at how rustls calls aws-lc, for
example, and how aws-lc in turn calls s2n-bignum; there are quite a few
languages involved there, and very little type information is passed
between those languages. The most convincing correctness verification by
far is in s2n-bignum, which already has a full X25519 implementation and
is accumulating more and more components of ML-KEM; maybe s2n-bignum
will add not just full ML-KEM but also a "C2PRI" proof, if that proof
holds up; the proof system, HOL Light, can trivially promote this
property to a type; but it's not as if the interfaces are set up to pass
this information through to rustls. Realistically, if the information
gets into rustls then it would instead be with rustls manually tracking
properties of each primitive that it's importing.

---D. J. Bernstein


===== NOTICES =====

IETF BCP 78, "Rights Contributors Provide to the IETF Trust", Section 5
(normative), "Rights in Contributions", provides a modification right
"unless explicitly disallowed in the notices contained in a Contribution
(in the form specified by the Legend Instructions)".

The official language from IETF's "Legend Instructions" for the
situation that "the Contributor does not wish to allow modifications nor
to allow publication as an RFC" is as follows: "This document may not be
modified, and derivative works of it may not be created, and it may not
be published except as an Internet-Draft."
<https://trustee.ietf.org/wp-content/uploads/Corrected-TLP-5.0-legal-provsions.pdf>

The same language is used in, e.g., RFC 5831. The same language hereby
applies to this document. This is not disclaiming or limiting the
applicability of IETF policies; it is strictly following IETF policies.

IESG claims that the "explicitly disallowed" provision in BCP 78 is
limited to the examples in Section 3 in BCP 78. That is incorrect. BCP
78 states that Section 5, "Rights in Contributions", is normative, while
Section 3, "Exposition of Why These Procedures Are the Way They Are", is
informative. The opt-out provision in the normative text is clear, and
cannot be limited by an informative section. BCP 78 does not give IESG
any authority to issue changes or purported clarifications of the rules.

Rationale for exercising the BCP 78 opt-out provision: I'm fine with
redistribution of copies of this document. The issue is instead with
modification, such as (1) IESG's May 2025 posting of an IESG-mangled
version of an appeal that I had filed and (2) IETF management selling
IETF mailing-list text to AI companies. This goes far beyond what
copyright law allows as fair use (such as giving quotes for purposes of
commentary). When I complained about the mangled document, the IETF
Executive Director responded not by apologizing but instead by asserting
that IETF management had the power to do whatever it wanted.