HKDF (EverCrypt_HKDF.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.

Note

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

Agile API

The expand and extract functions are agile and multiplexing:


void
EverCrypt_HKDF_extract(
  Spec_Hash_Definitions_hash_alg a,
  uint8_t *prk,
  uint8_t *salt,
  uint32_t saltlen,
  uint8_t *ikm,
  uint32_t ikmlen
);
  • prk is the output parameter
  • ikm means “input key material”
  • if saltlen approaches 4GB then you need to make sure it satisfies keysized in Spec.Agile.HMAC.fsti
  • if ikmlen approaches 4GB then you need to check the preconditions from extract_st, in EverCrypt.HKDF.fsti.

void
EverCrypt_HKDF_expand_sha1(
  uint8_t *okm,
  uint8_t *prk,
  uint32_t prklen,
  uint8_t *info,
  uint32_t infolen,
  uint32_t len
);
  • okm (“output key material”) is the output parameter
  • if prklen approaches 4GB then you need to make sure it satisfies keysized in Spec.Agile.HMAC.fsti
  • if infolen approaches 4GB then you need to check the precondition on infolen in expand_st, in EverCrypt.HKDF.fsti.

These functions dynamically dispatch onto one of the specialized, non-agile versions below. As such, the cost of agility is one test.

Non-agile API

The expand_* and extract_* functions are non-agile and multiplexing:


void
EverCrypt_HKDF_expand_sha2_512(
  uint8_t *okm,
  uint8_t *prk,
  uint32_t prklen,
  uint8_t *info,
  uint32_t infolen,
  uint32_t len
);



void
EverCrypt_HKDF_extract_sha2_512(
  uint8_t *prk,
  uint8_t *salt,
  uint32_t saltlen,
  uint8_t *ikm,
  uint32_t ikmlen
);

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