Expose is_supported_alg in EverCrypt.DRBG API

[victor-dumitrescu]

Blake2b and Blake2s are now supported as agility arguments for EverCrypt HMAC and thus is_supported_alg returns true for them. According to the docs this should be the authoritative source of which algorithms are also supported for HMAC-DRBG.

However, when passing Blake2b/Blake2s to instantiate it throws KreMLin incomplete match at EverCrypt_DRBG.c:265 because the check doesn't include them.

[s-zanella]

This is primarily a typo in the documentation. Where it says "As always, the source is authoritative and you should check is_supported_alg in EverCrypt.HMAC.fsti.", it should read EverCrypt.DRBG.fsti. This comes from a change in is_supported_alg, which used to be shared between HMAC and HMAC-DRBG but now each primitive has its own definition.

Extending HMAC to support Blake2 and other non-NIST approved hash functions is straightforward. For HMAC-DRBG, this requires estimating the security strength of Blake2-based HMACs. Now, Blake2 already has its own keying mechanism, so I'm not sure about the motivation to support instantiating HMAC with Blake2 or having a Blake2-based HMAC-DRBG. If there's a genuine use case, this can be done, but there are better ways to construct a DRBG from Blake2.

[victor-dumitrescu]

Thanks for the details! Just to clarify, I wasn't trying to use HMAC-DRBG with Blake2, it was just a small discrepancy that I found while testing and documenting the OCaml API.

[victor-dumitrescu]

I see there is an is_supported_alg in Spec.HMAC_DRBG but as far as I can tell it's not exposed in EverCrypt.DRBG or anywhere else.

[s-zanella]

You're right. is_supported_alg needs to be exposed in EverCrypt.DRBG in the same way as it is for EverCrypt.HMAC.