HPKE, published as RFC 9180, describes a scheme for hybrid public key encryption.

📚 Please go and read our TL;DR on HPKE if you nee more background on HPKE.

In this I describe the first executable HPKE specification using hacspec. It is not only an executable specification of HPKE, it is also an annotated version of the RFC that can be read instead of (or in addition to) the RFC. While the TL;DR on HPKE was intended for consumers or potential users of HPKE, this blog post is aimed at implementators that want to implement HPKE or understand it better.

It is a showcase for Cryspen’s technology stack. In a follow up blog post we will describe how to connect the hacspec specification to efficient cryptographic primitives and formal proofs.

This blog post focuses on the Base and Auth mode with DHKEM to demonstrate the capabilities of hacspec. For the full specification please read the full documentation, or look at the Github repository for the HPKE hacspec source code.

Recall that HPKE provides a variant of public-key encryption of arbitrary-sized plaintexts for a recipient public key. It works for any combination of an asymmetric key encapsulation mechanism (KEM), key derivation function (KDF), and authenticated encryption with additional data (AEAD) encryption function.

In the following I’ll first show the high-level API of HPKE works before giving details on the core functions within HPKE. All code examples are in hacspec.

💡 Go ahead and run the hacspec HPKE in the browser.

Encrypting to a Public Key

This is the most basic functionality HPKE offers; encrypting a payload to a public key. So how does this look on the outside?

The process consists of two steps. First a random shared_secret is generated that can be used for symmetric encryption with an AEAD, and an encapsulation that can be used by the receiver in combination with their private key to compute the same shared_secret. This function is denoted SetupBaseS below (because this is setting up the sender in the HPKE base mode). Note that the setup function expands the shared_secret to a key schedule that is used by the AEAD. More details in the Setup section. Then the shared_secret is used to encrypt the payload with an AEAD. This function is denoted AeadSeal below.

let (enc, (key, nonce, _, _)) = SetupBaseS(config, pkR, info, randomness)?;
let cipher_text = AeadSeal(aead_id, &key, &nonce, aad, payload)?;

The receiver gets cipher_text and enc that it can use to retrieve the payload.

let (key, nonce, _, _) = SetupBaseR(config, enc, skR, info)?;
let payload = AeadOpen(aead, &key, &nonce, aad, ct)?;

In the remainder of this blog post we’ll show how SetupBaseS is defined. For a description of the receiver please check out the documentation. We will not define AeadSeal and AeadOpen here as they follow the definition of RFC 5116.

The Auth Mode

In the Auth mode HPKE requires additional input to the Setup functions. The sender needs to provide their private key skS to authenticate themselves. The receiver uses the sender’s public key pkS in addition to authenticate the sender. The two functions are defined as follows.

SetupAuthS(config, pkR:, info, skS, randomness);
SetupAuthR(config, enc, skR, info, pkS);

Setup

In order to set up the KEM and key schedule the sender uses the following SetupBaseS function. Recall that the BaseS refers to the HPKE base mode and sender.

The function takes the receiver’s public key pkR and context information info (a sequence of bytes to bind the setup to a specific context). In addition we need to pass in the configuration that contains the mode as well as the algorithm identifiers for the KEM. Because hacspec can’t draw its own randomness, as explained below, it is passed in as well.

pub fn SetupBaseS(
    configuration: HPKEConfig,
    pkR: &HpkePublicKey,
    info: &Info,
    randomness: Randomness,
) -> SenderContextResult {
    let (shared_secret, enc) = Encap(kem(configuration), pkR, randomness)?;
    let key_schedule = KeySchedule(
        config,
        &shared_secret,
        info,
        &default_psk(),
        &default_psk_id(),
    )?;
    SenderContextResult::Ok((enc, key_schedule))
}

For comparison you can find the RFC pseudocode definition of SetupBaseS below (which is not well defined as is because it is missing the algorithm identifiers). The main difference between the two functions is the explicit configuration and randomness required in hacspec.

def SetupBaseS(pkR, info):
  shared_secret, enc = Encap(pkR)
  return enc, KeyScheduleS(mode_base, shared_secret, info,
                           default_psk, default_psk_id)

The setup function calls the two functions Encap and KeySchedule.

Encap

(Reminder: For demonstration purposes we use the DHKEM defined in the RFC.)

The Encap function takes the receiver’s public key pkR and generates a shared_secret as well as an encapsulation.

It is necessary to pass in the algorithm identifier to know which KEM to use and the randomness to generate a new ephemeral key pair for the KEM. See the discussion section below on the necessity of the API changes. Because the function can fail it returns a result instead of simply the computed values as described in the RFC pseudocode.

def Encap(pkR):
  skE, pkE = GenerateKeyPair()
  dh = DH(skE, pkR)
  enc = SerializePublicKey(pkE)

  pkRm = SerializePublicKey(pkR)
  kem_context = concat(enc, pkRm)

  shared_secret = ExtractAndExpand(dh, kem_context)
  return shared_secret, enc

All these changes make it much clearer what can happen within the function and in particular which error states might occur.

The Encap function generates a fresh DH key pair and computes the DH between the receivers public key and the ephemeral private key $\text{dh}=\text{skE}*\text{pkR}$. The shared_secret is then computed as the output of a key derivation function (HKDF) on input of the dh value and the context that binds the key derivation to the parameters and public values. The encapsulation enc is the serialized public key pkE generated in the first step.

pub fn Encap(pkR: &PublicKey, alg: KEM, rand: Randomness) -> EncapResult {
    let (skE, pkE) = GenerateKeyPair(alg, rand)?;
    let dh = DH(alg, &skE, pkR)?;
    let encapsulation = SerializePublicKey(alg, &pkE)?;

    let pkRm = SerializePublicKey(alg, pkR)?;
    let kem_context = enc.concat(&pkRm);

    let shared_secret = ExtractAndExpand(alg, &suite_id(alg), dh, kem_context)?;
    EncapResult::Ok((shared_secret, encapsulation))
}

KeySchedule

In order to use the shared_secret with an AEAD and allow exporting additional key material, the following KeySchedule derives the key and base_nonce for the AEAD and an exporter_secret to export other keys. The key schedule is essentially a series of HKDF calls to extract different keys from the shared secret.

The main difference to the RFC here is again that it is necessary to pass in algorithm identifiers and the suite_id to LabeledExtract and LabeledExpand. The suite_id binds the KDF extract and expand functions to the specific context and is implicit in the RFC.

pub fn KeySchedule(
    config: HPKEConfig,
    shared_secret: &SharedSecret,
    info: &Info,
    psk: &Psk,
    psk_id: &PskId,
) -> ContextResult {
    VerifyPSKInputs(config, psk, psk_id)?;
    let HPKEConfig(mode, _kem, kdf, aead) = config;

    let psk_id_hash = LabeledExtract(
        kdf,
        &suite_id(config),
        &empty_bytes(),
        &psk_id_hash_label(),
        psk_id,
    )?;
    let info_hash = LabeledExtract(
        kdf,
        &suite_id(config),
        &empty_bytes(),
        &info_hash_label(),
        info,
    )?;
    let key_schedule_context = hpke_mode_label(mode)
        .concat_owned(psk_id_hash)
        .concat_owned(info_hash);

    let secret = LabeledExtract(kdf, &suite_id(config), shared_secret, &secret_label(), psk)?;

    let key = LabeledExpand(
        kdf,
        &suite_id(config),
        &secret,
        &key_label(),
        &key_schedule_context,
        Nk(aead),
    )?;
    let base_nonce = LabeledExpand(
        kdf,
        &suite_id(config),
        &secret,
        &base_nonce_label(),
        &key_schedule_context,
        Nn(aead),
    )?;
    let exporter_secret = LabeledExpand(
        kdf,
        &suite_id(config),
        &secret,
        &exp_label(),
        &key_schedule_context,
        Nh(kdf),
    )?;
}

For comparison you can find the RFC pseudocode definition of KeySchedule below. Note that the significantly longer hacspec definition above is not in fact longer but has longer lines that are wrapped.

def KeySchedule<ROLE>(mode, shared_secret, info, psk, psk_id):
  VerifyPSKInputs(mode, psk, psk_id)

  psk_id_hash = LabeledExtract("", "psk_id_hash", psk_id)
  info_hash = LabeledExtract("", "info_hash", info)
  key_schedule_context = concat(mode, psk_id_hash, info_hash)

  secret = LabeledExtract(shared_secret, "secret", psk)

  key = LabeledExpand(secret, "key", key_schedule_context, Nk)
  base_nonce = LabeledExpand(secret, "base_nonce", key_schedule_context, Nn)
  exporter_secret = LabeledExpand(secret, "exp", key_schedule_context, Nh)

  return Context<ROLE>(key, base_nonce, 0, exporter_secret)

This is all that is needed to implement HPKE. All code examples here are taken directly from the Cryspen HPKE reference implementation. You can find the full code in the Github repository as well as the documentation.

Implementation Considerations

When defining HPKE in hacspec, or most other programming languages, there are a number of considerations that impact the way the code looks.

The hacspec code is as close to the RFC pseudocode as possible. But some changes are needed.

Randomness

hacspec does not allow to draw randomness. It is therefore necessary to pass in randomness every time it is needed.

This approach is pretty close to the way this would be implemented in native Rust where a random-number generator is passed in and used to generate randomness. For simplicity hacspec expects the randomness to be drawn on the outside instead of doing it within the specification.

Note that it is possible to pre-determine the amount of randomness needed by HPKE calls because randomness is only needed when setting up the sender. At this point the KEM mechanisms and hence the required randomness is known.

Configuration Parameters

The HPKE RFC makes most of the configuration implicit to the functions rather than passing the algorithm identifiers around. Because the hacspec implementation has to know which algorithm to pick, this is of course not possible here.

HPKE hacspec functions take either an HPKEConfig object with all algorithms in it or the specific algorithm identifier needed for the operation.

Naming

The HPKE RFC uses, in some cases, names that are impossible to use in hacspec because they are keywords or contain illegal characters. Further does hacspec not support member functions as defined for the Context.

We therefore replace . in member function calls such as Context.Export with an underscore, i.e. write Context_Export. Keywords such as open are replaced with a semantically equivalent version, i.e. HpkeOpen in this example.

Secret bytes

hacspec has the notion of secret integers that can’t be used for certain operations and should enforce secret-independent computation time.

For simplicity the hacspec HPKE implementation uses secret bytes everywhere even if not necessary, e.g. for cipher texts.

Errors

While the RFC defines a set of errors it does not always define which errors are raised. For example, it leaves open whether implementations convert errors from the Diffie-Hellman operations into KEM errors (EncapError/DecapError) or not.

With the specific implementation in hacspec here the errors are clearly defined.

About hacspec

hacspec is a specification language for cryptographic mechanisms, and more, embedded in Rust. It is a language for writing succinct, executable, formal specifications for cryptographic components. Syntactically, hacspec is a purely functional subset of Rust that aims to be readable by developers, cryptographers, and verification experts. An application developer can use hacspec to specify and prototype cryptographic components in Rust, and then either replace this specification with a verified implementation before deployment or use the hacspec code directly.

We used hacspec here to write an executable, succinct, specification of HPKE that’s embedding the full RFC into its documentation

hacspec is at the heart of a novel, modular verification framework for Rust applications developed by Cryspen in cooperation with the Prosecco team.

Summary

Even though HPKE is a relatively simple scheme it requires care when implementing. This blog post gives an overview of how hacspec can be used to achieve an executable version of the HPKE RFC that can be used as implementation on its own or as specification and reference implementation when implementing HPKE.

My company Cryspen offers support for using HPKE as well as high assurance implementations of HPKE and other protocols. Get in touch for more information.

• Github repository
• Documentation
• RFC