HMAC (EverCrypt_HMAC.h)

This API is:

  • agile
  • multiplexing: portable C (all); SHAEXT (SHA2-256)
  • NOT stateful

Possible values for the agility argument (Hacl_Spec.h) :

#define Spec_Hash_Definitions_SHA2_224 0
#define Spec_Hash_Definitions_SHA2_256 1
#define Spec_Hash_Definitions_SHA2_384 2
#define Spec_Hash_Definitions_SHA2_512 3
#define Spec_Hash_Definitions_SHA1 4
#define Spec_Hash_Definitions_MD5 5
#define Spec_Hash_Definitions_Blake2S 6
#define Spec_Hash_Definitions_Blake2B 7

Supported values for the agility argument: SHA1; SHA2_256; SHA2_384; SHA2_512.


As always, the source is authoritative and you should check is_supported_alg in EverCrypt.HMAC.fsti.

Agile API

The compute function is agile and multiplexing:

  Spec_Hash_Definitions_hash_alg a,
  uint8_t *mac,
  uint8_t *key,
  uint32_t keylen,
  uint8_t *data,
  uint32_t datalen

It dynamically dispatches onto one of the specialized, non-agile versions below. As such, the cost of agility is one test.

  • The mac argument must have a suitable hash length for the choice of algorithm; see hash_length in Spec.Agile.Hash.fsti
  • If keylen approaches 4GB then you need to make sure it satisfies keysized in Spec.Agile.HMAC.fsti
  • If your datalen approaches 4GB then you need to check the refinement on the data parameter of compute_st, in EverCrypt.HMAC.fsti.

Non-agile API

The compute_* functions are non-agile and multiplexing:

  uint8_t *dst,
  uint8_t *key,
  uint32_t key_len,
  uint8_t *data,
  uint32_t data_len

A non-agile, non-multiplexing copy of this API exists in Hacl_HMAC.h.