Ordering of parameters to XOF() call in ML-KEM correct?

GaloisInc / cryptol-specs

A central repository for specifications of cryptographic algorithms in Cryptol

BSD 3-Clause "New" or "Revised" License

34 stars 7 forks source link

Ordering of parameters to XOF() call in ML-KEM correct? #71

Closed rod-chapman closed 1 month ago

rod-chapman commented 8 months ago

I note that you have implemented the calls to XOF() in ML-KEM (lines 283 and 298 of MLKEM/specification.cry) exactly as specified in the August 23rd Draft of FIPS-203. Specifically, you have "XOF(rho,i,j)" in both cases.

This is a change from Kyber that was not mentioned in the Change Log of FIPS-203 and generated some debate and disagreement in the PQC community. It appears that the community (and NIST) have settled that this is a mistake in FIPS-203 and it should really be "XOF(rho,j,i)".

Do you agree?

Does you Cryptol code pass the KATs provided by PQShield (e.g. https://github.com/post-quantum-cryptography/KAT.git) with or without that change?

Many thanks, Rod Chapman, AWS

mariosge commented 8 months ago

Hi Rod. Thank you for your detailed observation.

For line 283, adhering to the draft seems justified since line 288 uses A_hat as is.
For line 298, the suggestion to swap i and j is valuable. If we make this change, then we would have to adjust line 303 from (transpose A_hat) to A_hat directly. What do you think?

Regarding your question about compatibility with the KATs: Yes, our Cryptol code successfully passes both the PQShield KATs and the intermediate KATs provided by NIST, with the current implementation.

rod-chapman commented 8 months ago

Still not sure my code matches yours, although I might have misunderstood the semantics of you matrix comprehension expression in Cryptol.

Note that the PQShield KATs went through several revisions before we agreed on the correct ordering of the parameters. See, for example, commit: https://github.com/post-quantum-cryptography/KAT/commit/93d9853362362578a3059bfe9d52639b66f1fa0a

Which commit of that repo have you tested against?

rod-chapman commented 8 months ago

and then swaps it back again: https://github.com/post-quantum-cryptography/KAT/pull/4

rod-chapman commented 8 months ago

And see the final comment in this thread from Robin Larrieu: https://groups.google.com/a/list.nist.gov/g/pqc-forum/c/s-C-zIAeKfE

rod-chapman commented 8 months ago

Are you planning to attend the HACS workshop in Toronto, March 21-22? I will be there, plus the designers of LibJade from the Formosa team, the people from Cryspen, and most of the Kyber/MLKEM design team - in short - almost everyone that's worked on verified implementations of MLKEM... it would be good to all meet...