Add support for PreHash ML-DSA

[mkannwischer]

This commit adds two functions crypto_sign_signature_pre_hash
and crypto_sign_verify_pre_hash implementing the pre-hashing mode of ML-DSA.
Instead of receiving a message, they receive a pre-hashed message.
Details can be found in Algorithm 4 and 5 in FIPS204.

The message to signed is formatted as
0x01 || ctxlen (1 byte) || ctx || oid || ph
where ph is the pre-hash and oid is the object identifier of the used hash
algorithm.

The ACVP client is adjusted to support the pre-hashing test cases. Note that
the ACVP testvectors only contain the message, not the pre-hash. I opted for
computing the hash in the ACVP Python client as for that we do not have to
add implementations for the 12 hash functions.

CBMC proofs for the new functions are added.

• Resolves ACVP: Consider adding preHash test cases #39
• Depends on ACVP: Add internal test cases #496

[mkannwischer]

Something that is not yet clear to me is if the pre hashing step should be included in mldsa-native or if it should be performed by the consumer.

If one strictly follows the NIST algorithms one should include it.

The reason for not including it was that the use case of PreHash ML-DSA is that the message is too large for the signer/verifier to process it internally.
But of course it could be that only one of signer/verifier cannot handle large message - for implementing the other party it can then be useful to have the regular signing API and perform prehashing internally.

I am not sure what we want here. The prospect of including 12 hash functions is not nice.

[mkannwischer]

Something that is not yet clear to me is if the pre hashing step should be included in mldsa-native or if it should be performed by the consumer.

If one strictly follows the NIST algorithms one should include it.

The reason for not including it was that the use case of PreHash ML-DSA is that the message is too large for the signer/verifier to process it internally. But of course it could be that only one of signer/verifier cannot handle large message - for implementing the other party it can then be useful to have the regular signing API and perform prehashing internally.

I am not sure what we want here. The prospect of including 12 hash functions is not nice.

I looked into how other crypto libraries are implementing this and it indeed seems to include the hashing internally. This PR will have to change and I will have to add a bunch of hash implementations. Probably going to take SHA-2 from https://github.com/pq-code-package/slhdsa-c.

[jakemas]

I looked into how other crypto libraries are implementing this and it indeed seems to include the hashing internally.

NIST provide some more details on this https://csrc.nist.gov/csrc/media/Projects/post-quantum-cryptography/documents/faq/fips204-sec6-03192025.pdf

They do mention HashML-DSA:

For example, as shown in the diagram below, module A may implement ML-DSA.Sign(sk, M, ctx) or
HashML-DSA.Sign(sk, M, ctx, PH). Module A’s implementation of either function may call MLDSA.Sign_mu(sk, mu), implemented on module B, which may then generate a random value rnd
and call ML-DSA.Sign_internal_mu(sk, mu, rnd). To perform a signature, module A would construct
M’, compute tr from pk, compute mu from tr and M’, then call module B via ML-DSA.Sign_mu(sk,
mu) to obtain the signature. Module A would be the module that computes mu, and module B
would be the signing module. In this case sk may not be the private key but a reference to it if it is
already available on module B. If module B only contains a single private key, sk may be omitted
from the interface.

Exciting stuff, looking forward to reviewing this. This also makes me think, with 3 variants: PureML-DSA, HashML-DSA, ExternalMuML-DSA all as options (plus various sign, sign_open, verify,verify_open combinations, perhaps we add a build mode configuration option that allows users to select which of these schemes are build by mldsa-native. Future work of course, just wanted to make a note of the idea.

[mkannwischer]

@jakemas @hanno-becker @rod-chapman
This is how it looks if we want to support all 12 hash functions for PreHash ML-DSA.
If we want to go down the path of having a local SHA-2 implementation, we will have to proof memory-safety of it. I tried this briefly, but I got stuck in proofing the compression function (it spins forever). It may be quite some work.
I currently don't see another way to pass all the ACVP testvectors.

Any better ideas?