Benjamin Lipp

Bruno Blanchet

Karthikeyan Bhargavan

A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol

Keywords: security protocols, verification, computational model, VPN

WireGuard is a free and open source Virtual Private Network (VPN) that aims to replace IPsec and OpenVPN. It is based on a new cryptographic protocol derived from the Noise Protocol Framework. This paper presents the first mechanised cryptographic proof of the protocol underlying WireGuard, using the CryptoVerif proof assistant. We analyse the entire WireGuard protocol as it is, including transport data messages, in an ACCE-style model. We contribute proofs for correctness, message secrecy, forward secrecy, mutual authentication, session uniqueness, and resistance against key compromise impersonation, identity mis-binding, and replay attacks. We also discuss the strength of the identity hiding provided by WireGuard.

Our work also provides novel theoretical contributions that are reusable beyond WireGuard. First, we extend CryptoVerif to account for the absence of public key validation in popular Diffie-Hellman groups like Curve25519, which is used in many modern protocols including WireGuard. To our knowledge, this is the first mechanised cryptographic proof for any protocol employing such a precise model. Second, we prove several indifferentiability lemmas that are useful to simplify the proofs for sequences of key derivations.

Une preuve cryptographique mécanisée du protocole de réseau privé virtuel WireGuard

Résumé : WireGuard est un logiciel de réseau privé virtuel (VPN) gratuit et open source qui cherche à remplacer IPsec et OpenVPN. Il est fondé sur un nouveau protocole cryptographique dérivé de la famille de protocoles Noise. Ce document présente la première preuve cryptographique mécanisée du protocole de WireGuard, obtenue avec l'assistant de preuve CryptoVerif.

Nous analysons le protocole WireGuard en entier, tel qu'il est, y compris les messages de transport de données, dans un modèle du style ACCE. Nous obtenons des preuves de correction, secret des messages, forward secrecy, authentification mutuelle, unicité des sessions, et résistance contre des attaques d'imposture par compromis de clés, de mauvaise liaison d'identités, et de rejeu. Nous discutons également la robustesse de la protection des identités fournie par WireGuard.

Notre travail fournit aussi de nouvelles contributions théoriques, réutilisables au-delà de WireGuard. Premièrement, nous étendons CryptoVerif pour tenir compte de l'absence de validation des clés publiques dans des groupes Diffie-Hellman populaires comme Curve25519, qui est utilisé dans beaucoup de protocoles modernes dont WireGuard. À notre connaissance, c'est la première preuve cryptographique mécanisée qui utilise un modèle aussi précis. Deuxièmement, nous prouvons plusieurs lemmes d'indifférentiabilité qui sont utiles pour simplifier les preuves de suites de dérivations de clés.

Mots-clés : protocoles cryptographiques, vérification, modèle calculatoire, VPN

Introduction

The traditional distinction between a secure intranet and the untrusted Internet is becoming less relevant as more and more enterprises host internal services on cloud-based servers distributed across multiple data centres. Sensitive data that used to travel only between physically proximate machines within secure buildings is now sent across an unknown number of network links that may be controlled by malicious entities.

To maintain the security of such distributed intranets, the most powerful tools at the disposal of system administrators are Virtual Private Network (VPN) protocols that set up low-level secure channels between machines, and hence can be used to transparently protect all the data exchanged between them. Indeed, all leading cloud providers now offer VPN gateways, so that enterprises can treat cloud-based servers as if they were located within their intranet. 1Standards vs. Custom Protocols. Most popular VPN solutions are based on Internet standards like IPsec [START_REF] Kent | Security Architecture for the Internet Protocol[END_REF] and TLS [39], for several reasons. First, these protocols typically have multiple interoperable implementations that are available on all mainstream operating systems, so the VPN software can be easily built as a layer on top. Second, standards are designed to be future-proof by relying on versioning and cryptographic agility, so that a VPN protocol can easily move from one protocol version or cryptographic algorithm to another if (say) a weakness were found on some configuration. Third, published standards typically have been closely scrutinised by numerous interested parties, and hence are believed to be less likely to contain obvious security flaws.

Conversely, using a standard protocol also has its disadvantages. Standardisation takes time, and so a standard protocol may not use the most modern cryptographic algorithms. On the contrary, the need for interoperability and backwards compatibility often force implementations to continue support for obsolete cryptographic algorithms, leading to cryptanalytic attacks [START_REF] Bhargavan | On the practical (in-)security of 64-bit block ciphers: Collision attacks on HTTP over TLS and OpenVPN[END_REF] and software flaws [START_REF] Beurdouche | A messy state of the union: Taming the composite state machines of TLS[END_REF]. Over time, standards and their implementations can grow to an unmanageable size that can no longer be studied as a whole, allowing logical flaws to hide in unused corners of the protocol [START_REF] Bhargavan | Triple handshakes and cookie cutters: Breaking and fixing authentication over TLS[END_REF].

Consequently, many new secure channel protocols eschew standardisation in favour of a lean design that uses only modern cryptography and supports minimal cryptographic agility. The succinctness of the protocol description aids auditability, and the lack of optional features reduces complexity. Examples of this approach are the Signal protocol [START_REF] Marlinspike | The X3DH key agreement protocol[END_REF] used in many secure messaging systems and the Noise protocol framework [START_REF] Perrin | The Noise protocol framework[END_REF].

WireGuard is a VPN protocol that adopts this design philosophy [START_REF] Donenfeld | WireGuard: Next generation kernel network tunnel[END_REF]. It implements and extends a secure channel protocol derived from the Noise framework, and it chooses a small set of modern cryptographic primitives. By making these choices, WireGuard is able to provide a high-quality VPN in a few thousand lines of code, and is currently being considered for adoption within the Linux kernel. The design of WireGuard is detailed and informally analysed in [START_REF] Donenfeld | WireGuard: Next generation kernel network tunnel[END_REF], but a protocol of such importance deserves a thorough security analysis.

A Need for Mechanised Proofs. Having a succinct, well-documented description is a good basis for understanding, auditing, and implementing a custom cryptographic protocol, but in itself is no guarantee that the protocol is secure. Symbolic analysis with tools like ProVerif [START_REF] Blanchet | Modeling and verifying security protocols with the applied pi calculus and ProVerif[END_REF] and Tamarin [START_REF] Meier | The TAMARIN prover for the symbolic analysis of security protocols[END_REF] can help find logical flaws, and WireGuard already has been analysed using Tamarin [START_REF] Donenfeld | Formal verification of the WireGuard protocol[END_REF]. However, symbolic analyses do not constitute a full cryptographic proof. For example, they cannot demonstrate the absence of cryptanalytic attacks on secure channels and VPNs (e.g. [START_REF] Bhargavan | On the practical (in-)security of 64-bit block ciphers: Collision attacks on HTTP over TLS and OpenVPN[END_REF].)

Cryptographic proofs provide the highest form of formal assurance, but writing proofs by hand requires significant expertise and effort, especially if the proof is to account for the precise low-level details of a real-world protocol. And as proofs get larger, the risk of introducing proof errors becomes non-negligible. All this effort is hard to justify for a custom protocol which may change as the software evolves. For example, a manual cryptographic proof for the WireGuard protocol appears in [START_REF] Dowling | A cryptographic analysis of the WireGuard protocol[END_REF], but this proof would need to be carefully reviewed and adapted if the WireGuard protocol were to change in any way or if a variant of WireGuard were to be proposed.

We advocate the use of mechanised provers to build cryptographic proofs, so that they can be checked for errors, and can be easily modified to accommodate different variants of the protocol. In this paper, we rely on the CryptoVerif protocol verifier [START_REF] Blanchet | Computationally sound mechanized proofs of correspondence assertions[END_REF]13] to build a proof of WireGuard. CryptoVerif relies on a computational model of cryptography, and generates machine-checkable proofs by sequences of games, like those manually written by cryptographers.

Uncovering Real-World Cryptographic Assumptions. A mechanised proof also allows the analyst to experiment with a variety of cryptographic assumptions and discover the precise set of assumptions that a protocol's security depends on.

In some cases, a protocol may require an unusual assumption about a hash function, or a stronger assumption about encryption than one may have expected, and these cases can provide a guide to implementers on what concrete cryptographic algorithms should or should not be used to instantiate the protocol. For example, in our analysis of WireGuard, we find that most of the standard properties require only standard assumptions about the underlying authenticated encryption scheme (AEAD) but identity hiding requires a stronger assumption, which is satisfied by the specific algorithms used by WireGuard, but may not be provided by other AEAD constructions.

In other cases, a protocol's use of a cryptographic primitive may motivate a new, more precise model of the primitive. Protocols like WireGuard seek to depend on a small set of primitives and reuse them in different ways. For example, WireGuard relies on the Curve25519 elliptic curve Diffie-Hellman operation for an ephemeral key exchange as well as for entity authentication. It uses Curve25519 public keys both as identities and as unique nonces to identify sessions. To verify that Curve25519 is appropriate for all these usages, and to prove the absence of attacks such as replays, identity mis-binding, and key compromise impersonation, we need to account for the details of the Curve25519 group, rather than rely on a generic Diffie-Hellman assumption. Hence, we propose a new model for Curve25519 in CryptoVerif and prove WireGuard secure against this model.

Contributions. We present the first mechanised proof for the cryptographic design of the WireGuard VPN, including the Noise IKpsk2 secure channel protocol it uses. Our analysis is done on WireGuard v1 as specified in [START_REF] Donenfeld | WireGuard: Next generation kernel network tunnel[END_REF]. In addition to classic key exchange security for IKpsk2, we examine the identity hiding and denial-of-service protections provided by WireGuard. We conclude with a discussion of the strengths and weaknesses of WireGuard, and propose improvements that would allow for stronger security theorems.

Our work also provides contributions reusable beyond the proof of WireGuard. To the best of our knowledge, this is the first mechanised proof for any cryptographic protocol that takes into account the precise structure of the Curve25519 group. We also prove a series of indifferentiability results that allow us to simplify sequences of random oracle calls, and we made several extensions to CryptoVerif that we mention in the rest of the paper when we use them. These extensions are included in CryptoVerif 2.01 available at https://cryptoverif.inria.fr/.

Our models of WireGuard are available at https://cryptoverif.inria.fr/WireGuard.

Inria 2 WireGuard

WireGuard [START_REF] Donenfeld | WireGuard: Next generation kernel network tunnel[END_REF] establishes a VPN tunnel between two remote hosts in order to securely encapsulate all Internet Protocol (IP) traffic between them. The main design goals of WireGuard are to be simple, fast, modern, and secure. In order to establish a tunnel, a system administrator only needs to configure the IP address and long-term public key for the remote host. With this information, WireGuard can establish a secure channel, using a protocol derived from the Noise framework, instantiated with fast, modern cryptographic primitives like Curve25519 and BLAKE2. The full WireGuard VPN is implemented in a few thousand lines of code that can run on multiple platforms, but for performance, is usually run within the operating system kernel. In particular, WireGuard is in the process of being incorporated into the Linux kernel (most likely Linux 4.2/5.0), as an alternative to IPsec.

In this section, we focus on the cryptographic design of WireGuard. We begin by describing the secure channel component, then the extensions WireGuard makes for denial-of-service and stealthy operation. We end the section by detailing the concrete cryptographic algorithms used by WireGuard and the list of informal security goals it seeks to achieve.

Secure Channel Protocol: Noise IKpsk2

Noise [START_REF] Perrin | The Noise protocol framework[END_REF] is a framework for building two-party cryptographic protocols that are secure by construction. Using the building blocks in this framework, a designer can create a new protocol that matches a desired subset of security guarantees: mutual or optional authentication, identity hiding, forward secrecy, etc. The Noise specification also includes a list of curated pre-defined protocols, with an informal analysis of their message-by-message security claims. WireGuard instantiates one of these protocols, which is called IKpsk2, and extends it to provide further guarantees needed by VPNs.

The secure channel protocol is depicted in Figure 1a, and the cryptographic computations are detailed in Figure 1b, using notations similar to [START_REF] Donenfeld | WireGuard: Next generation kernel network tunnel[END_REF]. Before the protocol begins, the initiator i and the responder r are assumed to have exchanged their long-term static public keys (S pub i , S pub r ). Optionally, they may have also established a pre-shared symmetric key (psk ); if this key is absent it is set to a key-sized bitstring of zeros.

Message Exchange. The protocol begins when i sends the first handshake message to r, which includes the following components:

• I i : a fresh session identifier, generated by i,

• E pub i : a fresh ephemeral public key, generated by i,

• S pub i : i's static public key, encrypted for r,

• ts : a timestamp, encrypted with a key that can be computed only by i and r, and

• mac 1 , mac 2 : message authentication codes (see §2.2).
In response, r sends the second handshake message containing:

• I i : i's session identifier,

• I r : a fresh session identifier, generated by r,

• E pub r : a fresh ephemeral public key, generated by r,

Initiator i Responder r First(Ii, E pub i , S pub i , ts , mac1, mac2 = 0 16 ) Second(Ir, Ii, E pub r , empty , mac1, mac2 = 0 16 ) → → TransportData(Ii, N → 1 , P1 ) TransportData(Ir, N ← 2 , P2 ) TransportData(Ii, N → 3 , P3 ) • • • Figure 1a: WireGuard's protocol messages. Initiator i Responder r
First(Ii, . . . , mac1, mac2 = 0 16 )

CookieReply(Ii, nonce, τ ) First(Ii, . . . , mac1 , mac2)
(continues with standard handshake)

--------CookieReply --------Rr ←$ {0, 1} 256 (refresh only every 2 minutes)

τ ← mac(Rr, A i ) with A i = IP i Port i nonce ←$ {0, 1} 192 τ ← xaenc(hash(label cookie S pub r ), nonce, τ, mac 1 ) --------Non-zero mac 2 ------- mac 2 ← mac(τ, msg β )
Figure 1c: Cookie mechanism under load.

--------First ------------

E pub i : (E priv i , E pub i ) ←$ keygen() C 0 ← hash(protocol_name) H 0 ← hash(C 0 prologue) H 1 ← hash(H 0 S pub r ) C 1 ← hkdf 1 (C 0 , E pub i ) H 2 ← hash(H 1 E pub i ) C 2 k 1 ← hkdf 2 (C 1 , dh(E priv i , S pub r )) S pub i : S pub i ← aenc(k 1 , 0, S pub i , H 2 ) H 3 ← hash(H 2 S pub i ) C 3 k 2 ← hkdf 2 (C 2 , dh(S priv i , S pub r )) ts : ts ← aenc(k 2 , 0, timestamp(), H 3 ) H 4 ← hash(H 3 ts ) mac 1 : mac 1 ← mac(hash(label mac1 S pub r ), msg α ) --------Second ----------- E pub r : (E priv r , E pub r ) ←$ keygen() C 4 ← hkdf 1 (C 3 , E pub r ) H 5 ← hash(H 4 E pub r ) C 5 ← hkdf 1 (C 4 , dh(E priv r , E pub i )) C 6 ← hkdf 1 (C 5 , dh(E priv r , S pub i )) C 7 π k 3 ← hkdf 3 (C 6 , psk ) H 6 ← hash(H 5 π) empty :
empty ← aenc(k 3 , 0, empty, H 6 )

H 7 ← hash(H 6 empty ) mac 1 : mac 1 ← mac(hash(label mac1 S pub i ), msg α ) --------Key Derivation ------- T → T ← ← hkdf 2 (C 7 , empty) --------TransportData -------- P 1 ← aenc(T → , N → 1 = 0, P 1 , empty) P 2 ← aenc(T ← , N ← 2 = 0, P 2 , empty) P 3 ← aenc(T → , N → 3 = 1, P 3 , empty)
Figure 1b: Cryptographic Computations for Protocol Messages.

Figure 1: (a) An overview of WireGuard's main protocol messages; (b) the cryptographic computations used to create these messages; they need to be adapted accordingly for the receiving side; and (c) the cookie mechanism used by WireGuard to protect hosts against Denial-of-Service attacks. We write x for a variable containing an encryption of x; x is just a variable identifier. The authenticated encryption functions aenc and xaenc take as arguments a key, a nonce, the plaintext to encrypt, and the additional data to authenticate, in this order. msg α refers to all the bytes of a message up to but not including mac 1 , msg β is the same but including mac 1 . Session key derivation takes places after the second protocol message, symbolised by →, at which point the initiator can send messages. The end of the handshake is symbolised by , after which transport data messages can be sent in both directions. The cookie mechanism is depicted in one direction, initiator to responder, but can actually be used by either initiator or responder, whichever is under load.

Inria

• empty : an empty bytestring encrypted with a key that can be computed only by i and r, and

• mac 1 , mac 2 : message authentication codes (see §2.2).

The encrypted payloads in the two messages serve as authenticators: by computing the corresponding encryption key, each party proves that it knows the private key for its static public key. The encryption key for the second message also requires knowledge of the optional psk providing an additional authentication guarantee. The two ephemeral keys add fresh sessionspecific key material that can be used to compute (forward) secret session keys known only to i and r.

At the end of these two messages, i and r derive authenticated encryption keys (T → , T ← ) that can be used to transport IP traffic in the two directions. Importantly, i sends the first transport message, hence confirming the successful completion of the handshake to r, before r sends it any encrypted traffic. Each of these transport messages includes:

• I i or I r : the recipient's session identifier,

• N ← j or N → j : the current message counter, • P j : an IP datagram, encrypted under the traffic key.

Cryptographic Computations. Figure 1b describes how each of these message components and traffic keys are computed. As the handshake proceeds, i and r compute a sequence of transcript hashes (H 0 , H 1 , . . . , H 7 ) that hashes in all the public data used in the two handshake messages, including:

• protocol_name, prologue: strings identifying the protocol,

• E pub i , E pub r : both ephemeral public keys,

• S pub r , S pub i : both static public keys, but with the initiator's key in encrypted form,

• ts , empty : both encrypted handshake payloads, and

• π: an identifier derived from the pre-shared key.

These transcript hashes serve as unique identifiers for the current stage of the session. In particular, no two completed WireGuard sessions should have the same H 7 .

Both parties also derive a sequence of chaining keys (C 0 , C 1 , . . . , C 7 ) by mixing in all the key material, including:

• protocol_name, E pub i , E pub r , • dh(E priv i , S pub r ) = dh(S priv r , E pub i ):
the ephemeral-static Diffie-Hellman shared secret computed using the initiator's ephemeral key (named first in ephemeral-static) and the responder's static key (named second in ephemeral-static),

• dh(S priv i , S pub r ) = dh(S priv r , S pub i ): the static-static shared secret, • dh(E priv i , E pub r ) = dh(E priv r , E pub i ): the ephemeral-ephemeral shared secret, • dh(S priv i , E pub r ) = dh(E priv r , S pub i
): the static-ephemeral shared secret, and

• psk : the (optional) pre-shared key.

RR n°9269

The function dh is the elliptic curve scalar multiplication, taking a private key and a public key as argument, permitting the computation of a shared secret [START_REF] Langley | Elliptic curves for security[END_REF]. In the preceding list, the initiator uses the first function call, and the responder the second one, respectively.

The protocol uses all four combinations of static and ephemeral Diffie-Hellman shared-secret computations to maximally protect against the compromise of some of these keys. The psk also serves as a defensive countermeasure against quantum adversaries who may be able to break the Diffie-Hellman construction, but not hkdf. Hence, by using a frequently updated psk , WireGuard users can protect current sessions against future quantum adversaries.

Each chaining key is mixed into the next chaining key via an hkdf key derivation that also outputs encryption keys as needed. This chain of key derivations outputs two encryption keys (k 1 , k 2 ) for the first handshake message, an encryption key (k 3 ) and a PSK identifier (π) for the second message, and traffic keys (T ← , T → ) for all subsequent transport messages.

To encrypt each message, WireGuard uses an authenticated encryption scheme with associated data (AEAD) that takes a key, a counter, a plaintext (padded up to the nearest blocksize) and an optional hash value as associated data. The encryptions in the handshake messages use the current transcript hash (H 2 , H 3 , H 6 ) as associated data, which guarantees that the two participants have a consistent session transcript. Transport messages use an empty string as associated data. The message counter is initially set to 0 for each AEAD key and incremented by 1 every time the key is reused.

Relationship with IKpsk2. The secure channel protocol described above is a direct instantiation of Noise IKpsk2, with five notable differences. First, WireGuard adds local session identifiers (I i , I r ) for the initiator and responder. Second, WireGuard fixes the payload of the first message to a timestamp, and the one of the second message to the empty string. Third, WireGuard stipulates that the first traffic message is sent from the initiator to the responder. Fourth, WireGuard excludes zero Diffie-Hellman shared secrets to avoid points of small order, while Noise recommends not to perform this check. Fifth, WireGuard adds two message authentication codes to the handshake messages, to provide stealth and to protect against DoS, as described in the next section. We also observe that although this protocol is superficially similar to other popular Noise protocols like IK (which is used in WhatsApp), there are important differences between these variants and a proof for one does not translate to the other.

Extensions for Stealth and Denial-of-Service

A VPN protocol operates at a low-level in the networking stack and hence needs to not only protect against cryptographic attacks, but also real-world network-level attacks such as denial of service (DoS). Indeed, a cryptographic protocol like IKpsk2 that needs to perform two expensive Diffie-Hellman operations before it can authenticate a handshake message is even more vulnerable to DoS: an adversary can send bogus messages that tie up computing resources on the recipient. A further security goal for WireGuard is that its VPN endpoints should be stealthy, in the sense that it should not be possible for a network adversary to blindly scan for WireGuard services.

To support stealthy operation, WireGuard endpoints do not respond to any handshake message unless the sender can prove that it knows the static public key of the recipient. This proof is incorporated in the mac 1 field included in each handshake message, which contains a message authentication code (MAC) computed over the prefix of the current handshake message up to but not including mac 1 , using a MAC key derived from the recipient's static public key. The recipient verifies this MAC before processing the message, and stays silent if the MAC fails. Hence, a network adversary who does not know the public key cannot detect whether WireGuard is running on a machine, and at the same time cannot force the recipient to perform two finally useless Diffie-Hellman operations.

Inria

To protect more actively against DoS, WireGuard incorporates a cookie-based protocol (depicted in Figure 1c) that a host can use when it is under load. For example, if the responder suspects it is under a DoS attack, it can refuse to process the first handshake message and instead send back an initiator-specific fresh cookie (τ ) that is computed from a frequently rotated secret key (R r ) (known only to the responder) and the initiator's IP address (IP i ) and source port (Port i ). The responder encrypts this cookie for the initiator, using a key derived from the initiator's static public key, a fresh nonce, and the mac 1 field of the first message as associated data.

The initiator decrypts τ and then retries the handshake by sending the first message again, but this time with a second field mac 2 that contains a MAC over the full message up to and including mac 1 , using τ as the MAC key. After verifying this MAC, the responder continues with the standard handshake.

However, to obtain τ , an adversary must be able to read messages on the network path between the initiator and responder and must also know the initiator's static key (which is never sent in the clear by the protocol). And even if the adversary has both these capabilities, it is required to perform session specific cryptographic computations for every handshake message it sends to the responder, significantly limiting its ability to mount a DoS attack. Hence, this cookie protocol protects the recipient from brute-force network attacks.

Note that the mac 2 field is included in both handshake messages, and hence can be used in both directions, to protect both the initiator and responder from DoS attacks.

The two MACs are WireGuard-specific mechanisms which are not present in IKpsk2. Since they do not use any of the session keys (or hashes or chaining keys) that are used in IKpsk2, adding these mechanisms should, in principle, not affect the security of the secure channel protocol. However, since the static public keys of the two hosts are used in the two MACs, we need to carefully study their impact on the identity-hiding guarantees of IKpsk2.

Instantiating the Cryptographic Algorithms

WireGuard uses a small set of cryptographic constructions and instantiates them with modern algorithms, carefully chosen to provide strong security as well as high performance:

• dh: all Diffie-Hellman operations use the Curve25519 elliptic curve [START_REF] Langley | Elliptic curves for security[END_REF], which uses 32-byte private and public keys;

• hash: all hash operations use the BLAKE2s hash function [START_REF] Saarinen | The BLAKE2 cryptographic hash and message authentication code (MAC)[END_REF], which returns a 32-byte hash;

• aenc: authenticated encryption for handshake and traffic message uses the AEAD scheme ChaCha20Poly1305 [START_REF] Nir | ChaCha20 and Poly1305 for IETF Protocols[END_REF], where the key has 32 bytes, the 96-bit nonce is composed of 32 bits of zeroes followed by the 64-bit little-endian value of the message counter, the plaintext is padded with zeroes up to the nearest 16-byte block, and the associated data is a hash value of 32 bytes;

• xaenc: cookie encryption uses an extended AEAD construction using XChaCha20Poly1305, which incorporates a 192-bit random nonce [START_REF] Bernstein | Extending the Salsa20 nonce[END_REF] into the standard ChaCha20Poly1305 construction;

• mac: all MAC operations use the keyed MAC variant of the BLAKE2s hash function, which returns a 16-byte tag;

• hkdf n : all key derivations use the HKDF construction [START_REF] Krawczyk | HMAC-based extract-and-expand key derivation function (HKDF)[END_REF], using BLAKE2s as the underlying hash function.

WireGuard also uses some constants to indicate the specific algorithms it uses and to disambiguate different uses of the mac and xaenc primitives. The protocol_name field is set to the UTF-8 string "Noise_IKpsk2_25519_ChaChaPoly_BLAKE2s" while the prologue is set to "WireGuard v1 zx2c4 Jason@zx2c4.com". The mac 1 computation uses the UTF-8 string "mac1--" as label mac1 , and the cookie computation uses "cookie-" as label cookie .

Security Goals, Informally

Using the mechanisms described in this section, WireGuard seeks to provide the following set of strong security guarantees, inheriting the security claims of Noise IKpsk2 [START_REF] Perrin | The Noise protocol framework[END_REF] and extending them with the additional DoS and stealth goals of WireGuard [START_REF] Donenfeld | WireGuard: Next generation kernel network tunnel[END_REF]. In the following, we use honest to refer to a party that follows the protocol specification, and dishonest to a party that doesn't, i.e. that is controlled by the adversary. Most properties are defined to hold within a clean session; we define this notion formally in Section §5.1.

• Correctness: If an honest initiator and an honest responder complete a WireGuard handshake and the messages are not altered by an adversary, then the transport data keys (T → , T ← ) and the transcript hash H 7 are the same on both hosts.

• Secrecy: If a transport data message P is sent over a tunnel between two honest hosts, then this message is kept confidential from the adversary. Furthermore, the traffic keys for this tunnel are also confidential.

• Forward Secrecy: Secrecy for a session holds even if both the static private keys (S priv i , S priv r ) and the pre-shared key (psk ) become known to the adversary, but only after the session has been completed and all its traffic keys and chaining keys are deleted by both parties.

Secrecy also holds even if the static and ephemeral keys are compromised (e.g. by a quantum adversary), as long as the pre-shared key is not compromised.

• Mutual Authentication: If an honest initiator (resp. responder) completed a handshake (ostensibly) with an honest peer, then that peer must have participated in this handshake. Moreover, if a host A receives a plaintext message over a WireGuard tunnel that claims to be from host B, then B must have (intentionally) sent this message to A.

• Resistance against Key Compromise Impersonation (KCI): The recipient of a message can authenticate the message's sender even if the recipient's static key is compromised.

• Resistance against Identity Mis-Binding: If two honest parties derive the same traffic keys in some WireGuard session, then they agree on each other's identities, even if one or both of them have been interacting with a dishonest party or a honest party with compromised keys. This property is also called resistance against unknown key-share attacks.

• Resistance against Replay: Any protocol message sent may be accepted at most once by the recipient.

• Session Uniqueness: There is at most one honest initiator session and at most one honest responder session for a given traffic key. Similarly, there is at most one honest initiator session and at most one honest responder session for given handshake messages.

• Channel Binding: Two sessions that have the same final session transcript hash H 7 share the same view and the same session keys.

Inria

• Identity Hiding: Just by looking at the messages transmitted over the network, a passive adversary cannot infer the static keys involved in a session. (However, these identities are not forward secret: If the responder's static key gets compromised, the adversary can later decrypt the initiator's static public key that was transmitted in the first message.)

• DoS Resistance: The adversary cannot have a message accepted by a recipient under load without having first made a round trip with that recipient. In practice, this means that the adversary has to be at the claimed address. Because we assume that the adversary controls the network, we cannot prove more than enforcing a round trip.

The security goals above are stated in terms of completed WireGuard sessions, with most security guarantees only applying after the third message, when both initiator and responder start freely sending and receiving data. In particular, the first transport data message (i.e. the third message) serves as key confirmation to the responder, and is needed to prove that the initiator has control over its ephemeral key. This is why, in WireGuard, the responder does not send any data until it sees this third message. In the rest of this paper, we investigate whether WireGuard achieves the goals set out above.

Cryptographic Assumptions

This section presents the assumptions that we make on the cryptographic primitives used by WireGuard. For most primitives, the desired assumption is already present in the library of primitives of CryptoVerif, so we just need to call a macro to use that assumption. Still, we had to design a new model for Curve25519, detailed below.

Random Oracle Model

We assume that BLAKE2s is a random oracle [START_REF] Bellare | Random oracles are practical: a paradigm for designing efficient protocols[END_REF]. This assumption is justified in [START_REF] Luykx | Security analysis of BLAKE2's modes of operation[END_REF] using a weak ideal block cipher. In particular, BLAKE2s uses a prefix-free Merkle-Damgård construction, thanks to the use of finalisation flags. Therefore, extension attacks which apply to pure Merkle-Damgård constructions do not apply to BLAKE2s.

IND-CPA and INT-CTXT for AEAD

We assume that the ChaCha20Poly1305 AEAD scheme [START_REF] Nir | ChaCha20 and Poly1305 for IETF Protocols[END_REF] is IND-CPA (indistinguishable under chosen plaintext attacks) and INT-CTXT (ciphertext integrity) [START_REF] Bellare | Authenticated encryption: Relations among notions and analysis of the generic composition paradigm[END_REF], provided the same nonce is never used twice with the same key. IND-CPA means that the adversary has a negligible probability of distinguishing encryptions of two distinct messages of the same length that it has chosen. INT-CTXT means that an adversary with access to encryption and decryption oracles has a negligible probability of forging a ciphertext that decrypts successfully and has not been returned by the encryption oracle. These properties are justified in [START_REF] Procter | A security analysis of the composition of ChaCha20 and Poly1305[END_REF], assuming ChaCha20 is a PRF (pseudo-random function) and Poly1305 is an -almost-∆-universal hash function. The latter property is shown to hold in [START_REF] Bernstein | The Poly1305-AES message-authentication code[END_REF].

Curve25519 and Gap Diffie-Hellman

WireGuard uses the elliptic curve Curve25519 [START_REF] Langley | Elliptic curves for security[END_REF] for Diffie-Hellman key exchanges. Curve25519, as implemented in WireGuard and as specified by RFC 7748 [START_REF] Langley | Elliptic curves for security[END_REF], satisfies the following properties:

1. It is an elliptic curve defined by an equation of the form Y 2 = X 3 + AX 2 + X in the field F p of non-zero integers modulo a large prime p, where A 2 -4 is not a square modulo p.

It forms a commutative group of order kq

where k (cofactor) is a small integer and q is a large prime, using point addition as group law and the point at infinity ∞ as neutral element. The base point g 0 is a point on the curve with prime order q.

3. The incoming public keys are not verified and the implementation uses a single coordinate ladder, that is, the curve points are only represented 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 twist is also an elliptic curve, which forms a group of order k q where k is a small integer and q is a large prime, using point addition as group law and the point at infinity ∞ as neutral element. (In particular, the incoming public keys can represent any point on the curve or its twist, and may not belong to the subgroup generated by the base point g 0 .)

4. The cofactor k of the curve is a multiple of the cofactor k of the twist.

5. The single coordinate ladder is defined following [6, Theorem 2.1]: We consider the elliptic curve E(F p 2 ) defined by the equation Y 2 = X 3 + AX 2 + X in a quadratic extension F p 2 of F p , we define X 0 : E(F p 2 ) → F p 2 by X 0 (∞) = 0 and X 0 (X, Y ) = X, and for X ∈ F p and y an integer, we define y

• X ∈ F p as y • X = X 0 (yQ) for all Q ∈ E(F p 2 ) such that X 0 (Q) = X.
6. The public keys (bitstrings in a finite set G) are mapped to elements of F p by the function decode_pk : G → F p and conversely, elements of F p are mapped to public keys by the function encode_pk : F p → G, such that decode_pk • encode_pk is the identity.

7. The Diffie-Hellman "exponentiation" exp : G × Z → G is defined by exp(X, y) = encode_pk(y • decode_pk(X))

8. The private keys are chosen uniformly in {kn | n ∈ S} where S ⊆ {n min , . . . , n max }, n min < n max , n max -n min < q, n max -n min < q , and all elements of S are prime to qq .

Curve25519 satisfies these properties with p = 2 255 -19, k = 8, k = 4, q = 2 252 + δ with 0 < δ < 2 128 (the exact value is δ = 0x14def9dea2f79cd65812631a5cf5d3ed), q = 2 253 -9 -2δ, S = {2 251 , . . . , 2 252 -1}. The set G of public keys consists of bitstrings of 32 bytes, or equivalently G = {0, . . . , 2 256 -1}. The function decode_pk : G → F p is defined by decode_pk(X) = (X mod 2 255 ) mod p. Conversely, encode_pk : F p → G is such that encode_pk(X) is the representation of X as an element of {0, . . . , p -1}. For generality, our model supports not only Curve25519, but any elliptic curve that satisfies assumptions 1 to 8 above.

Let us first establish a few properties of y • X.

Lemma 1. 1. We can define y • X for y in Z kqq . 2. y • (z • X) = (yz) • X.
3. Let Z be the set of integers multiple of k and prime to qq modulo kqq . For any z ∈ Z, for any X, Y ∈ F p , we have z

• X = z • Y if and only if k • X = k • Y . 4. Let G sub = {k • X | X ∈ F p }. For any z prime to qq , for any X, Y ∈ G sub , we have z • X = z • Y if and only if X = Y . Inria Proof. 1. We have kqq Q = ∞ for any Q: if Q is on the curve, then kqQ = ∞ since ∞ is
the neutral element of the curve and its order is kq, so kqq Q = ∞; if Q is on the twist, then k q Q = ∞ since ∞ is the neutral element of the twist and its order is k q , so kqq Q = ∞ since kqq is a multiple of k q . Hence, (y + nkqq )Q = yQ for any n, so we can define y • X when y is in Z kqq .

2. We have y

• (z • X) = X 0 (yQ ) for all Q ∈ E(F p 2 ) such that X 0 (Q ) = z • X = X 0 (zQ) for all Q ∈ E(F p 2 ) such that X 0 (Q) = X. Taking Q = zQ, we have y • (z • X) = X 0 (yzQ) for all Q ∈ E(F p 2 ) such that X 0 (Q) = X, so y • (z • X) = (yz) • X.
3. We have z = kz for some z prime to qq : there exist z and n such that z z + nqq = 1.

Then kz z + nkqq = k. Hence, z • (z • X) = (zz ) • X = (kz z ) • X = k • X and similarly z • (z • Y ) = k • Y . If k • X = k • Y , then z • X = (kz ) • X = z • (k • X) = z • (k • Y ) = (kz ) • Y = z • Y . Conversely, suppose z • X = z • Y . Thus, z • (z • X) = z • (z • Y ), so k • X = k • Y . 4. We have X = k • X and Y = k • Y for some X and Y . By 3. applied to kz, X , Y , we have (kz) • X = (kz) • Y if and only if k • X = k • Y . That is exactly z • X = z • Y if and only if X = Y . Property 2 implies that exp(exp(g, y), z) = encode_pk(z • (y • X 0 (g 0 ))) = encode_pk((zy) • X 0 (g 0 ))
, where g = encode_pk(X 0 (g 0 )) represents the base point. Hence, by commutativity of integer multiplication, exp(exp(g, y), z) = exp(exp(g, z), y): the same Diffie-Hellman shared secret is computed by both participants of the protocol.

We say that public keys X and Y such that k • decode_pk(X) = k • decode_pk(Y ) are equivalent, because they yield the same Diffie-Hellman shared secrets as shown by Lemma 1, property 3. There are in general several public keys equivalent to a public key X. Moreover, the public keys may be 0, and x • 0 = 0 for all x.

While most proofs of Diffie-Hellman key agreements assume a prime order group, that assumption is not correct for most implementations of Curve25519. For instance, the identity mis-binding issue that we discuss in Section 6 would not appear in a prime order group. Therefore, we need to provide a new model that takes into account the properties mentioned above.

In CryptoVerif, we first define the following types:

type G [bounded, large]. type G sub [bounded, large]. type Z [bounded, large, nonuniform].
The type G represents the set of public keys; it is bounded because it is represented by bitstrings of bounded length, and large because collisions between randomly chosen elements in G have a small probability. (The set G contains at least p elements since encode_pk is injective, and p is a large prime.) The type

G sub represents the set {k • X | X ∈ F p } = {X 0 (Q) | Q is in
the subgroup of order q of the curve or in the subgroup of order q of the twist}. The type Z corresponds to the set Z defined in Lemma 1. When honest participants choose private keys, they are chosen uniformly in a subset of Z, {kn | n ∈ S}, considered modulo kqq . By hypothesis, n ∈ S is prime to qq . Moreover, since k is small integer and q and q are large primes, k is not a multiple of q nor q , so k is also prime to qq . Hence, kn is a multiple of k and prime to qq , so kn considered modulo kqq is in Z. Since these elements do not cover the whole set Z, the distribution for choosing random private keys inside the whole Z is non-uniform, which is indicated by the annotation nonuniform.

The main idea of our model is to rely on a Diffie-Hellman assumption in G sub , and so to work as much as possible with elements in G sub . We rewrite the computations in G into computations in G sub by first mapping the public keys

X ∈ G to k • decode_pk(X) ∈ G sub .
We define functions:

fun exp(G, Z) : G. fun mult(Z, Z) : Z. equation builtin commut(mult).
We let exp(X, y) = encode_pk(y • decode_pk(X)) and mult be the product modulo kqq , in Z.

Since its two arguments are multiples of k and prime to qq , so is its result, and it is in Z. The last line states that the function mult is commutative. (We could add associativity and other algebraic properties, but commutativity is typically sufficient to prove security of basic Diffie-Hellman key exchanges. More algebraic properties may be needed to prove group Diffie-Hellman protocols, for instance. Note that not modelling these does not restrict the adversary in the computational model.)

fun pow _k (G) : G sub . fun exp_div _k (G sub , Z) : G sub . fun G sub 2G(G sub ) : G [data]. equation forall X : G sub , X : G sub ; (pow _k (G sub 2G(X)) = pow _k (G sub 2G(X ))) = (X = X ).
We have pow _k (X) = k •decode_pk(X), and it is in G sub for all X in G. We have exp_div _k (X, y) = (y/k) • X. This function is convenient since the private keys in Z are always multiples of k.

Let us show that it is well defined and operates on G sub . Since y is a multiple of k, there exists y such that y = ky . There are k representatives of y/k modulo kqq , y + nqq for n ∈ {0, . . . , k -1}, but all representatives yield the same value for

(y/k) • X: since X ∈ G sub , there exists X such that X = k • X , so (y + nqq ) • X = (y + nqq ) • (k • X ) = (ky + nkqq ) • X = y • X . Moreover, this value is equal to k • (y • X ), so it is in G sub . The function G sub 2G is encode_pk restricted to G sub ; it converts elements of type G sub to type G. The annotation data tells CryptoVerif that it is injective. The last equation says that pow _k • G sub 2G is injective. The function decode_pk • G sub 2G is the identity, so pow _k (G sub 2G(X)) = k • X and similarly pow _k (G sub 2G(X )) = k • X . By Lemma 1, property 4, k • X = k • X if and only if X = X .
We also define constants:

const zero : G. const zero sub : G sub . equation zero = G sub 2G(zero sub ). const g : G. const g_k : G sub . equation pow _k (g) = g_k . equation g_k = zero sub .
The constant 0 is zero as an element of G and zero sub as an element of G sub . The constant g = encode_pk(X 0 (g 0 )) represents the base point, and g_k = k • decode_pk(g).

We also state equations that hold on these functions:

equation forall X : G, y : Z; exp(X, y) = G sub 2G(exp_div _k (pow _k (X), y)). ( 1
)
equation forall X : G sub , y : Z, z : Z; exp_div _k (pow _k (G sub 2G(exp_div _k (X, y))), z) = exp_div _k (X, mult(y, z)). (2)
Equation ( 1) 2) applies in particular to simplify exp(exp(X, y), z) after applying (1):

follows from y • decode_pk(X) = (y/k) • (k • decode_pk(X)) and Equation (2) from (z/k) • k • (y/k) • X = (yz/k) • X. Equation (
exp(exp(X, y), z) = G sub 2G(exp_div _k (pow _k (G sub 2G(exp_div _k (pow _k (X), y))), z)) = G sub 2G(exp_div _k (pow _k (X), mult(y, z))) Inria
This equation with X = g, combined with the commutativity of mult, shows that both participants of the protocol compute the same Diffie-Hellman shared secret. These equations are used by CryptoVerif as rewrite rules, to rewrite the left-hand side into the right-hand side. They allow to rewrite computations in G into computations that happen in G sub , after mapping the public keys

X ∈ G to k • decode_pk(X) ∈ G sub .
In particular, exp(g, y) = G sub 2G(exp_div _k (g_k , y)) and exp(exp(g, y), z) = G sub 2G(exp_div _k (g_k , mult(y, z))).

The next equations allow CryptoVerif to simplify equality tests with 0, which are used by some protocols, including WireGuard, to exclude elements of low order from the allowed public keys.

equation forall X : G sub , y : Z; (exp_div _k (X, y) = zero sub ) = (X = zero sub ). equation forall X : G sub , y : Z; (exp_div _k (X, y) = zero sub ) = (X = zero sub ). equation forall X : G sub ; (pow _k (G sub 2G(X)) = zero sub ) = (X = zero sub ). equation forall X : G sub ; (pow _k (G sub 2G(X)) = zero sub ) = (X = zero sub ).
When y ∈ Z, y = ky for some y prime to qq . Moreover,

y • 0 = 0. Therefore, (y/k) • X = 0 if and only if y •X = y •0 if and only if X = 0 by Lemma 1, property 4. We have pow _k (G sub 2G(X)) = k • X and k is prime to qq , so k • X = 0 if and only if k • X = k • 0 if and only if X = 0 by Lemma 1, property 4.
Other properties serve to simplify equalities between Diffie-Hellman values in G sub , with the goal of showing that these equalities are false. When the Diffie-Hellman shared secrets are passed to a random oracle, these equality tests appear after using the random oracle assumption: we compare the arguments of each call to the random oracle with arguments of previous calls, to know whether the random oracle should return the result of a previous call.

equation forall X : G sub , X : G sub , y : Z; (exp_div _k (X, y) = exp_div _k (X , y)) = (X = X ). (3)
equation forall X : G sub , x : Z, y : Z;

(exp_div _k (X, y) = exp_div _k (g_k , mult(x , y))) = (X = pow _k (G sub 2G(exp_div _k (g_k , x )))).

(4)

collision y R ← Z; z R ← Z; [random_choices_may_be_equal] forall X : G sub ; return(exp_div _k (X, y) = exp_div _k (X, z)) ≈ Pcoll1rand(Z) return((X = zero sub ) ∨ (y = z)).
(5)

collision x R ← Z; forall X : G sub , Y : G sub ; return(exp_div _k (X, x) = Y ) ≈ 2×Pcoll1rand(Z) return((X = zero sub ) ∧ (Y = zero sub )) if X independent-of x ∧ Y independent-of x. (6) collision x R ← Z; forall y : Z, X : G sub ; return(exp_div _k (g_k , mult(x, y)) = X) ≈ 2×Pcoll1rand(Z) return(false) if y independent-of x ∧ X independent-of x. (7) collision x R ← Z; y R ← Z; [random_choices_may_be_equal] forall X : G sub ; return(exp_div _k (g_k , mult(x, y)) = X) ≈ 4×Pcoll1rand(Z) return(false) if X independent-of x ∨ X independent-of y. (8) collision x R ← Z; y R ← Z; y R ← Z; [random_choices_may_be_equal] return(exp_div _k (g_k , mult(x, y)) = exp_div _k (g_k , mult(x, y ))) ≈ Pcoll1rand(Z) return(y = y ). (9)
Equation ( 3) follows from Lemma 1, property 4 because y = ky for some y prime to qq . In particular, using (1), injectivity of G sub 2G, and (3), exp(X, y) = exp(X , y) simplifies into pow _k (X) = pow _k (X ). In contrast, in a prime order group, exp(X, y) = exp(X , y) implies X = X . This is the reason why, in the identity mis-binding issue of Section 6, we fail to prove equality of the public keys X = X and can only prove pow _k (X) = pow _k (X ). Equation ( 4) is a particular case of (3) when X = x •g_k = pow _k (G sub 2G(exp_div _k (g_k , x ))). However, CryptoVerif would not apply (3) to a term of the form exp_div _k (X, y) = exp_div _k (g_k , mult(x , y)).

Let us solve the equation y

• X = z • X for X ∈ G sub . If X = 0, then y • X = 0 = z • X
for all y and z. Otherwise, X = X 0 (Q) where Q is either in the subgroup of order q of the curve or in the subgroup of order q of the twist. Since X = 0, Q = ∞, so Q is a generator of either of these subgroups. The equation y

• X = z • X means X 0 (yQ) = X 0 (zQ), that is, yQ = zQ or yQ = -zQ.
If Q is on the curve, this means y ≡ z mod q or y ≡ -z mod q. If Q is on the twist, this means y ≡ z mod q or y ≡ -z mod q . In other words, z + mq and -z + mq are equivalent private keys for all m and all public keys in G sub that correspond to points on the curve, and z + mq and -z + mq are equivalent private keys for all m and all public keys in G sub that correspond to points on the twist. (In the case of Curve25519, there are indeed honestly generated equivalent private keys: kn and k(q -n) for n ∈ {2 251 , . . . , 2 251 + δ} can both be honestly generated since q-n ∈ {2 251 , . . . , 2 251 +δ} in this case. Similarly, kn and k(q -n) for n ∈ {2 252 -8-2δ, . . . , 2 252 -1} can both be honestly generated since q -n ∈ {2 252 -8 -2δ, . . . , 2 252 -1}.)

In the collision statement (5), Pcoll1rand(Z) is the probability that a randomly chosen element x in Z is equal to an element of Z independent of x. Since random private keys are chosen uniformly among a set of |S| elements, Pcoll1rand(Z) = 1/|S|. For Curve25519, Pcoll1rand(Z) = 2 -251 . Statement [START_REF] Bernstein | The Poly1305-AES message-authentication code[END_REF] means that the probability of distinguishing exp_div _k (X, y) = exp_div _k (X, z) from (X = zero sub ) ∨ (y = z) is at most Pcoll1rand(Z), assuming y and z are chosen randomly in

Z (y R ← Z; z R ← Z).
The annotation [random_choices_may_be_equal] means that the random choices y R ← Z and z R ← Z may be either independent or the same random choice. (Without this annotation, they would necessarily be independent.) Grouping the two cases in a single collision statement allows CryptoVerif to apply it even when it cannot determine whether the random choices are independent or identical: when x and y are two cells of the same array with indices that may be different or equal. In [START_REF] Bernstein | The Poly1305-AES message-authentication code[END_REF], when X = 0 or y = z, both sides are true. Suppose now that X = 0 and y = z. Then, y and z are independent random choices, and the right-hand side is false. The expressions differ when the left-hand side is true, that is, (y/k) • X = (z/k) • X, so y/k ≡ z/k mod q or y/k ≡ -z/k mod q when X = X 0 (Q) for Q on the curve and y/k ≡ z/k mod q or y/k ≡ -z/k mod q when X = X 0 (Q) for Q on the twist. Since q and q are greater than n max -n min and y/k and z/k are in S ⊆ {n min , . . . , n max }, the only possibility for y/k ≡ z/k mod q or y/k ≡ z/k mod q is y = z, which is excluded, and the equations y/k ≡ -z/k mod q and y/k ≡ -z/k mod q each have at most one solution for z once y is fixed, so they hold with probability at most Pcoll1rand(Z). Therefore, the two expressions differ with at most probability Pcoll1rand(Z).

Statement [START_REF] Bernstein | Curve25519: New Diffie-Hellman speed records[END_REF] means that the probability of distinguishing exp_div _k

(X, x) = Y from (X = zero sub ) ∧ (Y = zero sub ) is at most 2 × Pcoll1rand(Z) assuming x is chosen randomly in Z (x R ← Z
) and X and Y are independent of x. Indeed, suppose that exp_div _k (X, x) = Y differs from (X = zero sub ) ∧ (Y = zero sub ). If X = 0, then (x/k) • X = 0, so both expressions reduce to Y = 0, so they cannot differ. Therefore, X = 0. The second expression is then false. If (x/k) • X = Y , then Y = y • X for some y independent of x. Moreover x = kn for n ∈ S chosen randomly, and y is independent of n. The equality (x/k) • X = n • X = Y = y • X holds if and only if n ≡ y mod q or n ≡ -y mod q when X = X 0 (Q) for Q on the curve and n ≡ y mod q or n ≡ -y mod q when X = X 0 (Q) for Q on the twist. Each of these equations has at most one solution for n since q and q are greater than n max -n min , so there are at most two solutions for n Inria in total (for Curve25519, there are indeed two solutions for some values of y, due to the existence of equivalent private keys), hence the first expression (x/k) • X = Y is true with probability at most 2 × Pcoll1rand(Z), and the two expressions differ with at most that probability. The support for side-conditions in collision statements is an extension of CryptoVerif that we implemented.

In statement [START_REF] Bernstein | Extending the Salsa20 nonce[END_REF], when the equality exp_div _k (g_k , mult(x, y)) = X holds, we have X = exp_div _k (g_k , z) for some z ∈ Z independent of x. Hence, since g_k corresponds to a point on the curve, xy/k ≡ z/k mod q or xy/k ≡ -z/k mod q. Since y/k is prime to qq , so prime to q, y/k is invertible modulo q, so x ≡ z/y mod q or x ≡ -z/y mod q, and z/y is independent of x, so these equalities happen with probability at most 2 × Pcoll1rand(Z).

When x and y are independent, statement ( 8) is a consequence of statement [START_REF] Bernstein | Extending the Salsa20 nonce[END_REF]. Suppose that x and y are the same random choice: x = y. When the equality exp_div _k (g_k , mult(x, x)) = X holds, we have X = exp_div _k (g_k , z) for some z ∈ Z independent of x. Hence, since g_k corresponds to a point on the curve, x 2 /k ≡ z/k mod q or x 2 /k ≡ -z/k mod q, that is, x 2 ≡ z mod q or x 2 ≡ -z mod q, and z is independent of x. Each of these equations has at most 2 solutions for x, so these equalities happen with probability at most 4 × Pcoll1rand(Z). (Furthermore, for Curve25519, q ≡ 1 mod 4, so -1 is a square modulo q, hence both z and -z are squares simultaneously, so x 2 ≡ z mod q or x 2 ≡ -z mod q may have 4 solutions for x in total.) Statement (9) holds when y and y are the same random choice. When y and y are independent random choices and exp_div _k (g_k , mult(x, y)) = exp_div _k (g_k , mult(x, y )), since g_k corresponds to a point on the curve, we have xy/k ≡ xy /k mod q or xy/k ≡ -xy /k mod q. Since x is prime to qq , so prime to q, x is invertible modulo q, so y/k ≡ y /k mod q or y/k ≡ -y /k mod q. In the first case, since q is greater than n max -n min and y/k and y /k are in S ⊆ {n min , . . . , n max }, we have y = y . Hence the two sides of (9) differ only in the second case, which happens with probability less than Pcoll1rand(Z).

For simplicity, we omit 4 additional collision statements, which can be inferred from the ones above. CryptoVerif may be able to infer some of them automatically in the future. When CryptoVerif transforms a game using a Diffie-Hellman assumption, it renames exp_div _k into exp_div _k , in order to prevent the repeated application of the same game transformation. Hence, we define a symbol exp_div _k with the same equations and collision statements as exp_div _k .

This model is included as a macro in CryptoVerif's library of cryptographic primitives, so that it can easily be reused. Similar models also apply to other curves that have a similar structure, for instance Curve448 [START_REF] Langley | Elliptic curves for security[END_REF], which is also used by the Noise framework, and by other protocols like TLS 1.3. For Curve448, we have p = 2 448 -2 224 -1, k = k = 4, q = 2 446 -2 223 -δ with 0 < δ < 2 220 , q = 2 446 + δ, and the private keys are kn for n ∈ {2 445 , . . . , 2 446 -1}. We note the following differences with respect to Curve25519:

• Assumptions 1 to 8 are satisfied except that the elements of {2 445 , . . . , 2 446 -1} are not all prime to qq : q is in {2 445 , . . . , 2 446 -1}, so kq is a valid private key, and it is the only private key non-prime to qq . It is a weak private key in the sense that for all X that correspond to a point on the curve, (kq) • X = 0. Shared secrets generated using this private key are rejected when the participants verify that the shared secrets are non-zero. We first exclude this private key, which yields a probability difference of 1/2 445 = 2 -445 for each chosen private key, and then apply the previous results with S = {2 445 , . . . , 2 446 -1} \ {q}.

• q ≡ -1 mod 4, so -1 is not a square modulo q. Hence, in the proof of (8), the equalities x 2 ≡ z mod q and x 2 ≡ -z mod q cannot both have solutions for x for the same value of z. (Either z or -z is a square modulo q but not both.) Therefore, statement (8) can be strengthened by reducing the probability difference to 2 × Pcoll1rand(Z) instead of 4 × Pcoll1rand(Z).

We have also added to CryptoVerif's library of primitives the model for Curve448 outlined above, as well as a more general model that assumes neither that the private keys are prime to qq (eliminating weak private keys multiple of q or q as explained for Curve448), nor that q ≡ -1 mod 4. The latter model is sound for both Curve25519 and Curve448. We assume that G sub satisfies the gap Diffie-Hellman (GDH) assumption [START_REF] Okamoto | The gap-problems: a new class of problems for the security of cryptographic schemes[END_REF], in the following sense:

Definition 1 (Gap Diffie-Hellman). Given g that corresponds to a generator of the subgroup of order q of the curve and andb • g for random a, b ∈ E U , the adversary has a negligible probability to compute (ab) • g (computational Diffie-Hellman assumption), even when the adversary has access to decisional Diffie-Hellman oracles, which tell him

E U = {kn | n ∈ [(q + 1)/2, q -1]} considered modulo kqq , a • g,
• given U, V, W ∈ G sub , whether there exist β ∈ E U such that U = β • g, and W = β • V ; • given G, U, V, W ∈ G sub , whether there exist α, β ∈ E U such that G = α • g, U = β • g, and α • W = β • V .
Choosing the exponents in E U guarantees the unicity of β such that U = β • g (E stands for exponent, U for unique). Moreover, E U is close to the set of honestly generated exponents {kn | n ∈ S}: the statistical distance between the uniform distributions on these two sets is bounded by 2 -126 [1, Lemma 1]. The first decisional Diffie-Hellman oracle basically tells whether (U, V, W ) is a good Diffie-Hellman triple with generator g, and the second one basically tells whether (U, V, W ) is a good Diffie-Hellman triple with generator G, as we explain below. We need to separate the two oracles because there exists no α ∈ E U such that α • W = W for all W ∈ G sub . We use the formulation of Definition 1 for the decisional Diffie-Hellman oracles to accommodate elements V , W not necessarily in the group generated by g. When all elements are in the group generated by g of order q, we have for the first oracle U = u • g for u = β, V = v • g for some v so W = (uv) • g; and for the second oracle

U = u • G for u = β/α (since α is invertible modulo q) and V = v • G for some v, so α • W = β • V = (vβ) • G = (uvα) • G so W = (uv) • G, hence there exist u and v such that U = u • G, V = v • G, and W = (uv) • G. (U, V, W
) is then a good Diffie-Hellman triple with generator G. Note that we need the computational Diffie-Hellman assumption only for the curve, not for the twist, while the decisional Diffie-Hellman oracles may mix elements of the curve and of the twist: G and U always correspond to points of the curve, while V and W either correspond to points both on the curve or both on the twist. (If V corresponds to a point on the curve and W corresponds to a point on the twist, then β • V corresponds to a point on the curve and α • W corresponds to a point on the twist, so they cannot be equal except when V = W = 0.) This assumption was already modelled in CryptoVerif.

Interestingly, the obtained model is very similar to what we would obtain with the elliptic curve Curve25519 itself, without using a single coordinate ladder. In the latter case, G is the curve itself, a group of order kq. The base point g has prime order q; G sub is the prime order subgroup generated by g. The set Z is the set of integers multiple of k and prime to q, modulo kq. The operation y • X is point multiplication, the functions decode_pk and encode_pk are the identity. Then we have properties similar to Lemma 1, replacing qq with q: y • X is defined for y

∈ Z kq ; y • (z • X) = (yz) • X; for any z ∈ Z, X, Y ∈ G, we have z • X = z • Y if and only if k • X = k • Y (because z = kz
for some z invertible modulo q); for any z prime to q, for any

X, Y ∈ G sub , we have z • X = z • Y if and only if X = Y (because z is invertible modulo q).
Public keys X and Y are equivalent when k • X = k • Y , so each public key has k equivalent public keys, including itself. Similarly to the previous model, exp(X, y) = y • X, mult is the product modulo kq in Z, pow _k (X) = k • X, and exp_div _k (X, y) = (y/k) • X. The function G sub 2G maps each element of G sub to the same element in G. The constants zero in G and zero sub in Inria G sub represent the neutral element of G, that is, the point at infinity ∞. The properties of these functions and constants until (4) are proved similarly to the previous model, replacing qq with q. Let us solve the equation y

• X = z • X for X ∈ G sub . If X = ∞, then y • X = ∞ = z • X
for all y and z. Otherwise, X is a generator of G sub , so y • X = z • X if and only if y ≡ z mod q. As a result, we can strengthen (5) as follows:

equation forall X : G sub , y : Z, z : Z;

(exp_div _k (X, y) = exp_div _k (X, z)) = ((y = z) ∨ (X = zero sub )).

In the proof of ( 6), (x/k) • X = n • X = Y = y • X holds if and only if n ≡ y mod q, and the probability that the expressions differ is at most Pcoll1rand(Z) instead of 2 × Pcoll1rand(Z).

Due to the strengthened form of ( 5), equalities exp_div _k (g_k , y) = exp_div _k (g_k , z) are replaced with y = z. For this reason, we replace ( 7), [START_REF] Beurdouche | A messy state of the union: Taming the composite state machines of TLS[END_REF], and (9) with properties on private keys. Statement [START_REF] Bernstein | Extending the Salsa20 nonce[END_REF] becomes:

collision x R ← Z; forall y : Z, z : Z; return(mult(x, y) = z) ≈ Pcoll1rand(Z) return(false) if y independent-of x ∧ z independent-of x
since mult(x, y) = z means xy ≡ z mod kq, so xy/k ≡ z/k mod q and y is invertible modulo q, so x/k ≡ z/ky mod q, so x ≡ z/y mod kq. Since z/y is independent of x, the equality x ≡ z/y mod kq has probability at most Pcoll1rand(Z) to happen. Statement (8) becomes:

collision x R ← Z; y R ← Z; [random_choices_may_be_equal] forall z : Z; return(mult(x, y) = z) ≈ 2×Pcoll1rand(Z) return(false) if z independent-of x ∨ z independent-of y.
When x and y are independent, this statement is a consequence of the previous one. When they are the same random choice, x = y, and mult(x, x) = z implies x 2 ≡ z mod kq, so x 2 /k ≡ z/k mod q so (x/k) 2 ≡ z/k 2 mod q since k is invertible modulo q, and the probability that the expressions differ is at most 2 × Pcoll1rand(Z) instead of 4 × Pcoll1rand(Z) since each element has at most 2 square roots modulo q. The increased probability that we observe in the model with single coordinate ladder in the previous collision statements comes from the existence of equivalent private keys. Statement (9) becomes equation forall x : Z, y : Z, y : Z; (mult(x, y) = mult(x, y )) = (y = y ) since mult(x, y) = mult(x, y ) means xy ≡ xy mod kq, so xy/k ≡ xy /k mod q, so y/k ≡ y /k mod q since x is invertible modulo q, so y ≡ y mod kq, that is, y = y in Z. Finally, the GDH assumption is needed only in the subgroup G sub , so the twist is excluded. This model is presented in the conference version of this work [START_REF] Lipp | A mechanised cryptographic proof of the WireGuard virtual private network protocol[END_REF], where we unfortunately overlooked that Curve25519 implementations use a single coordinate ladder. To sum up, the main difference with the model using a single coordinate ladder is that some collisions have a slightly higher probability with a single coordinate ladder. Hence, in practice, using a single coordinate ladder has little impact on security.

In their cryptographic proof of WireGuard, Dowling and Paterson [START_REF] Dowling | A cryptographic analysis of the WireGuard protocol[END_REF] use the PRF-ODH assumption. We use the GDH and random oracle assumptions instead because CryptoVerif cannot currently use the PRF-ODH assumption in scenarios with key compromise. While in principle the PRF-ODH assumption is weaker, Brendel et al. [START_REF] Brendel | PRF-ODH: Relations, instantiations, and impossibility results[END_REF] show that it is implausible to instantiate the PRF-ODH assumption without a random oracle, so our assumptions and the one of [START_REF] Dowling | A cryptographic analysis of the WireGuard protocol[END_REF] are in fact fairly similar.

Indifferentiability of Hash Chains

Before modelling WireGuard, we first present a different, equally precise, formulation of hash chains that is more amenable to a mechanised proof in CryptoVerif. Indeed, WireGuard makes many hash oracle calls to BLAKE2s, and at each call to a random oracle, CryptoVerif tests whether the arguments are the same as in any other previous random oracle call (to return the previous result of the random oracle). Therefore, using directly BLAKE2s as a random oracle would introduce a very large number of cases and yield exaggeratedly large cryptographic games. In order to avoid that, we simplify the random oracle calls using indifferentiability lemmas. These lemmas are not specific to WireGuard and can be used to simplify sequences of random oracle calls in other protocols, including other Noise protocols and Signal [START_REF] Marlinspike | The X3DH key agreement protocol[END_REF]. In the future, these lemmas may serve as a basis for an indifferentiability prover inside CryptoVerif, which would simplify random oracle calls before proving the protocol.

Specifically, WireGuard uses HKDF in a chain of calls to derive symmetric keys at different stages of the protocol:

C 0 ← const C 1 ← hkdf 1 (C 0 , v 0 ) C 2 k 1 ← hkdf 2 (C 1 , v 1 ) C 3 k 2 ← hkdf 2 (C 2 , v 2 ) C 4 ← hkdf 1 (C 3 , v 3 ) C 5 ← hkdf 1 (C 4 , v 4 ) C 6 ← hkdf 1 (C 5 , v 5 ) C 7 π k 3 ← hkdf 3 (C 6 , v 6 ) T → T ← ← hkdf 2 (C 7 , v 7 )
We show, using the indifferentiability lemmas of this section, that hkdf n is indifferentiable from a random oracle, and that the chain above is indifferentiable from:

k 1 ← chain 1 (v 0 , v 1 )
k 2 ← chain 2 (v 0 , v 1 , v 2 ) ( 10
)
π k 3 T → T ← ← chain 6 (v 0 , v 1 , v 2 , v 3 , v 4 , v 5 , v 6 )
where chain 1 , chain 2 , and chain 6 are independent random oracles. Thus, we obtain a much simpler computation, which we use in our CryptoVerif model of WireGuard. Previous analyses of WireGuard did not use such a result because they do not rely on the random oracle model: [START_REF] Dowling | A cryptographic analysis of the WireGuard protocol[END_REF] relies on the PRF-ODH assumption, [START_REF] Donenfeld | Formal verification of the WireGuard protocol[END_REF] uses the symbolic model.

Definition of Indifferentiability

Indifferentiability can be defined as follows. This definition is an extension of [START_REF] Coron | Merkle-Damgård revisited: How to construct a hash function[END_REF] to several independent oracles.

Definition 2 (Indifferentiability). Functions (F i ) 1≤i≤n with oracle access to independent random oracles (H j ) 1≤j≤m are (t D , t S , (q Hj ) 1≤j≤m , (q Fi ) 1≤i≤n , (q H i ) 1≤i≤n , )-indifferentiable from independent random oracles (H i ) 1≤i≤n if there exists a simulator S such that for any distinguisher

D | Pr[D (Fi) 1≤i≤n ,(Hj ) 1≤j≤m = 1] -Pr[D (H i ) 1≤i≤n ,S = 1]| ≤ Inria
The simulator S has oracle access to (H i ) 1≤i≤n , makes at most q H i queries to H i , and runs in time t S . The distinguisher D runs in time t D and makes at most q Hj queries to H j for 1 ≤ j ≤ m and q Fi queries to F i for 1 ≤ i ≤ n.

In the game G 0 = D (Fi) 1≤i≤n ,(Hj ) 1≤j≤m , the distinguisher interacts with the real functions F i and the random oracles H j from which the functions F i are defined. In the game G 1 = D (H i ) 1≤i≤n ,S , the distinguisher interacts with independent random oracles H i instead of F i , and with a simulator S, which simulates the behaviour of the random oracles H j using calls to H i . (We may also present S as m simulators S j that each simulate a single random oracle H j using calls to H i , 1 ≤ i ≤ n; these simulators share a common state.) Indifferentiability means that these two games are indistinguishable.

Basic Lemmas

In this section, we show several basic indifferentiability lemmas, which are not specific to WireGuard. The proofs that are not included in this section can be found in the appendix. Lemma 2 shows that random oracle calls with disjoint domains are indifferentiable from calls to independent random oracles.

Lemma 2 (Version of [27, Lemma 2] with more precise evaluation of numbers of oracle calls). If H is a random oracle, then the functions H 1 , . . . , H n defined as H on disjoint subsets D 1 , . . . , D n of the domain D of H are (t D , t S , q H , (q Hi ) 1≤i≤n , (q Hi ) 1≤i≤n , 0)-indifferentiable from independent random oracles, where t S = O(q H ) assuming one can determine in constant time to which subset D i an element belongs, and q Hi is the number of requests to H in domain D i made by the distinguisher. Hence q H1 + • • • + q Hn ≤ q H , so in the worst case q Hi is bounded by q H . Lemma 3 shows that the concatenation of two independent random oracle calls is indifferentiable from a random oracle. Lemma 3. If H 1 and H 2 are independent random oracles with the same domain that return bitstrings of length l 1 and l 2 respectively, then the concatenation H of H 1 and H 2 is (t D , t S , (q H1 , q H2 ), q H , q H1 + q H2 , 0)-indifferentiable from a random oracle, where t S = O(q H1 + q H2 ).

Conversely, Lemma 4 shows that splitting the output of a random oracle into two fixed length outputs yields independent random oracles. Lemma 4. If H is a random oracle that returns bitstrings of length l, then the function H 1 returning the first l 1 bits of H and the function H 2 returning the last l -l 1 bits of H are (t D , t S , q H , (q H 1 , q H 2 ), (q H , q H ), 0)-indifferentiable from independent random oracles, where t S = O(q H ).

As a particular consequence, Lemma 5 shows that the truncation of a random oracle is indifferentiable from a random oracle.

Lemma 5 (Already stated in [27, Lemma 3]). If H is a random oracle that returns bitstrings of length l, then the truncation H of H to length l < l is (t D , t S , q H , q H , q H , 0)-indifferentiable from a random oracle, where t S = O(q H ).

Lemmas 6 and 7 deal with the composition of two random oracle calls in sequence. We extended CryptoVerif to be able to prove indistinguishability between two games given by the user. Thanks to this extension, CryptoVerif helps considerably with the proof of these lemmas: it shows the indistinguishability result between the games G 0 and G 1 described in Section 4.1, which implies the indifferentiability result. We present the proof of Lemma 6 as an illustration. Lemma 6. If H 1 : S 1 → S 1 and H 2 : S 1 × S 2 → S 2 are independent random oracles, then H 3 defined by H 3 (x, y) = H 2 (H 1 (x), y) is (t D , t S , (q H1 , q H2 ), q H3 , q H2 , )-indifferentiable from a random oracle, where t S = O(q H1 q H2 ) and = (2q H2 q H1 + q 2 H1 + q H2 q H3 + q 2 H3 )/|S

(x) = H 2 (H 1 (x),
x) are (t D , t S , (q H1 , q H2 ), (q H 1 , q H 2 ), (q H1 + q H2 , q H2 ), )indifferentiable from independent random oracles, where t S = O(q H2 ) and = q H2 (2q

H1 + 2q H 1 + q H 2 + 1)/|S 1 |.

Indifferentiability of HKDF

The hkdf key derivation function is defined as follows [START_REF] Krawczyk | HMAC-based extract-and-expand key derivation function (HKDF)[END_REF]:

hkdf-extract(salt, key) = hmac(salt, key) hkdf-expand n (prk , info) = k 1 . . . k n
where

k 1 = hmac(prk , info i 0 ) k i+1 = hmac(prk , k i info i + i 0 ) for 1 ≤ i < n hkdf n (salt, key, info) = hkdf-expand n (hkdf-extract(salt, key), info)
where n ≤ 255, and i 0 = 0x01 and i are of size 1 byte. In WireGuard, info is always empty, so we omit it in Section 2. Let S, K, and I be the sets of possible values of salt, key, and info respectively, and M the output of hmac.

We suppose that hmac is a random oracle, and we show that hkdf-expand n is indifferentiable from a random oracle. Lemma 8. If hmac is a random oracle, then hkdf-expand n is (t D , t S , q hmac , q hkdf-expand n , q hmac , )-indifferentiable from a random oracle, where t S = O(q hmac ) and = (3q hkdf-expand n q hmac + q 2 hmac )/|M|. Using this result, we show that hkdf n is indifferentiable from a random oracle, with the additional assumption that the calls to hmac use disjoint domains. (We show that this assumption is necessary and give full proofs of these results in the appendix.) Lemma 9. If hmac is a random oracle and K ∩ (I i 0 ∪ n-1 i=1 M I i + i 0 ) = ∅, then hkdf n with domain S × K × I is (t D , t S , q hmac , q hkdfn , q hmac , )-indifferentiable from a random oracle, where t S = O(q 2 hmac ) and = (q 2 hkdfn + 4q hkdfn q hmac + q 2 hmac )/|M|. This result extends the proof given for hkdf 2 in [27, Lemma 1]. Moreover, our proof is modular and partly made using CryptoVerif, thanks to the basic lemmas of Section 4.2.

Inria

Proof sketch. Since the domains are disjoint, by Lemma 2, the (n + 1) calls to hmac are indifferentiable from independent random oracles H 0 , . . . , H n . The constant i + i 0 can be removed from the arguments of H i+1 since it is fixed for a given H i+1 . By Lemma 7, the computation of k 2 = H 2 (H 1 (prk , info), prk , info) is indifferentiable from a random oracle k 2 = H 2 (prk , info). Applying this reasoning n times, the computation of k i for 1 ≤ i ≤ n is indifferentiable from independent random oracles k i = H i (prk , info). By Lemma 3, concatenation of H i for 1 ≤ i ≤ n is indifferentiable from a random oracle H, so hkdf n (salt, key, info) = k 1 . . . k n = H(prk , info), where prk = H 0 (salt, key). By Lemma 6, we conclude that hkdf n is indifferentiable from a random oracle.

Indifferentiability of a Chain of Random Oracle Calls

In this section, we prove the indifferentiability of a chain of random oracle calls defined as follows.

Definition 3 (Chain). Let m ≥ 1 be a fixed integer, let C and C j with 0 ≤ j ≤ m + 1 be bitstrings of length l , let v j with 0 ≤ j ≤ m be bitstrings of arbitrary length, let l be the length of the output of H(C j , v j ), and let r j with 0 ≤ j ≤ m be bitstrings of length (l -l ). We define the functions chain n , 0 ≤ n < m and the function chain m in the following way:

chain n (v 0 , . . . , v n ) = C 0 = const for j = 0 to n do C j+1 r j = H(C j , v j ) return r n (11)
chain m (v 0 , . . . , v m ) = C 0 = const for j = 0 to m do C j+1 r j = H(C j , v j ) return C m+1 r m (12)
The functions chain n , n < m, have an output of length (l -l ), and the output length of chain m is l.

Lemma 10. If H is a random oracle, then chain n , for n ≤ m, are (t D , t S , q H , (q chainn ) 0≤n≤m , (q H ) 0≤n≤m , )-indifferentiable from independent random oracles, where t S = O(q 2 H ) and = (

m n=0 n • q chainn ) • q H + q 2
H /2 l . This lemma is proved in the appendix. We could probably prove it for small values of m using CryptoVerif, but the generic result requires a manual proof because CryptoVerif does not support loops.

Application to WireGuard

WireGuard employs BLAKE2s [START_REF] Aumasson | BLAKE2: Simpler, smaller, fast as MD5[END_REF] both directly as the function hash and indirectly as hash function in hmac and thus also in hkdf. In our proof, we assume that hash is collisionresistant and use the random oracle assumption for usages of BLAKE2s via hkdf. Rigorously, to be able to use two distinct assumptions, we need the domains of these two uses to be disjoint. This is true in WireGuard: the length of the argument of hash is 64 bytes for hash(H 0 S pub r ), hash(H 1 E pub i ), hash(H 4 E pub r ), and hash(H 5 π), 80 bytes for hash(H 2 S pub i ), 60 bytes for hash(H 3 ts ), 48 bytes for hash(H 6 empty ), 40 bytes for hash(label mac1 S pub r ), hash(label mac1 S pub i ), and hash(label cookie S pub m ). In contrast, the length of the argument of BLAKE2s in hmac(k, m) is 96 bytes or 64 + length(m), and in the computation of hkdf, info is empty in WireGuard, so the length of m is 32 bytes (key), 1 byte (info i 0 ) or 33 bytes (k i info i + i 0 ), so the length of the argument of BLAKE2s in the computation of hkdf is 96, 65, or 97 bytes.

Then by Lemma 2, we can consider two independent random oracles, hash for the direct uses and hash for the uses via hkdf. Since hash is a random oracle, it is a fortiori collision-resistant.

Since hash is a random oracle, hmac-hash is indifferentiable from a random oracle by [START_REF] Dodis | To hash or not to hash again? (in)differentiability results for H 2 and HMAC[END_REF]Theorem 3].

Moreover, the domains of the calls to hmac in hkdf n are disjoint. Indeed, K consists of bitstrings of length 32 bytes, I i 0 consists of bitstrings of length 1 byte, and M I i + i 0 consists of bitstrings of length 33 bytes. By Lemma 9, hkdf n is indifferentiable from a random oracle.

In this section, we use the operator to concatenate blocks of 32 bytes and the placeholder _ for one unnamed 32-byte block. Since we prove Lemma 10 for a chain of calls to the same hkdf n function, we rewrite the chain of hkdf calls in WireGuard to use only calls to hkdf 3 , as 3 is the maximum number of outputs needed:

C 0 ← const C 1 _ _ ← hkdf 3 (C 0 , v 0 ) C 2 k 1 _ ← hkdf 3 (C 1 , v 1 ) C 3 k 2 _ ← hkdf 3 (C 2 , v 2 ) C 4 _ _ ← hkdf 3 (C 3 , v 3 ) C 5 _ _ ← hkdf 3 (C 4 , v 4 ) C 6 _ _ ← hkdf 3 (C 5 , v 5 ) C 7 π k 3 ← hkdf 3 (C 6 , v 6 ) T → T ← _ ← hkdf 3 (C 7 , v 7 )
Because of the way hkdf n is constructed, this is actually the same computation. By Lemma 10, the computation above can be replaced with the following one:

_ _ ← chain 0 (v 0 ) k 1 _ ← chain 1 (v 0 , v 1 ) k 2 _ ← chain 2 (v 0 , v 1 , v 2 ) _ _ ← chain 3 (v 0 , v 1 , v 2 , v 3 ) _ _ ← chain 4 (v 0 , v 1 , v 2 , v 3 , v 4 ) _ _ ← chain 5 (v 0 , v 1 , v 2 , v 3 , v 4 , v 5 ) π k 3 ← chain 6 (v 0 , v 1 , v 2 , v 3 , v 4 , v 5 , v 6 ) T → T ← _ ← chain 7 (v 0 , v 1 , v 2 , v 3 , v 4 , v 5 , v 6 , v 7 )
where chain i for i ≤ 7 are independent random oracles. The output of the random oracles can be truncated by Lemma 5 to avoid having to throw away parts of the output:

k 1 ← chain 1 (v 0 , v 1 ) k 2 ← chain 2 (v 0 , v 1 , v 2 ) π k 3 ← chain 6 (v 0 , v 1 , v 2 , v 3 , v 4 , v 5 , v 6 ) T → T ← ← chain 7 (v 0 , v 1 , v 2 , v 3 , v 4 , v 5 , v 6 , v 7 )
Inria where chain 1 , chain 2 , chain 6 , and chain 7 are independent random oracles. In WireGuard, v 7 = empty, so T → and T ← only depend on v 0 , . . . , v 6 , as do π and k 3 in the previous line. By Lemma 3, we can replace the last two lines with one random oracle call:

k 1 ← chain 1 (v 0 , v 1 ) k 2 ← chain 2 (v 0 , v 1 , v 2 ) π k 3 T → T ← ← chain 6 (v 0 , v 1 , v 2 , v 3 , v 4 , v 5 , v 6 )
where chain 1 , chain 2 , and chain 6 are independent random oracles.

Modelling WireGuard

This section presents our model of the WireGuard protocol in CryptoVerif. We prove security properties for that model in Section 6.

Execution Environment

In our model, we consider two honest entities A and B. In the initial setup, we generate the static key pairs for these two entities and publish their public keys, so that the adversary can use them. After this setup, we run parallel processes that represent a number of executions of A and B polynomial in the security parameter.

The entities A and B can play both the initiator and responder role. These two entities can run WireGuard between each other, but also with any number of dishonest entities included in the adversary: for each session, the adversary sends to the initiator its partner public key, that is, the public key of the entity with which it should start a session; the adversary sends to the responder the set of partner public keys that it accepts messages from.

This setting allows us to prove security for any sessions between two honest entities, in a system that may contain any number of (honest or dishonest) other entities. We prove security for sessions in which A is the initiator and B is the responder. We do not explicitly prove security for sessions in which B is the initiator and A is the responder, but the same security properties hold by symmetry.

The processes for the entities A and B model the entire protocol, including the first two protocol messages, the key confirmation message from the initiator, and then a number of transport data messages polynomial in the security parameter, in both directions between initiator and responder. The model also includes random oracles, and we allow the adversary to call any of the random oracles that we use.

We consider 3 variants of this model:

Variant 1. This variant does not rely at all on the pre-shared key for proving security, so A and B receive a pre-shared key chosen by the adversary at the beginning of each execution. That allows the adversary to model both the absence of a pre-shared key (by choosing the value 0) or a compromised pre-shared key of its choice. We model the dynamic compromise of the private static key of A (resp. B) by a process that the adversary can call at any time and that returns the private key of A (resp. B) and records the compromise by defining a particular variable, so that it can be tested in the security properties that we consider.

In WireGuard, four Diffie-Hellman operations and the pre-shared key contribute to the session keys. If the pre-shared key is not used or compromised, security is based on the four Diffie-Hellman operations. If one of them cannot be computed by the adversary, then the session keys are secret. Therefore, we consider all combinations of compromises but those where both keys on one side are compromised, that is:

1. A and B's private static keys may be dynamically compromised; 2. A's private static key may be dynamically compromised and B's private ephemeral key is compromised (by sending it to the adversary as soon as it is chosen);

3. B's private static key may be dynamically compromised and A's private ephemeral key is compromised;

4. A and B's private ephemeral keys are compromised.

We prove most security properties for clean sessions, that is, intuitively, sessions between honest entities; cleanliness is the minimal assumption needed to hope for security. A session of A is clean when either B's private static key is not compromised yet and A's partner public key is equivalent to B's static public key, or B's private static key is compromised and the public ephemeral key received by A is equivalent to a non-compromised ephemeral generated by B. B's session cleanliness is defined symmetrically. Intuitively, when B's private static key is not compromised, A can rely on that key to authenticate B, so A thinks she talks to B when she runs a session with B's public key. We consider a public key equivalent to B's public key rather than equal to B's public key to strengthen the properties: the authentication property shown in Section 6 then implies that when A successfully runs a session with a partner public key equivalent to B's public key, then these two keys are in fact equal. (We find an interesting scenario concerning equivalent public keys and identity mis-binding with variant 3 of our model, we discuss it in §6.) When B's private static key is compromised, A cannot authenticate B, but we can still prove security when the ephemeral key received by A has been generated by B. Like for static keys, when A successfully runs a session with a received ephemeral equivalent to an ephemeral generated by B, then these two ephemerals are in fact equal. (Instead of considering compromised ephemeral keys, we could also have modelled dishonestly generated ephemeral keys. We expect that some properties shown in §6, such as session uniqueness, would not hold in this case.)

Variant 2. This variant relies exclusively on the pre-shared key for security. In that variant, we consider all private static and ephemeral keys as always compromised. We choose a pre-shared key randomly in the initial setup, and run sessions between A and B with that pre-shared key. In this model, A's partner public key is always B's public key and symmetrically, and these sessions between A and B are always considered clean. The adversary can run A's and B's sessions with other entities since A and B's private static keys are compromised and these sessions use a different pre-shared key.

Variant 3. In this variant, all keys are compromised: all private static and ephemeral keys are always compromised and the pre-shared key is chosen by the adversary for each session. This model is useful for proving properties that do not rely on session cleanliness, that is, properties that hold even for sessions involving dishonest participants.

With this model, we analyse the whole WireGuard protocol as it is, tying together the authenticated key exchange and the transport data phase. A similar approach was chosen by the creators of the Authenticated and Confidential Channel Establishment (ACCE) [START_REF] Jager | On the security of TLS-DHE in the standard model[END_REF] model to analyse TLS.

Instead of reasoning about key indistinguishability, ACCE looks at the security of the messages exchanged encrypted using the key. We do the same, for the key confirmation and all subsequent transport data messages.

Inria

In ACCE, the adversary has to choose one clean test session in which it tries to break security by determining the secret bit. In all other sessions, it is allowed to reveal the session keys. In our model, all clean sessions are test sessions, and we explicitly reveal the session keys in sessions that are not clean.

Modelling Tricks

Apart from the HKDF chains where we prove that the way we model them is indifferentiable from the real protocol in Section 4, we use the following modelling tricks:

• 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.

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, rcvd_msg_responder, and rcvd_msg_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 5.

E pub r , empty , T → , T ← , N → , P , P )) ,
We also prove a third query (similar to the second one above) for transport data messages in the other direction, with events rcvd_msg_initiator and sent_msg_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 5.1). They also hold when neither both S priv i and E priv i nor both S priv r and E priv r 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 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 priv r ) 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.

Inria

CryptoVerif proves the secrecy of that bit, in variants 1 and 2 of Section 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 priv i and E priv i nor both S priv r and E priv r 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 priv i were compromised, the adversary can impersonate the initiator as the sender of this message. If S priv r 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:

inj-event(rcvd1(true, S pub r , E pub i , S pub i , S pub i , ts , ts)) ⇒ inj-event(sent1( S pub r , E pub i , S pub i , S pub i , ts , ts)) .
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:

event(responder_corr(E pub i , S pub i , ts , E pub r , empty , T → r , T ← r , H r7 )) ∧ event(initiator_corr(E pub i , S pub i , ts , E pub r , empty , T → i , T ← i , H i7 )) ⇒ T → i = T → r ∧ T ← i = T ← r ∧ H i7 = H r7 .
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 → or T ← . The query below shows that there cannot be two distinct initiator sessions with the same T → :

event(initiator_uniq_T → (i i , T → )) ∧ event(initiator_uniq_T → (i i , T → )) ⇒ i i = i i ,
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 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:

event(initiator_H7(params, H 7 )) ∧ event(responder_H7(params , H 7 )) ⇒ params = params
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 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 Inria and static keys used in that session. This is formalised by the following query:

event(responder_imb(T → , T ← , E pub i,rcvd , E pub r , S pub i,rcvd , S pub r )) ∧ event(initiator_imb(T → , T ← , E pub i , E pub r,rcvd , S pub i , S pub r,rcvd )) ⇒ E pub i = E pub i,rcvd ∧ E pub r = E pub r,rcvd ∧ S pub i = S pub i,rcvd ∧ S pub r = S pub r,rcvd .
CryptoVerif proves it in variant 1 of our model, so it holds when neither both S priv . This is possible because S priv r is compromised. In this session, the adversary acts as responder, and because the ephemeral is also compromised, gets A's E priv i .

• The adversary now acts as initiator to start a session with B using a public static key S pub i equivalent to the honest initiator public static key:

pow _k (S pub i ) = pow _k (S pub i ) but S pub i = S pub i
. This is possible because S priv i is compromised. The adversary uses E priv i as ephemeral. The ephemeral of this session is also compromised, so the adversary gets E priv r .

• The adversary continues the session with A using the ephemeral E priv r . 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 pub r ) and with B (presenting itself with S pub i ). The session keys T → and T ← for these two sessions are computed as hashes of E pub i , dh(E priv i , S pub r ), dh(S priv i , S pub r ), E pub r , dh(E priv i , E pub r ), dh(S priv i , E pub r ), 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 [START_REF] Chen | Bilateral unknown key-share attacks in key agreement protocols[END_REF] and of a key synchronisation attack [START_REF] Bhargavan | Triple handshakes and cookie cutters: Breaking and fixing authentication over TLS[END_REF]. 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 7.

Resistance against DoS. As described in Section 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 τ = mac(R r , A i ) upon receipt of messages 1 from A i with zero mac 2 , and verifies mac 2 upon receipt of messages 1 with non-zero mac 2 . 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 τ , 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:

event(accepted_cookie(A i , i r , τ, msg β , mac 2 )) ⇒ event(generated_cookie(A i , i r , τ )) ,
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 pseudo-random function (PRF).

Identity Hiding. When the adversary has a candidate public key S pub Y , it can determine whether this public key is involved in WireGuard sessions, as already mentioned in the WireGuard specification [START_REF] Donenfeld | WireGuard: Next generation kernel network tunnel[END_REF]. In the first message, it can test whether mac 1 = mac(hash(label mac1 S pub Y ), msg α ) and that reveals whether S pub Y = S pub r . A similar test on message 2 reveals whether S pub Y = S pub i . When an entity with public key S pub m sends a cookie reply, the adversary can try to decrypt the encrypted cookie τ with the key hash(label cookie S pub Y ), 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 pub Y = S pub m . 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 pub i , that is, hash(hash(H 0 S pub r ) E pub i ). It can compare this value with hash(hash(H 0 S pub Y ) E pub i ) since E pub i
is sent in the first message and H 0 is a constant. Thus, it can determine whether S pub r = S pub Y . 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 pub A1 , S pub A2 , S pub B1 , S pub B2 cannot distinguish a configuration in which the entity with public key S pub A1 initiates sessions with S pub B1 from one in which the entity with public key S pub A2 initiates sessions with S pub B2 . 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 [START_REF] Procter | A security analysis of the composition of ChaCha20 and Poly1305[END_REF].

We discuss possible solutions to strengthen the identity hiding for the protocol with MACs in Section 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.

Inria 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.) 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";

In the instruction above, 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\\[. (\\[ 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 pub i . 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: The construct find i <= N suchthat 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:

insert after_nth 2 "in(c_resp2init_recv\\[" "find j <= N_resp_parties suchthat defined(E_r_pub[j]) && pow_k(E_r_pub_rcvd_2) = pow_k(E_r_pub[j]) then"; insert after_nth 1 "in(c_resp2init_recv\\[" "find j <= N_resp_parties suchthat 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 simplify;

Then, we apply the random oracle assumption for the 3 random oracles chain 6 , chain 2 , chain 1 (named rom3_intermediate, rom2_intermediate, and 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 sub ), we distinguish whether the argument received by the random oracle from the adversary is in G sub before applying the random oracle assumption. (When it is not in G sub , it cannot collide with a call coming from the protocol.) This is done by the following instructions: The first case distinction distinguishes whether the argument x_rom3 of rom3_intermediate is of the form rom3_input(x1_rom3, Gsub_to_G(x2_rom3), Gsub_to_G(x3_rom3), x4_rom3, Gsub_to_G(x5_rom3), Gsub_to_G(x6_rom3), v_psk), that is, a tuple in which the 2nd, 3rd, 5th, and 6th components are in G sub . The next instruction applies the random oracle assumption to rom3_intermediate. The other two random oracles are handled similarly.

Next, we apply the gap Diffie-Hellman assumption to the function 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: Inria 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(concat_four_keys) **;

The indication ** means that we apply splitter(concat_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. splitter(concat_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_ctxt(enc) *;

The indication * means that we apply int_ctxt(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_ctxt_corrupt(enc) 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_ctxt_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.

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.

Inria

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 key 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 [START_REF] Donenfeld | WireGuard: Next generation kernel network tunnel[END_REF]. 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. [START_REF] Blanchet | Security protocol verification: Symbolic and computational models[END_REF]). CryptoVerif itself has been used to analyse modern protocols like Signal [27] and TLS 1.3 [9]. We conclude this paper by comparing our results with closely related work; Table 1 provides a condensed, high-level overview.

WireGuard itself has been formally analysed before. Donenfeld et al. [START_REF] Donenfeld | Formal verification of the WireGuard protocol[END_REF] symbolically analyse the IKpsk2 key exchange protocol used by WireGuard for a number of security goals, including identity mis-binding and identity hiding. 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 [START_REF] Cremers | Prime, order please! revisiting small subgroup and invalid curve attacks on protocols using Diffie-Hellman[END_REF]. It could probably be used to improve the symbolic analysis of WireGuard. Dowling et al. [START_REF] Dowling | A cryptographic analysis of the WireGuard protocol[END_REF] 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 x 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.

Inria 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, [START_REF] Dowling | A cryptographic analysis of the WireGuard protocol[END_REF] 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 [START_REF] Kobeissi | Noise Explorer: Fully automated modeling and verification for arbitrary Noise protocols[END_REF] 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 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 [START_REF] Girol | Formalizing and verifying the security protocols from the Noise framework[END_REF][START_REF] Suter-Dörig | Formalizing and verifying the security protocols from the Noise framework[END_REF].

A Indifferentiability Results

A.1 Basic Lemmas

(x) = H i (x) if x ∈ D i for some i ≤ n, and H(x) = H 0 (x) otherwise, where H 0 is a random oracle of domain D \ (D 1 ∪ • • • ∪ D n ).
It is easy to see that these two games are perfectly indistinguishable, which proves indifferentiability.

Proof of Lemma 3. Consider

• the game G 0 in which H 1 and H 2 are independent random oracles, and H (x) = H 1 (x) H 2 (x), and

• the game G 1 in which H is a random oracle that returns bitstrings of length l 1 + l 2 , H 1 (x) is the l 1 first bits of H (x) and H 2 (x) is the l 2 last bits of H (x).

It is easy to see that these two games are perfectly indistinguishable, which proves indifferentiability.

Proof of Lemma 4. Consider

• the game G 0 in which H is a random oracle, H 1 (x) is the first l 1 bits of H(x), and H 2 (x) is the last l -l 1 bits of H(x), and

• the game G 1 in which H 1 and H 2 are independent random oracles that return bitstrings of length l 1 and l -l 1 respectively, and

H(x) = H 1 (x) H 2 (x).
It is easy to see that these two games are perfectly indistinguishable, which proves indifferentiability.

(It is the same indistinguishability result as in Lemma 3, swapping G 0 and G 1 .)

Proof of Lemma 5. This is a consequence of Lemma 4, by not giving access to oracle H 2 to the distinguisher (so q H 2 = 0). H 2 is then included in the simulator. We assume that random oracles answer in constant time. CryptoVerif shows that these two games are indistinguishable, up to probability . (The oracles H 1 and H 1 are considered as a single oracle, which receives q H1 + q H 1 queries in total.)

A.2 Indifferentiability of HKDF

Much like for HMAC in [START_REF] Dodis | To hash or not to hash again? (in)differentiability results for H 2 and HMAC[END_REF] and as mentioned in [27], hkdf n is not indifferentiable from a random oracle in general. Intuitively, the problem comes from a confusion between the first and the second (or third) call to hmac, which makes it possible to generate prk by calling hkdf 2 rather than hmac. In more detail, let

prk _ = hkdf 2 (s, k, info) salt = hmac(s, k) x = hmac(prk , info i 0 ) x _ = hkdf 2 (salt, info i 0 , info )
where the notation x 1 x 2 = hkdf 2 (s, k, info) denotes that x 1 consists of the first 256 bits of hkdf 2 (s, k, info) and x 2 its last 256 bits. When hkdf 2 is defined from hmac as above, we have prk = hmac(prk , info i 0 ) where prk = hmac(s, k) = salt, so prk = hmac(salt, info i 0 ). Hence, x = hmac(prk , info i 0 ) = x. However, when hkdf 2 is a random oracle and hmac is defined from hkdf 2 , the simulator that computes hmac sees what seems to be two unrelated calls to hmac. (It is unable to see that prk is in fact related to the previous call salt = hmac(s, k): we have prk _ = hkdf 2 (s, k, info) but the simulator does not know which value of info it should use.) Therefore, the simulator can only return fresh random values for salt and x, and x = x in general.

Proof of Lemma 8. In this proof, we write S[H 1 , . . . , H n ] instead of S H1,...,Hn for a system S with oracle access to H 1 , . . . , H n , because we need to write systems in which the oracles are themselves systems that access other oracles. Consider the game G 0 in which hmac is a random oracle and hkdf-expand n is defined as above.

The different calls to hmac in the definition of hkdf-expand n use disjoint domains (the last byte differs among the calls to hmac), so by Lemma 2, there exists a simulator S 1 for hmac such that G 0 is perfectly indistinguishable from G 1 in which hmac = S 1 [H 1 . . . , H n ] and hkdf-expand n is defined by

hkdf-expand 1 n (prk , info) = k 1 . . . k n where k 1 = H 1 (prk , info) k i+1 = H i+1 (prk , k i info) for 1 ≤ i < n
where H 1 , . . . , H n are independent random oracles and the simulator S 1 calls H i at most q Hi times, with q H1 + • • • + q Hn ≤ q hmac , and runs in time O(q hmac ).

Slightly reorganising the arguments of H i , there exists a simulator S 2 for hmac such that G 1 is perfectly indistinguishable from G 2 in which hmac = S 2 [H 1 , . . . , H n ] and hkdf-expand n is defined by hkdf-expand 2 n (prk , info) = k 1 . . . k n where k 1 = H 1 (prk , info)

k i+1 = H i+1 (k i , prk , info) for 1 ≤ i < n
where H 1 , . . . , H n are independent random oracles and the simulator S 2 calls H i at most q Hi times, with q H1 + • • • + q Hn ≤ q hmac , and runs in time O(q hmac ).

By Lemma 7, there exists a simulator S 3,2 for H 2 (H 1 is simulated by

H 1 = H 1 itself) such that G 2 = G 3,
k i+1 = H i+1 (k i , prk , info) for 2 ≤ i < n
where H 1 , H 2 , H 3 , . . . , H n are independent random oracles; the simulator for hmac calls H 1 at most q H1 +q H2 times, H 2 at most q H2 times, H i at most q Hi times for i ≥ 3, with q H1 +• • •+q Hn ≤ q hmac , and runs in time O(q hmac + q H2 ); and 2 = q H2 (2q H1 + 3q hkdf-expand n + 1)/|M|. Furthermore, by definition of the simulator in the proof of Lemma 7, H 1 is called at most q H1 times via the first hole of S 2 and H 1 and H 2 are called with the same arguments at most q H2 times via the second hole of S 2 .

Repeating the same reasoning inductively, there exists a simulator S 3,j for H j such that G 3,j-1 is indistinguishable up to probability j from G 3,j in which hmac = S 2 [H 1 , S 3,2 [H 1 , H 2 ], . . . , S 3,j [H j-1 , H j ], H j+1 , . . . , H n ] and hkdf-expand n is defined by hkdf-expand 3,j n (prk , info) = k 1 . . . k n where k i = H i (prk , info) for 1 ≤ i ≤ j k i+1 = H i+1 (k i , prk , info) for j ≤ i < n where H 1 , . . . , H j , H j+1 , . . . , H n are independent random oracles; the simulator for hmac calls H 1 at most q H1 times via the first hole of S 2 , H i-1 and H i with the same arguments at most q Hi times via the i-th hole of S 2 for 1 < i ≤ j, H i at most q Hi times for i > j, with q H0 + • • • + q Hn ≤ q hmac , and runs in time O(q hmac + q H2 + • • • + q Hj ); and j = q Hj (2q Hj-1 + 3q hkdf-expand n + 1)/|M|.

For j = n, we obtain a game G 3,n in which hmac = S 2 [H 1 , S

i = H i (prk , info) for 1 ≤ i ≤ n
where H 1 , . . . , H n are independent random oracles; the simulator for hmac calls H 1 at most q H1 times via the first hole of S 2 , H i-1 and H i with the same arguments at most q Hi times via the i-th hole of S 2 for 1 < i ≤ n, with q H1 +• • •+q Hn ≤ q hmac , and runs in time O(q hmac +q H2 +• • •+q Hn ) = O(q hmac ).

By Lemma 3, there exist simulators S 4,j (1 ≤ j ≤ n) for H j such that G 3,n is perfectly indistinguishable from G 4 in which hmac = S P2. Given ((C j , v j ), (C, r j ), j) ∈ L, for some C j , v j , r j and j with 0 ≤ j < m then there is, for each k = j -1 to 0, a single matching element ((C k , v k ), (C k+1 , r k ), k) in L.

More informally, at no time there are entries in L that belong to chains that are incomplete in the front, i. e. that did not start by a call to H with C = const. And yet differently stated, the simulator can, in case 3, always reconstruct the whole chain of H calls and collect the arguments v j .

We first show the existence of ((C k , v k ), (C k+1 , r k ), k) in L for each k = j -1 to 0. If there is an element in L with j > 0, then case 3 was executed before for a matching H call and its result was added to the list with j = j -1. This is because of H2 and the fact that only in case 3 elements with j > 0 are added to the list. This argument can be repeated recursively until reaching j = 1. For j = 0, the matching element that started the chain was added by case 2, once again because of H2 and because only in case 2 elements with j = 0 are added to the list.

Moreover, the uniqueness of ((C k , v k ), (C k+1 , r k ), k) comes from H3: when an element ((C k , v k ), (C k+1 , r k ), k) is added to L, C k+1 is always a fresh C j , so by H3, there is a single element in L with a given C k+1 .

We now treat all possible traces of calls in both games.

Case 1 Suppose the distinguisher makes a direct oracle call to H or chain n with the same arguments as a previous direct call to the same oracle. Both G 0 and G 1 return the same result as in the previous call.

Case 2 Suppose the distinguisher makes a direct call to chain n that has not been done before as a direct call. In G 1 , because the whole chain of H calls was made in the right order, chain n (v 0 , . . . , v n ) has already been invoked indirectly by the call to H(C, v n ). Thus, this current call to chain n returns a previously fixed value, fulfilling the following equation:

H(C, v n ) = C j+1 chain n (v 0 , . . . , v n )
or in the case of n = m H(C, v m ) = chain m (v 0 , . . . , v m ) . This is the same result as in G 0 . Inria Case 2. b) In G 0 , the last H(C, v n ) in the chain that simulates chain n (v 0 , . . . , v n ) has not already been called directly. Like in the previous case, the result is _ chain n (v 0 , . . . , v n ) = H(C, v n ) or in the case of n = m chain m (v 0 , . . . , v m ) = H(C, v m ) , but as H(C, v n ) and chain n (v 1 , . . . , v n ) have not been called before directly, the result is independent of previously returned values and thus looks like a fresh random value to the distinguisher.

In G 1 , chain n (v 0 , . . . , v n ) has not been invoked before and thus returns a fresh random value.

Case 3 Suppose the distinguisher makes a direct call to H that has not been done before as a direct call.

Case 3. a) In G 0 , this call to H(C, v i ) has already been done from inside a chain n (v 0 , . . . , v n ) call. Hence all other H calls belonging to this chain have also been done from inside said chain n call, in particular the call H(C i-1 , v i-1 ) directly before the current call (except for C = const, thus if the current call is the beginning of a chain). H1 implies that the distinguisher has then made a direct call to H(C i-1 , v i-1 ) before the current H call. By recursively applying H1, the distinguisher has then directly made all H calls in the chain up to the current one, in the right order. This is similar to case 2. a) just that the order of the calls is inverted and the following small difference: the parts of H's result coming from chain are already known by the distinguisher, while C n+1 looks like a fresh random value.

In G 1 , because the whole chain of H calls was made in the right order, the current call will invoke case 3 of the simulator's algorithm and return

H(C, v n ) = C n+1 chain n (v 0 , . . . , v n )
or in the case of n = m H(C, v m ) = chain m (v 0 , . . . , v m ) .

The parts of H's result coming from chain are already known by the distinguisher, while C n+1 is a fresh random value. This is indistinguishable from the result in G 0 . Case 3. a) ii) In G 0 , the current direct call to H(C, v i ) has already been done from inside a chain n (v 0 , . . . , v n ) call, but not as the last one. This implies that said chain n call was not chain 0this is covered by case 3. a) i).

In G 0 , the result is thus a value fixed by a previous indirect call to H, but is independent of the results of previous direct calls, and thus looks like a fresh random value to the distinguisher.

In G 1 , because the whole chain of H calls was made in the right order, the current call will invoke case 3 of the simulator's algorithm and return a result via a chain n call. This chain n call has not been made before by hypothesis and thus the result is a fresh random value.

Case 3. b) In G 0 , this call to H(C, v i ) has not been done before, neither directly nor indirectly. 2Hence, H returns a fresh random value.

In G 1 , the simulator's case 1 is not relevant because this call has not been done before. Simulator's case 2: If C = const, then H returns a fresh random C 1 and a fresh random r 0 via chain 0 . This call to chain 0 has not been done before because this would have invoked the H call in G 0 , which is excluded by the hypothesis. Simulator's case 3: If ((C j , v j ), (C, r j ), j) ∈ L for some C j , v j , r j and 0 ≤ j < m, then the current call to H(C, v i ) appends to a chain. Thus, a fresh random C j+2 r j+1 is returned. The involved chain j+1 or chain m has not been called before for the same reason as chain 0 above. Simulator's case 4: A fresh random C -1 r -2 is returned. To conclude, a fresh random value is returned in every case in G 1 .

The previous proof shows that the games G 0 and G 1 are indistinguishable assuming the hypotheses H1, H2, and H3 hold. We will now bound the probability that they do not hold. Suppose that there are at most q H direct queries to H and q chainn direct queries to chain n .

• When H1 does not hold, the distinguisher does an H call from a chain corresponding to an earlier or later chain n call without having done the H calls starting from the beginning of the chain, by using the matching C value. There are at most ( m n=0 n • q chainn ) different C values from H, and the distinguisher has q H attempts to hit a matching one, so the probability that H1 does not hold is at most ( m n=0 n • q chainn ) • q H /2 l . • The probability that H2 does not hold at the q-th call to H is at most the probability that a fresh random value in {0, 1} l collides with q values in {0, 1} l , hence q/2 l . So in total, the probability that H2 does not hold is q H q=1 q/2 l = q H (q H + 1)/2 l +1 . • The probability that H3 does not hold is at most the probability that among q H random values in {0, 1} l , two of them collide, so it is at most q H (q H -1)/2 l +1 .

Hence, the probability that G 0 and G 1 are distinguished is at most

( m n=0 n • q chainn ) • q H + q 2 H 2 l .

  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 pow _k S pub i = pow _k S pub i,rcvd and pow _k S pub r = pow _k S pub r,rcvd . 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 pub r equivalent to our model's honest responder public static key: pow _k (S pub r ) = pow _k (S pub r ) but S pub r = S pub r

  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";

  insert after "in(ch1_rom3" "let rom3_input(x1_rom3, Gsub_to_G(x2_rom3), Gsub_to_G(x3_rom3), x4_rom3, Gsub_to_G(x5_rom3), Gsub_to_G(x6_rom3), v_psk) = x_rom3 in"; crypto rom(rom3_intermediate); insert after "in(ch1_rom2" "let rom2_input(x1_rom2, Gsub_to_G(x2_rom2), Gsub_to_G(x3_rom2)) = x_rom2 in"; crypto rom(rom2_intermediate); insert after "in(ch1_rom1" "let rom1_input(x1_rom1, Gsub_to_G(x2_rom1)) = x_rom1 in"; crypto rom(rom1_intermediate);

2 endifFigure 2 :

 22 Figure 2: Simulator for H

Case 2 .

 2 a) In G 0 , the last H(C, v n ) in the chain that simulates chain n (v 0 , . . . , v n ) has already been called directly. Then by H1 the distinguisher did all H calls in the chain that simulates chain n (v 0 , . . . , v n ) directly.The result in G 0 is_ chain n (v 0 , . . . , v n ) = H(C, v n )which is the last part of the result of the previous call to H, or in the case of n = m chain m (v 0 , . . . , v m ) = H(C, v m ) .

Case 3 .

 3 a) i) In G 0 , the current direct call to H(C, v n ) has already been done as the last one of the chain of calls indirectly invoked from inside a chain n (v 0 , . . . , v n ) call.In G 0 , the result fulfils the following equation:C n+1 chain n (v 0 , . . . , v n ) = H(C, v n ) ,and in the case of n = m: chain m (v 0 , . . . , v m ) = H(C, v m ) .

  1 |. Proof. Consider • the game G 0 in which H 1 and H 2 are independent random oracles, and H 3 (x, y) = H 2 (H 1 (x), y), and • the game G 1 in which H 3 is a random oracle; two lists L 1 and L 2 that are initially empty; H 1 (x) returns y if (x, y) ∈ L 1 for some y, and otherwise chooses a fresh random r in S 1 , adds (x, r) to L and returns r; H 2 (y, z) returns H 3 (x, z) if (x, y) ∈ L 1 for some x, otherwise returns u if ((y, z), u) ∈ L 2 for some u, and otherwise chooses a fresh random r in S 2 , adds ((y, z), r) to L 2 and returns r. CryptoVerif shows that the games G 0 and G 1 are indistinguishable, up to probability . Lemma 7. If H 1 : S 1 → S 1 and H 2 : S 1 ×S 1 → S 2 are independent random oracles, then H 1 = H 1 and H 2 defined by H 2

Table 1 :

 1 Security models (upper part) and properties analysed (lower part) in different works on WireGuard or Noise IKpsk2.

		Noise	Explorer [28]	Suter-	Dörig [41]	Girol [24]	Donenfeld,	Milner [22]	Dowling,	Paterson [23]	this work
	verified protocol	Noise IKpsk2		WireGuard
	tool set	PV	T	T	T	m	CV
	computational model	x	x	x	x
	Curve25519 with equivalent keys	x	x	x	x	x
	compromise static keys
	compromise ephemeral keys	x	x
	dishonest ephemeral keys	x	x		x	x	x
	compromise pre-shared key
	compromise all keys	x	x				x
	both roles per static key	x
	mutual authentication
	key compromise impersonation
	1st message replay	-	-	-	x	x
	transport data replay	x				x	x
	session uniqueness	x			x
	channel binding	x			x	x	x
	DoS resistance	-	-	-	x	x
	forward key
	forward message secrecy						x	x
	identity hiding	x	x			2	x
	identity mis-binding	x	x	x		1

  Proof of Lemma 2. Consider• the game G 0 in which H is a random oracle, and H i (x) = H(x) for each x ∈ D i and i ≤ n, and• the game G 1 in which H 1 , . . . H n are independent random oracles defined on D 1 , . . . , D n respectively, and H

  Consider• the game G 0 in which H 1 and H 2 are independent random oracles, H 1 (x) = H 1 (x), andH 2 (x) = H 2 (H 1 (x), x),and • the game G 1 in which H 1 and H 2 are independent random oracles; H 1 (x) = H 1 (x); H 2 (y, z) returns H 2 (z) if y = H 1 (z) and H 3 (y, z) otherwise, where H 3 is a random oracle (independent of H 1 and H 2 ).

Inria

Proof of Lemma 7.

  1 is indistinguishable up to probability 2 from G 3,2 in which hmac = S 2 [H 1 , S 3,2 [H 1 , H 2 ], H 3 , . . . , H n ] and hkdf-expand n is defined by hkdf-expand 3,2 n (prk , info) = k 1 . . . k n where k 1 = H 1 (prk , info) k 2 = H 2 (prk , info)

  3,2 [H 1 , H 2 ], . . . , S 3,n [H n-1 , H n ]] and hkdf-expand n is defined by hkdf-expand 3,n n (prk , info) = k 1 . . . k n where k

https://cloud.google.com/vpn/docs/concepts/overview, https://docs.aws.amazon.com/vpc/latest/userguide/vpn-connections.html, https://azure.microsoft.com/en-us/services/vpn-gateway/ RR n°9269

RR n°9269

This means that there is no involvement of previous calls to chainn, but the distinguisher can build an H chain with direct calls. Inria

rue Simone Iff -CS 42112

Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN 0249-6399

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 Union's Horizon 2020 NEXTLEAP Project (grant agreement nº 688722), ERC CIRCUS (grant agreement nº 683032), ANR AnaStaSec (decision number ANR-14-CE28-0014-01), and ANR TECAP (decision number ANR-17-CE39-0004-03).

and hkdf-expand n is a random oracle H where the simulator for hmac calls H at most q H1 + • • • + q Hn ≤ q hmac times, and runs in time O(q hmac ). (Since H is the concatenation of the H i for 1 ≤ i ≤ n and, for i > 1, the calls to H i-1 and H i via the i-th hole of S 2 have the same arguments, these two calls can be implemented by a single call to H, and hence there are at most q Hi calls to H via the i-th hole of S 2 .)

The probability of distinguishing G 0 from G 4 is then at most

q Hj q Hj-1

|M|

Proof of Lemma 9. As in the previous proof, we write S[H 1 , . . . , H n ] instead of S H1,...,Hn for a system S with oracle access to H 1 , . . . , H n . Consider the game G 0 in which hmac is a random oracle and hkdf n is defined as above.

By hypothesis, the calls to hmac in hkdf-extract and hkdf-expand n use disjoint domains, so by Lemma 2, there exists a simulator S 1 for hmac such that G 0 is perfectly indistinguishable from G 1 in which hmac = S 1 [H 0 , H 1 ] and hkdf n is defined by hkdf 1 n (salt, key, info) = hkdf-expand 1 n (H 0 (salt, key), info), where hkdf-expand 1 n is defined from the random oracle H 1 instead of hmac and the simulator S 1 calls H i at most q Hi times, with q H0 + q H1 ≤ q hmac and runs in time O(q hmac ).

By Lemma 8, there exists a simulator S 2 for

and hkdf n is defined by hkdf 1 n (salt, key, info) = H(H 0 (salt, key), info), where H is a random oracle, S 2 calls H at most q H ≤ q H1 times, runs in time O(q H1 ) = O(q hmac ), and = (3q hkdfn q H1 + q 2 H1 )/|M|. So the simulator for hmac calls H 0 at most q H0 times and H at most q H ≤ q H1 times and runs in time O(q hmac ).

By Lemma 6, there exist simulators S 3,1 for H 0 and S 3,

n ] and hkdf n = hkdf 3 n is a random oracle, where the simulator for hmac calls hkdf n at most q H ≤ q H1 ≤ q hmac times, runs in time O(q hmac + q H0 q H ) = O(q 2 hmac ), and = (2q H q H0 + q 2 H0 + q H q hkdfn + q 2 hkdfn )/|M|. The probability of distinguishing G 0 from G 3 is then at most

A.3 Chain of Random Oracle Calls

Proof of Lemma 10. We consider the following two games G 0 and G 1 .

• The game G 0 in which H is a random oracle and the functions chain n with 0 ≤ n ≤ m are defined from H by ( 11) and ( 12).

• The game G 1 in which the functions chain n with 0 ≤ n ≤ m are independent random oracles and H is defined from them in Figure 2. In this figure, L is a list of triples ((C, v), (C j+1 , r j ), j) such that C j+1 r j is the result of a previous call to H(C, v) and j indicates the index of this H call in a chain of calls to H. If a call to H was not coming from a chain of calls, the index j = -2 is used.

We shortly comment this simulator's four cases informally. In case 1, it returns a previous result because the same call has already been made before. In case 2, the call to H uses const as first argument and is thus the first call in a potential chain of calls to H. Therefore, the simulator uses chain 0 to get the result and writes it to the list L with index 0. In case 3, the simulator finds in L a previous call to H that returned the current call's C value as result. This means, with respect to the hypothesis we present just after this paragraph, that the current call belongs to a chain of previous calls that was started with a call responded to by case 2. The simulator collects the arguments v k of those previous calls to be able to call the appropriate chain n oracle. If the simulator reaches case 4, then the call did neither start a new chain nor belong to a previously started chain. Thus, it chooses fresh random values as a result and adds them with an index to L that makes sure that it will never be considered as part of a chain.

We name direct oracle calls to chain n or H calls that are done directly by the distinguisher, and indirect oracle calls the calls to H done from inside chain n in G 0 and the calls to chain n done from inside H in G 1 . Note for clarification that in G 0 there are no indirect calls to chain n and in G 1 there are no indirect calls to H. We show that the two games G 0 and G 1 are indistinguishable as long as the following hypotheses hold. In game G 0 : H1. Consider C j+1 r j = H(C j , v j ), j ≤ n < m that gets called from inside a direct call to chain n (v 1 , . . . , v j , . . . , v n ). If the distinguisher calls H(C j+1 , v j+1 ) before or after the call to chain n , then H(C j , v j ) has been called directly by the distinguisher before H(C j+1 , v j+1 ).

Stated informally, the distinguisher can only know C j+1 if it was received as result from H.

In game G 1 :

H2. No fresh C j is equal to the first argument of a previous call to H (including the call that generates C j ).

Stated informally, the distinguisher cannot prepend to a chain of H calls.

H3. There are no collisions between the fresh C j .

We have the following invariants:

P1. Given C, v, there is at most one pair ((C j+1 , r j ), j) such that ((C, v), (C j+1 , r j ), j) ∈ L.

Indeed, when L contains such an element, calls to H(C, v) immediately return C j+1 r j in case 1, and never add another element ((C, v), (C j+1 , r j ), j) to L.

Inria