* Timestamps: CryptoVerif has no support for time, so instead of generating the timestamp, we input it from the adversary. In other words, we delegate the task of timestamp generation to the adversary. In order to model replay protection for the first message, the responder stores a global table (that is, a list) of triples containing the received timestamp, the partner public key for that session, as well as its own public key. (This is equivalent to having a distinct table of timestamps and partner public keys for each responder, represented by its public key.) The responder rejects the first message when the triple (received timestamp, partner public key, and responder public key) is already in the table.

* Nonces for the AEAD scheme: The nonces in WireGuard are computed by incrementing a counter. CryptoVerif has no support for that, so we receive the desired value of the counter from the adversary. We guarantee that the same counter is never used twice in the same session for sending messages by storing all counters used for sending messages in a table of pairs (session index, counter), where the session index identifies the session uniquely: it indicates whether A or B is running, as initiator or as responder, and contains a unique integer index for the execution of that entity in that role. This is equivalent to having a distinct table of counters for each session. The message is not sent when the adversary provides a counter that is already in the table. We guarantee that the same counter is never used twice for receiving messages in the same way, using a separate table.

* We omit the MACs $mac_1$ and $mac_2$ in our model. This simplifies the proof but preserves its soundness, since they can be computed and verified by the adversary: we deliver the messages without MACs to the adversary, and the adversary can add the MACs; conversely, the adversary can remove the MACs before delivering messages to the protocol model. We let the adversary choose the key $R_r$ that the responder uses for computing cookies. All other elements needed to compute the MACs are public: constants and static public keys. We reintroduce the MACs in a separate model that we use for proving resistance against DoS.

Importantly, these modelling tricks increase the power of the adversary: the implementation done in WireGuard is a particular case of what the adversary can do in our model, in which the adversary chooses the current time as timestamp, increases the counter for sending messages at each emission, accepts incoming counters in a sliding window, and computes and verifies $mac_1$ and $mac_2$ by itself. As a result, a security proof in our model remains valid in WireGuard.

## 3.6 VERIFICATION RESULTS

In order to prove authentication properties, we insert events in our model, to indicate when each message is sent or received by the protocol. Specifically, we insert events $sent1$, $sent2$, $sent\_msg\_initiator$, and $sent\_msg\_responder$ just before sending message 1, message 2, and transport messages on the
initiator and responder sides respectively, and corresponding events rcvd1, rcvd2, rcvdMsg_responder, and rcvdMsg_initiator when these messages have been received and successfully decrypted. The event rcvd2 and the events for transport messages are executed only in clean sessions.

MUTUAL KEY AND MESSAGE AUTHENTICATION, RESISTANCE AGAINST KCI, RESISTANCE AGAINST REPLAY FROM MESSAGE 2. We show authentication for all messages starting from the second protocol message, by proving the following correspondence properties between events, in the first two variants of our CryptoVerif model of Section 3.5.1:

$$
\begin{align*}
& \text{inj-event}(\text{rcvd2}(S_r^{\text{pub}}, E_i^{\text{pub}}, S_{i\text{pub}}^{\text{pub}}, S_i^{\text{pub}}, \text{ts}_{\text{pub}}, \text{ts}, E_r^{\text{pub}}, \text{empty}_{\text{pub}}, T \to, T \leftarrow)) \\
& \Rightarrow \text{inj-event}(\text{sent2}(S_r^{\text{pub}}, E_i^{\text{pub}}, S_{i\text{pub}}^{\text{pub}}, S_i^{\text{pub}}, \text{ts}_{\text{pub}}, \text{ts}, E_r^{\text{pub}}, \text{empty}_{\text{pub}}, T \to, T \leftarrow)), \\
& \text{inj-event}(\text{rcvd\_msg\_responder}(S_r^{\text{pub}}, E_i^{\text{pub}}, S_{i\text{pub}}^{\text{pub}}, S_i^{\text{pub}}, \text{ts}_{\text{pub}}, \text{ts}, \\
& \qquad E_r^{\text{pub}}, \text{empty}_{\text{pub}}, T \to, T \leftarrow, N \to, P_{\text{pub}}, P)) \\
& \Rightarrow \text{inj-event}(\text{sent\_msg\_initiator}(S_r^{\text{pub}}, E_i^{\text{pub}}, S_{i\text{pub}}^{\text{pub}}, S_i^{\text{pub}}, \text{ts}_{\text{pub}}, \text{ts}, \\
& \qquad E_r^{\text{pub}}, \text{empty}_{\text{pub}}, T \to, T \leftarrow, N \to, P_{\text{pub}}, P)),
\end{align*}
$$

We also prove a third query (similar to the second one above) for transport data messages in the other direction, with events rcvdMsg_initiator and sentMsg_responder. A proven correspondence between two injective events (inj-event) means that each execution of the left-hand event corresponds to a distinct execution of the right-hand event.

The first query means that, if the initiator session is clean and the initiator has received the second message, then the responder sent it, and initiator and responder agree on their static and ephemeral public keys, session keys, timestamp, and communicated ciphertexts. This authenticates the responder to the initiator.

The second and third queries mean that, if the receiver session is clean and the receiver received a transport packet, then a sender sent that transport packet, and the receiver and the sender agree on their static and ephemeral public keys, session keys, timestamp, sent plaintext, message counter, and communicated ciphertexts. In particular, for the key confirmation message, this authenticates the initiator to the responder. These queries also provide message authentication for the transport data messages.

All these properties hold when the pre-shared key is not compromised (variant 2 of Section 3.5.1). They also hold when neither both $S_i^{\text{priv}}$ and $E_i^{\text{priv}}$ nor both $S_r^{\text{priv}}$ and $E_r^{\text{priv}}$ are compromised and the receiver session is clean; this is true, in particular, when the sender's static private key is not compromised yet (variant 1 of Section 3.5.1).

The above queries include resistance against replays because the correspondences are injective: each reception corresponds to a distinct emission. They also include resistance against KCI attacks because the rcvd* events are issued even if the receiver's static key has already been compromised: the receiver session is still clean in this case. Note that, for the responder, resistance against KCI attacks only starts after it receives the first data transport message. Indeed, the first protocol message is subject to a KCI attack: if the private static key of the responder ($S_r^{\text{priv}}$) is compromised, then the
adversary can forge the first message and impersonate the initiator to the responder.

### SECRECY AND FORWARD SECRECY.
We show secrecy of transport data messages in clean sessions by a left-or-right message indistinguishability game. In the initial setup, we randomly choose a secret bit. For each transport data message in a clean session, the adversary provides two padded plaintexts of the same length, and we encrypt one of them depending on the value of that bit. CryptoVerif proves the secrecy of that bit, in variants 1 and 2 of Section 3.5.1, showing that the adversary cannot determine which of the two plaintexts was encrypted.

The secrecy query includes forward secrecy, because we allow dynamic compromise of static keys after the session keys have been established, if the ephemeral key of the same party is not compromised. This assumes that the parties delete the sessions' ephemeral and chaining keys after key derivation.

In variant 2 of our model, the query also shows secrecy provided the pre-shared key is not compromised, even if all other keys (static and ephemeral) are compromised. Our models do not consider the dynamic compromise of the pre-shared key, due to a limitation of CryptoVerif. We can still obtain forward secrecy with respect to the compromise of the pre-shared key using the following manual argument. As mentioned above, variant 2 of our model shows authentication when the pre-shared key is not compromised (all other keys are compromised in this model). This authentication property is preserved when the pre-shared key is compromised after the rcvd* event, because the later compromise cannot alter the fact that the sent* event has been executed. Furthermore, authentication guarantees that the ephemeral public key received by the initiator was generated by the responder and conversely. Variant 1 of our model then guarantees secrecy in this case, because the session is clean when the ephemeral received by the initiator was generated by the responder and conversely. Hence, we get the desired forward secrecy property: we have message secrecy when the pre-shared key is compromised after the session, and neither both $S_i^{\text{priv}}$ and $E_i^{\text{priv}}$ nor both $S_r^{\text{priv}}$ and $E_r^{\text{priv}}$ are compromised.

We cannot prove key secrecy for the session keys in the full protocol, because the session keys are used for encrypting transport data messages, and this allows an adversary to distinguish them from fresh random keys. Instead, we prove key secrecy for a model in which all transport data messages, including key confirmation, are removed. To prove this result, we need to strengthen the session cleanliness condition. Indeed, the first message is subject to a KCI attack, as mentioned above. Therefore, when the private static key of the responder is compromised, we additionally require that the ephemeral received by the responder is equivalent to one generated by the initiator. With this stronger cleanliness condition, we show that the session keys are secret, that is, the keys for various clean sessions are indistinguishable from independent random keys. We do not need this stronger cleanliness condition when we study the full protocol, since the key confirmation message protects the responder against KCI attacks.
## RESISTANCE AGAINST REPLAY FOR THE FIRST MESSAGE.
We prove that the first message cannot be replayed but only if no static key is compromised when it is received. If $S_i^{\text{priv}}$ were compromised, the adversary can impersonate the initiator as the sender of this message. If $S_r^{\text{priv}}$ is compromised, we have a KCI attack, as described above. So we prove the following injective correspondence in a model where the static keys cannot be compromised but the ephemeral keys may be compromised, so we rely on the static-static Diffie-Hellman shared secret:

$$ \begin{aligned} & \text{inj-event}(\text{rcvd1}(\text{true}, S_r^{\text{pub}}, E_i^{\text{pub}}, S_{i\hat{\cap}}^{\text{pub}}, S_i^{\text{pub}}, ts_{\hat{\cap}}, \text{ts})) \\ & \Rightarrow \text{inj-event}(\text{sent1}(S_r^{\text{pub}}, E_i^{\text{pub}}, S_{i\hat{\cap}}^{\text{pub}}, S_i^{\text{pub}}, ts_{\hat{\cap}}, \text{ts})). \end{aligned} $$

The first parameter of rcvd1 is true if the public static key received by the responder with the first message is the public static key of the honest initiator: we prove this property only for sessions between honest peers. Replay protection is guaranteed by each timestamp being accepted only once. With this check removed, the first message can be replayed, but we still prove a non-injective correspondence between the two events, replacing inj-event by event in the query. This is a weaker property, meaning that, if an event rcvd1 has been executed, then at least one event sent1 with matching parameters has been executed before. Thus, even with the replay protection removed, we can prove that the origin of the first message cannot be forged in a model without static key compromise.

## CORRECTNESS.
Correctness means that, if the adversary does not modify the first two messages, then the initiator and responder share the same session keys and transcript hash $H_7$. Actually, it suffices that the adversary does not modify the ephemerals and ciphertexts of the first two messages. We prove it with the following query:

$$ \begin{aligned} & \text{event}(\text{responder\_corr}(E_i^{\text{pub}}, S_{i\hat{\cap}}^{\text{pub}}, ts_{\hat{\cap}}, E_r^{\text{pub}}, \text{empty}_{\hat{\cap}}, T_r^{\leftarrow}, T_r^{\rightarrow}, H_{r7})) \\ & \wedge \text{event}(\text{initiator\_corr}(E_i^{\text{pub}}, S_{i\hat{\cap}}^{\text{pub}}, ts_{\hat{\cap}}, E_r^{\text{pub}}, \text{empty}_{\hat{\cap}}, T_i^{\leftarrow}, T_i^{\rightarrow}, H_{i7})) \\ & \Rightarrow T_i^{\rightarrow} = T_r^{\rightarrow} \wedge T_i^{\leftarrow} = T_r^{\leftarrow} \wedge H_{i7} = H_{r7}. \end{aligned} $$

The events `initiator_*` and `responder_*` used in this query and in the following ones are issued after key derivation, in the initiator and responder respectively. Here, the two events given as assumptions guarantee that the adversary did not modify the ephemerals and ciphertexts of the first two messages, and the query concludes that the session keys and transcript hash must be equal. However, in our main models, CryptoVerif is currently unable to prove that the ciphertexts have not been created by the adversary, although this is true in the sessions considered by the correctness query. Thus, we created a separate model to prove correctness, in which the assumption is hard-coded by interleaving the initiator and responder in a single sequential process. In this model, we prove correctness even if all keys are compromised.

## SESSION UNIQUENESS.
First, we prove that there is a single initiator and a single responder session with a given $T^{\rightarrow}$ or $T^{\leftarrow}$. The query below shows
that there cannot be two distinct initiator sessions with the same $T^→$:

$$ \begin{gathered} \text{event(initiator\_uniq\_T^→}(i_i, T^→)) \\ \wedge \text{event(initiator\_uniq\_T^→}(i'_i, T^→)) \Rightarrow i_i = i'_i, \end{gathered} $$

where $i_i, i'_i$ are replication indices: CryptoVerif assigns each execution of the initiator (or responder) process a unique replication index, so the query means that if we execute two events initiator_uniq_T^→ with the same $T^→$, then they have the same replication index $i_i = i'_i$, hence they belong to the same session. This query is proved in variant 3 of Section 3.5.1, so the property holds even if all keys are compromised. (It relies on the choice of a fresh ephemeral at each session.) The queries for the other cases are similar.

Second, we show similarly that there is a single initiator and a single responder session for a given set of publicly transmitted protocol values.

**CHANNEL BINDING.** We prove channel binding with the query:

$$ \begin{gathered} \text{event(initiator\_H7}(\text{params}, H_7)) \\ \wedge \text{event(responder\_H7}(\text{params}', H_7)) \Rightarrow \text{params} = \text{params}' \end{gathered} $$

This query shows that if the initiator and responder have the same value of the session transcript $H_7$, then they share the same value of all session parameters `params` (static and ephemeral public keys, timestamp, pre-shared key, session keys). This query is also proved in variant 3 of Section 3.5.1, so the property holds even if all keys are compromised. (It relies on the collision resistance of hash.)

**IDENTITY MIS-BINDING.** For this property, we need to show that if an initiator and a responder session share the same session keys $T^→$ and $T^←$, then they share the same view on the ephemeral and static keys used in that session. This is formalised by the following query:

$$ \begin{gathered} \text{event(responder\_imb}(T^→, T^←, E_{i,rcvd}^{\text{pub}}, E_r^{\text{pub}}, S_{i,rcvd}^{\text{pub}}, S_r^{\text{pub}})) \\ \wedge \text{event(initiator\_imb}(T^→, T^←, E_{i}^{\text{pub}}, E_{r,rcvd}^{\text{pub}}, S_{i}^{\text{pub}}, S_{r,rcvd}^{\text{pub}})) \\ \Rightarrow E_{i}^{\text{pub}} = E_{i,rcvd}^{\text{pub}} \wedge E_{r}^{\text{pub}} = E_{r,rcvd}^{\text{pub}} \wedge S_{i}^{\text{pub}} = S_{i,rcvd}^{\text{pub}} \wedge S_{r}^{\text{pub}} = S_{r,rcvd}^{\text{pub}}. \end{gathered} $$

CryptoVerif proves it in variant 1 of our model, so it holds when neither both $S_i^{\text{priv}}$ and $E_i^{\text{priv}}$ nor both $S_r^{\text{priv}}$ and $E_r^{\text{priv}}$ are compromised. However, the proof fails when all static and ephemeral keys are compromised (variant 3 of our model): CryptoVerif can prove only the weaker property that $\text{pow}_k(S_i^{\text{pub}}) = \text{pow}_k(S_i^{\text{pub}})$ and $\text{pow}_k(S_r^{\text{pub}}) = \text{pow}_k(S_r^{\text{pub}})$. An adversary can indeed break the equality of public static keys in this case:

* The adversary instructs A to initiate a session to a public static key $S_r^{\text{pub}/'}$ equivalent to our model's honest responder public static key: $\text{pow}_k(S_r^{\text{pub}}) = \text{pow}_k(S_r^{\text{pub}/'})$ but $S_r^{\text{pub}} \neq S_r^{\text{pub}/'}$. This is possible because $S_r^{\text{priv}}$ is compromised. In this session, the adversary acts as responder, and because the ephemeral is also compromised, gets A's $E_i^{\text{priv}}$.

* The adversary now acts as initiator to start a session with B using a public static key $S_i^{\text{pub}/'}$ equivalent to the honest initiator public static key $S_i^{\text{pub}}$.
key: pow_k(S<sub>i</sub><sup>pub</sup>) = pow_k(S<sub>i</sub><sup>pub</sup>) but S<sub>i</sub><sup>pub</sup> ≠ S<sub>i</sub><sup>pub'</sup>. This is possible because S<sub>i</sub><sup>priv</sup> is compromised. The adversary uses E<sub>i</sub><sup>priv</sup> as ephemeral. The ephemeral of this session is also compromised, so the adversary gets E<sub>r</sub><sup>priv</sup>.

* The adversary continues the session with A using the ephemeral E<sub>r</sub><sup>priv</sup>.

If a pre-shared key is used, we assume that the adversary has the same pre-shared key with A (presenting itself with key S<sub>i</sub><sup>pub'</sup>) and with B (presenting itself with S<sub>i</sub><sup>pub'</sup>). The session keys T<sub>←</sub> and T<sub>→</sub> for these two sessions are computed as hashes of E<sub>i</sub><sup>pub</sup>, dh(E<sub>i</sub><sup>priv</sup>, S<sub>r</sub><sup>pub</sup>), dh(S<sub>i</sub><sup>priv</sup>, S<sub>r</sub><sup>pub</sup>), E<sub>r</sub><sup>pub</sup>, dh(E<sub>i</sub><sup>priv</sup>, E<sub>r</sub><sup>pub</sup>), dh(S<sub>i</sub><sup>priv</sup>, E<sub>r</sub><sup>pub</sup>), and psk. They are the same in both sessions, so the session keys are also the same.

This scenario, with a session between A and B' and one between B and A' that share the same session keys, is an instance of a bilateral unknown key-share attack [CT08] and of a key synchronisation attack [Bha+14a]. It appears only when all static and ephemeral Diffie-Hellman keys are compromised, and hence should be considered a corner-case. However, we note that this scenario does not require the psk shared by A and B to be compromised, since this psk does not get used in the execution above. We suggest a possible fix of this identity mis-binding issue in Section 3.7.

### RESISTANCE AGAINST DOS.
As described in Section 3.2, WireGuard provides a cookie mechanism that a peer under load can use to enforce a round trip per sender address, and thus to bind a handshake message to a sender address; this permits per-address rate limiting. We model this mechanism in a separate model in which a responder generates $R_r$, replies with a cookie $\tau = \text{mac}(R_r, A_i)$ upon receipt of messages 1 from $A_i$ with zero mac<sub>2</sub>, and verifies mac<sub>2</sub> upon receipt of messages 1 with non-zero mac<sub>2</sub>. The rest of the protocol is run by the adversary, which has the long-term static keys. In particular, we do not model the encryption of the cookie $\tau$, but send it in the clear, assuming that the adversary carries out the encryption and decryption, which depend only on values it knows.

In this model, we prove that, if a responder under load accepts a handshake message from a sender with address $A_i$, then this sender passed through a round trip, that is, the responder did indeed previously generate a cookie for the address $A_i$. This formalised by the following query:

$$ \begin{gathered} \text{event}(\text{accepted\_cookie}(A_i, i_r, \tau, \text{msg}_\beta, \text{mac}_2)) \\ \Rightarrow \text{event}(\text{generated\_cookie}(A_i, i_r, \tau)), \end{gathered} $$

where $i_r$ is an index that uniquely identifies the key $R_r$ used for generating the cookie. This query is proved under the assumption that mac is a pseudorandom function (PRF).

### IDENTITY HIDING.
When the adversary has a candidate public key $S_Y^{pub}$, it can determine whether this public key is involved in WireGuard sessions, as already mentioned in the WireGuard specification [Don17]. In the first message, it can test whether $\text{mac}_1 = \text{mac}(\text{hash}(\text{label}_{\text{mac}_1} \| S_Y^{pub})$, $\text{msg}_\alpha$) and that reveals whether $S_Y^{pub} = S_r^{pub}$. A similar test on message 2 reveals whether $S_Y^{pub} = S_i^{pub}$. When an entity with public key $S_m^{pub}$ sends a cookie reply, the adversary can try to decrypt the encrypted cookie $\tau \triangleq$ with the key

<footnote>[CT08] Chen and Tang, “Bilateral Unknown Key-Share Attacks in Key Agreement Protocols”</footnote>

<footnote>[Bha+14a] Bhargavan et al., “Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS”</footnote>

<footnote>[Don17] Donenfeld, “WireGuard: Next Generation Kernel Network Tunnel”</footnote>
hash label$_{cookie}$ ||$S_Y^{pub}$), the nonce nonce (obtained from the cookie reply), and the associated data mac$_1$ (obtained from a previous message). If decryption succeeds, then the adversary knows that $S_Y^{pub} = S_m^{pub}$. In practice, the public keys of VPN endpoints may be easy to obtain: they are often published to subscribers on a web page. In such scenarios, WireGuard does not provide identity hiding.

If we consider the protocol without MACs and cookie reply, that is, basically the Noise protocol IKpsk2, we can obtain stronger identity protection guarantees, however with the additional assumption that the AEAD scheme also preserves the secrecy of the associated data. Indeed, if the AEAD scheme is only IND-CPA and INT-CTXT, then the adversary may obtain the associated data of the first ciphertext $S_i^{pub}$, that is, $hash(hash(H_0||S_r^{pub})||E_i^{pub})$. It can compare this value with $hash(hash(H_0||S_Y^{pub})||E_i^{pub})$ since $E_i^{pub}$ is sent in the first message and $H_0$ is a constant. Thus, it can determine whether $S_r^{pub} = S_Y^{pub}$.

However, assuming that the AEAD scheme also preserves the secrecy of the associated data, we prove using CryptoVerif that the protocol without MACs and cookie reply satisfies the following identity hiding property: an adversary that has $S_{A1}^{pub}, S_{A2}^{pub}, S_{B1}^{pub}, S_{B2}^{pub}$ cannot distinguish a configuration in which the entity with public key $S_{A1}^{pub}$ initiates sessions with $S_{B1}^{pub}$ from one in which the entity with public key $S_{A2}^{pub}$ initiates sessions with $S_{B2}^{pub}$. ChaCha20Poly1305 indeed preserves the secrecy of the associated data, because it satisfies the stronger IND-CPA property, which requires the ciphertext to be indistinguishable from random bits, as shown in [Pro14].

We discuss possible solutions to strengthen the identity hiding for the protocol with MACs in Section 3.7.

PROOF GUIDANCE AND METRICS. CryptoVerif needs to be manually guided to perform these proofs. We detail the instructions given to CryptoVerif for proving authentication and message secrecy in variant 1 of our model, with dynamic compromise of the private static keys. The guidance we give for other proofs follows similar ideas.

First, we set some options, in particular to speed up the proof and save memory.

set casesInCorresp = false;

reduces the number of cases that CryptoVerif considers in proofs of correspondences. This option does not affect the soundness; in complex cases, CryptoVerif might just not be able to prove a correspondence with this option set to false.

set mergeBranches = false;

prevents CryptoVerif from trying to automatically merge branches of tests when they execute the same code.

set forgetOldGames = true;

tells CryptoVerif to remove games generated by previous instructions from memory, in order to save memory. (However, that prevents undoing previous proof steps.)

[Pro14] Procter, *A Security Analysis of the Composition of ChaCha20 and Poly1305*
set useKnownEqualitiesWithFunctionsInMatching = true;

tells CryptoVerif to apply known equalities that start with a function symbol when it tests whether a term matches another term. CryptoVerif would not do that by default because it is costly. However, when using Curve25519, we need to apply equalities of the form `pow_k(·) = pow_k(·)`, so we use this setting. We unset it later when it is no longer needed, to speed up the proof.

Next, we distinguish cases. In the initiator A, we add a test to distinguish whether the partner public key `S_X_pub` is equivalent to B's static public key `S_B_pub`. This test is added just after the input that receives `S_X_pub` from the adversary on channel `c_config_initiator`, by the instruction:

```
insert after "in(c_config_initiator\\["
    "if pow_k(S_X_pub) = pow_k(S_B_pub) then";
```

Here, the test `if pow_k(S_X_pub) = pow_k(S_B_pub) then` is inserted after the line that contains the regular expression `in(c_config_initiator\\[`. (the character sequence `\\[` denotes the character `[` in regular expressions.) This is an improvement that we implemented in CryptoVerif. Before, CryptoVerif required indicating the program point at which a case distinction should be inserted by an integer number, and this number often varied with very minor changes in the protocol specification. We modified CryptoVerif to allow specifying program points as the beginning of a line that matches a certain regular expression, or as the line that follows a matching line. This is much more stable to small changes in the protocol model.

As a result, the initiator ephemeral is then chosen at two different places, in the then branch and in the else branch of the test that was just introduced. We rename the variable `E_i_pub_4` containing the initiator public ephemeral to two distinct names (these names are chosen by CryptoVerif and are here `E_i_pub_6` and `E_i_pub_7`) by the instruction:

```
SArename E_i_pub_4;
```

In the responder B, we distinguish whether the partner public key `S_i_pub_rcvd_4` is equivalent to A's static public key `S_A_pub`, by the instruction:

```
insert after
    "let injbot(G_to_bitstring(S_i_pub_rcvd_4: G_t))"
    "if pow_k(S_i_pub_rcvd_4) = pow_k(S_A_pub) then";
```

The test is inserted after the decryption of the ciphertext $S_i^{pow_k}$. In the responder B, we also distinguish whether the received ephemeral `E_i_pub_rcvd_3` is equivalent to an ephemeral generated by A, `E_i_pub_6[i]` or `E_i_pub_7[i]` for any i. (`E_i_pub_6` and `E_i_pub_7` are arrays containing one public ephemeral for each execution of the A.) This test is inserted after the reception of the ephemeral by the responder B, by the following instruction:

```
insert after "in(c_init2resp_recv\\["
    "find i <= N_init_parties suchthat defined(E_i_pub_7[i])
        && pow_k(E_i_pub_rcvd_3) = pow_k(E_i_pub_7[i]) then
orfind i <= N_init_parties suchthat defined(E_i_pub_6[i])
        && pow_k(E_i_pub_rcvd_3) = pow_k(E_i_pub_6[i]) then";
```
The construct find $i \le N$ such that $\text{defined}(x[i])$ && $M$ then $P$ else $P'$ looks for an index $i$ such that $x[i]$ is defined and the condition $M$ holds. If it finds one, it runs $P$ with that index; otherwise, it runs $P'$. It is extended to several branches by using orfind. Finally, in the initiator $A$, we distinguish whether the responder's ephemeral $E_r\_pub\_rcvd_2$ received with the second protocol message is equivalent to an ephemeral generated by $B$, $E_r\_pub[j]$, by the instructions:

```sql
insert after nth 2 "in(cresp2init_recv\["
    "find j <= Nresp_parties such that defined(E_r_pub[j]) &&
    pow_k(E_r_pub_rcvd_2) = pow_k(E_r_pub[j]) then";
insert after nth 1 "in(cresp2init_recv\["
    "find j <= Nresp_parties such that defined(E_r_pub[j]) &&
    pow_k(E_r_pub_rcvd_2) = pow_k(E_r_pub[j]) then";
```

We insert two tests because we need to insert one test in each branch of the initial case distinction made in the initiator. These case distinctions allow us to isolate Diffie-Hellman shared secrets that the adversary will be unable to compute because both shares come from honest participants. We simplify the obtained game by

```sql
simplify;
```

Then, we apply the random oracle assumption for the 3 random oracles $\text{chain}'_6$, $\text{chain}'_2$, $\text{chain}'_1$ (named $\text{rom3_intermediate}$, $\text{rom2_intermediate}$, and $\text{rom1_intermediate}$ in the CryptoVerif file). For the arguments of these oracles that are Diffie-Hellman shared secrets in the protocol (and thus are in $G_{\text{sub}}$), we distinguish whether the argument received by the random oracle from the adversary is in $G_{\text{sub}}$ before applying the random oracle assumption. (When it is not in $G_{\text{sub}}$, it cannot collide with a call coming from the protocol.) This is done by the following instructions:

```sql
insert after "in(ch1Roman3"
    "let rom3_input(x1Roman3, Gsub_to_G(x2Roman3),
    Gsub_to_G(x3Roman3), x4Roman3, Gsub_to_G(x5Roman3),
    Gsub_to_G(x6Roman3), vpsk) = xRoman3 in";
crypto rom(rom3_intermediate);
insert after "in(ch1Roman2"
    "let rom2_input(x1Roman2, Gsub_to_G(x2Roman2),
    Gsub_to_G(x3Roman2)) = xRoman2 in";
crypto rom(rom2_intermediate);
insert after "in(ch1Roman1"
    "let rom1_input(x1Roman1, Gsub_to_G(x2Roman1)) = xRoman1 in";
crypto rom(rom1_intermediate);
```

The first case distinction distinguishes whether the argument $x_{\text{rom3}}$ of $\text{rom3_intermediate}$ is of the form $\text{rom3\_input}(x_1_{\text{rom3}}, G_{\text{sub\_to\_G}}(x_2_{\text{rom3}}), G_{\text{sub\_to\_G}}(x_3_{\text{rom3}}), x_4_{\text{rom3}}, G_{\text{sub\_to\_G}}(x_5_{\text{rom3}}), G_{\text{sub\_to\_G}}(x_6_{\text{rom3}}), v_{\text{psk}})$, that is, a tuple in which the 2nd, 3rd, 5th, and 6th components are in $G_{\text{sub}}$. The next instruction applies the random oracle assumption to $\text{rom3_intermediate}$. The other two random oracles are handled similarly.
Next, we apply the gap Diffie-Hellman assumption to exp_div_k; the
associated private keys are the private static and ephemeral keys of the
initiator and the responder:

crypto gdh(exp_div_k)
    S_B_priv E_i_priv_8 S_A_priv E_r_priv_4;

We modify settings to speed up the rest of the proof by the following
instructions:

set useKnownEqualitiesWithFunctionsInMatching = false;
set elsefindFactsInSimplify = false;

The setting elsefindFactsInSimplify, when true, tells CryptoVerif to simplify games using the information obtained from being in an else branch of a find. It is the default, but it can be costly for large games.

We split the keys generated by chain'_6' into 4 keys by

crypto splitter concaten four keys //;

The indication ** means that we apply splitterconcat four keys) as
many times as we can, without performing a full simplification between
each application. Avoiding that simplification speeds up the proof a bit.
splitterconcat four keys) means that a random bitstring of length 4
times the length of a key is indistinguishable from the concatenation of 4
random keys.

By default, when a cryptographic transformation fails, CryptoVerif tries
to determine syntactic transformations that might make it succeed, applies
those transformations, and retries the cryptographic transformation. For
speed, we disable this behaviour by the following instruction:

set noAdviceCrypto = true;

We apply ciphertext integrity of the AEAD scheme:

crypto int_ctxtext(enc) *;

The indication * means that we apply int_ctxtext(enc) as many times as we
can. Then we try to prove security properties:

success;

CryptoVerif shows the impossibility of nonce reuse in the AEAD scheme and
the absence of identity mis-binding attacks. We simplify the game

simplify;

For keys that the adversary may have after compromising the static keys,
we apply a variant of the ciphertext integrity transformation that allows
corruption, as follows:

crypto int_ctxtext_corruptenc k_51;
The key k_51 is generated by the initiator when the partner static key is equivalent to B's static public key but the received ephemeral is not equivalent to an ephemeral generated by B, and B's static key is not compromised. In this case, the adversary cannot produce a valid ciphertext in protocol message 2 (empty plaintext), thus the decryption will fail on the initiator's side and the protocol will not continue.

Then we try to prove security properties:

success;

CryptoVerif proves that the initiator can authenticate the second protocol message as well as transport data messages sent by the responder. We simplify the game

simplify;

and again apply the variant of the ciphertext integrity transformation that allows corruption:

crypto int_ctx corrupt(enc) "T_i_send_[0-9]*";

We apply this transformation to all keys of the form T_i_send_n for integers n. We want to apply this transformation to keys generated by the responder, in case the partner public key is equivalent to A's static public key, but the received ephemeral is not equivalent to an ephemeral generated by A, and A's static key is not compromised. In this case, the adversary cannot produce a valid ciphertext for a transport data message, thus the decryption will fail on the responder's side and the protocol will not continue. The keys in question are many variables of the form T_i_send_n; we apply the transformation to all variables of this form as it is easier and the proof still works. Then we try to prove security properties:

success;

CryptoVerif shows that the responder can authenticate transport data messages sent by the initiator. We again simplify the game

simplify;

That removes all events, which are no longer useful since all correspondence properties are proved. Then we apply the IND-CPA property of the AEAD scheme as many times as we can:

crypto ind_cpa(enc) **;

and finally prove message secrecy:

success

In total, we give 36 instructions to CryptoVerif to perform this proof (not counting the instruction to display the current game), and CryptoVerif generates a sequence of 168 games. This proof takes 17 min, the proof of key secrecy with dynamic compromise of private static keys takes 19 min, and the one for identity hiding 26 min on one core of an Intel Xeon 3.6 GHz; these are our longest proofs.
3.7 DISCUSSION

WireGuard is a promising new VPN protocol that aims to replace IPsec and OpenVPN, and is being considered for adoption within the Linux kernel. We presented a mechanised cryptographic proof for a detailed model of WireGuard using the CryptoVerif prover. Our model accounts for the full Noise IKpsk2 secure channel protocol as well as WireGuard's extensions for stealthy operation and DoS resistance. We consider an arbitrary number of parallel sessions, with an arbitrary number of transport data messages. Furthermore, we base our proof on a precise model of the Curve25519 group.

We proved correctness, message and key secrecy, forward secrecy, mutual authentication, session uniqueness, channel binding, and resistance against replay, key compromise impersonation, and denial of service attacks. In some cases, our analysis pointed out potential improvements in the protocol (which we did not prove secure using CryptoVerif):

### ADDING PUBLIC KEYS TO THE CHAINING KEY DERIVATION.
When analysing WireGuard for Identity Mis-Binding attacks, our analysis uncovered a corner case. Suppose all the Diffie-Hellman keys in a session between two hosts A and B were compromised, but the pre-shared key between them is still secret. Then the adversary can set up a man-in-the-middle attack where A thinks it is connected to $B'$, B thinks it is connected to $A'$, but in fact they are both connected to each other, in the sense that the two connections have the same traffic keys, even though they have different static keys.

In particular, once it has set up the session, the adversary can step away and let A and B directly communicate with each other, while retaining the ability to read and modify messages at will. Interestingly, this vulnerability only appears in our precise model of Curve25519; it cannot be detected under a classic Diffie-Hellman assumption.

Although this attack scenario may be quite unrealistic, it points to a theoretical weakness in the protocol that is easy to prevent with a simple modification. Noise IKpsk2 already adds ephemeral public keys to the chaining key derivation; we recommend that the static public keys be added as well. Alternatively, adding the full transcript hash to the traffic key derivation would also prevent this corner case.

Separately, it is also worth noting that adding public keys to the key derivation significantly helps with the cryptographic proof. For example, consider the Noise IK protocol, which is similar to IKpsk2 except that it does not use PSKs. IK does not mix the ephemeral keys into the chaining key, and it turns out that it is much harder for CryptoVerif to verify than IKpsk2, since we now have to reason about mis-matched ephemeral keys. In particular, even if we use a public PSK of all-zeroes, the IKpsk2 protocol is easier to prove secure than IK. In fact, our recommendation is to add further contextual information to the key derivation. It would not only prevent theoretical attacks, but also make proofs easier.

### BALANCING STEALTH AND IDENTITY HIDING.
Our analysis also points out that the use of static public keys in $mac_1$ and $mac_2$ in WireGuard negatively
affects the identity hiding guarantees provided by IKpsk2. This is a conscious trade-off that WireGuard makes to achieve stealthy operation [Don17]. However, in deployment scenarios where identity hiding is more important than stealth, we recommend that the protocol use a constant (say all-zeroes) instead of the static public keys to compute the MACs and cookies.

While it is difficult to preserve stealth while hiding the responder's identity, a modification to the protocol can still hide the initiator's identity. We recommend that the initiator should send a MAC key (along with the timestamp) in the first handshake message, and the responder should use this MAC key to compute $mac_1$ in the second handshake message. The initiator can verify this MAC to get DoS protection, but its static public key is kept hidden from a network adversary. Essentially, the MAC key acts as an in-session cookie.

**RELATED WORK.** The use of formal verification tools to analyse real-world cryptographic protocols is now a well-established research area with hundreds of case studies (see e.g. [Bla12]). CryptoVerif itself has been used to analyse modern protocols like Signal [KBB17] and TLS 1.3 [BBK17]. We conclude this chapter by comparing our results with closely related work; Table 3.1 provides a condensed, high-level overview.

WireGuard itself has been formally analysed before. Donenfeld et al. symbolically analyse the IKpsk2 key exchange protocol used by WireGuard for a number of security goals, including identity mis-binding and identity hiding [DM18]. However, they do not model the MACs or the cookie mechanism, and hence they do not prove DoS resistance. Interestingly, their analysis concludes the absence of identity mis-binding attacks even if all keys are compromised, because their model does not include equivalent public keys. We disprove this property by considering a precise model of Curve25519. An improved modelling of Diffie-Hellman groups in the symbolic model has independently been proposed, using Tamarin [CJ19]. It could probably be used to improve the symbolic analysis of WireGuard.

Dowling and Paterson [DP18] present a manual cryptographic analysis of WireGuard. In particular, they prove key indistinguishability for the WireGuard handshake based on the PRF-ODH assumption in an extension of the eCK-PFS key exchange model. (Because of this difference in the used assumption, our mechanisation cannot be used directly to find issues in proof steps; it is a different proof.) Key indistinguishability no longer holds once the key is used, so they prove security for a slightly modified variant of the IKpsk2 protocol that includes a key confirmation message independent of the session keys. In contrast, our proof requires no changes to the protocol, since we use an ACCE-style model. Furthermore, [DP18] focuses only on the key exchange, and does not consider other properties like identity hiding or DoS resistance. Their analysis also does not find the identity mis-binding issue since they do not consider a scenario where all Diffie-Hellman keys are compromised.

Finally, the Noise Explorer tool [KNB19] has been used to perform a comprehensive symbolic analysis of numerous Noise protocols using the ProVerif analyser. Noise Explorer can be used to find violations of secrecy and authentication properties for any protocol expressed in the language defined

<footnote>[Don17] Donenfeld, "WireGuard: Next Generation Kernel Network Tunnel"</footnote>

<footnote>[Bla12] Blanchet, "Security Protocol Verification: Symbolic and Computational Models"</footnote>

<footnote>[KBB17] Kobeissi et al., "Automated Verification for Secure Messaging Protocols and their Implementations: A Symbolic and Computational Approach"</footnote>

<footnote>[BBK17] Bhargavan et al., "Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate"</footnote>

<footnote>[DM18] Donenfeld and Milner, *Formal Verification of the WireGuard Protocol*</footnote>

<footnote>[CJ19] Cremers and Jackson, "Prime, Order Please! Revisiting Small Subgroup and Invalid Curve Attacks on Protocols using Diffie-Hellman"</footnote>

<footnote>[DP18] Dowling and Paterson, "A Cryptographic Analysis of the WireGuard Protocol"</footnote>

<footnote>[KNB19] Kobeissi et al., "Noise Explorer: Fully Automated Modeling and Verification for Arbitrary Noise Protocols"</footnote>
<table><caption>TABLE 3.1: Security models (upper part) and properties analysed (lower part) in different works on WireGuard or Noise IKpsk2.</caption><thead><tr><th></th><th colspan="3">Noise Explorer [KNB19]</th><th colspan="3">WireGuard</th></tr><tr><th></th><th colspan="3">Noise IKpsk2</th><th colspan="3">WireGuard</th></tr><tr><th>verified protocol</th><th colspan="3"></th><th colspan="3"></th></tr><tr><th>tool set</th><th>PV</th><th>T</th><th>T</th><th>T</th><th>m</th><th>CV</th></tr></thead><tbody><tr><td>computational model</td><td>x</td><td>x</td><td>x</td><td>x</td><td>✓</td><td>✓</td></tr><tr><td>Curve25519 with equivalent keys</td><td>x</td><td>x</td><td>x</td><td>x</td><td>x</td><td>✓</td></tr><tr><td>compromise static keys</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>compromise ephemeral keys</td><td>x</td><td>x</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>dishonest ephemeral keys</td><td>x</td><td>x</td><td>✓</td><td>x</td><td>x</td><td>x</td></tr><tr><td>compromise pre-shared key</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>compromise all keys</td><td>x</td><td>x</td><td>✓</td><td>✓</td><td>x</td><td>✓</td></tr><tr><td>both roles per static key</td><td>x</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>mutual authentication</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>key compromise impersonation</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>1st message replay</td><td>—</td><td>—</td><td>—</td><td>x</td><td>x</td><td>✓</td></tr><tr><td>transport data replay</td><td>x</td><td>✓</td><td>✓</td><td>x</td><td>x</td><td>✓</td></tr><tr><td>session uniqueness</td><td>x</td><td>✓</td><td>x</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>channel binding</td><td>x</td><td>✓</td><td>x</td><td>x</td><td>x</td><td>✓</td></tr><tr><td>DoS resistance</td><td>—</td><td>—</td><td>—</td><td>x</td><td>x</td><td>✓</td></tr><tr><td>forward key secrecy</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>forward message secrecy</td><td>✓</td><td>✓</td><td>✓</td><td>x</td><td>x</td><td>✓</td></tr><tr><td>identity hiding</td><td>x</td><td>x</td><td>✓</td><td>✓<sup>2</sup></td><td>x</td><td>✓</td></tr><tr><td>identity mis-binding</td><td>x</td><td>x</td><td>x</td><td>✓<sup>1</sup></td><td>x</td><td>✓</td></tr></tbody></table>

Definitions differ between models.

T = Tamarin, PV = ProVerif, CV = CryptoVerif, m = manual.

✓ = included, x = not included, — = not applicable.

1) The identity mis-binding issue we found was *not* found.

2) Weaker identity hiding property using a surrogate term.
by Noise, using per-message authentication and confidentiality grades. It
includes a symbolic analysis of Noise IKpsk2. A similar work has been done
in Tamarin [SD18; Gir19].

ACKNOWLEDGEMENTS

We thank Jason A. Donenfeld (the author of WireGuard), Nadim Kobeissi, and the anonymous reviewers of EuroS&P'19 for their helpful feedback on our work. This research was partly funded by the European Unions Horizon 2020 NEXTLEAP Project (grant agreement no. 688722), ERC CIRCUS (grant agreement no. 683032), ANR AnaStaSec (decision number ANR-14-CE28-0014-01), and ANR TECAP (decision number ANR-17-CE39-0004-03).

<footnote>[SD18] Suter-Dörig, “Formalizing and verifying the security protocols from the Noise framework”</footnote>

<footnote>[Gir19] Girol, “Formalizing and Verifying the Security Protocols from the Noise Framework”</footnote>
<figure><img src="image_23.png" /></figure>
This chapter and the appendices belonging to it are based on the long version [Alw+20] of the paper "Analysing the HPKE Standard", published at IACR's Eurocrypt 2021 with co-authors Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, and Doreen Riepel [Alw+21].

ABSTRACT. The *Hybrid Public Key Encryption* (HPKE) scheme is a standard developed by the Crypto Forum Research Group (CFRG) of the Internet Research Task Force (IRTF), and has been published as RFC 9180 in February 2022 [Bar+22].

In this chapter, of the four modes of HPKE, we analyse the authenticated mode $HPKE_{Auth}$ in its single-shot encryption form as it contains what is, arguably, the most novel part of HPKE. An analysis of all modes including $HPKE_{Auth}$ is described in Section 5.1.

$HPKE_{Auth}$'s intended application domain is captured by a new primitive which we call Authenticated Public Key Encryption (APKE). We provide syntax and security definitions for APKE schemes, as well as for the related Authenticated Key Encapsulation Mechanisms (AKEMs). We prove security of the AKEM scheme DH-AKEM underlying $HPKE_{Auth}$ based on the Gap Diffie-Hellman assumption and provide general AKEM/DEM composition theorems with which to argue about $HPKE_{Auth}$'s security. To this end, we also formally analyse $HPKE_{Auth}$'s key schedule and key derivation functions. To increase confidence in our results we use the automatic theorem proving tool CryptoVerif. All our bounds are quantitative and we discuss their practical implications for $HPKE_{Auth}$.

As an independent contribution we propose the new framework of *nomi-nal groups* that allows us to capture abstract syntactical and security prop-erties of practical elliptic curves, including the Curve25519 and Curve448 based groups (which do not constitute cyclic groups).

At the time of writing of the paper, an effort was underway by the Crypto Forum Research Group (CFRG) to agree upon a new open standard for public key encryption [Bar+22]. The standard is called *Hybrid Public Key Encryption* (HPKE) and it is, in particular, expected to be used as a building block by the Internet Engineering Task Force (IETF) in at least two further

<footnote>[Alw+21] Alwen et al., "Analysing the HPKE Standard"</footnote>

<footnote>[Bar+22] Barnes et al., *Hybrid Public Key Encryption*</footnote>
upcoming standardized security protocols [Bar+20a; Res+20]. The primary
source for HPKE is an RFC [Bar+22] (on draft 8 [Bar+20b] at the time
this analysis was done) which lays out the details of the construction and
provides some rough intuition for its security properties.

At first glance the HPKE standard might be thought of as a “public key encryption” scheme in the spirit of the KEM/DEM paradigm [CS03]. That is, it combines a Key Encapsulation Mechanism (KEM) and an Authenticated Encryption with Associated Data (AEAD) acting as a Data Encapsulation Mechanism (DEM) according to the KEM/DEM paradigm. However, upon closer inspection HPKE turns out to be more complex than this perfunctory description implies.

First, HPKE actually consists of 2 different KEM/DEM constructions. Moreover, each construction can be instantiated with a pre-shared key (PSK) known to both sender and receiver, which is used in the key schedule to derive the DEM key. In total this gives rise to 4 different modes for HPKE. The basic mode $HPKE_{Base}$ makes use of a standard (say IND-CCA-secure) KEM to obtain a “message privacy and integrity” only mode. This mode can be extended to $HPKE_{PSK}$ to support authentication of the sender via a PSK.

The remaining 2 HPKE modes make use of a different KEM/DEM construction built from a rather non-standard KEM variant which we call an *Authenticated KEM* (AKEM). Roughly speaking, an AKEM can be thought of the KEM analogue of signcryption [Zhe97]. In particular, sender and receiver both have their own public/private keys. Each party requires their own private and the other party’s public key to perform en/decryption. The HPKE RFC constructs an AKEM based on a generic Diffie-Hellman group. It goes on to fix concrete instantiations of such groups using either the P-256, P-384, or P-521 NIST curves [Nat13] or the Curve25519 or Curve448 curves [LHT16]. The AKEM-based HPKE modes also intend to authenticate the sender to the receiver. Just as in the KEM-based case, the AKEM/DEM construction can be instantiated in modes either with or without a PSK. We refer to the AKEM/DEM-based mode without a PSK as the *authenticated mode* and, for reasons described below, it is the main focus of this work. The corresponding HPKE scheme is called $HPKE_{Auth}$.

Orthogonal to the choice of mode in use, HPKE also provides a so called single-shot and a multi-shot API. The single-shot API can be thought of as pairing a single instance of the DEM with a KEM ciphertext while the multi-shot API establishes a key schedule allowing a single KEM shared secret to be used to derive keys for an entire sequence of DEMs. Finally, HPKE also supports exporting keys from the key schedule for use by arbitrary higher-level applications.

**APPLICATIONS.** As an open standard of the IRTF, we believe HPKE to be an interesting topic of study in its own right. Indeed, HPKE is already slated for use in at least two upcoming protocols; the Messaging Layer Security (MLS) [Bar+20a] secure group messaging protocol and the Encrypted Server Name Indication (ESNI) extension for TLS 1.3 [Res+20]. Both look to be well-served by the single-shot API as they require a single DEM to be produced (at the same time as the KEM) and the combined KEM/DEM ciphertext to be sent as one packet.

<footnote>[Bar+20a] Barnes et al., *The Messaging Layer Security (MLS) Protocol*</footnote>

<footnote>[Res+20] Rescorla et al., *TLS Encrypted Client Hello*</footnote>

<footnote>[Bar+22] Barnes et al., *Hybrid Public Key Encryption*</footnote>

<footnote>[Bar+20b] Barnes et al., *Hybrid Public Key Encryption*</footnote>

<footnote>[CS03] Cramer and Shoup, “Design and Analysis of Practical Public-Key Encryption Schemes Secure against Adaptive Chosen Ciphertext Attack”</footnote>

<footnote>[Zhe97] Zheng, “Digital Signcryption or How to Achieve Cost(Signature & Encryption) << Cost(Signature) + Cost(Encryption)”</footnote>

<footnote>[Nat13] National Institute of Standards and Technology, *Digital Signature Standard (DSS)*</footnote>

<footnote>[LHT16] Langley et al., *Elliptic Curves for Security*</footnote>
More interestingly, at least for MLS, authenticating the sender of an
HPKE ciphertext (based on their public keys) is clearly also a useful property.
(For the ESNI application things are less clear.<fnref n="1" />)

In a bit more detail, MLS is already equipped with a notion of a PKI
involving public keys bound to long-term identities of parties (as described
in [*Oma+20*]). To invite a new member to an existing MLS protocol session
the inviter must send an HPKE ciphertext to the new member. In line with
MLS's strong authentication goals, the new member is expected to be able
to cryptographically validate the (supposed) identity of the sender of such
ciphertexts.

Currently, MLS calls for the HPKE ciphertext to be produced using HPKE's
basic mode HPKE<sub>Base</sub> and the resulting ciphertext to be signed by the inviter
using a digital signature scheme (either ECDSA or EdDSA). However, an
alternative approach to achieve the same ends could be to directly use
HPKE in its authenticated mode HPKE<sub>Auth</sub>. This would save on at least 2
modular exponentiations as well as result in packets containing 2 fewer group
elements. Reducing computational and communication complexity has been
a central focus of the MLS design process as such costs are considered the
main hurdles to achieving the MLS's stated goal of supporting extremely
large groups. Unfortunately, in our analysis, we discovered that HPKE<sub>Auth</sub>
does not authenticate the sender when the receiver's secret key leaked, a
key compromise impersonation (KCI) attack (*Section 4.5.4*). MLS aims to
provide strong security in the face of state leakage (which includes KCI
attacks), so switching from HPKE<sub>Base</sub> and signatures to HPKE<sub>Auth</sub> would
result in a significant security downgrade.

HPKE<sub>Auth</sub> could also be a replacement for the authenticated public-key encryption originally implemented by the NaCl cryptographic library. HPKE<sub>Auth</sub> is safer than the NaCl implementation because, in HPKE<sub>Auth</sub>, the shared secret is bound to the intended sender and recipient public keys.

4.1.1 *Our Contributions*

So far, there has been no formal analysis of the HPKE standard. Unfortunately,
due to its many modes, options and features a complete analysis of HPKE
from scratch seems rather too ambitious for a single work such as this one.
Thus, we are forced to choose our scope more carefully. The basic mode
HPKE<sub>Base</sub> (especially using the single-shot API) seems to be a quite standard
construction. Therefore, and in light of the above discussion around MLS, we
have opted to focus on the more novel authenticated mode in its single-shot
API form HPKE<sub>Auth</sub>. To this end we make the following contributions.

AUTHENTICATED KEM AND PKE. We begin, in Section 4.5, by introducing *Authenticated Key Encapsulation Mechanisms* (AKEM) and *Authenticated Public Key Encryption* (APKE) schemes, where the syntax of APKE matches that of the single-shot authenticated mode of HPKE<sub>Auth</sub>. In terms of security, we define (multi-user) security notions capturing both authenticity and (2 types of) privacy for an AKEM and an APKE. In a bit more detail, both for authenticity and for privacy we consider so called weaker *outsider* and stronger *insider* variants. Intuitively, outsider notions model settings where the adversary is an outside observer. Conversely, insider notions model

[Oma+20] Omara et al., *The Messaging Layer Security (MLS) Architecture*

<footnote n="1">¹The ESNI RFC calls for a client initiating a TLS connection to send an HPKE ciphertext to the server. Although not as common, TLS can also be used in settings with bi-directional authentication. In particular, clients can use certificates binding their identities to their public key to authenticate themselves to the server. Unfortunately, it is unclear how the server would know, a priori, which public key to use for the client when attempting to decrypt the HPKE ciphertext.</footnote>
<table><caption>TABLE 4.1: Security properties needed to prove Outsider-Auth, Outsider-CCA, and Insider-CCA security of APKE obtained by the AKEM/DEM construction.</caption><thead><tr><th rowspan="2"></th><th colspan="3">AKEM</th><th colspan="2">AEAD</th></tr><tr><th>Outsider-Auth</th><th>Outsider-CCA</th><th>Insider-CCA</th><th>INT-CTXT</th><th>IND-CPA</th></tr></thead><tbody><tr><th>Outsider-Auth<sub>APKE</sub></th><td>X</td><td>X</td><td></td><td>X</td><td></td></tr><tr><th>Outsider-CCA<sub>APKE</sub></th><td></td><td>X</td><td></td><td>X</td><td>X</td></tr><tr><th>Insider-CCA<sub>APKE</sub></th><td></td><td></td><td>X</td><td>X</td><td>X</td></tr></tbody></table>

settings where the adversary is somehow directly involved; in particular, even selecting some of the secrets used to produce target ciphertexts. A bit more formally, we call an honestly generated key pair *secure* if the secret key was not (explicitly) leaked to the adversary and *leaked* if it was. A key pair is called *bad* if it was sampled arbitrarily by the adversary. A scheme is *outsider-secure* if target ciphertexts are secure when produced using secure key pairs. Meanwhile, insider security holds even if one *secure* and one *bad key pair* are used. For example, insider privacy (Insider-CCA) for AKEM requires that an encapsulated key remains indistinguishable from random despite the encapsulating ciphertext being produced using bad sender keys (but secure receiver keys). Similarly, insider authenticity (Insider-Auth) requires that an adversary cannot produce a valid ciphertext for bad receiver keys as long as the sender keys are secure. In particular, insider authenticity implies (but is strictly stronger than) Key Compromise Impersonation (KCI) security as KCI security only requires authenticity for leaked (but not bad) receiver keys.

Moreover, as an independent contribution we show that for each security notion of an AKEM a (significantly simpler) single-user and single-challenge-query version already implies security for its (more complex but practically relevant) multi-user version. In particular, this provides an easier target for future work on AKEMs, e.g. when building a post-quantum variant of $HPKE_{Auth}$.

AKEM/DEM: *FROM AKEM TO APKE*. Next we turn to the AKEM/DEM construction used in the HPKE standard. We prove a set of composition results each showing a different type of security for the single-shot AKEM/DEM construction depending on which properties the underlying AKEM guarantees. Each of these results also assumes standard security properties for the AEAD (namely IND-CPA and INT-CTXT) and for the key schedule KS (namely pseudo-randomness). In particular, these results are proven in the standard model. Somewhat to our surprise, it turns out that the APKE obtained by the AKEM/DEM construction does not provide insider authenticity (and so, nor does $HPKE_{Auth}$ itself). Indeed, we give an attack in Section 4.5.4.

Table 4.1 summarises the AKEM and AEAD properties we use to prove each of the remaining 3 types of security for the AKEM/DEM APKE construction.

THE $HPKE_{Auth}$ SCHEME. In Section 4.6 we analyse the generic $HPKE_{Auth}$ scheme proposed in the RFC. $HPKE_{Auth}$ is an instantiation of the AKEM/DEM paradigm discussed above.

Thus, we first analyse DH-AKEM, the particular AKEM underlying $HPKE_{Auth}$. The RFC builds DH-AKEM from a key-derivation function KDF and an underlying generic Diffie-Hellman group. As one of our main results
we show that DH-AKEM provides authenticity and privacy based on the
Gap Diffie-Hellman assumption over the underlying group. To show this we
model KDF as a random oracle.

Next we consider HPKE<sub>Auth</sub>'s key schedule and prove it to be pseudo-random based on pseudo-randomness of its building blocks, the functions Extract and Expand. Similarly, we argue why DH-AKEM's key derivation function KDF can be modelled as a random oracle. Finally, by applying our results about the AKEM/DEM paradigm from the previous sections, we obtain security proofs capturing the privacy and authenticity of HPKE<sub>Auth</sub> as an APKE. Our presentation ends with concrete bounds of HPKE<sub>Auth</sub>'s security and their interpretation.

PRACTICE-ORIENTED CRYPTOGRAPHY. Due to the very applied nature of
HPKE we have taken care to maximise the practical relevance of our results.
All security properties we analyse for HPKE<sub>Auth</sub> are defined directly for a
multi-user setting. Further, to help practitioners set sound parameters for
their HPKE applications, our results are stated in terms of very fine-grained
exact (as opposed to asymptotic) terms. That is, the security loss for each
result is bounded as an explicit function of various parameters such as the
numbers of key pairs, queries, etc.

Finally, instead of relying on a generic prime-order group to state our un-
derlying security assumptions, we ultimately reduce security to assumptions
on each of the concrete elliptic-curve-based instantiations. For the P-256,
P-384, and P-521 curves, this is relatively straightforward. However, for
Curve25519 and Curve448, this is a less than trivial step as those groups
(and their associated Diffie-Hellman functions X25519 and X448) depart
significantly from the standard generic group abstraction. To this end we
introduce the new abstraction of *nominal groups* which allows us to argue
about correctness and security of our schemes over all above-mentioned
elliptic curve groups, including Curve25519 and Curve448. (We believe this
abstraction has applications well beyond its use in this work.) Ultimately, this
approach results in both an additional security loss and the explicit consider-
ation of (potential) new attacks not present for generic groups. In particular,
both Curve25519 and Curve448 exhibit similar (but different) idiosyncrasies
such as having non-equal but functionally equivalent curve points as well as
self-reducibility with non-zero error probability, all of which we take into
account in our reductions to the respective underlying assumption.

4.1.2 *Proof Techniques*

The results in this work have been demonstrated using a combination of
traditional “pen-and-paper” techniques and the automated theorem proving
tool CryptoVerif [Bla08], which was already used to verify important practi-
cal protocols such as TLS 1.3 [BBK17], Signal [KBB17], and WireGuard, the
latter in Chapter 3 of this thesis. CryptoVerif produces game-based proofs:
it starts from an initial game provided by the user, which represents the
protocol or scheme to prove; it transforms this game step by step using a
predefined set of game transformations, until it reaches a game on which
the desired security properties can easily be proved from the form of the
game. The game transformations are guaranteed to produce computation-

<footnote>[Bla08] Blanchet, "A Computationally Sound Mechanized Prover for Security Protocols"</footnote>

<footnote>[BBK17] Bhargavan et al., "Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate"</footnote>

<footnote>[KBB17] Kobeissi et al., "Automated Verification for Secure Messaging Protocols and their Implementations: A Symbolic and Computational Approach"</footnote>
ally indistinguishable games, and either rely on a proof by reduction to a
computational assumption or are syntactic transformations (e.g. replace a
variable with its value). Using CryptoVerif to prove statements can result in
greater confidence in their correctness, especially when the proofs require
deriving (otherwise quite tedious) exact bounds on the security loss and/or
reasoning about relatively complicated, e.g. multi-instance, security games.

However, CryptoVerif also has its limitations. Fortunately, these can be
readily overcome using traditional techniques. The language used to define
security statements in CryptoVerif is rather unconventional in the context
of cryptography, not to mention (necessarily) very formal and detailed. To-
gether this can make it quite challenging to build an intuitive understanding
for a given notion (e.g. to verify that it captures the desired setting). To
circumvent this, we present each of our security definitions using the more
well-known language of game-based security. Next we map these to corre-
sponding CryptoVerif definitions. Thus, the intuition can be built upon a
game-based notion and it remains only to verify the *functional equivalence*
of the CryptoVerif instantiation.

CryptoVerif was designed with multi-instance security in mind and so relies on more unconventional multi-instance number theoretic assumptions. However, the simpler a definition (say, for a KEM) the easier it is to demonstrate for a given construction. Similarly, in cryptography we tend to prefer simpler, static, not to mention well-known, number theoretic assumptions so as to build more confidence in them. Consequently, we have augmented the automated proofs with further pen-and-paper proofs reducing multi-instance security notions and assumptions to simpler (and more conventional) single-instance versions.

4.1.3 *Related Work*

Hybrid cryptography (of which the AKEM/DEM construction in this work is
an example) is a widely used technique for constructing practically efficient
asymmetric primitives. In particular, there exist several hybrid PKE-based
concrete standards predating HPKE, mostly based on the DHIES scheme
of [ABR01] defined over a generic (discrete log) group. When the group
is instantiated using elliptic curves the result is often referred to as ECIES
(much like the Diffie-Hellman scheme over an elliptic curve group is referred
to as ECDH). A description and comparison of the most important such
standards can be found in [GM+10]. However, per the HPKE RFC, “All
these existing schemes have problems, e.g., because they rely on outdated
primitives, lack proofs of IND-CCA2 security, or fail to provide test vectors.”
Moreover, to the best of our knowledge, none of these standards provide a
means for authenticating senders.

The APKE primitive we analyse in this chapter can be viewed as a
flavour of signcryption [Zhe97]; a family of primitives intended to efficiently
combine signatures and public key encryption. Signcryption literature is
substantial and we refer to the textbook [DZ10] for an extensive exposition
thereof. We highlight some chapters of particular relevance. Chapters 2
and 3 cover 2-party and multi-party security notions, respectively; both
for insider and outsider variants. Chapter 4 of [DZ10] contains several

<footnote>[ABR01] Abdalla et al., "The Oracle Diffie-Hellman Assumptions and an Analysis of DHIES"</footnote>

<footnote>[GM+10] Gayoso Martínez et al., "A comparison of the standardized versions of ECIES"</footnote>

<footnote>[Zhe97] Zheng, "Digital Signcryption or How to Achieve Cost(Signature & Encryption) << Cost(Signature) + Cost(Encryption))"</footnote>

<footnote>[DZ10] Dent and Zheng, *Practical Signcryption*</footnote>
(Gap)-Diffie-Hellman-based signcryption constructions. Finally, Chapter 7 covers some AKEM security notions and constructions (aka. "signcryption KEM") as well as hybrid signcryption constructions such as the outsider-secure one of [Den05b] and insider-secure one of [Den05a]. In contrast to our work, almost all security notions in [DZ10] forbid honest parties from reusing the same key pair for both sending and receiving (even if sender and receiver keys have identical distribution).² Nor is it clear that a scheme satisfying a "key-separated" security notion could be converted into an equally efficient scheme supporting key reuse. The naïve transformation (embedding a sender and receiver key pair into a single reusable key pair) would double key sizes. However, an HPKE public key consists of a single group element which can be used simultaneously as a sender and receiver public key.

Recently, Bellare and Stepanovs analysed the signcryption scheme underlying the iMessage secure messaging protocol [BS20]. Although their security notions allow for key reuse as in our work, they fall outside the outsider/insider taxonomy common in signcryption literature. Instead, they capture an intermediary variant more akin to KCI security.

A detailed model of Curve25519 [LHT16] in CryptoVerif was already presented in Chapter 3 of this thesis; such a model was needed for the proof of the WireGuard protocol. In this chapter, we present a more generic model that allows us to deal not only with Curve25519 but also with prime order groups such as NIST curves [Nat13] in a single model. Moreover, we handle rerandomisation of curve elements, which was not taken into account in Chapter 3.

A preliminary version of this work analyses HPKE as a single protocol, not in a modular KEM/DEM setting, it is presented in Section 5.1 of this thesis. The proven theorems are less strong than the ones in this work, e.g. the adversary cannot choose secret keys but only compromise them. However, the analysis covers the single-shot encryption form of all four modes including the secret export API.

[Den05b] Dent, "Hybrid Signcryption Schemes with Outsider Security"

[Den05a] Dent, "Hybrid Signcryption Schemes with Insider Security"

[DZ10] Dent and Zheng, *Practical Signcryption*

²The only exception we are aware of are the security notions used to analyse 2 bilinear-pairing-based schemes in Sections 5.5 and 5.6 of [DZ10].

[BS20] Bellare and Stepanovs, "Security Under Message-Derived Keys: Signcryption in iMessage"

[LHT16] Langley et al., *Elliptic Curves for Security*

[Nat13] National Institute of Standards and Technology, *Digital Signature Standard (DSS)*

## 4.2 PRELIMINARIES

SETS AND ALGORITHMS. We write $h \stackrel{s}{\leftarrow} S$ to denote that the variable $h$ is uniformly sampled from the finite set $S$. For integers $N, M \in \mathbb{N}$, we define $[N, M] := \{N, N+1, \dots, M\}$ (which is the empty set for $M < N$), $[N] := [1, N]$ and $[N]_0 := [0, N]$. The statistical distance between two random variables $U$ and $V$ having a common domain $U$ is defined as $\Delta[U, V] = \sum_{u \in U} |\Pr[U = u] - \Pr[V = u]|$. The notation $\llbracket B \rrbracket$, where $B$ is a boolean statement, evaluates to 1 if the statement is true and 0 otherwise.

We use uppercase letters $\mathcal{A}, \mathcal{B}$ to denote algorithms. Unless otherwise stated, algorithms are probabilistic, and we write $(y_1, \dots) \stackrel{\mathcal{A}}{\leftarrow} \mathcal{A}(x_1, \dots)$ to denote that $\mathcal{A}$ returns $(y_1, \dots)$ when run on input $(x_1, \dots)$. We write $\mathcal{A}^B$ to denote that $\mathcal{A}$ has oracle access to $\mathcal{B}$ during its execution. For a randomised algorithm $\mathcal{A}$, we use the notation $y \in \mathcal{A}(x)$ to denote that $y$ is a possible output of $\mathcal{A}$ on input $x$. We denote the running time of an algorithm $\mathcal{A}$ by $t_{\mathcal{A}}$.
**SECURITY GAMES.** We use standard code-based security games [BR04]. A game G is a probability experiment in which an adversary $\mathcal{A}$ interacts with an implicit challenger that answers oracle queries issued by $\mathcal{A}$. The game G has one main procedure and an arbitrary amount of additional oracle procedures which describe how these oracle queries are answered. We denote the (binary) output b of game G between a challenger and an adversary $\mathcal{A}$ as $G^A \Rightarrow b$. $\mathcal{A}$ is said to win G if $G^A \Rightarrow 1$. Unless otherwise stated, the randomness in the probability term $\Pr[G^A \Rightarrow 1]$ is over all the random coins in game G.

[BR04] Bellare and Rogaway, *Code-Based Game-Playing Proofs and the Security of Triple Encryption*

## 4.3 STANDARD CRYPTOGRAPHIC DEFINITIONS

A keyed function $F$ with a finite key space $\mathcal{K}$ and a finite output range $\mathcal{R}$ is a function $F: \mathcal{K} \times \{0, 1\}^* \to \mathcal{R}$.

**Definition 4.1 (Multi-Key Pseudorandom Function).** The $(n_k, q_{\text{PRF}})$-PRF advantage of an adversary $\mathcal{A}$ against a keyed function $F$ with finite key space $\mathcal{K}$ and finite range $\mathcal{R}$ is defined as

$$ \mathrm{Adv}_{F, \mathcal{A}}^{(n_k, q_{\text{PRF}})-\text{PRF}} := \left| \Pr[\mathcal{A}^{f_1(\cdot), \dots, f_{n_k}(\cdot)}] - \Pr_{k_1, \dots, k_{n_k} \stackrel{\S}{\leftarrow} \mathcal{K}}[\mathcal{A}^{F(k_1, \cdot), \dots, F(k_{n_k}, \cdot)}] \right|, $$

where $f_i: \{0, 1\}^* \to \mathcal{R}$ for $i \in [n_k]$ are perfect random functions and $\mathcal{A}$ makes at most $q_{\text{PRF}}$ queries in total to the oracles $f_i$, resp. $F(k_i, \cdot)$.

**Definition 4.2 (Collision Resistance).** Let $\mathcal{H}$ be a family of hash functions from $\{0, 1\}^*$ to the finite range $\mathcal{R}$. We define the advantage of an adversary $\mathcal{A}$ against collision resistance of $\mathcal{H}$ as

$$ \mathrm{Adv}_{\mathcal{H}, \mathcal{A}}^{\mathrm{CR}} := \Pr[\mathcal{H} \stackrel{\S}{\leftarrow} \mathcal{H}; x_1, x_2 \stackrel{\S}{\leftarrow} \mathcal{A}^{\mathrm{H}} : \mathrm{H}(x_1) = \mathrm{H}(x_2) \land x_1 \neq x_2]. $$

We now define (nonce-based) Authenticated Encryption with Associated Data.

**Definition 4.3 (AEAD).** A nonce-based authenticated encryption scheme with associated data and key space $\mathcal{K}$ consists of the following two algorithms:

* Deterministic algorithm AEAD.Enc takes as input a key $k \in \mathcal{K}$, a message $m$, associated data aad and a nonce nonce and outputs a ciphertext $c$.

* Deterministic algorithm AEAD.Dec takes as input a key $k \in \mathcal{K}$, a ciphertext $c$, associated data aad and a nonce nonce and outputs a message $m$ or the failure symbol $\perp$.

We require that for all aad $\in \{0, 1\}^*$, $m \in \{0, 1\}^*$, nonce $\in \{0, 1\}^{N_n}$

$$ \Pr_{k \stackrel{\S}{\leftarrow} \mathcal{K}}[\mathrm{AEAD}.\mathrm{Dec}(k, \mathrm{AEAD}.\mathrm{Enc}(k, m, \mathrm{aad}, \mathrm{nonce}), \mathrm{aad}, \mathrm{nonce}) \neq \perp] = 1, $$

where $N_n$ is the length of the nonce in bits.
We define the multi-key security games $n_k$-IND-CPA$_\ell$ and $n_k$-IND-CPA$_r$ in Listing 4.1 and $(n_k, q_d)$-INT-CTXT$_\ell$ and $(n_k, q_d)$-INT-CTXT$_r$ in Listing 4.2. The advantage of an adversary $\mathcal{A}$ is

$$
\begin{align*}
\text{Adv}_{\mathcal{A}, \text{AEAD}}^{n_k\text{-IND-CPA}} &:= \left| \Pr[n_k\text{-IND-CPA}_\ell(\mathcal{A}) \Rightarrow 1] \\ &\quad - \Pr[n_k\text{-IND-CPA}_r(\mathcal{A}) \Rightarrow 1] \right|, \\
\text{Adv}_{\mathcal{A}, \text{AEAD}}^{(n_k, q_d)\text{-INT-CTXT}} &:= \left| \Pr[(n_k, q_d)\text{-INT-CTXT}_\ell(\mathcal{A}) \Rightarrow 1] \\ &\quad - \Pr[(n_k, q_d)\text{-INT-CTXT}_r(\mathcal{A}) \Rightarrow 1] \right|.
\end{align*}
$$

Here, we define the IND-CPA and INT-CTXT notions as indistinguishability properties between a left game $G_\ell$ and a right game $G_r$, since this is required by CryptoVerif. In order to use such assumptions, CryptoVerif automatically recognizes when a game corresponds to an adversary interacting with $G_\ell$, and it replaces $G_\ell$ with $G_r$ in that game. Moreover, CryptoVerif requires the games $G_\ell$ and $G_r$ to be formulated in a multi-key setting. That allows CryptoVerif to apply the assumption directly in case the scheme is used with several keys, without having to do a hybrid argument itself. (CryptoVerif infers the multi-key assumption automatically from a single-key assumption only in very simple cases.) Also, we allow only one query to the ENC oracle, where the experiment chooses nonces randomly. It is easy to see that these notions are implied by multi-key definitions of IND-CPA and INT-CTXT where the adversary can choose (non-repeating) nonces.

Listing 4.1: Games $n_k$-IND-CPA$_\ell$ and $n_k$-IND-CPA$_r$ for AEAD. Adversary $\mathcal{A}$ makes at most one query per key to ENC.

$n_k$-IND-CPA$_\ell$ and
$$
\begin{array}{l}
01 \quad \mathbf{for} \ i \in [n_k] \\
02 \quad k_i \leftarrow \mathcal{K} \\
03 \quad \text{nonce}_i \leftarrow \{0, 1\}^{N_n} \\
04 \quad b \leftarrow \mathcal{A}^{\text{ENC}} \\
05 \quad \mathbf{return} \ b
\end{array}
$$

Oracle ENC(i, m, aad)
06 $c \leftarrow$ AEAD.Enc($k_i$, m, aad, nonce$_i$)
07 $c \leftarrow$ AEAD.Enc($k_i$, $0^{|m|}$, aad, nonce$_i$)
08 \textbf{return} (c, nonce$_i$)

Listing 4.2: Games $(n_k, q_d)$-INT-CTXT$_\ell$ and $(n_k, q_d)$-INT-CTXT$_r$ for AEAD. Adversary $\mathcal{A}$ makes at most one query per key to ENC and at most $q_d$ queries in total to DEC.

$ (n_k, q_d)$-INT-CTXT$_\ell$ and
$$
\begin{array}{l}
01 \quad \mathbf{for} \ i \in [n_k] \\
02 \quad k_i \leftarrow \mathcal{K} \\
03 \quad \text{nonce}_i \leftarrow \{0, 1\}^{N_n} \\
04 \quad \mathcal{E} \leftarrow \emptyset \\
05 \quad b \leftarrow \mathcal{A}^{\text{ENC,DEC}} \\
06 \quad \mathbf{return} \ b
\end{array}
$$

Oracle ENC(i, m, aad)
07 $c \leftarrow$ AEAD.Enc($k_i$, m, aad, nonce$_i$)
08 $\mathcal{E} \leftarrow \mathcal{E} \cup \{i, m, c, \text{aad}\}$
09 \textbf{return} (c, nonce$_i$)

Oracle DEC(i, c, aad)
10 $m \leftarrow$ AEAD.Dec($k_i$, c, aad, nonce$_i$)
11 \textbf{if} $\exists m' : (i, m', c, \text{aad}) \in \mathcal{E}$
12 \quad $m \leftarrow m'$
13 \textbf{else}
14 \quad $m \leftarrow \bot$
15 \textbf{return} $m$
## 4.4 ELLIPTIC CURVES

In this section we introduce the elliptic curves relevant for the HPKE standard, P-256, P-384, P-521 [Nat13], Curve25519 and Curve448 [LHT16], together with relevant security assumptions.

### 4.4.1 Nominal Groups

We first define nominal groups, a general abstract model of elliptic curves, and then show how we instantiate it for each of the above-mentioned curves.

**Definition 4.4.** A nominal group $\mathcal{N} = (\mathcal{G}, g, p, \mathcal{E}_H, \mathcal{E}_U, \exp)$ consists of an efficiently recognizable finite set of elements $\mathcal{G}$ (also called “group elements”), a base element $g \in \mathcal{G}$, a prime $p$, a finite set of honest exponents $\mathcal{E}_H \subset \mathbb{Z}$, a finite set of exponents $\mathcal{E}_U \subset \mathbb{Z} \setminus p\mathbb{Z}$, and an efficiently computable exponentiation function $\exp : \mathcal{G} \times \mathbb{Z} \to \mathcal{G}$, where we write $X^y$ for $\exp(X, y)$. The exponentiation function is required to have the following properties:

1. $(X^y)^z = X^{yz}$ for all $X \in \mathcal{G}, y, z \in \mathbb{Z}$;

2. the function $\phi$ defined by $\phi(x) = g^x$ is a bijection from $\mathcal{E}_U$ to $\{g^x | x \in [1, p-1]\}$.

A nominal group is said to be *rerandomisable* when:

3. $g^{x+py} = g^x$ for all $x, y \in \mathbb{Z}$;

4. for all $y \in \mathcal{E}_U$, the function $\phi_y$ defined by $\phi_y(x) = g^{xy}$ is a bijection from $\mathcal{E}_U$ to $\{g^x | x \in [1, p-1]\}$.

We remark that even though $\mathcal{G}$ is called the set of (group) elements, it is not required to form a group. Property 2 guarantees that the discrete logarithm is unique in the set $\mathcal{E}_U$. (The index $U$ in $\mathcal{E}_U$ stands for unique.) It is needed to define the DH oracle in Definitions 4.5 and 4.6.

For a nominal group $\mathcal{N} = (\mathcal{G}, g, p, \mathcal{E}_H, \mathcal{E}_U, \exp)$, we let $D_H$ be the distribution of honestly generated exponents, that is, the uniform distribution on $\mathcal{E}_H$. Let $D_U$ be the uniform distribution on $\mathcal{E}_U$. Depending on the choice of $\mathcal{E}_H$ and $\mathcal{E}_U$, these distributions may differ. We define the two statistical parameters

$$ \Delta_{\mathcal{N}} := \Delta[D_H, D_U], \quad \text{and} \quad P_{\mathcal{N}} = \max_{Y \in \mathcal{G}} \Pr_{x \leftarrow \mathcal{E}_H} [Y = g^x]. $$

We summarise the expected security level and the concrete upper bounds for $\Delta_{\mathcal{N}}$ and $P_{\mathcal{N}}$ in Table 4.2 of Section 4.6.3 and compute them below.

**PRIME-ORDER GROUPS.** The simplest example of a *rerandomisable* nominal group is when $\mathcal{G} = \mathcal{G}$ is a group of prime order $p$ with generator $g$, $\exp$ is defined via the usual scalar multiplication on $\mathcal{G}$, and $\mathcal{E}_H = \mathcal{E}_U = [1, p-1]$.

Since $\mathcal{E}_U = [1, p-1]$, the image of $\phi$ is obviously $\{g^x | x \in [1, p-1]\}$. Furthermore, $\phi(x) = \phi(x')$ if and only if $x \equiv x' \mod p$, so $\phi$ is injective on $\mathcal{E}_U$.

For all $x, y \in \mathcal{E}_U$, there exists $x' \in [1, p-1]$ such that $xy \equiv x' \mod p$ (since $x$ and $y$, and so $xy$, are prime to $p$). Since we work in a group of order $p$, $\phi_y(x) = g^{xy} = g^{x'}$, so the image of $\phi_y$ is included in $\{g^{x'} | x' \in [1, p-1]\}$. Moreover, for all $y \in \mathcal{E}_U$ and $x' \in [1, p-1]$, there exists $x \in \mathcal{E}_U$ such that

[Nat13] National Institute of Standards and Technology, Digital Signature Standard (DSS)

[LHT16] Langley et al., *Elliptic Curves for Security*
$xy \equiv x' \mod p$, so $\phi_y(x) = g^{x'}$, so the image of $\phi_y$ is $\{g^{x'} | x' \in [1, p-1]\}$. Finally, for $y \in \mathcal{E}_U$, $\phi_y(x) = \phi_y(x')$ if and only if $xy \equiv x'y \mod p$, if and only if $x \equiv x' \mod p$ so $\phi_y$ is injective on $\mathcal{E}_U$.

The two distributions $D_H$ and $D_U$ are identical, so $\Delta_N = 0$. Since all elements have the same probability, we have $P_N = 1/(p-1)$. The NIST curves P-256, P-384, and P-521 [Nat13] are examples of prime-order groups. CURVE25519 AND CURVE448. We now show that both Curve25519 and Curve448 [LHT16] can also be seen as rerandomisable nominal groups. They are elliptic curves defined by equations of the form $Y^2 = X^3 + AX^2 + X$ in the field $\mathbb{F}_q$ for a large prime $q$. The curve points are represented only by their $X$ coordinate. When $X^3 + AX^2 + X$ is a square $Y^2$, $X$ represents the curve point $(X, Y)$ or $(X, -Y)$. When $X^3+AX^2+X$ is not a square, $X$ does not represent a point on the curve, but on its quadratic twist. The curve is a group of cardinal $kp$ and the twist is a group of cardinal $k'p'$, where $p$ and $p'$ are large primes and $k$ and $k'$ are small integers. For Curve25519, $q = 2^{255}-19$, $k = 8$, $k' = 4$, $p = 2^{252} + \delta$, $p' = 2^{253} - 9 - 2\delta$ with $0 < \delta < 2^{125}$. For Curve448, $q = 2^{448} - 2^{224} - 1$, $k = k' = 4$, $p = 2^{446} - 2^{223} - \delta$, $p' = 2^{446} + \delta$ with $0 < \delta < 2^{220}$. The base point $Q_0$ is an element of the curve, of order $p$, which generates a subgroup $G_s$ of the curve. The set of elements $G$ is the set of bitstrings of 32 bytes for Curve25519, of 56 bytes for Curve448.

The exponentiation function is specified as follows, using [Ber06, Theorem 2.1]: We consider the elliptic curve $E(\mathbb{F}_{q^2})$ defined by the equation $Y^2 = X^3 + AX^2 + X$ in a quadratic extension $\mathbb{F}_{q^2}$ of $\mathbb{F}_q$. We define $X_0 : E(\mathbb{F}_{q^2}) \to \mathbb{F}_{q^2}$ by $X_0(\infty) = 0$ and $X_0(X, Y) = X$. For $X \in \mathbb{F}_q$ and $y$ an integer, we define $y \cdot X \in \mathbb{F}_q$ as $y \cdot X = X_0(yQ_X)$, where $Q_X \in E(\mathbb{F}_{q^2})$ is any of the two elements satisfying $X_0(Q_X) = X$. (It is not hard to verify that this mapping is well-defined.) Elements in $G$ are mapped to elements of $\mathbb{F}_q$ by the function $\text{decode\_pk} : G \to \mathbb{F}_q$ and conversely, elements of $\mathbb{F}_q$ are mapped to the group elements by the function $\text{encode\_pk} : \mathbb{F}_q \to G$, such that $\text{decode\_pk} \circ \text{encode\_pk}$ is the identity. (For Curve25519 we have $\text{decode\_pk}(X) = (X \bmod 2^{255}) \bmod q$, for Curve448 $\text{decode\_pk}(X) = X \bmod q$, and $\text{encode\_pk}(X)$ is the representation of $X$ as an element of $\{0, \dots, q-1\}$.) Finally, $X^y = \text{encode\_pk}(y \cdot \text{decode\_pk}(X))$.

As required by **Definition 4.4**, we have $(X^y)^z = X^{yz}$. Indeed,

$$ 
\begin{align*}
(X^y)^z &= \text{encode\_pk}(z \cdot \text{decode\_pk}(\text{encode\_pk}(y \cdot \text{decode\_pk}(X))))) \\
&= \text{encode\_pk}(z \cdot y \cdot \text{decode\_pk}(X)) \\
&= \text{encode\_pk}(yz \cdot \text{decode\_pk}(X)) = X^{yz}.
\end{align*}
$$

The base element is $g = \text{encode\_pk}(X_0(Q_0))$. It is easy to check that $g^{x+py} = g^x$, since $Q_0$ is an element of order $p$. The honest exponents are chosen uniformly in the set $\mathcal{E}_H = \{kn | n \in [M, N]\}$. For Curve25519, $M = 2^{251}$, $N = 2^{252} - 1$. For Curve448, $M = 2^{445}$, $N = 2^{446} - 1$.

Our exponentiation function is closely related to the function X25519 (resp. X448 for Curve448) as defined in [LHT16], namely $X25519(y, X) = X^{\text{clamp}(y)}$, where $\text{clamp}(y)$ sets and resets some bits in the bitstring $y$ to make sure that $\text{clamp}(y) \in \mathcal{E}_H$. Instead of clamping secret keys together with exponentiation, we clamp them when we generate them, hence we generate honest secret keys in $\mathcal{E}_H$.

<footnote>[Nat13] National Institute of Standards and Technology, Digital Signature Standard (DSS)</footnote>

<footnote>[LHT16] Langley et al., *Elliptic Curves for Security*</footnote>

<footnote>[Ber06] Bernstein, “Curve25519: New Diffie-Hellman Speed Records”</footnote>
We let $\mathcal{E}_U = \{kn \mid n \in [(p+1)/2, p-1]\}$. We have $\phi(x) = g^x = \text{encode\_pk}(X_0(xQ_0))$, so $\phi(x) = \phi(x')$ if and only if $\text{encode\_pk}(X_0(xQ_0)) = \text{encode\_pk}(X_0(x'Q_0))$, if and only if $X_0(xQ_0) = X_0(x'Q_0)$ since $\text{encode\_pk}$ is injective, if and only if $xQ_0 = x'Q_0$ or $xQ_0 = -x'Q_0$, if and only if $x \equiv x'$ mod $p$ or $x \equiv -x'$ mod $p$ since $Q_0$ is an element of order $p$.

Let us show that $\phi$ is injective on $\mathcal{E}_U$. Suppose $x = kn$ and $x' = kn'$ are in $\mathcal{E}_U$. We have $\phi(x) = \phi(x')$ if and only if $kn \equiv kn'$ mod $p$ or $kn \equiv -kn'$ mod $p$, if and only if $n \equiv n'$ mod $p$ or $n \equiv -n'$ mod $p$ since $k$ is prime to $p$, so invertible modulo $p$. Since $n$ and $n'$ are in $[(p+1)/2, p-1]$, that implies $n = n'$, so $x = x'$, which shows the injectivity of $\phi$.

Let us now show that $\phi(\mathcal{E}_U) = \{g^x \mid x \in [1, p-1]\}$. If $x \in \mathcal{E}_U$, then there exists $x'$ such that $x \equiv x'$ mod $p$ and $x' \in [1, p-1]$ (because $x$ is prime to $p$), so $\phi(x) = \phi(x') \in \{g^x \mid x \in [1, p-1]\}$. Conversely, let $X' = g^{x'} = \phi(x')$ with $x' \in [1, p-1]$. Computing modulo $p$, we can find $n_0 \in [1, p-1]$ such that $kn_0 \equiv x'$ mod $p$ (by inverting $k$ modulo $p$). If $n_0 \in [(p+1)/2, p-1]$, we let $n = n_0$. Otherwise, $n_0 \in [1, (p-1)/2]$, and we let $n = p - n_0$. In all cases, $n \in [(p+1)/2, p-1]$ and $kn \equiv x'$ mod $p$ or $kn \equiv -x'$ mod $p$, so $\phi(kn) = \phi(x') = X'$. Therefore, $\phi$ is a bijection from $\mathcal{E}_U$ to $\{g^x \mid x \in [1, p-1]\}$.

Similarly, for $y \in \mathcal{E}_U$, $\phi_y(x) = \phi_y(x')$ if and only if $xy \equiv x'y$ mod $p$ or $xy \equiv -x'y$ mod $p$ if and only if $x \equiv x'$ mod $p$ or $x \equiv -x'$ mod $p$ since $y$ is prime to $p$. Like for $\phi$, that shows the injectivity of $\phi_y$ on $\mathcal{E}_U$. Let us now show that $\phi_y(\mathcal{E}_U) = \{g^x \mid x \in [1, p-1]\}$. If $x \in \mathcal{E}_U$, then there exists $x'$ such that $xy \equiv x'$ mod $p$ and $x' \in [1, p-1]$ (because $x$ and $y$ are prime to $p$), so $\phi_y(x) = g^{x'} \in \{g^x \mid x \in [1, p-1]\}$. Conversely, let $X' = g^{x'}$ with $x' \in [1, p-1]$. Computing modulo $p$, we can find $n_0 \in [1, p-1]$ such that $ykn_0 \equiv x'$ mod $p$ (by inverting $k$ and $y$ modulo $p$). If $n_0 \in [(p+1)/2, p-1]$, we let $n = n_0$. Otherwise, $n_0 \in [1, (p-1)/2]$, and we let $n = p - n_0$. In all cases, $n \in [(p+1)/2, p-1]$ and $ykn \equiv x'$ mod $p$ or $ykn \equiv -x'$ mod $p$, so $\phi_y(kn) = g^{x'} = X'$. Therefore, $\phi_y$ is a bijection from $\mathcal{E}_U$ to $\{g^x \mid x \in [1, p-1]\}$.

**Lemma 4.1.** For Curve25519, $\Delta_N < 2^{-126}$ and $P_N = 2^{-250}$, and for Curve448, $\Delta_N < 2^{-221}$ and $P_N = 2^{-444}$.

*Proof.* We have

$$ \Delta_N = \Delta[D_H, D_U] = \frac{1}{2} \sum_{x \in \mathbb{Z}} |\Pr(x) - \Pr(x)|. $$

For Curve25519, we have $M < (p+1)/2 < N < p-1$. The exponents $kn$ for $n \in [M, (p-1)/2]$ each have probability 0 in $D_U$ and $1/2^{251}$ in $D_H$. The exponents $kn$ for $n \in [(p+1)/2, N]$ each have probability $2/(p-1)$ in $D_U$ and $1/2^{251}$ in $D_H$. The exponents $kn \in [N+1, p-1]$ each have probability $2/(p-1)$ in $D_U$ and 0 in $D_H$. Then

$$ 2\Delta_N = \left(\frac{p-1}{2} - M + 1\right) \times \frac{1}{2^{251}} + \left(N - \frac{p+1}{2} + 1\right) \times \left|\frac{2}{p-1} - \frac{1}{2^{251}}\right| \\ + (p-1 - (N+1) + 1) \times \frac{2}{p-1}. $$
Since $1/(p-1) < 2^{-252}$, a straightforward computation shows that

$$ \Delta_N < 2^{-126}. $$

For Curve448, we have $(p+1)/2 < M < p-1 < N$. The exponents $kn$ for $n \in [(p+1)/2, M-1]$ each have probability $2/(p-1)$ in $D_U$ and $0$ in $D_H$. The exponents $kn$ for $n \in [M, p-1]$ each have probability $2/(p-1)$ in $D_U$ and $1/2^{445}$ in $D_H$. The exponents $kn$ for $n \in [p, N]$ have probability $0$ in $D_U$ and $1/2^{445}$ in $D_H$. Then

$$ 2\Delta_N = \left(M-1-\frac{p+1}{2}+1\right) \times \frac{2}{p-1} + (p-1-M+1) \times \left|\frac{2}{p-1}-\frac{1}{2^{445}}\right| + (N-p+1) \times \frac{1}{2^{445}}. $$

Since $2/(p-1) > 2^{-445}$, a straightforward computation shows that

$$ \Delta_N < 2^{-221}. $$

Some elements $g^x$ are generated from 2 exponents $x = kn$ for $n \in [M, N]$ (for Curve25519, the exponents $kn$ for $n \in [M, (p+1)/2-1]$ yield the same elements as those for $n \in [(p+1)/2, p-M]$; for Curve448, the exponents $kn$ for $n \in [p+1, N]$ yield the same elements as those for $n \in [2p-N, p-1])$, so they have probability $\frac{2}{N-M+1}$, and all other elements are generated from one exponent $kn$ with $n \in [M, N]$, so they have probability $\frac{1}{N-M+1}$. Therefore, $P_N = \frac{2}{N-M+1}$, which yields $P_N = 2^{-250}$ for Curve25519 and $P_N = 2^{-444}$ for Curve448. $\square$

### 4.4.2 Diffie-Hellman Assumptions

Let us first recall the Gap Diffie-Hellman and Square Gap Diffie-Hellman assumptions, as in this chapter, we use slightly different definitions than for the work on WireGuard (cf. Definition 3.1). We adapt them to the setting of a nominal group $\mathcal{N} = (\mathcal{G}, g, p, \mathcal{E}_H, \mathcal{E}_U, \exp)$ of the previous section, by allowing elements in $\mathcal{G}$ as arguments of the Diffie-Hellman decision oracle. Moreover, we choose secret keys in $\mathcal{E}_U$, not in $\mathcal{E}_H$, as it guarantees that the secret key $p$, or equivalently $0$, is never chosen, which helps in the following theorems.

**Definition 4.5 (Gap Diffie-Hellman (GDH) Problem).** We define the advantage function of an adversary $\mathcal{A}$ against the Gap Diffie-Hellman problem over nominal group $\mathcal{N}$ as

$$ \mathrm{Adv}_{\mathcal{A}, \mathcal{N}}^{\mathrm{GDH}} := \Pr_{x,y \stackrel{s}{\leftarrow} \mathcal{E}_U} [Z = g^{xy} | Z \stackrel{s}{\leftarrow} \mathcal{A}^{\mathrm{DH}}(g^x, g^y)] $$

where DH is a decision oracle that on input $(g^x, Y, Z)$ with $\hat{x} \in \mathcal{E}_U$ and $Y, Z \in \mathcal{G}$, returns $1$ iff $Y^x = Z$ and $0$ otherwise.

Since $\phi$ is injective on $\mathcal{E}_U$ by Property 2 of Definition 4.4, the value of $\hat{x} \in \mathcal{E}_U$ is unambiguously defined by $g^x$.

**Definition 4.6 (Square Gap Diffie-Hellman (sqGDH) Problem).** We define the advantage function of an adversary $\mathcal{A}$ against the Square Gap Diffie-Hellman problem over nominal group $\mathcal{N}$ as

$$ \mathrm{Adv}_{\mathcal{A}, \mathcal{N}}^{\mathrm{sqGDH}} := \Pr_{x \stackrel{s}{\leftarrow} \mathcal{E}_U} [Z = g^{x^2} | Z \stackrel{s}{\leftarrow} \mathcal{A}^{\mathrm{DH}}(g^x)] $$
where DH is a decision oracle that on input $(g^{\hat{x}}, Y, Z)$, with $\hat{x} \in \mathcal{E}_U$ and $Y, Z \in \mathcal{G}$, returns 1 iff $Y^{\hat{x}} = Z$ and 0 otherwise.

CryptoVerif cannot use cryptographic assumptions directly in this form: as explained in Section 4.3, it requires assumptions to be formulated as computational indistinguishability axioms between a left game $G_\ell$ and a right game $G_r$, formulated in a multi-key setting. Therefore, we reformulate the Gap Diffie-Hellman assumption to satisfy these requirements, and prove that our formulation is implied by the standard assumption.

We also take into account at this point that secret keys are actually chosen in $\mathcal{E}_H$ rather than in $\mathcal{E}_U$.

**Definition 4.7** (Left-or-Right $(n, m)$-Gap Diffie-Hellman Problem). We define the advantage function of an adversary $\mathcal{A}$ against the left-or-right $(n, m)$-Gap Diffie-Hellman problem over nominal group $\mathcal{N}$ as

$$ \mathrm{Adv}_{\mathcal{A}, \mathcal{N}}^{\mathrm{LoR}-(n,m)-\mathrm{GDH}} := \left| \begin{array}{@{}l@{}} \displaystyle \Pr_{\substack{\forall i \in [n]: x_i \stackrel{\$}{\leftarrow} \mathcal{E}_H \\ \forall j \in [m]: y_j \stackrel{\$}{\leftarrow} \mathcal{E}_H}} [\mathcal{A}^{\mathrm{DH}_\ell, \mathrm{DH}_x, \mathrm{DH}_y}(g^{x_1}, \dots, g^{x_n}, g^{y_1}, \dots, g^{y_m}) \Rightarrow 1] \\ \\ \displaystyle - \Pr_{\substack{\forall i \in [n]: x_i \stackrel{\$}{\leftarrow} \mathcal{E}_H \\ \forall j \in [m]: y_j \stackrel{\$}{\leftarrow} \mathcal{E}_H}} [\mathcal{A}^{\mathrm{DH}_r, \mathrm{DH}_x, \mathrm{DH}_y}(g^{x_1}, \dots, g^{x_n}, g^{y_1}, \dots, g^{y_m}) \Rightarrow 1] \end{array} \right| $$

where $DH_x$ is a decision oracle that on input $(i, Y, Z)$ for $i \in [n]$ returns 1 iff $Y^{x_i} = Z$ and 0 otherwise; $DH_y$ is a decision oracle that on input $(j, Y, Z)$ for $j \in [m]$ returns 1 iff $Y^{y_j} = Z$ and 0 otherwise; $DH_\ell$ is a decision oracle that on input $(i, j, Z)$ for $i \in [n], j \in [m]$ returns 1 iff $Z = g^{x_i y_j}$ and 0 otherwise; and $DH_r$ is an oracle that on input $(i, j, Z)$ for $i \in [n], j \in [m]$ always returns 0.

**Definition 4.8** (Left-or-Right $n$-Square Gap Diffie-Hellman Problem). We define the advantage function of an adversary $\mathcal{A}$ against the left-or-right $n$-Square Gap Diffie-Hellman problem over nominal group $\mathcal{N}$ as

$$ \mathrm{Adv}_{\mathcal{A}, \mathcal{N}}^{\mathrm{LoR}-n \cdot \mathrm{sqGDH}} := \left| \begin{array}{@{}l@{}} \displaystyle \Pr_{\substack{\forall i \in [n]: x_i \stackrel{\$}{\leftarrow} \mathcal{E}_H}} [\mathcal{A}^{\mathrm{DH}_\ell, \mathrm{DH}_x}(g^{x_1}, \dots, g^{x_n}) \Rightarrow 1] \\ \\ \displaystyle - \Pr_{\substack{\forall i \in [n]: x_i \stackrel{\$}{\leftarrow} \mathcal{E}_H}} [\mathcal{A}^{\mathrm{DH}_r, \mathrm{DH}_x}(g^{x_1}, \dots, g^{x_n}) \Rightarrow 1] \end{array} \right| $$

where $DH_x$ is a decision oracle that on input $(i, Y, Z)$ for $i \in [n]$ returns 1 iff $Y^{x_i} = Z$ and 0 otherwise; $DH_\ell$ is a decision oracle that on input $(i, j, Z)$ for $i, j \in [n]$ returns 1 iff $Z = g^{x_i x_j}$ and 0 otherwise; and $DH_r$ is an oracle that on input $(i, j, Z)$ for $i, j \in [n]$ always returns 0.

**Theorem 4.1** ($\mathrm{GDH} \Rightarrow \mathrm{LoR}-(n, m)-\mathrm{GDH}$). Let $\mathcal{N}$ be a *rerandomisable* nominal group. For any adversary $\mathcal{A}$ against $\mathrm{LoR}-(n, m)-\mathrm{GDH}$, there exists an adversary $\mathcal{B}$ against $\mathrm{GDH}$ such that

$$ \mathrm{Adv}_{\mathcal{A}, \mathcal{N}}^{\mathrm{LoR}-(n,m)-\mathrm{GDH}} \le \mathrm{Adv}_{\mathcal{B}, \mathcal{N}}^{\mathrm{GDH}} + (n+m)\Delta_{\mathcal{N}}, $$

$\mathcal{B}$ queries the DH oracle as many times as $\mathcal{A}$ queries $DH_x$, $DH_y$, $DH_\ell$, or $DH_r$, and $t_B \approx t_A$.
*Proof.* Let $\mathcal{A}$ be an adversary against LoR-(n, m)-GDH. We consider a game $G_1 = \forall i \in [n]: x_i \stackrel{s}{\leftarrow} \mathcal{E}_H; \forall j \in [m]: y_j \stackrel{s}{\leftarrow} \mathcal{E}_H; \mathcal{A}^{DH_b, DH_x, DH_y}(g^{x_1}, \dots, g^{x_n}, g^{y_1}, \dots, g^{y_m})$ where $DH_b$ is an oracle that on input $(i, j, \hat{Z})$ for $i \in [n]$, $j \in [m]$ raises event BAD iff $\hat{Z} = g^{x_i y_j}$, and always returns 0. We have $\mathrm{Adv}_{\mathcal{A}, \mathcal{N}}^{\mathrm{LoR}-(n,m)-\mathrm{GDH}} \le \mathrm{Pr}[G_1 : \mathrm{BAD}]$.

We define a game $G_2$ that runs as $G_1$ except that the exponents $x_i$ and $y_j$ are chosen in $\mathcal{E}_U$ instead of $\mathcal{E}_H$. The probability of distinguishing one exponent in $\mathcal{E}_U$ from one in $\mathcal{E}_H$ is at most $\Delta_{\mathcal{N}}$ and there are $(n+m)$ such exponents, so the probability of distinguishing $G_1$ from $G_2$ is at most $(n+m)\Delta_{\mathcal{N}}$ and $\mathrm{Adv}_{\mathcal{A}, \mathcal{N}}^{\mathrm{LoR}-(n,m)-\mathrm{GDH}} \le \mathrm{Pr}[G_2 : \mathrm{BAD}] + (n+m)\Delta_{\mathcal{N}}$.

We define a game $G_3$ that runs as $G_2$ except that it defines $X_i = g^{x_i}$ and $Y_j = g^{y_j}$ and runs adversary $\mathcal{A}$ on input $(X_1, \dots, X_n, Y_1, \dots, Y_m)$; $\mathrm{DH}_x(i, \hat{Y}, \hat{Z})$ returns $\mathrm{DH}(X_i, \hat{Y}, \hat{Z})$, $\mathrm{DH}_y(j, \hat{Y}, \hat{Z})$ returns $\mathrm{DH}(Y_j, \hat{Y}, \hat{Z})$, $\mathrm{DH}_b(i, j, \hat{Z})$ raises event BAD when $\mathrm{DH}(X_i, Y_j, \hat{Z}) = 1$, and always returns 0, where $\mathrm{DH}$ is the oracle of Definition 4.5. In the call to $\mathrm{DH}$ inside $\mathrm{DH}_x$, we have $\hat{x} = x_i$ since $g^{x_i} = X_i = g^{\hat{x}}$, $x_i$ and $\hat{x}$ are in $\mathcal{E}_U$, and $\phi$ is injective on $\mathcal{E}_U$ by Property 2 of Definition 4.4. The situation is similar in the other oracles, so $G_3$ is perfectly indistinguishable from $G_2$.

We show how to construct an adversary $\mathcal{B}$ against GDH using random self-reducibility.

Adversary $\mathcal{B}$ inputs $(X, Y)$ and samples $r_i \stackrel{s}{\leftarrow} \mathcal{E}_U$ for $i \in [n]$ and $s_j \stackrel{s}{\leftarrow} \mathcal{E}_U$ for $j \in [m]$. It computes $X_i = X^{r_i}$ and $Y_j = Y^{s_j}$ and runs adversary $\mathcal{A}$ on input $(X_1, \dots, X_n, Y_1, \dots, Y_m)$. On query $\mathrm{DH}_x(i, \hat{Y}, \hat{Z})$, $\mathcal{B}$ queries $\mathrm{DH}(X_i, \hat{Y}, \hat{Z})$ and forwards the answer to $\mathcal{A}$ (like $G_3$). On query $\mathrm{DH}_y(j, \hat{Y}, \hat{Z})$, $\mathcal{B}$ queries $\mathrm{DH}(Y_j, \hat{Y}, \hat{Z})$ and forwards the answer to $\mathcal{A}$ (like $G_3$). On query $\mathrm{DH}_b(i, j, \hat{Z})$, $\mathcal{B}$ queries $\mathrm{DH}(X_i, Y_j, \hat{Z})$. If the output is 0, $\mathcal{B}$ answers 0. If the output is 1, $\mathcal{B}$ immediately aborts the simulation. We can write $X = g^x$ and $Y = g^y$ with $x, y \in \mathcal{E}_U$. Then $X_i = X^{r_i} = g^{x r_i}$ and $Y_j = Y^{s_j} = g^{y s_j}$. Since $\mathrm{DH}$ outputs 1, there exists $\hat{x} \in \mathcal{E}_U$ such that $X_i = g^{\hat{x}}$ and $\hat{Z} = Y_j^{\hat{x}} = g^{\hat{x} y s_j} = X_i^{y s_j} = g^{x y r_i s_j}$. $\mathcal{B}$ computes the inverse modulo $p$ of $r_i s_j$, which is an integer $t$ such that $r_i s_j t \equiv 1 \pmod{p}$, and $Z = \hat{Z}^t = g^{x y r_i s_j t} = g^{x y}$ since $g^{a+p b} = g^a$ for all $a, b \in \mathbb{Z}$ (Property 3 of Definition 4.4). $\mathcal{B}$ terminates with output $Z$.

Let us show that $X_i$ in this simulation follows the same distribution as $X_i$ in $G_3$. In $G_3$, since $x_i$ is uniformly distributed in $\mathcal{E}_U$ and $\phi$ is a bijection from $\mathcal{E}_U$ to $\{g^x \mid x \in [1, p-1]\}$ (Property 2 of Definition 4.4), $X_i$ is uniformly distributed in $\{g^x \mid x \in [1, p-1]\}$. In the simulation, we have $X_i = X^{r_i} = g^{x r_i}$. Since $r_i$ is uniformly distributed in $\mathcal{E}_U$ and $\phi_x$ is a bijection from $\mathcal{E}_U$ to $\{g^x \mid x \in [1, p-1]\}$ (Property 4 of Definition 4.4), $X_i$ is also uniformly distributed in $\{g^x \mid x \in [1, p-1]\}$. The situation is similar for the keys $Y_j$. Therefore, the simulation perfectly simulates $G_3$, and $G_3$ raises event BAD if and only if the simulation successfully computes $Z$, so $\mathrm{Pr}[G_3 : \mathrm{BAD}] = \mathrm{Adv}_{\mathcal{B}, \mathcal{N}}^{\mathrm{GDH}}$, and $\mathrm{Adv}_{\mathcal{A}, \mathcal{N}}^{\mathrm{LoR}-(n,m)-\mathrm{GDH}} \le \mathrm{Adv}_{\mathcal{B}, \mathcal{N}}^{\mathrm{GDH}} + (n+m)\Delta_{\mathcal{N}}$.

The rerandomisation performed here generalizes the one defined for Curve25519 and Curve448 in [BAC19] to a rerandomisable nominal group.

<figure><img src="image_24.png" /></figure>

**Theorem 4.2** (sqGDH $\Rightarrow$ LoR-n-sqGDH). Let $\mathcal{N}$ be a rerandomisable nominal group. For any adversary $\mathcal{A}$ against LoR-n-sqGDH, there exists an adver-

<footnote>[BAC19] Barnes et al., *Homomorphic Multiplication for X25519 and X448*</footnote>
sary $\mathcal{B}$ against sqGDH such that

$$ \mathrm{Adv}_{\mathcal{A}, \mathcal{N}}^{\mathrm{LoR-n-sqGDH}} \le \mathrm{Adv}_{\mathcal{B}, \mathcal{N}}^{\mathrm{sqGDH}} + n\Delta_{\mathcal{N}}, $$

$\mathcal{B}$ queries the DH oracle as many times as $\mathcal{A}$ queries $DH_x$, $DH_\ell$, or $DH_r$, and $t_B \approx t_A$.

*Proof.* The proof is similar to the proof of **Theorem 4.1**. Let $\mathcal{A}$ be an adversary against LoR-n-sqGDH. We consider a game $G_1 = \forall i \in [n] : x_i \stackrel{s}{\leftarrow} \mathcal{E}_H; \mathcal{A}^{DH_b, DH_x}(g^{x_1}, \dots, g^{x_n})$ where $DH_b$ is an oracle that on input $(i, j, \hat{Z})$ for $i, j \in [n]$ raises event BAD iff $\hat{Z} = g^{x_i x_j}$, and always returns 0. We have $\mathrm{Adv}_{\mathcal{A}, \mathcal{N}}^{\mathrm{LoR-n-sqGDH}} \le \mathrm{Pr}[G_1 : \mathrm{BAD}]$.

We define a game $G_2$ that runs as $G_1$ except that the exponents $x_i$ are chosen in $\mathcal{E}_U$ instead of $\mathcal{E}_H$. The probability of distinguishing one exponent in $\mathcal{E}_U$ from one in $\mathcal{E}_H$ is at most $\Delta_N$ and there are $n$ such exponents, so the probability of distinguishing $G_1$ from $G_2$ is at most $n\Delta_N$ and $\mathrm{Adv}_{\mathcal{A}, \mathcal{N}}^{\mathrm{LoR-n-sqGDH}} \le \mathrm{Pr}[G_2 : \mathrm{BAD}] + n\Delta_N$.

We define a game $G_3$ that runs as $G_2$ except that it defines $X_i = g^{x_i}$ and runs adversary $\mathcal{A}$ on input $(X_1, \dots, X_n)$; $DH_x(i, \hat{Y}, \hat{Z})$ returns $DH(X_i, \hat{Y}, \hat{Z})$, $DH_b(i, j, \hat{Z})$ raises event BAD when $DH(X_i, X_j, \hat{Z}) = 1$, and always returns 0, where DH is the oracle of Definition 4.6. Like in **Theorem 4.1**, $G_3$ is perfectly indistinguishable from $G_2$.

We show how to construct an adversary $\mathcal{B}$ against sqGDH.

Adversary $\mathcal{B}$ inputs $X$ and samples $r_i \stackrel{s}{\leftarrow} \mathcal{E}_U$ for $i \in [n]$. It computes $X_i = X^{r_i}$ and runs adversary $\mathcal{A}$ on input $(X_1, \dots, X_n)$. On query $DH_x(i, \hat{Y}, \hat{Z})$, $\mathcal{B}$ queries $DH(X_i, \hat{Y}, \hat{Z})$ and forwards the answer to $\mathcal{A}$ (like $G_3$). On query $DH_b(i, j, \hat{Z})$, $\mathcal{B}$ queries $DH(X_i, X_j, \hat{Z})$. If the output is 0, $\mathcal{B}$ answers 0. If the output is 1, $\mathcal{B}$ immediately aborts the simulation. We can write $X = g^x$ with $x \in \mathcal{E}_U$. Then $X_i = X^{r_i} = g^{xr_i}$ and $X_j = g^{xr_j}$. Since DH outputs 1, there exists $\hat{x} \in \mathcal{E}_U$ such that $X_i = g^{\hat{x}}$ and $\hat{Z} = X_j^{\hat{x}} = g^{\hat{x}xr_j} = X_i^{xr_j} = g^{x^2r_i r_j}$. $\mathcal{B}$ computes the inverse modulo $p$ of $r_i r_j$, which is an integer $t$ such that $r_i r_j t \equiv 1 \pmod{p}$, and $Z = \hat{Z}^t = g^{x^2 r_i r_j t} = g^{x^2}$ since $g^{a+pb} = g^a$ for all $a, b \in \mathbb{Z}$ (Property 3 of Definition 4.4). $\mathcal{B}$ terminates with output $Z$.

As in the proof of **Theorem 4.1**, $X_i$ in this simulation follows the same distribution as $X_i$ in $G_3$. Therefore, the simulation perfectly simulates $G_3$, and $G_3$ raises event BAD if and only if the simulation successfully computes $Z$, so $\mathrm{Pr}[G_3 : \mathrm{BAD}] = \mathrm{Adv}_{\mathcal{B}, \mathcal{N}}^{\mathrm{sqGDH}}$, and $\mathrm{Adv}_{\mathcal{A}, \mathcal{N}}^{\mathrm{LoR-n-sqGDH}} \le \mathrm{Adv}_{\mathcal{B}, \mathcal{N}}^{\mathrm{sqGDH}} + n\Delta_N$. $\square$

IMPLEMENTATION IN CRYPTOVERIF. Definitions in this style for many cryptographic primitives are included in a standard library of cryptographic assumptions in CryptoVerif. As a matter of fact, this library includes a more general variant of the Gap Diffie-Hellman assumption, with corruption oracles and with a decision oracle $DH(g, X, Y, Z)$, which allows the adversary to choose $g$. In this chapter, we use the definition above as it is sufficient for our proofs.

## 4.5 AUTHENTICATED KEY ENCAPSULATION AND PUBLIC KEY ENCRYPTION

In **Section 4.5.1**, we introduce notation and security notions for an authenticated key encapsulation mechanism (AKEM), namely Outsider-CCA, Insider-
CCA and Outsider-Auth. In Section 4.5.2, we introduce notation and security notions for authenticated public key encryption (APKE) which follow the ideas of the notions defined for AKEM. Additionally, we define Insider-Auth security.

In Section 4.5.3, we show how to construct an APKE scheme which achieves Outsider-CCA, Insider-CCA and Outsider-Auth, from an AKEM, a PRF, and an AEAD scheme. For Insider-Auth, we give a concrete attack in Section 4.5.4.

### 4.5.1 Authenticated Key Encapsulation Mechanism

**Definition 4.9 (AKEM).** An authenticated key encapsulation mechanism AKEM consists of three algorithms:

* Gen outputs a key pair $(sk, pk)$, where $pk$ defines a key space $\mathcal{K}$.

* AuthEncap takes as input a (sender) secret key $sk$ and a (receiver) public key $pk$, and outputs an encapsulation $c$ and a shared secret $\mathcal{K} \in \mathcal{K}$.

* Deterministic AuthDecap takes as input a (receiver) secret key $sk$, a (sender) public key $pk$, and an encapsulation $c$, and outputs a shared key $\mathcal{K} \in \mathcal{K}$.

We require that for all $(sk_1, pk_1) \in \text{Gen}, (sk_2, pk_2) \in \text{Gen}$,

$$ \Pr_{(c, \mathcal{K}) \leftarrow \text{AuthEncap}(sk_1, pk_2)}[\text{AuthDecap}(sk_2, pk_1, c) = \mathcal{K}] = 1. $$

The two sets of secret and public keys, $SK$ and $PK$, are defined via the support of the Gen algorithm as $SK := \{sk | (sk, pk) \in \text{Gen}\}$ and $PK := \{pk | (sk, pk) \in \text{Gen}\}$. We assume that there exists a projection function $\mu: SK \to PK$, such that for all $(sk, pk) \in \text{Gen}$ it holds that $\mu(sk) = pk$. Note that such a function exists without loss of generality by defining $sk$ to be the randomness $rnd$ used in the key generation.

Finally, the key collision probability $P_{AKEM}$ of AKEM is defined as

$$ P_{AKEM} := \max_{pk \in \mathcal{PK}} \Pr_{(sk', pk') \leftarrow \text{Gen}} [pk = pk'] $$

**PRIVACY.** The following security notions for privacy aim to capture that KEM ciphertexts issued to an honest and uncompromised receiver are secure, i. e., do not leak any information about the KEM shared key. In Outsider-CCA, the adversary is an outsider, meaning it has no knowledge about the secret keys of honest senders or honest receivers. In Insider-CCA, the adversary is an insider, meaning it gets to choose the secret key of the sender. In both variants, the adversary gets access to encapsulation and decapsulation oracles that it can call multiple times, and in any order.

We define the games $(n, q_e, q_d)$-Outsider-CCA$_{\ell}$ and $(n, q_e, q_d)$-Outsider-CCA$_r$ in Listing 4.3 and the games $(n, q_e, q_d, q_c)$-Insider-CCA$_{\ell}$ and $(n, q_e, q_d, q_c)$-Insider-CCA$_r$ in Listing 4.4. The games follow the left-or-right style, as CryptoVerif requires this for assumptions, and we use these notions as assumptions in the composition theorems. In Appendix C.2, we compare the code-based game syntax with the CryptoVerif syntax for Outsider-CCA.
In all games, the adversary has access to a key generation oracle $GEN$, which allows to create key pairs for up to $n$ users. The adversary will get the public key and an index as identifier for use in other oracles. In the Outsider-CCA games, the adversary has additional access to oracles $AENCAP$ and $ADECAP$. $AENCAP$ takes as input an index specifying the sender, as well as an arbitrary public key specifying the receiver, and returns a ciphertext and a KEM key. In the left game $Outsider-CCA_ℓ$, $AENCAP$ always returns the real KEM key. In the right game $Outsider-CCA_r$, it outputs a uniformly random key if the receiver public key was generated by the experiment. Queries to $ADECAP$, where the adversary specifies an index for a receiver public key, an arbitrary sender public key and a ciphertext, output a KEM key. In the $Outsider-CCA_r$ game, we use a multiset $\mathcal{E}$ to store queries to $AENCAP$ ($\mathcal{W}$ denotes multiset union), which allows us to keep the output of $ADECAP$ consistent. We use a multiset rather than a set here since it may happen that $\mathcal{E}$ contains more than one entry $(pk, pk', c, K)$, for the same or for different $K$, in case ciphertexts chosen by $AENCAP$ collide. The instruction **try get K** s. t. $(pk, pk_j, c, K) \in \mathcal{E}$ **then** computes the multiset $\{K | (pk, pk', c, K) \in \mathcal{E}\}$. If that multiset is not empty, it chooses one element of it uniformly at random and stores it in $K$. Then, it executes the code in the **then** branch. If that multiset is empty, the code in the **then** branch is not executed.

In the Insider-CCA games, there is an additional challenge oracle $CHALL$. The adversary provides an index specifying the receiver and the secret key of the sender, thus taking the role of an insider. $CHALL$ will then output the real KEM key in the Insider-CCA$_ℓ$ game, and a uniformly random key in the Insider-CCA$_r$ game. Thus, even if the target ciphertext was produced with a bad sender secret key (and honest receiver public key), the KEM key should be indistinguishable from a random key. $AENCAP$ will always output the real key and the output of $ADECAP$ is kept consistent with challenges using the same notation for the multiset $\mathcal{E}$ as described above.

In all games, the adversary makes at most $n$ queries to $GEN$, at most $q_e$ queries to oracle $AENCAP$ and at most $q_d$ queries to oracle $ADECAP$. In the Insider-CCA experiment, it can additionally make at most $q_c$ queries to oracle $CHALL$. We define the advantage of an adversary $\mathcal{A}$ as

$$ \text{Adv}_{\mathcal{A},AKEM}^{(n,q_e,q_d)-\text{Outsider-CCA}} := \left| \Pr[(n, q_e, q_d)-\text{Outsider-CCA}_\ell(\mathcal{A}) \Rightarrow 1] - \Pr[(n, q_e, q_d)-\text{Outsider-CCA}_r(\mathcal{A}) \Rightarrow 1] \right|, $$

$$ \text{Adv}_{\mathcal{A},AKEM}^{(n,q_e,q_d,q_c)-\text{Insider-CCA}} := \left| \Pr[(n, q_e, q_d, q_c)-\text{Insider-CCA}_\ell(\mathcal{A}) \Rightarrow 1] - \Pr[(n, q_e, q_d, q_c)-\text{Insider-CCA}_r(\mathcal{A}) \Rightarrow 1] \right|. $$

**AUTHENTICITY.** The following Outsider-Auth security notion aims to capture that the adversary is unable to forge a KEM ciphertext to an honest receiver, pretending to come from an honest sender. We do not define an insider security notion because Insider-Auth security is infeasible both for the APKE construction used in HPKE (see Section 4.5.4), and the instantiation of AKEM proposed in HPKE (see end of Section 4.6.1).

We define the games $(n, q_e, q_d)$-Outsider-Auth$_ℓ$ and $(n, q_e, q_d)$-Outsider-Auth$_r$ in Listing 4.5. The adversary has access to oracles $GEN$, $AENCAP$
Listing 4.3: Games $(n, q_e, q_d)$-Outsider-CCA$_ℓ$ and $(n, q_e, q_d)$-Outsider-CCA$_r$ for AKEM. Adversary $\mathcal{A}$ makes at most $n$ queries to $\text{GEN}$, at most $q_e$ queries to $\text{AENCAP}$ and at most $q_d$ queries to $\text{ADECAP}$.

$(n, q_e, q_d)$-Outsider-CCA$_ℓ$ and

$(n, q_e, q_d)$-Outsider-CCA$_r$

01 $\ell \leftarrow 0$

02 $\mathcal{E} \leftarrow \emptyset$

03 $b \stackrel{\mathcal{S}}{\leftarrow} \mathcal{A}^{\text{GEN}, \text{AENCAP}, \text{ADECAP}}$

04 **return** $b$

Oracle GEN

05 $\ell \leftarrow \ell + 1$

06 $(\text{sk}_\ell, \text{pk}_\ell) \stackrel{\mathcal{S}}{\leftarrow} \text{Gen}$

07 **return** $(\text{pk}_\ell, \ell)$

Oracle $\text{AENCAP}(i \in [\ell], \text{pk})$

08 $(c, K) \stackrel{\mathcal{S}}{\leftarrow} \text{AuthEncap}(\text{sk}_i, \text{pk})$

09 **if** $\text{pk} \in \{\text{pk}_1, \dots, \text{pk}_\ell\}$

10 $K \stackrel{\mathcal{S}}{\leftarrow} \mathcal{K}$

11 $\mathcal{E} \leftarrow \mathcal{E} \uplus \{(\text{pk}_i, \text{pk}, c, K)\}$

12 **return** $(c, \mathcal{K})$

Oracle $\text{ADECAP}(j \in [\ell], \text{pk}, c)$

13 **try get** $K$ s.t. $(\text{pk}, \text{pk}_j, c, K) \in \mathcal{E}$

14 **then return** $K$

15 $\mathcal{K} \leftarrow \text{AuthDecap}(\text{sk}_j, \text{pk}, c)$

16 **return** $K$

Listing 4.4: Games $(n, q_e, q_d, q_c)$-Insider-CCA$_ℓ$ and $(n, q_e, q_d, q_c)$-Insider-CCA$_r$ for AKEM. Adversary $\mathcal{A}$ makes at most $n$ queries to $\text{GEN}$, at most $q_e$ queries to $\text{AENCAP}$, at most $q_d$ queries to $\text{ADECAP}$ and at most $q_c$ queries to $\text{CHALL}$.

$(n, q_e, q_d, q_c)$-Insider-CCA$_ℓ$ and

$(n, q_e, q_d, q_c)$-Insider-CCA$_r$

01 $\ell \leftarrow 0$

02 $\mathcal{E} \leftarrow \emptyset$

03 $b \stackrel{\mathcal{S}}{\leftarrow} \mathcal{A}^{\text{GEN}, \text{AENCAP}, \text{ADECAP}, \text{CHALL}}$

04 **return** $b$

Oracle GEN

05 $\ell \leftarrow \ell + 1$

06 $(\text{sk}_\ell, \text{pk}_\ell) \stackrel{\mathcal{S}}{\leftarrow} \text{Gen}$

07 **return** $(\text{pk}_\ell, \ell)$

Oracle $\text{AENCAP}(i \in [\ell], \text{pk})$

08 $(c, K) \stackrel{\mathcal{S}}{\leftarrow} \text{AuthEncap}(\text{sk}_i, \text{pk})$

09 **return** $(c, K)$

Oracle $\text{ADECAP}(j \in [\ell], \text{pk}, c)$

10 **try get** $K$ s.t. $(\text{pk}, \text{pk}_j, c, K) \in \mathcal{E}$

11 **then return** $K$

12 $\mathcal{K} \leftarrow \text{AuthDecap}(\text{sk}_j, \text{pk}, c)$

13 **return** $K$

Oracle $\text{CHALL}(j \in [\ell], \text{sk})$

14 $(c, K) \stackrel{\mathcal{S}}{\leftarrow} \text{AuthEncap}(\text{sk}, \text{pk}_j)$

15 $K \stackrel{\mathcal{S}}{\leftarrow} \mathcal{K}$

16 $\mathcal{E} \leftarrow \mathcal{E} \uplus \{(\mu(\text{sk}), \text{pk}_j, c, K)\}$

17 **return** $(c, \mathcal{K})$

Listing 4.5: Games $(n, q_e, q_d)$-Outsider-Auth$_\ell$ and $(n, q_e, q_d)$-Outsider-Auth$_r$ for AKEM. Adversary $\mathcal{A}$ makes at most $n$ queries to $\text{GEN}$, at most $q_e$ queries to $\text{AENCAP}$ and at most $q_d$ queries to $\text{ADECAP}$.

$(n, q_e, q_d)$-Outsider-Auth$_\ell$ and

$(n, q_e, q_d)$-Outsider-Auth$_r$

01 $\ell \leftarrow 0$

02 $\mathcal{E} \leftarrow \emptyset$

03 $b \stackrel{\mathcal{S}}{\leftarrow} \mathcal{A}^{\text{GEN}, \text{AENCAP}, \text{ADECAP}}$

04 **return** $b$

Oracle GEN

05 $\ell \leftarrow \ell + 1$

06 $(\text{sk}_\ell, \text{pk}_\ell) \stackrel{\mathcal{S}}{\leftarrow} \text{Gen}$

07 **return** $(\text{pk}_\ell, \ell)$

Oracle $\text{AENCAP}(i \in [\ell], \text{pk})$

08 $(c, K) \stackrel{\mathcal{S}}{\leftarrow} \text{AuthEncap}(\text{sk}_i, \text{pk})$

09 $\mathcal{E} \leftarrow \mathcal{E} \uplus \{(\text{pk}_i, \text{pk}, c, K)\}$

10 **return** $(c, K)$

Oracle $\text{ADECAP}(j \in [\ell], \text{pk}, c)$

11 **try get** $K$ s.t. $(\text{pk}, \text{pk}_j, c, K) \in \mathcal{E}$

12 **then return** $K$

13 $\mathcal{K} \leftarrow \text{AuthDecap}(\text{sk}_j, \text{pk}, c)$

14 **if** $\text{pk} \in \{\text{pk}_1, \dots, \text{pk}_\ell\}$ and $\mathcal{K} \neq \bot$

15 $\mathcal{K} \stackrel{\mathcal{S}}{\leftarrow} \mathcal{K}$

16 $\mathcal{E} \leftarrow \mathcal{E} \uplus \{(\text{pk}, \text{pk}_j, c, K)\}$

17 **return** $\mathcal{K}$
and ADECAP, where GEN is defined as in the CCA games. AENCAP will always output the real KEM key. ADECAP will output the real key in game Outsider-Auth<sub>l</sub>. In the Outsider-Auth<sub>r</sub> game, the adversary (acting as an outsider) will receive a uniformly random key if the receiver public key was generated by the experiment. Thus, the adversary should not be able to distinguish the real KEM key from a random key for two honest users, even if it can come up with the target ciphertext. Again we use the multiset E to ensure consistency.

The adversary makes at most n queries to GEN, at most q<sub>e</sub> queries to oracle AENCAP and at most q<sub>d</sub> queries to oracle ADECAP. We define the advantage of an adversary A as

$$
\mathrm{Adv}_{\mathcal{A}, \mathrm{AKEM}}^{(n, q_e, q_d)\text{-Outside-Auth}} := \left| \Pr[(n, q_e, q_d)\text{-Outside-Auth}_{\ell}(\mathcal{A}) \Rightarrow 1] - \Pr[(n, q_e, q_d)\text{-Outside-Auth}_{r}(\mathcal{A}) \Rightarrow 1] \right|.
$$

In Appendix C.1, we provide simpler single-user or 2-user versions of these
properties, and show that they non-tightly imply the definitions above.
These results could be useful to simplify the proof for new AKEMs that
could be added to HPKE, such as post-quantum AKEMs. However, because
the reduction is not tight, a direct proof of multi-user security may yield
better probability bounds. This is the case for our proof of DH-AKEM in
Section 4.6.1.

4.5.2 Authenticated Public Key Encryption

**Definition 4.10 (APKE).** An authenticated public key encryption scheme APKE consists of the following three algorithms:

• Gen outputs a key pair (sk, pk).

* AuthEnc takes as input a (sender) secret key sk, a (receiver) public key pk, a message m, associated data aad, a bitstring info, and outputs a ciphertext c.

* Deterministic AuthDec takes as input a (receiver) secret key sk, a (sender) public key pk, a ciphertext c, associated data aad and a bitstring info, and outputs a message m.

We require that for all messages $m \in \{0, 1\}^*$, aad $\in \{0, 1\}^*$, info $\in \{0, 1\}^*$,

$$
\Pr_{(sk_S, pk_S) \leftarrow \text{Gen}} \left[ \begin{array}{l} c \leftarrow \text{AuthEnc}(sk_S, pk_R, m, \text{aad}, \text{info}), \\ \text{AuthDec}(sk_R, pk_S, c, \text{aad}, \text{info}) = m \end{array} \right] = 1.
$$

PRIVACY. We define the games (n, qe, qd, qc)-Outside-CCA and (n, qe, qd, qc)-
Insider-CCA in Listing 4.6, which follow ideas similar to the games for
outsider and insider-secure AKEM. The security notions for APKE use the
common style where challenge queries are with respect to a random bit
b. In particular, the additional challenge oracle CHALL will encrypt either
message m0 or m1 provided by the adversary, depending on b. Oracles
AENC and ADEC will always encrypt and decrypt honestly (except for
challenge ciphertexts). In these games, we use a set E to store queries to
Listing 4.6: Games $(n, q_e, q_d, q_c)$-Outside-CCA and $(n, q_e, q_d, q_c)$-Insider-CCA for APKE, where $(n, q_e, q_d, q_c)$-Outside-CCA uses oracle CHALL in the dashed box and $(n, q_e, q_d, q_c)$-Insider-CCA uses oracle CHALL in the solid box. Adversary $\mathcal{A}$ makes at most $n$ queries to GEN, at most $q_e$ queries to AEnc, at most $q_d$ queries to ADEC and at most $q_c$ queries to CHALL.

<figure><img src="image_25.png" /></figure>

Listing 4.7: Games $(n, q_e, q_d)$-Outside-Auth and $(n, q_e, q_d)$-Insider-Auth for APKE. Adversary $\mathcal{A}$ makes at most $n$ queries to GEN, at most $q_e$ queries to AEnc and at most $q_d$ queries to ADEC.

<figure><img src="image_26.png" /></figure>

Listing 4.8: Authenticated PKE scheme APKE[AKEM, KS, AEAD] construction from AKEM, KS and AEAD, where APKE.Gen = AKEM.Gen.

<figure><img src="image_27.png" /></figure>
CHALL and the adversary is not allowed to trivially decrypt a challenge using ADEC.

In these games, the adversary $\mathcal{A}$ makes at most $n$ queries to $\text{GEN}$, at most $q_e$ queries to oracle $\text{AENC}$, at most $q_d$ queries to oracle $\text{ADEC}$, and at most $q_c$ queries to oracle $\text{CHALL}$. The advantage of $\mathcal{A}$ is

$$ \text{Adv}_{\mathcal{A}, \text{APKE}}^{(n, q_e, q_d, q_c)\text{-Outsider-CCA}} := \left| \Pr[(n, q_e, q_d, q_c)\text{-Outsider-CCA}(\mathcal{A}) \Rightarrow 1] - \frac{1}{2} \right|, $$

$$ \text{Adv}_{\mathcal{A}, \text{APKE}}^{(n, q_e, q_d, q_c)\text{-Insider-CCA}} := \left| \Pr[(n, q_e, q_d, q_c)\text{-Insider-CCA}(\mathcal{A}) \Rightarrow 1] - \frac{1}{2} \right|. $$

AUTHENTICITY. Furthermore, we define the games $(n, q_e, q_d)$-Outsider-Auth and $(n, q_e, q_d)$-Insider-Auth in Listing 4.7. The adversary has access to an encryption and decryption oracle and has to come up with a new tuple of ciphertext, associated data and info for any honest receiver secret key (Outsider-Auth) or any (possibly leaked or bad) receiver secret key (Insider-Auth), provided that the sender public key is honest.

In these games, adversary $\mathcal{A}$ makes at most $n$ queries to $\text{GEN}$, at most $q_e$ queries to oracle $\text{AENC}$ and at most $q_d$ queries to oracle $\text{ADEC}$. The advantage of $\mathcal{A}$ is defined as

$$ \text{Adv}_{\mathcal{A}, \text{APKE}}^{(n, q_e, q_d)\text{-Outsider-Auth}} := \Pr[(n, q_e, q_d)\text{-Outsider-Auth}(\mathcal{A}) \Rightarrow 1], $$

$$ \text{Adv}_{\mathcal{A}, \text{APKE}}^{(n, q_e, q_d)\text{-Insider-Auth}} := \Pr[(n, q_e, q_d)\text{-Insider-Auth}(\mathcal{A}) \Rightarrow 1]. $$

### 4.5.3 From AKEM to APKE

In this section we define and analyse a general transformation that models HPKE's way of constructing APKE from an AKEM (c.f. Definition 4.9) and an AEAD (c.f. Definition 4.3 on Page 85). It also uses a so-called key schedule KS which we model as a keyed function $\text{KS} : \mathcal{K} \times \{0, 1\}^* \rightarrow \{0, 1\}^*$, where $\mathcal{K}$ matches the AKEM's key space. KS outputs an AEAD key $k$ and an initialisation vector nonce (called base nonce in the RFC) from which the AEAD's nonces are computed. (The key schedule defined in the HPKE standard also outputs an additional key called exporter secret that can be used to derive keys for use by arbitrary higher-level applications. This export API is not part of the single-shot encryption API that we are analysing, and thus we omit it in our definitions.) Listing 4.8 gives the formal specification of APKE built from AKEM, KS and AEAD.

We observe that in the single-shot encryption API, every AEAD key $k$ is used to produce exactly one ciphertext, and thus is only used with one nonce. In HPKE, messages are counted with a sequence number $s$ starting at 0 and the nonce for a message is computed by nonce $\oplus s$. For the single-shot encryption API this means that the nonce is equal to the initialisation vector nonce. At the same time, this means that nonce is by definition unique.

We now give theorems stating the $(n, q_e, q_d, q_c)$-Outsider-CCA, $(n, q_e, q_d)$-Outsider-Auth and $(n, q_e, q_d, q_c)$-Insider-CCA security of APKE[AKEM, KS, AEAD] defined in Listing 4.8. Theorems 4.3 to 4.5 are proven using CryptoVerif version 2.05. This version includes an improvement in the computation of probability bounds that allows us to express these bounds as functions of the total numbers of queries to the $\text{AENC}$, $\text{ADEC}$, and $\text{CHALL}$
oracles instead of the number of users and the numbers of queries per user. The CryptoVerif input files are given in hpke.auth.outsider-cca.ocv, hpke.auth.insider-cca.ocv, and hpke.auth.outsider-auth.ocv [Alw+]. These proofs are fairly straightforward. As an example, we prefer explaining the proof of Theorem 4.7 later, which is more interesting. In Section 4.5.4, we show that APKE[AKEM, KS, AEAD] cannot achieve Insider-Auth security.

As detailed in Section 4.3, we define a multi-key PRF security experiment $(n_k, q_{PRF})$-PRF with $n_k$ keys, in which the adversary makes at most $q_{PRF}$ queries for each key. We also define multi-key IND-CPA and INT-CTXT security experiments for the AEAD: $n_k$-IND-CPA and $(n_k, q_d)$-INT-CTXT, with $n_k$ keys, in which the adversary makes at most one encryption query for each key and, for the INT-CTXT experiment, at most $q_d$ decryption queries in total. In these experiments, the nonces of the AEAD are chosen randomly.

**Theorem 4.3 (AKEM Outsider-CCA+KS PRF+AEAD IND-CPA+AEAD INT-CTXT) ⇒ APKE Outsider-CCA).** For any $(n, q_e, q_d, q_c)$-Outsider-CCA adversary $\mathcal{A}$ against APKE[AKEM, KS, AEAD], there exist an $(n, q_e + q_c, q_d)$-Outsider-CCA adversary $\mathcal{B}$ against AKEM, an $(q_c, q_c + q_d)$-PRF adversary $\mathcal{C}$ against KS, an $q_c$-IND-CPA adversary $\mathcal{D}_1$ against AEAD and an $(q_c, q_d)$-INT-CTXT adversary $\mathcal{D}_2$ against AEAD such that $t_B \approx t_A$, $t_C \approx t_A$, $t_{D_1} \approx t_A$, $t_{D_2} \approx t_A$, and

$$ \mathrm{Adv}_{\mathcal{A}, \mathrm{APKE}[\mathrm{AKEM}, \mathrm{KS}, \mathrm{AEAD}]}^{(n, q_e, q_d, q_c)\text{-Outsider-CCA}} \le 2 \cdot \mathrm{Adv}_{\mathcal{B}, \mathrm{AKEM}}^{(n, q_e + q_c, q_d)\text{-Outsider-CCA}} + 2 \cdot \mathrm{Adv}_{\mathcal{C}, \mathrm{KS}}^{(q_c, q_c + q_d)\text{-PRF}} \\ + 2 \cdot \mathrm{Adv}_{\mathcal{D}_1, \mathrm{AEAD}}^{q_c \text{-IND-CPA}} + 2 \cdot \mathrm{Adv}_{\mathcal{D}_2, \mathrm{AEAD}}^{(q_c, q_d)\text{-INT-CTXT}} \\ + 6n^2 \cdot P_{\mathrm{AKEM}}. $$

**Theorem 4.4 (AKEM Insider-CCA+KS PRF+AEAD IND-CPA+AEAD INT-CTXT) ⇒ APKE Insider-CCA).** For any $(n, q_e, q_d, q_c)$-Insider-CCA adversary $\mathcal{A}$ against APKE[AKEM, KS, AEAD], there exist an $(n, q_e, q_d, q_c)$-Insider-CCA adversary $\mathcal{B}$ against AKEM, an $(q_c, q_c + q_d)$-PRF adversary $\mathcal{C}$ against KS, an $q_c$-IND-CPA adversary $\mathcal{D}_1$ against AEAD and an $(q_c, q_d)$-INT-CTXT adversary $\mathcal{D}_2$ against AEAD such that $t_B \approx t_A$, $t_C \approx t_A$, $t_{D_1} \approx t_A$, $t_{D_2} \approx t_A$, and

$$ \mathrm{Adv}_{\mathcal{A}, \mathrm{APKE}[\mathrm{AKEM}, \mathrm{KS}, \mathrm{AEAD}]}^{(n, q_e, q_d, q_c)\text{-Insider-CCA}} \le 2 \cdot \mathrm{Adv}_{\mathcal{B}, \mathrm{AKEM}}^{(n, q_e, q_d, q_c)\text{-Insider-CCA}} + 2 \cdot \mathrm{Adv}_{\mathcal{C}, \mathrm{KS}}^{(q_c, q_c + q_d)\text{-PRF}} \\ + 2 \cdot \mathrm{Adv}_{\mathcal{D}_1, \mathrm{AEAD}}^{q_c \text{-IND-CPA}} + 2 \cdot \mathrm{Adv}_{\mathcal{D}_2, \mathrm{AEAD}}^{(q_c, q_d)\text{-INT-CTXT}} \\ + 6n^2 \cdot P_{\mathrm{AKEM}}. $$

**Theorem 4.5 (AKEM Outsider-CCA+AKEM Outsider-Auth+KS PRF+AEAD INT-CTXT) ⇒ APKE Outsider-Auth).** For any $(n, q_e, q_d)$-Outsider-Auth adversary $\mathcal{A}$ against APKE[AKEM, KS, AEAD], there exist an $(n, q_e, q_d + 1)$-Outsider-CCA adversary $\mathcal{B}_1$ against AKEM, an $(n, q_e, q_d + 1)$-Outsider-Auth adversary $\mathcal{B}_2$ against AKEM, an $(q_e + q_d + 1, q_e + 2q_d + 1)$-PRF adversary $\mathcal{C}$ against KS, and an $(q_e + q_d + 1, 2q_d + 1)$-INT-CTXT adversary $\mathcal{D}$ against AEAD such that $t_{B_1} \approx t_A$, $t_{B_2} \approx t_A$, $t_C \approx t_A$, $t_D \approx t_A$, and

$$ \mathrm{Adv}_{\mathcal{A}, \mathrm{APKE}[\mathrm{AKEM}, \mathrm{KS}, \mathrm{AEAD}]}^{(n, q_e, q_d)\text{-Outsider-Auth}} \le \mathrm{Adv}_{\mathcal{B}_1, \mathrm{AKEM}}^{(n, q_e, q_d+1)\text{-Outsider-CCA}} + \mathrm{Adv}_{\mathcal{B}_2, \mathrm{AKEM}}^{(n, q_e, q_d+1)\text{-Outsider-Auth}} \\ + \mathrm{Adv}_{\mathcal{C}, \mathrm{KS}}^{(q_e+q_d+1, q_e+2q_d+1)\text{-PRF}} \\ + \mathrm{Adv}_{\mathcal{D}, \mathrm{AEAD}}^{(q_e+q_d+1, 2q_d+1)\text{-INT-CTXT}} + n(q_e + 11n) \cdot P_{\mathrm{AKEM}}. $$

[Alw+] Alwen et al., Analysing the HPKE Standard Supplementary Material
### 4.5.4 Infeasibility of Insider-Auth security

For any AKEM, KS, and AEAD, the construction APKE[AKEM, KS, AEAD] given in Listing 4.8 is not $(n, q_e, q_d)$-Insider-Auth secure. The inherent reason for this construction to be vulnerable against this attack is that the KEM ciphertext does not depend on the message. Thus, the KEM ciphertext can be reused and the DEM ciphertext can be exchanged by the encryption of any other message.

**Theorem 4.6.** There exists an efficient adversary $\mathcal{A}$ against (1, 1, 0)-Insider-Auth security of APKE[AKEM, KS, AEAD] such that

$$ \mathrm{Adv}_{\mathcal{A}, \mathrm{APKE}[\mathrm{AKEM}, \mathrm{KS}, \mathrm{AEAD}]}^{(1,1,0)-\mathrm{Insider}-\mathrm{Auth}} = 1, $$

which means that $\mathcal{A}$ makes a single query to $\mathrm{GEN}$, a single query to $\mathrm{AENC}$ and no query to $\mathrm{ADEC}$.

*Proof.* We construct adversary $\mathcal{A}$ in Listing 4.9. It has oracle access to $\mathrm{GEN}$, $\mathrm{AENC}$ and $\mathrm{ADEC}$. It first creates a key pair using the $\mathrm{GEN}$ oracle to receive a public key $pk_1$. It then generates a challenge key pair $(sk^*, pk^*)$ and queries the $\mathrm{AENC}$ oracle on any index 1, receiver public key $pk^*$, an arbitrary message $m_1$, as well as arbitrary associated data aad and string info.

Listing 4.9: Adversary $\mathcal{A}$ against (1, 1, 0)-Insider-Auth security (as defined in Listing 4.7) of APKE[AKEM, KS, AEAD].

Adversary $\mathcal{A}^{\mathrm{GEN}, \mathrm{AENC}, \mathrm{ADEC}}$

01 $(pk_1, \ell = 1) \leftarrow \mathrm{GEN}$

02 $(sk^*, pk^*) \leftarrow \mathrm{AKEM}.\mathrm{Gen}$

03 $m_1 := \mathrm{aad} := \mathrm{info} := 1$

04 $(c_1, c_2) \leftarrow \mathrm{AENC}(1, pk^*, m_1, \mathrm{aad}, \mathrm{info})$

05 $K \leftarrow \mathrm{AuthDecap}(sk^*, pk_1, c_1)$

06 $(k, \mathrm{nonce}) \leftarrow \mathrm{KS}(K, \mathrm{info})$

07 $m_2 := 2$

08 $c'_2 \leftarrow \mathrm{AEAD}.\mathrm{Enc}(k, m_2, \mathrm{aad}, \mathrm{nonce})$

09 **return** $(1, sk^*, (c_1, c'_2), \mathrm{aad}, \mathrm{info})$

The challenger computes $(c_1, K) \stackrel{\$}{\leftarrow} \mathrm{AuthEncap}(sk_1, pk^*)$, $(k, \mathrm{nonce}) \leftarrow \mathrm{KS}(K, \mathrm{info})$ and $c_2 \leftarrow \mathrm{AEAD}.\mathrm{Enc}(k, m_1, \mathrm{aad}, \mathrm{nonce})$, and returns $(c_1, c_2)$ to $\mathcal{A}$.

Since $\mathcal{A}$ knows the secret key $sk^*$, it is able to compute the underlying KEM key $K$ using $\mathrm{AuthDecap}$. Next, it computes $(k, \mathrm{nonce})$ and thus retrieves the key $k$ used in the AEAD scheme. Finally, $\mathcal{A}$ encrypts any other message $m_2$ to ciphertext $c'_2$ and replaces the AEAD ciphertext $c_2$ with the new ciphertext. Since $(c_1, c_2) \neq (c_1, c'_2)$, the latter constitutes a valid forgery in the (1, 1, 0)-Insider-Auth security experiment. $\square$

## 4.6 THE HPKE STANDARD

In Section 4.6.1, we show how to construct HPKE's abstract AKEM construction DH-AKEM from a nominal group $\mathcal{N}$ and a key derivation function
<table><caption>Listing 4.10: DH-AKEM[$\mathcal{N}$, KDF] = (Gen, AuthEncap, AuthDecap) as defined in the RFC [Bar+22], constructed from a nominal group $\mathcal{N}$ and key derivation function KDF : $\{0, 1\}^* \to \mathcal{K}$, with $\mathcal{K} = \{0, 1\}^N$.</caption><tr><td>Gen</td><td>AuthEncap(sk &isin; E<sub>H</sub>, pk &isin; G)</td></tr><tr><td>01 sk &larr; &epsilon;<sub>H</sub></td><td>07 (esk, epk) &larr; Gen</td></tr><tr><td>02 pk &larr; g<sup>sk</sup></td><td>08 context &larr; (epk, pk, g<sup>sk</sup>)</td></tr><tr><td>03 return (sk, pk)</td><td>09 dh &larr; (pk<sup>esk</sup>, pk<sup>sk</sup>)</td></tr><tr><td>ExtractAndExpand(dh, context)</td><td>10 K &larr; ExtractAndExpand(dh, context)</td></tr><tr><td>04 IKM &larr; "HPKE-v1" || suite<sub>id</sub> || "eae_prk" || dh</td><td>11 return (epk, K)</td></tr><tr><td>05 info &larr; Encode(N) || "HPKE-v1" || suite<sub>id</sub> || "shared_secret" || context</td><td>12 context &larr; (epk, g<sup>sk</sup>, pk)</td></tr><tr><td>06 return KDF empty, IKM, info</td><td>13 dh &larr; (epk<sup>sk</sup>, pk<sup>sk</sup>)</td></tr><tr><td></td><td>14 return ExtractAndExpand(dh, context)</td></tr></table>

KDF. In Section 4.6.2, we define and analyse HPKE's specific key schedule KS<sub>Auth</sub> and key derivation function HKDF<sub>N</sub>. Finally, in Section 4.6.3 we put everything together and obtain the HPKE standard in Auth mode from all previous sections.

### 4.6.1 HPKE's AKEM Construction DH-AKEM

In this section we present the RFC's instantiation of the AKEM definition, and prove that it satisfies the security notions defined earlier. Listing 4.10 shows the formal definition of DH-AKEM[$\mathcal{N}$, KDF] relative to a nominal group $\mathcal{N}$ (c.f. Definition 4.4) and a key derivation function KDF : $\{0, 1\}^* \to \mathcal{K}$, where $\mathcal{K}$ is the key space. (The RFC uses a key space $\mathcal{K}$, consisting of bitstrings of length $N$, which corresponds to Nsecret in the RFC.) The construction also depends on the fixed-size protocol constants "HPKE-v1" and suite<sub>id</sub>, where suite<sub>id</sub> identifies the KEM in use: it is a string "KEM" plus a two-byte identifier of the KEM algorithm. The bitstring Encode($N$) is the two-byte encoding of the length $N$ expressed in bytes. Correctness follows by property 1 of Definition 4.4. We make the implicit convention that AuthEncap and AuthDecap return reject ($\perp$) if their inputs are not of the right data type as specified in Listing 4.10.

We continue with statements about the $(n, q_e, q_d)$-Outsider-CCA, $(n, q_e, q_d, q_c)$-Insider-CCA, and $(n, q_e, q_d)$-Outsider-Auth security of DH-AKEM[$\mathcal{N}$, KDF], modelling KDF as a random oracle. The proofs are written with CryptoVerif version 2.05; the input files are dhkem.auth.outsider-cca-lr.ocv, dhkem.auth.insider-cca-lr.ocv, and dhkem.auth.outsider-auth-lr.ocv [Alw+]. We sketch the proof of one of the three theorems as an example, to help understand CryptoVerif's approach.

Our results hold for any rerandomisable nominal group, which covers the three NIST curves allowed by the RFC, as well as for the other two allowed curves, Curve25519 and Curve448. The bounds given in Theorems 4.7 to 4.9 depend on the probabilities $\Delta_{\mathcal{N}}$ and $P_{\mathcal{N}}$, which can be instantiated for these five different curves using the values indicated in Table 4.2 on Page 109.

The RFC mandates that implementations abort if the Diffie-Hellman shared secret is the point at infinity for P-256, P-384, and P-521, or the all-zero value for Curve25519 and Curve448. The security notions in this work do not contain this check, and the theorems are valid for both implementa-

[Alw+] Alwen et al., Analysing the HPKE Standard Supplementary Material
tions that do or do not contain it (this is because the properties we prove are not concerned about contributiveness). More formally, the adversary could check for all public keys leading to problematic Diffie-Hellman shared secrets before calling the oracles in our security games.

At the end of this section, we sketch the attack against the Insider-Auth security.

**Theorem 4.7** (Outsider-CCA security of DH-AKEM). Let $\mathcal{N}$ be a randomisable nominal group. Under the GDH assumption in $\mathcal{N}$ and modelling KDF as a random oracle, DH-AKEM[$\mathcal{N}$, KDF] is Outsider-CCA secure. In particular, for any adversary $\mathcal{A}$ against $(n, q_e, q_d)$-Outsider-CCA security of DH-AKEM[$\mathcal{N}$, KDF] that issues at most $q_h$ queries to the random oracle KDF, there exists an adversary $\mathcal{B}$ against GDH such that

$$ \mathrm{Adv}_{\mathcal{A}, \mathrm{DH-AKEM}[\mathcal{N}, \mathrm{KDF}]}^{(n,q_e,q_d)-\mathrm{Outsider-CCA}} \le \mathrm{Adv}_{B, \mathcal{N}}^{\mathrm{GDH}} + (n+q_e) \cdot \Delta_{\mathcal{N}} + (q_e q_d + 2nq_e + 10q_e^2 + 11n^2) \cdot P_{\mathcal{N}} $$

$\mathcal{B}$ issues $5q_h$ queries to the DH oracle, and $t_B \approx t_A$.

*Proof.* This proof is mechanized using the tool CryptoVerif. We give to the tool the assumptions that $\mathcal{N}$ is a nominal group that satisfies the GDH assumption, formalized by Definition 4.7 and Theorem 4.1, and that KDF is a random oracle. We also give the definition of DH-AKEM, and ask it to show that the games $(n, q_e, q_d)$-Outsider-CCA$_\ell$ and $(n, q_e, q_d)$-Outsider-CCA$_r$ are computationally indistinguishable. In the particular case of DH-AKEM, these two games include an additional oracle: the random oracle KDF. The theorem, the initial game definitions, and the proof indications are available in the file dhkem.auth.outsider-cca-lr.ocv [Alw+].

The proof proceeds by transforming the game $(n, q_e, q_d)$-Outsider-CCA$_\ell$ by several steps into a game $G_{\mathrm{final}}$ and the game $(n, q_e, q_d)$-Outsider-CCA$_r$ into the same game $G_{\mathrm{final}}$. Since all transformation steps performed by CryptoVerif are designed to preserve computational indistinguishability, we obtain that $(n, q_e, q_d)$-Outsider-CCA$_\ell$ and $(n, q_e, q_d)$-Outsider-CCA$_r$ are computationally indistinguishable. We guide the transformations with the following main steps.

Starting from $(n, q_e, q_d)$-Outsider-CCA$_\ell$, in the oracle AENCAP, we first distinguish whether the provided public key pk is honest, by testing whether $pk = pk_i$ for some $i$ (a test that appears in $(n, q_e, q_d)$-Outsider-CCA$_r$). We rename some variables to give them different names when $pk \in \{pk_1, \dots, pk_n\}$ and when $pk \notin \{pk_1, \dots, pk_n\}$, to facilitate future game transformations. In the oracle ADECAP, we test whether $\exists K : (pk, pk_j, c, K) \in \mathcal{E}$, which corresponds to a test done in $(n, q_e, q_d)$-Outsider-CCA$_r$. Furthermore, when this test succeeds, we replace the result normally returned by ADECAP, AuthDecap(sk$_j$, pk, c) with the key K found in $\mathcal{E}$. CryptoVerif shows that this replacement does not modify the result, which corresponds to the correctness of DH-AKEM. In the random oracle, we distinguish whether the argument received from the adversary has a format that matches the one used by DH-AKEM or not. Only when the format matches, this argument may coincide with a call to the hash oracle made from DH-AKEM. Next, we apply the random oracle assumption. Each call to the random oracle is

<footnote>[Alw+] Alwen et al., Analysing the HPKE Standard Supplementary Material</footnote>
replaced with the following test: if the argument is equal to the argument of a previous call, we return the previous result; otherwise, we return a fresh random value. Finally, we apply the GDH assumption, which allows us to show that some comparisons between Diffie-Hellman values are false. In particular, CryptoVerif shows that the arguments of calls to the random oracle coming from AENCAP with pk ∈ {pk₁, ..., pkₙ} cannot coincide with arguments of other calls. Hence, they return a fresh random key, as in (n, q_e, q_d)-Outsider-CCA_r.

Starting from (n, q_e, q_d)-Outsider-CCA_r, in the random oracle, we distinguish whether the argument received from the adversary has a format that matches the one used by DH-AKEM or not. Next, we apply the random oracle assumption, as we did on the left-hand side.

The transformed games obtained respectively from (n, q_e, q_d)-Outsider-CCA_ℓ and from (n, q_e, q_d)-Outsider-CCA_r are then equal, which concludes the proof.

CryptoVerif computes the bound on the probability of distinguishing the games (n, q_e, q_d)-Outsider-CCA_ℓ and (n, q_e, q_d)-Outsider-CCA_r by adding bounds computed at each transformation step. During this proof, CryptoVerif automatically eliminates unlikely collisions, in particular between public Diffie-Hellman keys. By default, CryptoVerif eliminates these collisions aggressively, even when that is not required for the proof to succeed, which results in a large probability bound. To avoid that, we allow the tool to eliminate collisions of probability P_N times a power 4 in n, q_e^per user, and q_d^per user, where q_e^per user and q_d^per user are the number of AENCAP and ADECAP queries respectively, per user. But we do not allow eliminating collisions with more than a power 4 in n, q_e^per user, and q_d^per user, nor collisions that involve q_h.
□

**Theorem 4.8 (Insider-CCA security of DH-AKEM).** Let $\mathcal{N}$ be a rerandomisable nominal group. Under the GDH assumption in $\mathcal{N}$ and modelling KDF as a random oracle, DH-AKEM[$\mathcal{N}$, KDF] is Insider-CCA secure. In particular, for any $(n, q_e, q_d, q_c)$-Insider-CCA adversary $\mathcal{A}$ against DH-AKEM[$\mathcal{N}$] that issues at most $q_h$ queries to the random oracle, there exists an adversary $\mathcal{B}$ against GDH such that

$$ \text{Adv}_{\mathcal{A}, \text{DH-AKEM}[\mathcal{N}, \text{KDF}]}^{(n,q_e,q_d,q_c)\text{-Insider-CCA}} \le \text{Adv}_{\mathcal{B}, \mathcal{N}}^{\text{GDH}} + (n+q_c) \cdot \Delta_{\mathcal{N}} \\ + (q_c q_d + 4q_c q_e + 2nq_e + 10q_e^2 + 3q_c^2 + 9n^2) \cdot P_{\mathcal{N}} $$

$\mathcal{B}$ makes 5$q_h$ queries to the DH oracle, and $t_B \approx t_A$.

**Theorem 4.9 (Outsider-Auth security of DH-AKEM).** Let $\mathcal{N}$ be a rerandomisable nominal group. Under the sqGDH assumption in $\mathcal{N}$ and modelling KDF as a random oracle, DH-AKEM[$\mathcal{N}$, KDF] is Outsider-Auth secure. In particular, for any $(n, q_e, q_d)$-Outsider-Auth adversary $\mathcal{A}$ against DH-AKEM[$\mathcal{N}$] that issues at most $q_h$ queries to the random oracle, there exists an adversary $\mathcal{B}$ against sqGDH such that

$$ \text{Adv}_{\mathcal{A}, \text{DH-AKEM}[\mathcal{N}, \text{KDF}]}^{(n,q_e,q_d)\text{-Outsider-Auth}} \le 2\text{Adv}_{\mathcal{B}, \mathcal{N}}^{\text{sqGDH}} + 2(n+q_e) \cdot \Delta_{\mathcal{N}} \\ + (2q_e q_d + 4nq_d + 16q_e^2 + 4nq_e + 12n^2) \cdot P_{\mathcal{N}} $$

$\mathcal{B}$ issues 7$q_h$ queries to the DH oracle, and $t_B \approx t_A$.
**INFEASIBILITY OF Insider-Auth SECURITY.** As for APKE, we could define an Insider-Auth security notion for AKEM, which precludes forgeries even when the receiver key pair is dishonest, provided the sender key pair is honest. However, the DH-AKEM construction does not even achieve KCI security, a relaxation of Insider-Auth security only precluding forgeries for leaked, but still honestly generated, receiver key pairs. Indeed, in DH-AKEM, knowledge of an arbitrary receiver secret key is already sufficient to compute the Diffie-Hellman shared key for any sender public key. Thus, in a KCI attack, an adversary that learns a target receiver's keys can trivially produce a KEM ciphertext and corresponding encapsulated key for any target sender public key.

### 4.6.2 HPKE's Key Schedule and Key Derivation Function

HPKE's key schedule $KS_{Auth}$ and key derivation function $HKDF_N$ are both instantiated via the functions Extract and Expand which are defined below. We proceed to prove a theorem that $KS_{Auth}$ is a PRF, as needed for the composition results presented in Theorems 4.3 to 4.5. Then, we argue why $HKDF_N$ can be modelled as a random oracle, as assumed by Theorems 4.7 to 4.9 on DH-AKEM. Finally, we indicate how the entire $HPKE_{Auth}$ scheme is assembled from the individual building blocks presented in the previous sections.

**Extract AND Expand.** The RFC defines two functions Extract and Expand as follows.

* Extract(salt, IKM) is a function keyed by a bitstring salt, with input keying material IKM as parameter, and returns a bitstring of fixed length $N_h$ bits.

* Expand(PRK, info, L) is a function keyed by PRK, with an arbitrary bitstring info and a length L as parameters, and returns a bitstring of length L.

In Theorem 4.10, we assume that Extract and Expand are PRFs with the first parameter being the PRF key. HPKE instantiates Extract and Expand with HMAC-SHA-2, for which the PRF assumption is justified by [Bel15; BCK96]. (Generally, HPKE's instantiation of Expand uses HMAC iteratively to achieve the variable output length L. However, all values L used in HPKE are less or equal than the output length of one HMAC call.) We also assume that Extract is collision resistant, provided its keys are not larger than blocks of SHA-2, which is needed to avoid that the keys be hashed before computing HMAC, and true in HPKE. This property is immediate from the collision resistance of SHA-2, studied in [GH04].

**KEY SCHEDULE.** The key schedule $KS_{Auth}$ serves as a bridging step between the AKEM and the AEAD of APKE. The computations done by $KS_{Auth}$ are as indicated in Listing 4.11. The function KeySchedule used internally is the common key schedule function that the RFC defines for all modes. In $HPKE_{Auth}$, the mode parameter is set to the constant one-byte value 0x02 identifying the mode Auth. Similarly, mode Auth does not use a pre-shared key, so the psk parameter is always set to the empty string empty, and the value psk_id that is identifying which pre-shared key is used, is equally set

<footnote>[Bel15] Bellare, "New Proofs for NMAC and HMAC: Security without Collision Resistance"</footnote>

<footnote>[BCK96] Bellare et al., "Keying Hash Functions for Message Authentication"</footnote>

<footnote>[GH04] Gilbert and Handschuh, "Security Analysis of SHA-256 and Sisters"</footnote>
<caption>Listing 4.11: The key schedule KS<sub>Auth</sub> used in HPKE<sub>Auth</sub> [Bar+22].</caption>

```
KSAuth(kPRF, info)
    01     return KeySchedule(kPRF, 0x02, info, empty, empty)

KeySchedule(kPRF, mode, info, psk, psk_id)
    02     context ← mode ||
                LabeledExtract empty, "psk_id_hash", psk_id) ||
                LabeledExtract empty, "info_hash", info)
    03     secret ← LabeledExtract(kPRF, "secret", psk)
    04     k ← LabeledExpand(secret, "key", context, Nk)
    05     nonce ← LabeledExpand(secret, "base Nonce", context, Nn)
    06     return (k, nonce)

LabeledExtract(salt, label, IKM')
    07     return Extract(salt, "HPKE-v1" || suiteid || label || IKM')

LabeledExpand(PRK, label, context, L)
    08     return Expand(PRK, Encode(L) || "HPKE-v1" || suiteid || label || context, L)
```

to empty. The RFC defines LabeledExtract and LabeledExpand as wrappers around Extract and Expand, for domain separation and context binding. The value `suiteid` is a 10-byte string identifying the ciphersuite, composed as a concatenation of the string "HPKE", and two-byte identifiers of the KEM, the KDF, and the AEAD algorithm in use. The bitstring `Encode(L)` is the two-byte encoding of the length L expressed in bytes. The values $N_k$ and $N_n$ indicate the length of the AEAD key and nonce.

The composition results established by Theorems 4.3 to 4.5 assume that KS<sub>Auth</sub> is a PRF. The following theorem proves this property for HPKE<sub>Auth</sub>'s instantiation of KS<sub>Auth</sub>.

**Theorem 4.10** (Extract CR + Extract PRF + Expand PRF $\Rightarrow$ KS<sub>Auth</sub> PRF). Assuming that Extract is a collision-resistant hash function for calls with the labels "psk_id_hash" and "info_hash", that Extract is a PRF for calls with the label "secret", and that Expand is a PRF, it follows that KS<sub>Auth</sub> is a PRF.

In particular, for any $(n_k, q_{PRF})$-PRF adversary $\mathcal{A}$ against KS<sub>Auth</sub>, there exist an adversary $\mathcal{B}$ against the collision resistance of Extract, a $(n_k, n_k)$-PRF adversary $\mathcal{C}_1$ against Extract, and a $(n_k, 2q_{PRF})$-PRF adversary $\mathcal{C}_2$ against Expand such that $t_B \approx t_A$, $t_{C_1} \approx t_A$, $t_{C_2} \approx t_A$, and

$$ \mathrm{Adv}_{\mathcal{A}, \mathrm{KS}_{\mathrm{Auth}}}^{(n_k, q_{\mathrm{PRF}})-\mathrm{PRF}} \le \mathrm{Adv}_{\mathcal{B}, \mathrm{Extract}}^{\mathrm{CR}} + \mathrm{Adv}_{\mathcal{C}_1, \mathrm{Extract}}^{(n_k, n_k)-\mathrm{PRF}} + \mathrm{Adv}_{\mathcal{C}_2, \mathrm{Expand}}^{(n_k, 2q_{\mathrm{PRF}})-\mathrm{PRF}} $$

This theorem is proven by CryptoVerif in keyschedule.auth.prf.ocv [Alw+].

THE KEY DERIVATION FUNCTION KDF IN DH-AKEM. The AKEM instantiation DH-AKEM as we defined it in Listing 4.10 uses a function KDF to derive the KEM shared secret. In HPKE<sub>Auth</sub>, this function is instantiated by HKDF<sub>N</sub>, as defined in Listing 4.12, using the above-defined Extract and Expand internally. The output length N corresponds to N<sub>secret</sub> in the RFC.

<footnote>[Alw+] Alwen et al., Analysing the HPKE Standard Supplementary Material</footnote>
<caption>Listing 4.12: Function HKDF<sub>N</sub> [Extract, Expand] as used in HPKE<sub>Auth</sub>.</caption>

HKDF<sub>N</sub>(salt, IKM, info)
01 PRK ← Extract(salt, IKM)
02 return Expand(PRK, info, N)

In the analysis of the key schedule presented above, we assume that Extract and Expand are pseudo-random functions. However, this assumption would not be sufficient to prove the security of DH-AKEM: the random oracle model is required. The simplest choice is to assume that the whole key derivation function KDF = HKDF<sub>N</sub> is a random oracle, as we do in Theorems 4.7 to 4.9. (Alternatively, we could probably rely on some variant of the PRF-ODH assumption [Bre+17]. While in principle the PRF-ODH assumption is weaker than the random oracle model, Brendel, Fischlin, Günther, and Janson [Bre+17] show that it is implausible to instantiate the PRF-ODH assumption without a random oracle, so that would not make a major difference.) The invocations of Extract and Expand in DH-AKEM and KS<sub>Auth</sub> use different labels for domain separation, so choosing different assumptions is sound. Next, we further justify the random oracle assumption for HKDF<sub>N</sub>.

As mentioned at the beginning of Section 4.6, HPKE instantiates Extract and Expand with HMAC [KBC97], which makes HKDF<sub>N</sub> exactly the widely-used HKDF key derivation function [KE10]. HPKE specifies SHA-2 as the hash function underlying HMAC. Lemma 3.9 in Chapter 3 shows that HKDF is indifferentiable from a random oracle under the following assumptions<sup>3</sup>: (1) HMAC is indifferentiable from a random oracle. For HMAC-SHA-2, this is justified by Theorem 4.4 in the full version of [Dod+12] assuming the compression function underlying SHA-2 is a random oracle. The theorem's restriction on HMAC's key size is fulfilled, because DH-AKEM uses either the empty string, or a bitstring of hash output length as key. (2) Values of IKM do not collide with values of info || 0x01. This is guaranteed by the prefix "HPKE-v1" of IKM, which is used as a prefix for info as well, but shifted by two characters, because the two-byte encoding of the length N comes before it. The shared secret lengths N<sub>secret</sub> specified in the RFC correspond exactly to the output length of the hash function; this means there is only one internal call to Expand, and thus we do not need to consider collisions of IKM with the input to later HMAC calls.

### 4.6.3 HPKE's APKE Scheme HPKE<sub>Auth</sub>

Let $HPKE_{Auth} := APKE[DH-AKEM[\mathcal{N}, HKDF_N], KS_{Auth}, AEAD]$ be the construction of APKE obtained by applying the black-box AKEM/DEM composition of Listing 4.8 to the DH-AKEM[\mathcal{N}, HKDF_N] authenticated KEM (Listing 4.10), where \mathcal{N} is a rerandomisable nominal group. For the key schedule of $HPKE_{Auth}$ we use $KS_{Auth}$ of Listing 4.11 and for the key derivation function we use $HKDF_N$ of Listing 4.12. For both $KS_{Auth}$ and $HKDF_N$ we implement the Extract and Expand functions using HMAC (as described in the HPKE specification). Finally, we instantiate HMAC using one of the SHA2 family of hash functions. (Which one depends on the target bit security

[Bre+17] Brendel et al., "PRF-ODH: Relations, Instantiations, and Impossibility Results"

[KBC97] Krawczyk et al., HMAC: Keyed-Hashing for Message Authentication

[KE10] Krawczyk and Eronen, HMAC-based Extract-and-Expand Key Derivation Function (HKDF)

[Dod+12] Dodis et al., "To Hash or Not to Hash Again? (In)Differentiability Results for $H^2$ and HMAC"

<footnote n="3">³The exact probability bound is indicated in Lemma 8 of that paper's full version.</footnote>
of HPKE<sub>Auth</sub>, as we discuss below.)

The AKEM/DEM composition Theorems 4.3 to 4.5, together with Theorem 4.10 on the key schedule KS<sub>Auth</sub>, and Theorems 4.7 to 4.9 on DH-AKEM's security, and P<sub>DH-AKEM</sub> = P<sub>N</sub> provide the following concrete security bounds for HPKE<sub>Auth</sub>. For simplicity, we ignore all constants and set q := q<sub>e</sub> + q<sub>d</sub> + q<sub>c</sub>.

$$
\begin{align*}
\mathrm{Adv}_{\mathcal{A}, \mathrm{HPKE}_{\mathrm{Auth}}}^{(n,q_e,q_d,q_c)\text{-Outsider-CCA}} &\le \mathrm{Adv}_{B_1, \mathcal{N}}^{\mathrm{GDH}} + (n+q)^2 \cdot P_{\mathcal{N}} + (n+q) \cdot \Delta_{\mathcal{N}} \\
&\phantom{\le} + \mathrm{Adv}_{C, \mathrm{KS}_{\mathrm{Auth}}}^{(q,q)\text{-PRF}} + \mathrm{Adv}_{D_1, \mathrm{AEAD}}^{q\text{-IND-CPA}} + \mathrm{Adv}_{D_2, \mathrm{AEAD}}^{(q,q)\text{-INT-CTXT}} \\
\mathrm{Adv}_{\mathcal{A}, \mathrm{HPKE}_{\mathrm{Auth}}}^{(n,q_e,q_d)\text{-Outsider-Auth}} &\le \mathrm{Adv}_{B_1, \mathcal{N}}^{\mathrm{GDH}} + \mathrm{Adv}_{B_2, \mathcal{N}}^{\mathrm{sqGDH}} + (n+q)^2 \cdot P_{\mathcal{N}} + (n+q) \cdot \Delta_{\mathcal{N}} \\
&\phantom{\le} + \mathrm{Adv}_{C, \mathrm{KS}_{\mathrm{Auth}}}^{(q,q)\text{-PRF}} + \mathrm{Adv}_{D_1, \mathrm{AEAD}}^{(q,q)\text{-INT-CTXT}}.
\end{align*}
$$

The bound for Insider-CCA is the same as the one for Outsider-CCA. In all bounds, we have $\mathrm{Adv}_{C,KS_{\mathrm{Auth}}}^{(q,q)-\mathrm{PRF}} \le \mathrm{Adv}_{C_1,Extract}^{\mathrm{CR}} + \mathrm{Adv}_{C_2,Extract}^{(q,q)-\mathrm{PRF}} + \mathrm{Adv}_{C_3,Expand}^{(q,q)-\mathrm{PRF}}$. Moreover, the adversaries $B_1, B_2, C, D_1, D_2$ have (roughly) the same running time as $A$.

PARAMETER CHOICES OF HPKE<sub>Auth</sub>. The HPKE standard allows different choices of rerandomisable nominal groups $\mathcal{N}$ to obtain a concrete instance of HPKE<sub>Auth</sub>, that lead to different bounds on the statistical parameters $P_{\mathcal{N}}$ and $\Delta_{\mathcal{N}}$. The standard also fixes the length $N$ of the KEM keyspace, c.f. Table 4.2. Even though lengths are expressed in bytes in the RFC and the implementation, we express them in bits in this section as this is more convenient to discuss the number of bits of security.

All concrete instances of HPKE<sub>Auth</sub> proposed by the HPKE standard build Extract and Expand from HMAC which, in turn, uses a hash function. HPKE proposes several concrete hash functions (all in the SHA2 family). For our security bounds, the relevant consequence of choosing a particular hash function is the resulting key length $N_h$ of Expand when used as a PRF, c.f. Table 4.3.

Finally, to instantiate HPKE<sub>Auth</sub>, we must also specify the AEAD scheme. HPKE allows for several choices which affect the AEAD key length $N_k$, nonces length $N_n$, and tag length $N_t$, c.f. Table 4.4.

DISCUSSION. We say that an instance of HPKE<sub>Auth</sub> achieves $\kappa$ bits of security if the success ratio $\mathrm{Adv}_{\mathcal{A},\mathrm{HPKE}_{\mathrm{Auth}}}/t_{\mathcal{A}}$ is upper bounded by $2^{-\kappa}$ for any adversary $\mathcal{A}$ with runtime $t_{\mathcal{A}} \le 2^{\kappa}$. In particular, we say that a term $\varepsilon$ has $\kappa$ bits of security if $\varepsilon/t_{\mathcal{A}} \le 2^{-\kappa}$. We discuss the implications of our results for the bit security of the various instances of HPKE<sub>Auth</sub> proposed by the standard.

The runtime $t_{\mathcal{A}}$ of any adversary $\mathcal{A}$ in an APKE security game is lower-bounded by $n+q$, since the adversary needs $n$ steps to parse the $n$ public keys and additional $q$ steps to make the oracle queries. We assume that $t_{\mathcal{A}} \le 2^{\kappa}$, where $\kappa$ is the target security level.

We now estimate the security level supported by each term in $\mathrm{Adv}_{\mathcal{A},\mathrm{HPKE}_{\mathrm{Auth}}}$.

* Term $\mathrm{Adv}_{B_1, \mathcal{N}}^{\mathrm{GDH}}$. Rerandomisable nominal groups $\mathcal{N}$ proposed for use by the HPKE standard were designed to provide $\kappa_{\mathcal{N}}$ bits of security (c.f. Table 4.2). That is, we assume that $\mathrm{Adv}_{B_1, \mathcal{N}}^{\mathrm{GDH}}/t_{B_1} \le 2^{-\kappa_{\mathcal{N}}}$. Since $t_{\mathcal{A}} \approx t_{B_1}$, we conclude that this term has $\kappa_{\mathcal{N}}$ bits of security. The same arguments hold for $\mathrm{Adv}_{B_2, \mathcal{N}}^{\mathrm{sqGDH}}$.

* Term $(n+q)^2 \cdot P_{\mathcal{N}}$. Let us show that this term also has $\kappa_{\mathcal{N}}$ bits of security. We have $n+q \le t_{\mathcal{A}}$. Thus, it suffices to show that $(n+q) \cdot P_{\mathcal{N}} \le 2^{-\kappa_{\mathcal{N}}}$.
<table><caption>TABLE 4.2: Parameters of DH-AKEM[$\mathcal{N}$, HKDF$_N$] depending on the choice of the rerandomizable nominal group $\mathcal{N}$.</caption><thead><tr><th></th><th>P-256</th><th>P-384</th><th>P-521</th><th>Curve25519</th><th>Curve448</th></tr></thead><tbody><tr><td>Security level $\kappa_N$ (bits)</td><td>128</td><td>192</td><td>256</td><td>128</td><td>224</td></tr><tr><td>$P_N \le$</td><td>$2^{-255}$</td><td>$2^{-383}$</td><td>$2^{-520}$</td><td>$2^{-250}$</td><td>$2^{-444}$</td></tr><tr><td>$\Delta_N \le$</td><td>0</td><td>0</td><td>0</td><td>$2^{-126}$</td><td>$2^{-221}$</td></tr><tr><td>KEM keyspace $N$ (bits)</td><td>256</td><td>384</td><td>512</td><td>256</td><td>512</td></tr></tbody></table>

<table><caption>TABLE 4.3: Choices of HMAC and the PRF key lengths of Expand, instantiated with HMAC.</caption><thead><tr><th></th><th>HMAC- SHA256</th><th>HMAC- SHA384</th><th>HMAC- SHA512</th></tr></thead><tbody><tr><td>PRF key length $N_h$ of Expand (bits)</td><td>256</td><td>384</td><td>512</td></tr></tbody></table>

<table><caption>TABLE 4.4: Choices of the AEAD scheme and their parameters.</caption><thead><tr><th></th><th>AES-128- GCM</th><th>AES-256- GCM</th><th>ChaCha20- Poly1305</th></tr></thead><tbody><tr><td>AEAD key length $N_k$ (bits)</td><td>128</td><td>256</td><td>256</td></tr><tr><td>AEAD nonces length $N_n$ (bits)</td><td>96</td><td>96</td><td>96</td></tr><tr><td>AEAD tag length $N_t$ (bits)</td><td>128</td><td>128</td><td>128</td></tr></tbody></table>

Since $t_A \le 2^{\kappa_N}$, we get that $(n+q) \le 2^{\kappa_N}$. The statement now follows as, according to Table 4.2, $P_N \le 2^{-2\kappa_N}$.

* Term $(n+q) \cdot \Delta_N$. Let us show that this term also has $\kappa_N$ bits of security. For all NIST curves, we have $\Delta_N = 0$ trivially implying the statement. In contrast, for Curve25519 and Curve448, $\Delta_N \le 2^{-\kappa_N}$, so $(n+q) \cdot \Delta_N \approx (n+q) \cdot 2^{-\kappa_N}$. As $n+q \le t_A$, the statement also holds for these curves.

* Term $\text{Adv}_{C_1, \text{Extract}}^{\text{CR}}$. The output length $N_h$ of the concrete hash functions are listed in Table 4.3. Since the generic bound on collision resistance is $t_C^2/2^{N_h}$, this term has $N_h/2$ bits of security.

* Term $\text{Adv}_{C_3, \text{Expand}}^{(q,q)-\text{PRF}}$. The PRF key lengths $N_h$ of Expand are specified in Table 4.3. Modelling the PRF as a random oracle, we have $\text{Adv}_{C_3, \text{Expand}}^{(q,q)-\text{PRF}} \le q^2/2^{N_h}$. So this term also has $N_h/2$ bits of security.

* Term $\text{Adv}_{C_2, \text{Extract}}^{(q,q)-\text{PRF}}$. The PRF key length $N$ of Extract is specified in Table 4.2. By the same argument as for the previous term, this term has $N/2$ bits of security. Since $N/2 \ge \kappa_N$ by Table 4.2, this term has $\kappa_N$ bits of security.

* Terms $\text{Adv}_{D_1, \text{AEAD}}^{q-\text{IND-CPA}} + \text{Adv}_{D_2, \text{AEAD}}^{(q,q)-\text{INT-CTXT}}$. The terms refer to the multi-key security of the AEAD schemes (c.f. Section 4.3), studied for instance in [BT16]. However, the current results are not sufficient to guarantee the expected security level, such as 128 bits for AES-128-GCM. We recommend further research to study the exact bounds of the terms instantiated with the AEAD schemes from Table 4.4. In any case a simple key/nonce-collision attack has success probability

<footnote>[BT16] Bellare and Tackmann, “The Multi-user Security of Authenticated Encryption: AES-GCM in TLS 1.3”</footnote>
$\text{Adv}_{D_1,AEAD}^{q\text{-IND-CPA}} = q^2/2^{N_k+N_n}$, where $N_k$ is the AEAD key length and $N_n$ is the nonce length. A simple computation shows that this term has at most $N_k$ bits of security (assuming $q \le 2^{N_n}$). Moreover, a simple attack against INT-CTXT by guessing the authentication tag has success probability $\text{Adv}_{D_2,AEAD}^{(q,q)\text{-INT-CTXT}} = q/2^{N_t}$, where $N_t$ is the length of the authentication tag. Hence, this term has at most $N_t$ bits of security. Assuming these attacks also serve as an upper bound, these terms would have $\min(N_k, N_t)$ bits of security if $q \le 2^{N_n}$. Since for all AEAD schemes of Table 4.4, we have $N_t = 128$ bits, that limits the security level of HPKE to 128 bits.

To sum up, the analysis above suggests that HPKE has about $\kappa = \min(\kappa_N, N_h/2, N_k, N_t)$ bits of security, under the assumption that $t_A \le 2^\kappa$ and $q \le 2^{N_n}$. Since the tag length of the AEAD is $N_t = 128$ bits, we obtain $\kappa = 128$ bits; a greater security level could be obtained by using AEADs with longer tags. More research on the multi-key security of AEAD schemes is still needed to confirm this analysis.

**ACKNOWLEDGEMENTS.** The authors would like to thank the HPKE RFC co-authors Richard Barnes, Karthikeyan Bhargavan, and Christopher Wood for fruitful discussions during the preparation of this work. The authors also thank Pierre Boutry and Christian Doczkal for very helpful feedback on a previous version of this work.

Bruno Blanchet was supported by ANR TECAP (decision number ANR-17-CE39-0004-03). Eduard Hauck was supported by the DFG SPP 1736 Big Data. Eike Kiltz was supported by the BMBF iBlockchain project, the EU H2020 PROMETHEUS project 780701, the DFG SPP 1736 Big Data, and the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) under Germany's Excellence Strategy - EXC 2092 CASA - 390781972. Benjamin Lipp was supported by ERC CIRCUS (grant agreement no. 683032) and ANR TECAP (decision number ANR-17-CE39-0004-03). Doreen Riepel was funded by the DFG under Germany's Excellence Strategy - EXC 2092 CASA - 390781972.
<figure><img src="image_28.png" /></figure>
# 5

## The Hybrid Public Key Encryption Standard

This chapter gives an overview of our other involvements in analysis, development, and implementation of the HPKE standard. Section 5.1 presents a preliminary analysis done in CryptoVerif before the detailed work on $HPKE_{Auth}$, presented in Chapter 4, was started. Section 5.2.5 describes an implementation of HPKE in the F* programming language. Section 5.2 gives insights about how the two analyses and the implementation influenced the HPKE standard.

### 5.1 AN ANALYSIS OF ALL HPKE MODES

This section is based on the preprint "An Analysis of Hybrid Public Key Encryption" [Lip20] that presents a preliminary analysis of all modes of HPKE using CryptoVerif. More precisely, it proves asymptotic cryptographic guarantees for the single-shot encryption and the secret export interfaces of all modes. The analysis looks at the HPKE construction as a whole, without decomposing it into its KEM and DEM building blocks like the analysis presented in Chapter 4. It was started at a time when the HPKE standard was still at an early stage, at Draft 2 of overall 12 drafts that it went through. For this reason, we start by laying out how the cryptographic dependencies and algorithm definitions differ from the version analysed in Chapter 4. From a cryptographic point-of-view, the version analyzed in Chapter 4 is the final version. Changes in later drafts did not concern the protocol.

[Lip20] Lipp, *An Analysis of Hybrid Public Key Encryption*

#### 5.1.1 Hybrid Public Key Encryption at Draft 2

In Draft 2, the KEM and the KeySchedule function were defined differently than in the final version. The most significant changes were made to them in Draft 3 as a result of feedback we provided to the authors of the standard. This is described in more detail in Section 5.2.

**KEY ENCAPSULATION MECHANISM (KEM).** Similarly to how the Authenticated KEM is defined in *Definition 4.9*, HPKE Draft 2 uses a standard KEM for $HPKE_{Base}$ and $HPKE_{PSK}$. A KEM consists of a tuple of algorithms (Gen, Encap, Decap):

* Gen is the same as in *Definition 4.9*.
* Encap takes as input a receiver public key pk, and outputs an encapsulation c and a shared secret $K \in \mathcal{K}$.

* Deterministic Decap takes as input a receiver secret key sk and an encapsulation c, and outputs a shared key $K \in \mathcal{K}$.

Similarly to the authenticated variant, we require that for all $(sk, pk) \in \text{Gen}$

$$ (c, K) \stackrel{s}{\leftarrow} \text{Encap}(pk) \qquad [\text{Decap}(sk, c) = K] = 1. $$

The sets of secret and public keys $SK$ and $PK$, the projection function $\mu$, and the key collision probability are the same as for the authenticated variant, as both use the same key generation algorithm.

In this analysis, we focus on the instantiation by the Diffie-Hellman-based KEM defined in the HPKE standard. We recall how Encap and AuthEncap were defined at the time of Draft 2:

* Encap(pkR): Given input pkR, output a ciphertext enc of size $N_{enc}$ bytes and shared key zz of size $N_{pk}$ bytes:

$$ (skE, pkE) \leftarrow_s \text{Gen}() $$

$$ \mathit{zz} \leftarrow \mathit{pkR}^{\mathit{skE}} $$

$$ \text{enc} \leftarrow \text{pkE} $$

* AuthEncap(pkR, skS): Given input pkR and skS, output a ciphertext enc of size $N_{enc}$ bytes and shared key zz of size $2N_{pk}$ bytes:

$$ (skE, pkE) \leftarrow_s \text{Gen}() $$

$$ \mathit{zz} \leftarrow \mathit{pkR}^{\mathit{skE}} \parallel \mathit{pkR}^{\mathit{skS}} $$

$$ \text{enc} \leftarrow \text{pkE} $$

The most notable difference to the final version is that the Diffie-Hellman shared secret is directly used as KEM shared secret, and not first processed by a key derivation function. The consequences of this are discussed in Section 5.2.

### HASH FUNCTION AND KEY DERIVATION FUNCTION (KDF)

HPKE Draft 2 defined a KDF as a tuple of deterministic algorithms (Hash, Extract, Expand) used for secret derivation and expansion. The functions Extract and Expand are defined as in Section 4.6.2. Hash($m$) is defined as a function taking a bitstring $m$ as parameter and returning its hash of length $N_h$ bits. The difference of Draft 2 compared to the final version is how these functions are used. The final version does not use any Hash function directly, and it uses Extract and Expand only via labeled wrappers. We will see this in the definition of the KeySchedule function, shortly.

### KEY SCHEDULE

The KeySchedule function is defined as follows, where $\mathit{zz}$ and $\text{enc}$ are the shared secret and the ciphertext returned by the KEM, and pkR and pkS are the receiver and sender public keys. The other parameters are as in the final version.
KeySchedule(zz, enc, mode, pkR, info, psk, psk_id, pkS):

ciphersuite ← kem_id || kdf_id || aead_id

psk_id_hash ← Hash(psk_id)

info_hash ← Hash(info)

ctx ← mode || ciphersuite || enc || pkR || pkS || psk_id_hash || info_hash

s ← Extract(psk, zz)

k ← Expand(s, “hpke key” || ctx, N_k)

n ← Expand(s, “hpke nonce” || ctx, N_n)

s_exp ← Expand(s, “hpke exp” || ctx, N_h)

In the Base and Auth modes, psk and psk_id are set to all-zero default values. In the Base and PSK modes, pkS is set to an all-zero default value. The values kem_id, kdf_id, and aead_id are 2-byte identifiers of the algorithm in use, respectively. The key schedule function returns an encryption context containing the symmetric key k, nonce n, and the exporter secret s_exp. This encryption context can then be used to call the encryption and secret export interfaces.

The differences to the final version of the KeySchedule are: the hash function is used directly on psk_id and info; the context bitstring includes enc, pkR, and pkS, which have been moved into the context of the KEM key derivation in the final version; Extract and Expand are used instead of LabeledExtract and LabeledExpand.

AEAD. Authenticated Encryption with Additional Data is defined as in Definition 4.3, there is no difference to the final version.

APPLICATION INTERFACE. The encryption function exposed by the single-shot encryption interface is defined as follows:

Context.Seal(aad, pt):

ct ← AEAD.Enc(k, pt, aad, n)

Here, pt is the plaintext, and aad the additional data that is authenticated by the AEAD. The interface uses the values from the encryption context.

The secret export interface takes as input a context string ctx and a desired length L in bytes and produces a secret derived from the internal exporter secret using the Expand function of the KDF:

Context/exporter ctx, L):

k_exp ← Expand(s_exp, “exp key” || ctx, L)

5.1.2 Analysis

STRUCTURE OF THE SECURITY GAME. In this analysis, we prove a two-user security notion for HPKE. In the setup of the game, we create key pairs (skS, pkS), (skR, pkR) and a pre-shared key psk for two honest users S and
R, and sample a secret bit b. Then, we give the adversary access to an encryption and a decryption oracle that can be called $q_e$ and $q_d$ times.

The encryption oracle acts as user S and takes a receiver public key, two plaintexts $p_0, p_1$ of same length, and additional data aad as parameter. Internally, the oracle prepares an HPKE encryption context for the appropriate mode, using the receiver public key provided by the adversary. It always uses the honest sender private key and pre-shared key, in the relevant modes, respectively. Then, it encrypts $p_b$ using the encryption interface and exports two secrets using the secret export interface, with two different but constant contexts. Finally, the oracle returns the KEM and the AEAD ciphertext and the two exported secrets.

The decryption oracle acts as user R and takes a KEM and an AEAD ciphertext and additional data aad as parameter and returns whether the decryption was successful. Internally, it prepares an HPKE encryption context using the honest receiver R's private key, honest sender S's public key, and their pre-shared key, depending on the mode.

Depending on the mode, we give the adversary access to oracles that leak the private keys and the pre-shared key of S and R. We do not allow compromise scenarios that would trivially break secrecy. In $HPKE_{Base}$, we do not allow any compromise. In $HPKE_{PSK}$, we allow compromise of either skR or psk. In $HPKE_{Auth}$, we allow compromise of skS. In $HPKE_{AuthPSK}$, we allow combinations of compromising skS, skR, and the psk, but disallow scenarios where the psk and skR are both compromised.

**PROOF GOALS.** We attempt to prove two secrecy properties for sessions between the honest users S and R: secrecy of the bit b and real-or-random indistinguishability of the exported secrets in all modes. For $HPKE_{PSK}$, $HPKE_{Auth}$, and $HPKE_{AuthPSK}$, we attempt to prove sender authentication in scenarios where it is not trivially broken: in $HPKE_{PSK}$ for sessions before compromise of the psk; in $HPKE_{Auth}$ for sessions before compromise of skS; in $HPKE_{AuthPSK}$ for sessions before the compromise of the psk, and for sessions before the compromise of skS and skR (because HPKE is vulnerable to key-compromise impersonation).

We use the following CryptoVerif queries to express the secrecy proof goals:

1. query secret b.

2. query secret export<sub>1</sub>_secr public_vars export<sub>2</sub>_secr.

3. query secret export<sub>2</sub>_secr public_vars export<sub>1</sub>_secr.

Here, we rely on CryptoVerif's built-in support for real-or-random indistinguishability. Using the public_vars keyword, we prove secrecy of an export key even if the other one was compromised.

We use events and a correspondance query to express the authentication properties for $HPKE_{PSK}$, $HPKE_{Auth}$, $HPKE_{AuthPSK}$. In the model, we issue two events sent and rcvd just before the sender sends a message and just after the recipient successfully decrypts a message. We ask CryptoVerif to prove the following correspondence:

$$ \begin{aligned} & \text{event}(\text{rcvd}(\text{true}, \text{mode}, \text{pkR}, \text{pkS}, \text{psk\_id}, \text{info}, \text{aad}, \text{pt}, k_{\text{exp},1}, k_{\text{exp},2}) \\ \Rightarrow & \text{event}(\text{sent}(\text{mode}, \text{pkR}, \text{pkS}, \text{psk\_id}, \text{info}, \text{aad}, \text{pt}, k_{\text{exp},1}, k_{\text{exp},2}) \end{aligned} $$
We only prove a non-injective correspondence, which means that we do not prove that each rcvd event has a unique corresponding sent event. Instead, a single sent event can satisfy the condition for arbitrary many matching rcvd events. This is because HPKE does not provide protection against replay. The last two parameters are only used in the export variants of the model and absent in the oneshot variants. The first parameter is true only in scenarios where sender authentication is possible; in others we do not attempt the proof.

**CRYPTOGRAPHIC ASSUMPTIONS.** We use the following cryptographic assumptions. We assume that Extract is indifferentiable from a random oracle. We assume that Expand is a PRF, where the first parameter is the key. We write proofs for two different assumptions on Hash: that it is a collision-resistant hash function, and that it is indifferentiable from a random oracle. We assume that the AEAD scheme used is IND-CPA- and INT-CTXT-secure [BN00]. We assume that the KEM uses a prime-order group that satisfies the Gap Diffie-Hellman (GDH) assumption [OP01]. We also assume that an implementation of HPKE validates public keys before usage.

Due to the specific length parameters used with Extract and Expand, both are implemented by exactly one call to HMAC. Thus, we are using a PRF and a random oracle assumption on the same building block. By the following reasoning, we establish that the HMAC call inside Extract operates on a different input domain than the ones inside Expand: The first argument to Extract's HMAC call is the psk which has length $N_h$. The first argument to all HMAC calls inside Expand is the result of Extract; and this has length $N_h$ as well. Thus, the first argument does not directly separate the input domains. The second argument to Extract's HMAC call is the result from the DH operation. This has either length $N_{pk}$ or $2N_{pk}$. The second argument to all HMAC calls inside Expand has at least the length of the ctx variable, which is defined as:

$$ \begin{align} \text{ciphersuite} &= \text{concat}(\underbrace{\text{kem\_id}, \text{kdf\_id}, \text{ead\_id}}_{2 \text{ bytes}}, \underbrace{\text{ciphersuite}, \underbrace{\text{enc}, \text{pkRm}, \text{pkSm}}_{6 \text{ bytes}}, \underbrace{\text{enc}, \text{N}_{\text{enc}}, \text{N}_{\text{pk}}, \text{N}_{\text{pk}}}_{2 \text{ bytes}}) \nonumber \\ \text{ctx} &= \text{concat}(\underbrace{\text{mode}, \text{ciphersuite}, \text{enc}, \text{pkRm}, \text{pkSm}}_{1 \text{ byte}}, \underbrace{\text{pskID\_hash}, \text{info\_hash}}_{N_h}, \underbrace{\text{info\_hash}}_{N_h}) \tag{5.1} \end{align} $$

With this, we conclude that for all modes of HPKE, the length of `ctx` is strictly greater than the length of `zz`. In turn, the input domain of Extract's HMAC call is different from the input domains to the HMAC calls inside `Expand`.

**RESULTS.** Using CryptoVerif's interactive mode, we succeed to write proofs for the desired properties in all modes and compromise scenarios using the above cryptographic assumptions.<fnref n="1" /> The only exception are the proofs for the export variant in mode AuthPSK for a collision-resistant hash function, which we were not able to complete at the time.

**DISCUSSION AND LIMITATIONS.** This analysis constitutes a first confirmation of asymptotic security of the HPKE standard's desired security properties. However, it comes with several cryptographic limitations. The proofs are only

[BN00] Bellare and Namprempre, “Authenticated Encryption: Relations among notions and analysis of the generic composition paradigm”

[OP01] Okamoto and Pointcheval, “The Gap-Problems: a New Class of Problems for the Security of Cryptographic Schemes”

<footnote n="1">¹The model files of this analysis can be accessed at https://github.com/blipp/hpke-analysis-material.</footnote>
valid for prime-order Diffie-Hellman groups, although HPKE is also specified for Curve25519 and Curve448. For $HPKE_{Auth}$, we provide an analysis in Chapter 4 that also covers these elliptic curves using the framework of nominal groups. An analysis of the other modes in this framework is left for future work. In the authenticated modes, the model does not currently allow that the sender encrypts a message to its own public key. Furthermore, the adversary could get more power to strengthen the security notion: it could be allowed to choose the user's private keys, and not only to compromise them (this has been implemented in the analysis presented in Chapter 4); it could be allowed to choose the context used for secret export. Generally, the analysis of the so-called *multi-shot* interface is left for future work, where multiple messages can be encrypted and multiple secrets can be exported. Finally, a modular analysis of HPKE using the KEM/DEM paradigm would be desirable for all modes. For $HPKE_{Auth}$, this has been done as presented in Chapter 4.

## 5.2 INFLUENCE OF OUR ANALYSES ON THE STANDARD

Before and after I became an official co-author of the HPKE standard, I contributed a total of 39 pull requests that got merged.² In the following, we cover those that are related to the cryptographic design of HPKE.

²https://github.com/cfrg/draft-ir
tf-cfrg-hpke/pulls?q=is%3Apr+autho
r%3Ablipp

### 5.2.1 Making the KEM IND-CCA-Secure

After the analysis presented in Section 5.1, we started a modular analysis of HPKE using the KEM/DEM paradigm. As a start, we tried to prove that the variant of DHKEM used in $HPKE_{Base}$ and $HPKE_{PSK}$ is IND-CCA-secure. However, it turned out that DHKEM of HPKE Draft 2 was not provably IND-CCA-secure on its own, using the Gap Diffie-Hellman assumption. We use this assumption because an HPKE recipient can be used as an oracle for the Decisional Diffie-Hellman problem (see Definition 4.5). We recall that at that time, as presented in Section 5.1.1, DHKEM returned the Diffie-Hellman shared secret directly as KEM shared secret. Trying to prove that $pkR^{skE}$ is indistinguishable from a random group element $Z$ fails, because the adversary can submit $pkE$, $pkR$, and $pkR^{skE}$ (or $Z$) to the DDH oracle. Thus, the Diffie-Hellman shared secret cannot be used directly as shared secret of the KEM. The usual mitigation is to use a key derivation function to compute the KEM shared secret.

Then, a proof using the random oracle assumption can be sketched as follows. Let $H$ be a random oracle, and assume the KEM shared secret is computed by $zz \leftarrow H(pkR^{skE})$. Assume that the adversary attempts to distinguish $zz$ from a random value by querying the random oracle with values called $Z$. If $Z = pkR^{skE}$, the random oracle returns $zz$. By the GDH assumption, the probability that the adversary computes $pkR^{skE}$ is negligible, and so we can replace the boolean $Z = pkR^{skE}$ by false in a game transformation. In the new game, the random oracle never returns $zz$ to the adversary, and thus, the adversary cannot distinguish $zz$ from a random value.
With this in mind, it becomes clear that the security proof for HPKE as a
whole, as described in Section 5.1, succeeded because we assumed Extract
in the KeySchedule to be a random oracle.

We proposed a change to the HPKE standard introducing a key derivation
function call within DHKEM. <fnref n="3" /> It became part of HPKE as of Draft 3.

Another reason to use a key derivation function to derive the final KEM
shared secret is that practical pseudo-random functions require a key that is a
uniformly random bitstring, and not only a uniformly random group element.
In general, the bitstring representation of Diffie-Hellman public keys is not a
surjective function, and so, the bitstring representation of uniformly random
group elements could be distinguished from uniformly random bitstrings.

### 5.2.2 Identity Binding

As presented in Section 5.1.1, the KEM ciphertext and the public keys of sender and receiver were used as context of the key derivation inside KeySchedule. In the pull request mentioned above, we moved these three values into the context of the KEM's key derivation to strengthen its IND-CCA security against identity mis-binding issues, also known as *unkown key-share attacks* (see Section 3.2.4 and Section 3.6 for our informal and formal definitions used when analysing WireGuard). X25519 and X448 are particularly prone to this because they have “equivalent” public keys, as we discussed already in Chapter 3: These are public keys that are different, but lead to the *same* Diffie-Hellman shared secret when used with the same private key. Putting the bitstring representation of the public keys explicitly into the context of the key derivation makes sure that the KEM shared secret ends up different, even for equivalent public keys.

Generally, as mentioned in the discussion of the WireGuard analysis in Section 3.7, including as much identity information as possible in the context of a key derivation increases security and simplifies the formal analysis.

### 5.2.3 Oracle Separation by Domain Separation

In our WireGuard analysis, we gave a detailed reasoning why using a random-
oracle and a collision-resistance assumption for the same hash function is
sound, by carefully analysing the input domains of its different usages
(Section 3.4.5). When introducing the key derivation function into DHKEM,
we wanted to make analysis as easy as possible with regards to the use of
hash functions, as in practice, it is possible that the same hash function is
used within DHKEM and for the remainder of HPKE. As a start, we decided
to not use the hash function directly, but only via Extract and Expand, to
avoid the need to consider how Extract and Expand use the hash functions
internally. Then, we gave each usage a unique label as prefix, such that the
set of labels is prefix-free (i. e., no label is the prefix of another label). The
result of this design is what we presented in Section 4.6.1 for DHKEM and
Listing 4.11 for KeySchedule. The term “Oracle Separation” stems from the
discussion after the presentation of the paper [BDG20] at Eurocrypt 2020,
where Daniel J. Bernstein suggested this term.<fnref n="4" />

<footnote n="3">³“Modifications for IND-CCA-secure DHKEM and independent random oracles”
https://github.com/cfrg/draft-irtf-cfrg-hpke/pull/50</footnote>

<footnote>[BDG20] Bellare et al., “Separate Your Domains: NIST PQC KEMs, Oracle Cloning and Read-Only Indifferentiability”</footnote>

<footnote n="4">⁴https://chat.iacr.org/#narrow/stream/47-RWC-2021/topic/TUE.3A.20PoSt-quantum.20Cryptography/near/18995</footnote>
### 5.2.4 Influences of the Analysis of HPKE<sub>Auth</sub>

When we started working on the analysis of HPKE<sub>Auth</sub>, the KeySchedule function of HPKE was defined slightly differently: Line 03 of Listing 4.11 was not

$$s \leftarrow \text{LabeledExtract}(k_{\text{PRF}}, \text{"secret"}, \text{psk})$$

but

$$\text{psk\_hash} \leftarrow \text{LabeledExtract}(\text{empty}, \text{"psk\_hash"}, \text{psk})$$

$$s \leftarrow \text{LabeledExtract}(\text{psk\_hash}, \text{"secret"}, k_{\text{PRF}}).$$

We suggested this change, and it was integrated into Draft 6, in time before we submitted the paper.<fnref n="5" /> Swapping the KEM shared secret $k_{\text{PRF}}$ and the psk allows us to use a standard PRF assumption on HKDF-Extract, using the KEM shared secret as uniformly random PRF key. In the previous version, this was problematic: in general, the psk cannot be used as PRF key because it is not present in all modes, and in particular not in HPKE<sub>Auth</sub>; using the second parameter of Extract as PRF key is not straightforward because there, the KEM shared secret $k_{\text{PRF}}$ is prefixed by several constants, making it non-uniformly random (see Line 07 in Listing 4.11). While this change improves the situation for proofs based on the security of the KEM shared secret $k_{\text{PRF}}$, the question of how to prove security of HPKE<sub>PSK</sub> and HPKE<sub>AuthPSK</sub> based on the psk in case of compromised $k_{\text{PRF}}$ remains for future work. The RFC does not require the psk to be drawn from a uniform distribution, so a PRF assumption with the psk as PRF key would not cover all cases, even if applicable in a straightforward way. The only requirement that the RFC imposes on the psk is that it must have at least “32 bytes of entropy” [Bar+22], following an analysis by Len, Grubbs, and Ristenpart, “effectively barring human-chosen passwords” [LGR21].

Finally, the results of the analysis of HPKE<sub>Auth</sub> have been summarized in Section 9.1 “Security Properties” of the standard, notably to add text on the generic key-compromise impersonation attack that was surfaced by our work. Also, the composition theorems proved during the analysis have informed Section 9.2 “Security Requirements on a KEM used within HPKE” of the standard, which is important for when HPKE is used with other (Authenticated) KEMs.

### 5.2.5 A Verified Implementation of HPKE and Input Length Limits

A verified implementation of HPKE in the F\* programming language has been developed and contributed to the HACL\* library as prior work by other authors [Pol+20]. F\* is a general-purpose functional programming language aimed at program verification [Swa+16]. HACL\* is a cryptographic library written and verified in F\* [Bha+17]. The HPKE implementation of [Pol+20] includes a high-level specification, and efficient low-level implementations that are optimized for multiple processor architectures. The specification and the implementations have been proved to be functionally equivalent. They are based on Draft 2 of HPKE, and only support the Base mode.

As part of our involvement in the development of the HPKE standard, we updated the existing F\* specification to the final version of HPKE, added

<footnote n="5">⁵“Use shared_secret as salt and psk as ikm in LabeledExtract” https://github.com/cfrg/draft-irtf-cfrg-hpke/pull/162</footnote>

<footnote>[Bar+22] Barnes et al., *Hybrid Public Key Encryption*</footnote>

<footnote>[LGR21] Len et al., “Partitioning Oracle Attacks”</footnote>

<footnote>[Pol+20] Polubelova et al., “HACLxN: Verified Generic SIMD Crypto (for All Your Favourite Platforms)”</footnote>

<footnote>[Swa+16] Swamy et al., “Dependent Types and Multi-Monadic Effects in F\*”</footnote>

<footnote>[Bha+17] Bhargavan et al., “HACL\*: A Verified Modern Cryptographic Library”</footnote>
the remaining modes, added the secret export interface that was introduced
with Draft 3, and added the DeriveKeyPair function that was introduced
in Draft 5. This function allows to deterministically derive a KEM key pair
from a bitstring value. We made sure the updated specification passes the
test vectors provided by the RFC. For this, we extracted it to OCaml using
F*'s built-in toolchain. We contributed this work to the HACL* library. <fnref n="6" /> We
leave the update of the efficient low-level implementations for future work.

As described in Section 4.6.2, HPKE uses HKDF to implement Extract and Expand. The specifications of HKDF-Extract and HKDF-Expand in HACL* indicate maximum input lengths for IKM and info that are enforced by the type system. These maximum lengths come from the specifications of the underlying hash functions. We propagate these maximum lengths from HKDF-Extract and HKDF-Expand through LabeledExtract and LabeledExpand all the way up to the input parameters of HPKE that were a priori not length-restricted by HPKE. At each step, we take into account the constant prefixes that are added to the function parameters. This way, we compute the maximum length of HPKE input parameters. The goal is to indicate them in the RFC as guidance for implementations. The affected input parameters are: psk, psk_id, and info as parameters of KeySchedule, ctx as parameter of the secret export interface, and the IKM input parameter of the DeriveKeyPair function. In the F* specification, we define the types of these input parameters taking into account their maximum lengths, parametrized by the hash function in use. <fnref n="7" /> This specification is accepted by the F* type checker, which means that the computed maximum lengths are indeed valid input lengths, and in particular result in inputs to HKDF-Extract and HPKE-Expand with valid input lengths.

The concrete maximum lengths evaluated for all three hash functions
specified for use with HPKE have been documented in Section 7.2.1 “Input
Length Restrictions” in the RFC.<fnref n="8" /> To give an example, the maximum length
of the secret export’s context parameter, when used with the SHA256 hash
function, is 2⁶¹ − 120 bytes. The maximum input length of the SHA256
hash function is 2⁶¹ − 1 bytes, and thus, the maximum length of the context
parameter is only marginally smaller. The difference is due to the HKDF
construction and the constant prefixes used in HPKE. For practical usages,
the HPKE standard recommends a limit of 64 bytes for the 5 input parameters
mentioned above.

<footnote n="6">⁶https://github.com/project-everest/hacl-star/tree/_blippmani</footnote>

<footnote n="7">⁷We do this using refinement types, a concept that is explained later, in Section 6.6.1.</footnote>

<footnote n="8">⁸Pull request for the change “Add section on input limits ...” https://github.com/cfrg/draft-irtf-cfrg-hpke/pull/117</footnote>
<figure><img src="image_29.png" /></figure>
<figure><img src="image_30.png" /></figure>
# Part III

## LINKING COMPUTATIONAL PROOFS AND IMPLEMENTATIONS
<figure><img src="image_31.png" /></figure>
# 6

## cv2fstar: A Compiler from CryptoVerif to F\*

In the previous chapters of this thesis, we presented multiple case studies for mechanized cryptographic proofs done with CryptoVerif. Furthermore, we briefly mentioned the topic of verified implementations in F\*, while writing about our implementation of HPKE in Section 5.2.5. The two worlds of CryptoVerif and F\* have so far not been connected in an automated way. In this chapter, we present cv2fstar, a compiler extending CryptoVerif. It compiles CryptoVerif models to executable F\* specifications that are set up to use the HACL\* library as cryptographic backend. With this, we close the remaining gap between CryptoVerif proofs and F\* implementations: cv2fstar produces F\* code that corresponds to the CryptoVerif model, and that keeps its cryptographic guarantees. The compiler translates CryptoVerif processes to pure F\* functions in state-passing style. Equations and some of the kinds of assumptions used by CryptoVerif are translated to F\* lemmas, as proof obligations for the implementation.

We showcase cv2fstar on the example of the Needham-Schroeder-Lowe (NSL) protocol. In its CryptoVerif model, we assume message encoding and decoding functions that are correct and that produce disjoint encodings for the three NSL protocol messages. Furthermore, serialization and deserialization functions for the types used in the protocol are assumed to exist and to be inverses of each other. cv2fstar translates these assumptions to F\* lemma statements that we prove for the specific functions chosen in the implementation. We implement the cryptographic building blocks used in the CryptoVerif model with already existing HACL\* functions. With this, the F\* specification generated by cv2fstar successfully executes as OCaml code in a toy example.

cv2fstar connects CryptoVerif to the large F\* ecosystem, eventually allowing to guarantee cryptographic properties on verified efficient low-level code – for example C code extracted with KaRaMeL.

In Section 6.1, we introduce and motivate cv2fstar in more detail. Section 6.2 gives an overview over related work. In Section 6.3, we briefly introduce the target language of our compiler. In Section 6.4, we present how the CryptoVerif input language is modified for cv2fstar. Section 6.5 gives an overview of the cv2fstar framework and the code generation of the cv2fstar compiler. Section 6.6 and Section 6.7 describe how types, and functions and constants in a CryptoVerif model are translated to F\*. In Section 6.8, we discuss the polymorphic state type used in the F\* framework. Sections 6.9,
6.10, and 6.11 show the translation of tables, events, and terms. Section 6.12 explains how oracles are translated as F\* functions. In Section 6.13, we describe the translation of equations and assumptions to lemmas. Section 6.14 clarifies the differences between cv2ocaml and cv2fstar. In Section 6.15, we showcase cv2fstar on the example of the Needham-Schroeder-Lowe protocol. Section 6.16 discusses the contributions of the work presented in this chapter. Finally, we discuss future work, both immediate and long-term, in Section 6.17.

The source code of cv2fstar consists of the extension to CryptoVerif, and the F\* framework within which the generated F\* code can be used. It is made available alongside the code for the NSL case study.<fnref n="1" />

## 6.1 MOTIVATION AND INTRODUCTION

cv2fstar's goal is to establish a formal link between two analysis tools that work in different domains: CryptoVerif and F\*.<fnref n="2" /> Cryptographic security proofs done in CryptoVerif [Bla08] form an important part of past and current security research, as shown in Chapters 3 to 5 of this thesis about WireGuard and HPKE, and in analyses of TLS 1.3 [BBK17], Signal [KBB17], and SSH [CB13].

F\* [Swa+16] is a “general-purpose functional programming language aimed at program verification”.<fnref n="3" /> F\* has a rich type system, including dependent types and refinement types. Proofs can be done interactively and by discharging proof obligations to an SMT backend. F\* programs can be extracted to OCaml and F\# for execution, as well as to C when using the Low\* subset of F\* and the KaRaMeL<fnref n="4" /> extraction tool [Pro+17], to WebAssembly [Pro+19], and to assembly code using Vale [Fro+19]. The F\* ecosystem has been used to verify functional correctness and security of real-world protocols and systems, some of which we cite in the next section about related work. One important development that we want to mention here is the High-Assurance Cryptographic Library HACL\* [Bha+17; Pol+20] that is written in F\*. It has made its way into various production systems: Mozilla's NSS library, the Windows kernel, the Linux kernel, Microsoft's implementation of the QUIC protocol, the Tezos blockchain, and WireGuard.<fnref n="5" />

The motivation for a link between CryptoVerif and F\* is twofold. First, we would like to have verified implementations that have concrete cryptographic security guarantees, and in particular by a mechanized formal link. Before cv2fstar, it was possible to write a CryptoVerif model and an F\* specification such that their styles are sufficiently close to enable manual comparison and thus a more-or-less handwavy argument saying that they match. cv2fstar provides an automated translation between the two languages and allows protocols modeled in CryptoVerif to be embedded within F\* programs. Together with the remainder of the F\* ecosystem, we can then go all the way down to extracted C code that will have concrete cryptographic security guarantees. So, we preserve the cryptographic guarantees proved by CryptoVerif on the F\* side, and can augment it with F\*'s capabilities of proving functional correctness, memory safety, arithmetic safety, and secret-independent computation (e. g., against some timing side

<footnote n="1">¹https://www.benjaminlipp.de/phd-thesis/</footnote>

<footnote n="2">²With my bachelor degree in physics in mind, I like to think about it as a great unification of forces, but it's the unification of verification forces – in this case CryptoVerif and F\*.</footnote>

<footnote>[Bla08] Blanchet, "A Computationally Sound Mechanized Prover for Security Protocols"</footnote>

<footnote>[BBK17] Bhargavan et al., "Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate"</footnote>

<footnote>[KBB17] Kobeissi et al., "Automated Verification for Secure Messaging Protocols and their Implementations: A Symbolic and Computational Approach"</footnote>

<footnote>[CB13] Cadé and Blanchet, "From Computationally-Proved Protocol Specifications to Implementations and Application to SSH"</footnote>

<footnote>[Swa+16] Swamy et al., "Dependent Types and Multi-Monadic Effects in F\*"</footnote>

<footnote n="3">³https://www.fstar-lang.org/</footnote>

<footnote n="4">⁴https://github.com/FStarLang/karamel</footnote>

<footnote>[Pro+17] Protzenko et al., "Verified Low-Level Programming Embedded in F\*"</footnote>

<footnote>[Pro+19] Protzenko et al., "Formally Verified Cryptographic Web Applications in WebAssembly"</footnote>

<footnote>[Fro+19] Fromherz et al., "A Verified, Efficient Embedding of a Verifiable Assembly Language"</footnote>

<footnote>[Bha+17] Bhargavan et al., "HACL\*: A Verified Modern Cryptographic Library"</footnote>

<footnote>[Pol+20] Polubelova et al., "HACLxN: Verified Generic SIMD Crypto (for All Your Favourite Platforms)"</footnote>

<footnote n="5">⁵https://hacl-star.github.io/</footnote>