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

HAL
open science

# Mechanized Cryptographic Proofs of Protocols and their Link with Verified Implementations

Benjamin Lipp

► To cite this version:

Benjamin Lipp. Mechanized Cryptographic Proofs of Protocols and their Link with Verified Implementations. Cryptography and Security [cs.CR]. Université Paris sciences et lettres, 2022. English.
NNT: tel-03933719

HAL Id: tel-03933719

https://inria.hal.science/tel-03933719

Submitted on 10 Jan 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

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

Distributed under a Creative Commons Attribution 4.0 International License
# Preuves mécanisées de protocoles cryptographiques et leur lien avec des implémentations vérifiées

Soutenue par

**Benjamin LIPP**

Le 28 juin 2022

École doctorale n°386

**Sciences Mathématiques de Paris Centre**

Spécialité

**Informatique**

## Composition du jury :

**David POINTCHEVAL**
Directeur de recherche, CNRS
Président

**Véronique CORTIER**
Directrice de recherche, CNRS
Rapporteure

**Ralf KÜSTERS**
Professeur, Université de Stuttgart
Rapporteur

**Cédric FOURNET**
Senior Principal Research Manager, Microsoft Research
Examinateur

**Bruno BLANCHET**
Directeur de recherche, Inria
Directeur de thèse

**Karthikeyan BHARGAVAN**
Directeur de recherche, Inria
Directeur de thèse
<figure><img src="image_3.png" /></figure>
# Mechanized Cryptographic Proofs of Protocols and their Link with Verified Implementations
This thesis was typeset using `TEX` and the `memoir` documentclass. It is based on Friedrich Wiemer's thesis *Security Arguments and Tool-Based Design of Block Ciphers*<fnref n="1" />, itself based on Aaron Turon's thesis *Understanding and expressing scalable concurrency*<fnref n="2" />, itself a mixture of *classicthesis*³ by André Miede and `tufte-latex`<fnref n="4" />, based on Edward Tufte's *Beautiful Evidence*.

The bibliography was processed by Biblatex.

The body text is set 10/14pt (long primer) on a 26pc measure. The margin text is set 8/9pt (brevier) on a 12pc measure. Matthew Carter's Charter acts as both the text and display typeface. Monospaced text uses Jim Lyles's Bitstream Vera Mono ("Bera Mono").

<footnote n="1">¹https://asante.dev/publication/p
hd_thesis/, source code available at http
s://github.com/pfasante/phd_thesis.</footnote>

<footnote n="2">²https://people.mpi-sws.org/~turo
n/turon-thesis.pdf</footnote>

<footnote>`³https://bitbucket.org/amiede/cla
ssicthesis/`</footnote>

<footnote n="4">⁴https://github.com/Tufte-LaTeX/tufte-latex</footnote>
<figure><img src="image_4.png" /></figure>
<figure><img src="image_5.png" /></figure>
Acknowledgements

My time in the Prosecco research group at Inria Paris has been enormously rich for me – in personal and academic growth, in the colleagues I met, and the friends I made. I am very grateful to my PhD advisors Bruno and Karthik, and thank them wholeheartedly for giving me this opportunity, funding my PhD, and for guiding me through this adventure, by offering challenging projects, with patience and vision. Thank you for being there in countless meetings, for discussing my work, my ideas, and for navigating any difficult situations. I also thank you for offering me the freedom to travel to a summer school, a student program committee meeting, and many workshops and conferences.

I thank Véronique Cortier and Ralf Küsters for having served as reviewers of my thesis, and for being part of the jury of my defence. I thank Cédric Four-net and David Pointcheval for being part of the jury, and David Pointcheval for being president of the jury.

I am grateful to Bruno for carefully proofreading my thesis manuscript through multiple iterations and helping me find ways to present my work, to Karthik for providing valuable feedback on the manuscript, and to Anna for her helpful comments on the cv2fstar chapter. I thank Aymeric, Bruno, Christian, Denis, Goutam, Itsaka, and Rob for their comments and advice on my rehearsal defence talk.

Scientifically, this journey started with Bruno teaching me how to use the CryptoVerif proof assistant during my master internship. This has certainly been the right way for me to get into the field of provable security. Before this initiation to CryptoVerif, I did not see myself writing cryptographic proofs by hand; now, I feel ready for that, too. Although, for manual proofs, I am missing CryptoVerif's last output line in case of success, All queries proved. Besides its comforting guarantees, it has some addiction potential. Sometimes, when I used the tool in some strange ways that made it crash, CryptoVerif would tell me to contact a certain Bruno.Blanchet@inria.fr, and to [p]lease report [a] bug [...] including input file and output. For this, I was of course in the greatly privileged position of being able to just walk over three offices. Thus, Bruno, many thanks for patiently initiating me to mechanized cryptographic proofs, and for implementing some of my usability improvement ideas into the tool over the last years.

The other proof-oriented development environment in which I have been spending a lot of time is the F\* ecosystem. I want to thank everyone who helped me find my ways, and who welcomed me in the community, especially: Karthik, for some insightful pair programming sessions; Ben, who helped me navigate the voodoo sequence of commands needed to get Project Everest running, and who spent multiple pair programming sessions with me; Anna for helping to debug P-256 in my HACL\* setup; Marina for help with using HACL\*; my office mate Denis for answering everyday F\* questions; Son and Vincent for providing helpful code snippets; Aymeric for explaining to me the version of the HPKE specification that I built upon;
Victor for help with HACL''s OCaml interface; and Catalin for an insightful discussion about my cv2fstar work. I also thank those who answered my questions on the various online channels, in particular Cezar, Jonathan, Nik, and Tahina; and finally, Cédric, for organizing the Project Everest all-hands meeting that I attended in Cambridge.

I spent a long part of my PhD on the Hybrid Public Key Encryption standardization effort, and I am very happy and grateful that I could be part of it. I thank Karthik for bringing me into this project, and the other RFC co-authors Chris Wood and Richard Barnes for their interest in my provable security work, and their openness to my suggestions that came out of this work. I thank Chris for working on a preprint with me, and asking me if I want to be an official co-author of the RFC. It was a pleasure to work with you and the CFRG community, and I thank everyone who was involved in bringing this RFC to publication as RFC 9180. I am glad that the HPKE project also led me to my external co-authors Eike, Joël, Doreen, and Eduard, with whom, together with Bruno, we published a paper containing mechanized cryptographic proofs at Eurocrypt. I learned a lot from you about cryptographic proofs and how to present them, and I am very grateful for our collaboration. Thank you! Finally, I thank Franziskus for helpfully pushing me through finishing writing my blog post about HPKE, which turned out to be pretty effective on science Twitter.

During two years of my PhD, I was a teaching assistant at the university that is now called Université Paris Cité, and I am thankful for the teaching experience that I could gather in this time. I thank everyone who made this possible, especially Thomas Béraud, Ralf Treinen, Michele Pagani, and Cristina Sirangelo; the colleagues who helped me navigate the bureaucratic jungle coming with this, especially Glen; Pablo who administered our teaching Discord server during lockdown time, and Sam who found an online programming environment suitable for teaching.

I want to thank Véronique, Catalin, Bruno, Gilles, Karthik, and the PETS community for allowing me to gain paper reviewing experience as an external reviewer for individual papers. I also had the opportunity to participate in the shadow program committee of IEEE's Security&Privacy 2020 conference, which was an insightful experience that I am grateful for, and I thank Tom Moyer for organizing it.

I thank Rakesh Bobba, David Evans, and Cas Cremers for insightful conversations during mentoring sessions at online conferences.

Although it dates back to my master internship in Prosecco starting end of the year 2017, I want to repeat my gratefulness to Julian Herr, Mario Strefler, Mathieu Goessens, Jeff Burdges, and Harry Halpin, who helped me make my way to the Prosecco research group.

At Inria Paris and in Prosecco, I had an amazing time with great colleagues, and I want to thank you: Denis, my long-time office mate, for helping me with French bureaucracy and explaining French politics with a passion, and also for great dinners and French theater; Carmine, my other long-time office mate, for almost always beating me to arriving early in the office; Ben, for great discussions about cryptographic protocols; Rob, for valuable feedback on practice talks; Catalin, for organizing many Prosecco pub evenings, inviting to brunches, and helpful advice about academia;
Antonin, for asking me why I do cryptographic research and thereby making me remember Rogaway's essay that I read for the first time several years ago; Aymeric, for pointing me to the Science of Security survey paper; Prasad, for great advice, hikes, dinners, and working sessions on contact tracing; Victor, for sadly only one after-work drink as neighbors in the 13th before I moved to Bochum; Anna and Marina, for organizing a board game evening and many pub evenings; Kenji, for introducing cake Tuesday; Nadim, for his magical appearance on multiple occasions when I needed advice on new computer hardware; and Aaron, Adrien, Alain, Bruno, Florian, Iness, Jérémy, Justine, Karthik, Kristina, Marc, Paul-Nicolas, Ram, Son, Théo, Théophile, and Vincent, for the daily encouragement and distractions that made the time worthwhile and comfortable. I thank our team assistant Mathieu Mourey, for his great support, executed with ease and pragmatism, in all things administration and bureaucracy, especially for the travel expense reports of my long-distance train travels. Outside of Prosecco, I thank Léo for giving me insights into the politics of science, Inria, and IACR, and for helping me maintain my bike. I thank Sébastien, Matthieu, Juliette, Ivan, Yohan, Mauricio, and Nastassia who started the local sustainability group at Inria Paris together with me.

I want to thank Sylvain, a friend I made through meetings at multiple conferences, for his socio-anthropologic interest in security research and the stimulating conversations about it. I want to thank Karolin for interesting discussions about WireGuard and academia, offering refreshing point-of-views from a different angle.

For the last science-ish thank you, of course, not to forget the co-authors of the Eurocrypt 2021 rump session talk about the $(\alpha, \beta)$-technique that won us the rump session award: Phillip, Benedikt, Christoph, Doreen, Eduard, Fabian, Jonas, and Noemi.

I thank the developer aegis and the kind community of the Talon voice control and hands-free input software. You helped me bridge the time of recovery from my injury by providing a technologically astonishing software ecosystem. Without Talon, this thesis would certainly have been delayed some more or have less content.

Besides the academic parts of my life in Paris, I am happy to have enjoyed the company of many friends throughout the time of my PhD. I enjoyed a lot being part of the choir of Cité Internationale Universitaire de Paris; singing La Marseillaise with a large choir and orchestra in La Philharmonie de Paris is probably a level of integration that not many non-French people have the privilege to experience. Thank you Beate, Franzi, Josephine, Romy, Sahita, Marine, Gregory, Pierre, Julian, Antoine, and Olivier, to name only a few of my fellow choristes. I want to thank my friends who visited me in Paris physically or virtually: Felix and Jenny, Jakob, Julian and Evi, Vicky and Johannes, Xandra, Julian, Nico, Max, Nora, Nora and Johannes and Fiona and Clemens, Bogdan, Astrid, David, Nefta and Christian, Josi and Ekrem, Jens, Julian, ChrKr, and Bölz, Gunnar, Joachim, Anke, Sonja, Julia, and Harry. I want to thank Julian for our mostly perfectly asynchronous Signal chats; and Miriam, Marcel, and Lukas, for being there in our infamous Signal group. I am deeply grateful to my former flatmate Laura, and happy that we found a nice apartment in the 13th arrondissement together. Thank
you for teaching me many useful psychological and philosophical tools. I
thank my then-following but now also former flatmate Franziska for bearing
with me when I was mostly focussing on thesis work during the last months
in Paris.

Finally, I want to express my gratitude to my parents Pia and Bernhard, who have been supporting me without hesitation on this journey, also financially. Without this I would not have been able to afford living in the 13th arrondissement of Paris for a good part of my PhD. I thank my sister Beatrice for always having an open ear and checking in on me. I am grateful that my grandparents Ernst and Johanna have supported me in all the journeys I took during my bachelor, master, and PhD studies. And finally, I am grateful that I could go this way together with my girlfriend Yvette, who has been a constant source of support and encouragement.
<figure><img src="image_6.png" /></figure>
<figure><img src="image_7.png" /></figure>
Abstract

Cryptographic protocols are one of the foundations for the trust people put
in computer systems nowadays, be it online banking, any web or cloud
services, or secure messaging. One of the best theoretical assurances for
cryptographic protocol security is reached through proofs in the computa-
tional model. Writing such proofs is prone to subtle errors that can lead
to invalidation of the security guarantees and, thus, to undesired security
breaches. Proof assistants strive to improve this situation, have got traction,
and have increasingly been used to analyse important real-world protocols
and to inform their development. Writing proofs using such assistants re-
quires a substantial amount of work. It is an ongoing endeavour to extend
their scope through, for example, more automation and detailed modelling
of cryptographic building blocks. This thesis shows on the example of the
CryptoVerif proof assistant and two case studies, that mechanized crypto-
graphic proofs are practicable and useful in analysing and designing complex
real-world protocols.

The first case study is on the free and open source Virtual Private Network (VPN) protocol WireGuard that has recently found its way into the Linux kernel. We contribute proofs for several properties that are typical for secure channel protocols. Furthermore, we extend CryptoVerif with a model of unprecedented detail of the popular Diffie-Hellman group Curve25519 used in WireGuard.

The second case study is on the new Internet standard Hybrid Pub-
lic Key Encryption (HPKE), that has already been picked up for use in a
privacy-enhancing extension of the TLS protocol (ECH), and in the Mes-
saging Layer Security secure group messaging protocol. We accompanied
the development of this standard from its early stages with comprehensive
formal cryptographic analysis. We provided constructive feedback that led to
significant improvements in its cryptographic design. Eventually, we became
an official co-author. We conduct a detailed cryptographic analysis of one of
HPKE's modes, published at Eurocrypt 2021, an encouraging step forward
to make mechanized cryptographic proofs more accessible to the broader
cryptographic community.

The third contribution of this thesis is of methodological nature. For
practical purposes, security of implementations of cryptographic protocols is
crucial. However, there is frequently a gap between a cryptographic security
analysis and an implementation that have both been based on a protocol
specification: no formal guarantee exists that the two interpretations of the
specification match, and thus, it is unclear if the executable implementation
has the guarantees proved by the cryptographic analysis. In this thesis,
we close this gap for proofs written in CryptoVerif and implementations
written in F*. We develop cv2fstar, a compiler from CryptoVerif models to
executable F* specifications using the HACL* verified cryptographic library
as backend. cv2fstar translates non-cryptographic assumptions about, e.g.,
message formats, from the CryptoVerif model to F* lemmas. This allows to
prove these assumptions for the specific implementation, further deepening
the formal link between the two analysis frameworks. We showcase cv2fstar
on the example of the Needham-Schroeder-Lowe protocol. cv2fstar con-
nects CryptoVerif to the large F* ecosystem, eventually allowing to formally
guarantee cryptographic properties on verified, efficient low-level code.
<figure><img src="image_8.png" /></figure>
<figure><img src="image_9.png" /></figure>
Résumé

Les protocoles cryptographiques sont l'un des fondements de la confiance que la société accorde aujourd'hui aux systèmes informatiques, qu'il s'agisse de la banque en ligne, d'un service web, ou de la messagerie sécurisée. Une façon d'obtenir des garanties théoriques fortes sur la sécurité des protocoles cryptographiques est de les prouver dans le modèle calculatoire. L'écriture de ces preuves est délicate : des erreurs subtiles peuvent entraîner l'invalidation des garanties de sécurité et, par conséquent, des failles de sécurité. Les assistants de preuve visent à améliorer cette situation. Ils ont gagné en popularité et ont été de plus en plus utilisés pour analyser des protocoles importants du monde réel, et pour contribuer à leur développement. L'écriture de preuves à l'aide de tels assistants nécessite une quantité substantielle de travail. Un effort continu est nécessaire pour étendre leur champ d'application, par exemple, par une automatisation plus poussée et une modélisation plus détaillée des primitives cryptographiques. Cette thèse montre sur l'exemple de l'assistant de preuve CryptoVerif et deux études de cas, que les preuves cryptographiques mécanisées sont praticables et utiles pour analyser et concevoir des protocoles complexes du monde réel.

La première étude de cas porte sur le protocole de réseau virtuel privé (VPN) libre et open source WireGuard qui a récemment été intégré au noyau Linux. Nous contribuons des preuves pour plusieurs propriétés typiques des protocoles de canaux sécurisés. En outre, nous étendons CryptoVerif avec un modèle d'un niveau de détail sans précédent du groupe Diffie-Hellman populaire Curve25519 utilisé dans WireGuard.

La deuxième étude de cas porte sur la nouvelle norme Internet Hybrid Public Key Encryption (HPKE), qui est déjà utilisée dans une extension du protocole TLS destinée à améliorer la protection de la vie privée (ECH), et dans Messaging Layer Security, un protocole de messagerie de groupe sécurisée. Nous avons accompagné le développement de cette norme dès les premiers stades avec une analyse cryptographique formelle. Nous avons fourni des commentaires constructifs ce qui a conduit à des améliorations significatives dans sa conception cryptographique. Finalement, nous sommes devenus un co-auteur officiel. Nous effectuons une analyse cryptographique détaillée de l'un des modes de HPKE, publiée à Eurocrypt 2021, un pas encourageant pour rendre les preuves cryptographiques mécanisées plus accessibles à la communauté des cryptographes.

La troisième contribution de cette thèse est de nature méthodologique. Pour des utilisations pratiques, la sécurité des implémentations de protocoles cryptographiques est cruciale. Cependant, il y a souvent un écart entre l'analyse de la sécurité cryptographique et l'implémentation, tous les deux basées sur la même spécification d'un protocole : il n'existe pas de garantie formelle que les deux interprétations de la spécification correspondent, et donc, il n'est pas clair si l'implémentation exécutable a les garanties prouvées par l'analyse cryptographique. Dans cette thèse, nous comblons cet écart pour les preuves écrites en CryptoVerif et les implémentations écrites en F*.
Nous développons cv2fstar, un compilateur de modèles CryptoVerif vers des spécifications exécutables F* en utilisant la bibliothèque cryptographique vérifiée HACL* comme fournisseur de primitives cryptographiques. cv2fstar traduit les hypothèses non cryptographiques concernant, par exemple, les formats de messages, du modèle CryptoVerif vers des lemmes F*. Cela permet de prouver ces hypothèses pour l'implémentation spécifique, ce qui approfondit le lien formel entre les deux cadres d'analyse. Nous présentons cv2fstar sur l'exemple du protocole Needham-Schroeder-Lowe. cv2fstar connecte CryptoVerif au grand écosystème F*, permettant finalement de garantir formellement des propriétés cryptographiques sur du code de bas niveau efficace vérifié.
<figure><img src="image_10.png" /></figure>
# Contents

ACKNOWLEDGEMENTS v

ABSTRACT xi

RÉSUMÉ xv

I PROLOGUE 1

1 INTRODUCTION 3

1.1 Outline and Contributions 6

1.2 List of Publications 8

2 THE CRYPTOVERIF PROOF ASSISTANT 11

2.1 Proofs Based on Sequences of Games 11

2.2 Introduction to CryptoVerif 14

2.3 Syntax and Semantics: Overview 15

2.4 Security Queries 17

2.5 Example: The Needham-Schroeder-Lowe Protocol 18

2.6 Contributions to CryptoVerif's Usability 27

II CRYPTOVERIF CASE STUDIES ON REAL-WORLD PROTOCOLS 31

3 ANALYSING THE WIREGUARD VPN PROTOCOL 33

3.1 Introduction 33

3.2 WireGuard 36

3.3 Cryptographic Assumptions 43

3.4 Indifferentiability of Hash Chains 53

3.5 Modelling WireGuard 59

3.6 Verification Results 62

3.7 Discussion 73

4 ANALYSING HPKE'S AUTHENTICATED MODE 78

4.1 Introduction 78

4.2 Preliminaries 84

4.3 Standard Cryptographic Definitions 85

4.4 Elliptic Curves 87

4.5 Authenticated Key Encapsulation and Public Key Encryption 93

4.6 The HPKE Standard 101

5 THE HYBRID PUBLIC KEY ENCRYPTION STANDARD 112

5.1 An Analysis of All HPKE Modes 112

5.2 Influence of Our Analyses on the Standard 117

III LINKING COMPUTATIONAL PROOFS AND IMPLEMENTATIONS 123

6 CV2FSTAR: A COMPILER FROM CRYPTOVERIF TO F\* 125

6.1 Motivation and Introduction 126
<table>
  <tbody>
    <tr>
      <td>6.2 Related Work</td>
      <td>127</td>
    </tr>
    <tr>
      <td>6.3 The Output Language</td>
      <td>129</td>
    </tr>
    <tr>
      <td>6.4 The Input Language</td>
      <td>131</td>
    </tr>
    <tr>
      <td>6.5 Translating to F*: An Overview</td>
      <td>135</td>
    </tr>
    <tr>
      <td>6.6 Translating Types</td>
      <td>137</td>
    </tr>
    <tr>
      <td>6.7 Translating Functions and Constants</td>
      <td>143</td>
    </tr>
    <tr>
      <td>6.8 The State Type</td>
      <td>144</td>
    </tr>
    <tr>
      <td>6.9 Translating Tables</td>
      <td>145</td>
    </tr>
    <tr>
      <td>6.10 Translating Events</td>
      <td>148</td>
    </tr>
    <tr>
      <td>6.11 Translating Terms</td>
      <td>149</td>
    </tr>
    <tr>
      <td>6.12 Translating Oracles as Functions</td>
      <td>157</td>
    </tr>
    <tr>
      <td>6.13 Translating Assumptions as Lemmas</td>
      <td>163</td>
    </tr>
    <tr>
      <td>6.14 Differences to the OCaml Extraction</td>
      <td>167</td>
    </tr>
    <tr>
      <td>6.15 Case Study: The Needham-Schroeder-Lowe Protocol</td>
      <td>168</td>
    </tr>
    <tr>
      <td>6.16 Conclusion</td>
      <td>175</td>
    </tr>
    <tr>
      <td>6.17 Future Work</td>
      <td>176</td>
    </tr>
    <tr>
      <td>IV EPILOGUE</td>
      <td>179</td>
    </tr>
    <tr>
      <td>7 CONCLUSION</td>
      <td>181</td>
    </tr>
    <tr>
      <td>7.1 Mechanized Proofs within the Cryptographic Community</td>
      <td>182</td>
    </tr>
    <tr>
      <td>7.2 Future Work</td>
      <td>185</td>
    </tr>
    <tr>
      <td>BIBLIOGRAPHY</td>
      <td>187</td>
    </tr>
    <tr>
      <td>V APPENDIX</td>
      <td>197</td>
    </tr>
    <tr>
      <td>A APPENDICES TO THE CRYPTOVERIF INTRODUCTION</td>
      <td>199</td>
    </tr>
    <tr>
      <td>A.1 CryptoVerif Model nsl.ocv</td>
      <td>199</td>
    </tr>
    <tr>
      <td>B APPENDICES TO THE WIREGUARD ANALYSIS</td>
      <td>203</td>
    </tr>
    <tr>
      <td>B.1 Indifferentiability Results</td>
      <td>203</td>
    </tr>
    <tr>
      <td>C APPENDICES TO THE ANALYSIS OF HPKE'S AUTHENTICATED MODE</td>
      <td>213</td>
    </tr>
    <tr>
      <td>C.1 Single- and Two-User Definitions for AKEM</td>
      <td>213</td>
    </tr>
    <tr>
      <td>C.2 Comparison of Pseudocode Definitions and their Implementation in CryptoVerif</td>
      <td>223</td>
    </tr>
    <tr>
      <td>D CV2FSTAR CASE STUDY: CRYPTOVERIF MODEL AND GENERATED CODE</td>
      <td>229</td>
    </tr>
    <tr>
      <td>D.1 CryptoVerif Model nsl.ocv</td>
      <td>229</td>
    </tr>
    <tr>
      <td>D.2 NSL.Initiator.fsti, Generated by cv2fstar</td>
      <td>233</td>
    </tr>
    <tr>
      <td>D.3 NSL.Initiator.fst, Generated by cv2fstar</td>
      <td>233</td>
    </tr>
    <tr>
      <td>D.4 NSL.Responder.fsti, Generated by cv2fstar</td>
      <td>234</td>
    </tr>
    <tr>
      <td>D.5 NSL.Responder.fst, Generated by cv2fstar</td>
      <td>235</td>
    </tr>
    <tr>
      <td>D.6 Excerpt of Application.fst, Manually Written</td>
      <td>236</td>
    </tr>
    <tr>
      <td>D.7 Output of Application.fst</td>
      <td>238</td>
    </tr>
  </tbody>
</table>
<figure><img src="image_11.png" /></figure>
Part I

PROLOGUE
<figure><img src="image_12.png" /></figure>
# 1

## Introduction

Cryptology is a fascinating science, concerned with security and privacy of information, communication, and computation in the presence of adversaries.<fnref n="1" /> Cryptographic systems form an important pillar of security and privacy of the digital aspects of our life styles, organisations, and governments: They are a technological basis for the trust we put into, e. g., web or cloud services, online banking, software updates for connected devices, and secure messaging. This last example, secure messaging, is especially important for groups susceptible to surveillance, like journalists, activists, and whistleblowers.

Work in the domain of cryptology and the resulting cryptographic systems are inherently political, because of their ability to implement power structures, as laid out in Rogaway's essay "The Moral Character of Cryptographic Work" published in the year 2015 [Rog15]. He states:

> I am [...] concerned with what surveillance does to society and human rights. Totalized surveillance vastly diminishes the possibility of effective political dissent. And without dissent, social progress is unlikely.

Recent examples where a cryptographic protocol being developed and deployed (or planned to be deployed) provoked intense discussions and worries of being yet another hard-to-revert first step to ubiquitous surveillance are pandemic contact tracing [RBS20] and Apple's plans to introduce client-side scanning on smartphones to detect child sexually abuse material (CSAM).² In his essay, Rogaway calls for the cryptographic community to engage in anti-surveillance research and suggests several avenues to do so. One of them is *practice-oriented provable security*, and it is this area to which this thesis mainly aims to contribute. The term *provable security* stands for work on the strongest kind of assurance of cryptographic security that one can hope to achieve for the specification level of a cryptosystem. In practice, this kind of security is obtained by reduction proofs in the computational model. However, the relevance of theorems established by such proofs for actual real-world systems depends on the assumptions and abstractions they use. A common critique summarized by a survey on the *Science of Security* [Hv17] is that assumptions and abstractions are too far from reality such that the analyses' applicability to real-world cryptographic systems is rather limited. Practice-oriented provable security strives to use assumptions and abstractions that are as close to reality as possible, and aims to enable

[Rog15] Rogaway, *The Moral Character of Cryptographic Work*

[RBS20] Reichert et al., *A Survey of Automatic Contact Tracing Approaches Using Bluetooth Low Energy*

²https://www.theverge.com/2021/8/6/22613365apple-icloud-csam-scanning-whatsapp-surveillance-reactions

[Hv17] Herley and van Oorschot, "SoK: Science, Security and the Elusive Goal of Security as a Scientific Pursuit"

<footnote n="1">¹Adapted from the website of the International Association for Cryptologic Research (IACR), https://www.iacr.org/.</footnote>
useful assessments of, e. g. key sizes and number of users for practical cryp-
tographic systems. This requires modelling cryptosystems on a low-level
and with a higher detail, which is tedious and error prone to do by hand;
we present our suggestion to approach this issue in a bit.

Providing a proof along with the presentation of a new cryptographic
protocol was not always standard. The Needham-Schroeder authentica-
tion protocol published in 1978 [NS78] did not have a security proof. In
1989, a proof was published [BAN90], but years later, in 1995, an attack
was found using formal methods [Low95; Low96]. Nowadays, game-based
proofs are broadly viewed as a means to facilitate cryptographic security
proofs [Sho04; BR06]. However, with complex protocols like TLS [Res18]
and the WireGuard VPN protocol published in 2017 [Don17], and the goal
to have highly-detailed models, game-based proofs tend to get long and com-
plex, which makes it hard to proofread them. In 2004, Bellare and Rogaway
use clear words to describe how they perceive the situation [BR06]:

In our opinion, many proofs in cryptography have become es-
sentially unverifiable. Our field may be approaching a crisis of
rigor.

Halevi, in his essay “A plausible approach to computer-aided cryptographic proofs” [Hal05], adds:

Some of the reasons for this problem are social (e. g., we mostly
publish in conferences rather than journals), but the true cause
of it is that our proofs are truly complex.

Finally, Bellare and Rogaway agree with Halevi by repeating his call for the
creation of “automated tools, that can help write and verify game-based
proofs” [Hal05; BR06].

In this thesis, we propose to tackle the issue of practice-oriented provable
security and highly detailed models by increasing the applicability and
visibility of computer-aided proofs. We focus on real-world protocols. Our
hypothesis is that cryptographic proofs of practical usefulness, are feasible
using automated proof assistants, provide a high assurance that the theorems
are correct, and are a useful part of protocol development.

Before introducing the computational model of cryptography, we want
to say that computer-aided analysis of cryptographic protocols is mainly
conducted in two conceptually different models, the *symbolic model* and the
*computational model*. Both models consider an active adversary, which con-
trols the network and can observe, duplicate, suppress, as well as construct
new messages from messages it observed, and inject them. In the symbolic
model, cryptographic building blocks <fnref n="3" /> are considered perfect and modeled
as function symbols, and messages are terms on these symbols. This means
the adversary cannot exploit any internal structure of terms like public keys
or ciphertexts. For example, a particular ciphertext can only be decrypted if
exactly the key used for encryption is used in the decryption function. The
adversary in the symbolic model is a Dolev-Yao adversary [DY83]. In terms
of computation, it is restricted to the functions that are available within
the protocol model. This defines explicitly what the adversary *can* do. In
the symbolic model, logical protocol flaws and protocol traces leading to
them, and thus to the violation of a security property can be found. The

[NS78] Needham and Schroeder, "Using encryption for authentication in large networks of computers"

[BAN90] Burrows et al., "A Logic of Authentication"

[Low95] Lowe, "An attack on the Needham-Schroeder public-key authentication protocol"

[Low96] Lowe, "Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR"

[Sho04] Shoup, *Sequences of games: a tool for taming complexity in security proofs*

[BR06] Bellare and Rogaway, "The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs"

[Res18] Rescorla, *The Transport Layer Security (TLS) Protocol Version 1.3*

[Don17] Donenfeld, "WireGuard: Next Generation Kernel Network Tunnel"

[Hal05] Halevi, *A plausible approach to computer-aided cryptographic proofs*

<footnote n="3">³We use the terms *cryptographic building blocks* and *cryptographic primitives* interchangeably in this thesis.</footnote>

<footnote>[DY83] Dolev and Yao, "On the Security of Public Key Protocols"</footnote>
symbolic model facilitates automated analysis, as implemented for example
in the tools ProVerif [Bla16] and Tamarin [Mei+13]. However, cryptographic
building blocks are not perfect in reality, there is always at least a small pos-
sibility that the adversary guesses a key. The computational model considers
a more realistic adversary and allows to quantify the probability with which
an adversary breaks desired security properties. In this model, the adver-
sary is described as a probabilistic Turing machine, messages are bitstrings,
cryptographic building blocks are modeled as functions from bitstrings to
bitstrings, and they are not perfect, but assumed to be broken with a certain
negligible probability [GM84]. An analysis in this model aims to establish an
upper bound for the probability that a security property of the protocol can
be broken, and, more constructively, to inform protocol parameter choices
like key sizes and the number of users to keep this probability negligible in
a real-world scenario. Proofs in the computational model are reductionist:
they reduce the security of a cryptographic system to hardness assumptions
on cryptographic building blocks used within it. The style of cryptographic
proofs in the computational model has evolved over the years, and nowa-
days, code-based game-playing proofs have become the norm for the type of
protocols considered in this thesis [BR04].

RELATED WORK. In this thesis, we use CryptoVerif, a proof assistant working in the computational model and specialized on game-based proofs for protocols and less on cryptographic building blocks. It provides a relatively high degree of automation which allows to treat complex protocols. Various automated proof assistants have been developed to formalize game-based proofs. CryptoVerif is not foundational in that its entire implementation is part of the trusted computing base: while its game transformations are proven correct on paper, the implementation itself is not formally proven correct. CertiCrypt was an attempt to create a foundational proof assistant for cryptographic proofs based on Coq [BGZB09]. The successor EasyCrypt has been developed because CertiCrypt did not scale well enough [Bar+11] – the desire to be foundational has been dropped as a compromise, and so EasyCrypt’s implementation and external SMT solvers are part of its trusted computing base. Still, EasyCrypt requires users to indicate all intermediate games and write proofs of indistinguishability manually, the tool only checks them. This makes EasyCrypt struggle for large protocols like TLS and Signal, that can be treated in CryptoVerif [BBK17; KBB17]. However, EasyCrypt works better for cryptographic building blocks [Alm+19] because its input language is more expressive. In contrast to CryptoVerif, e. g., it can handle loops with mutable state, and allows to organise model code in modules. Furthermore, it can express generic reduction proofs and in particular generic hybrid arguments. These reasons make EasyCrypt better equipped for use with other kinds of security notions than only game-based ones. First, it has been used for simulation-based security, that is usually employed for secure multi-party computation protocols [Haa+18]. Second, there is a development under the name of EasyUC [CSV19], using EasyCrypt for the universal composability (UC) framework [Can00]. The UC model provides strong composability theorems. However, proofs are hard to obtain for efficient protocols, or, necessitate changes to the protocol. An interesting

[Bla16] Blanchet, "Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif"

[Mei+13] Meier et al., "The TAMARIN Prover for the Symbolic Analysis of Security Protocols"

[GM84] Goldwasser and Micali, "Probabilistic Encryption"

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

[BGZB09] Barthe et al., "Formal Certification of Code-Based Cryptographic Proofs"

[Bar+11] Barthe et al., "Computer-Aided Security Proofs for the Working Cryptographer"

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

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

[Alm+19] Almeida et al., "Machine-Checked Proofs for Cryptographic Standards: Indistinguishability of Sponge and Secure High-Assurance Implementations of SHA-3"

[Haa+18] Haagh et al., "Computer-Aided Proofs for Multiparty Computation with Active Security"

[CSV19] Canetti et al., "EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security"

[Can00] Canetti, *Universally Composable Security: A New Paradigm for Cryptographic Protocols*
area of real-world application of UC is password-based authenticated key exchange, e. g., a recent paper by Gu, Jarecki, and Krawczyk [GJK21].

The Foundational Cryptography Framework [PM15] is built based on the Coq proof assistant, and thus foundational as in that it has a small trusted computing base that can be reviewed manually. It can be used to do exact security proofs, and has been used for cryptographic building blocks [Ber+15] and not for complex protocols; it is constrained by the same scaling problems as CertiCrypt and EasyCrypt.

Another possibility to obtain cryptographic guarantees in the computational model is to work in the symbolic model and use computational soundness results to lift analyses to the computational model. Then, one can benefit from the high degree of automation facilitated by the symbolic model. A survey by Cortier, Kremer, and Warinschi gives an overview of the state of computational soundness literature in the year 2011 [CKW11], summarizing computational soundness results and under which conditions they hold. The authors also survey computationally sound proof systems that “use symbolic methods and techniques in computational models”. A more recent computationally sound proof system has been introduced in 2014 by Bana and Comon, for a bounded number of sessions [BC14]. Intuitively, compared to symbolic models presented above, such models define what the adversary cannot do (up to a negligible probability). An extension to an arbitrary number of sessions, and the development of an interactive tool working in this framework, called Squirrel, have been presented by Baelde, Delaune, Jacomme, Koutsos, and Moreau [Bae+21]. A current practical limitation of this methodology is that the addition of new axioms to the prover requires extending the tool’s OCaml code – it is not yet possible to define axioms using the input language, like in CryptoVerif and EasyCrypt.

Back to the computational model, a recently introduced and promising methodology for game-based security proofs that provides some composition theorems is that of state-separating proofs [Brz+18]. A recent not-yet-published work applies it to parts of the Messaging Layer Security (MLS) secure group messaging protocol [BCK21]. A first mechanization in Coq has been done with SSProve [Aba+21], and work is being done for implementation in EasyCrypt [DKO21].

## 1.1 OUTLINE AND CONTRIBUTIONS

In Chapter 2, we introduce the proof methodology of game-based proofs, and the CryptoVerif proof assistant based on the example of the Needham-Schroeder-Lowe authentication protocol.

In the first part of this thesis, we present work supporting the main hypothesis of this thesis: that cryptographic proof assistants, and in particular CryptoVerif are practical for writing cryptographic proofs for complex real-world protocols using highly-detailed models, and that such analysis can substantially inform the design of cryptographic protocols.

[GJK21] Gu et al., “KHAPE: Asymmetric PAKE from Key-Hiding Key Exchange”

[PM15] Petcher and Morrisett, “The Foundational Cryptography Framework”

[Ber+15] Beringer et al., “Verified Correctness and Security of OpenSSL HMAC”

[CKW11] Cortier et al., “A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems”

[BC14] Bana and Comon-Lundh, “A Computationally Complete Symbolic Attacker for Equivalence Properties”

[Bae+21] Baelde et al., “An Interactive Prover for Protocol Verification in the Computational Model”

[Brz+18] Brzuska et al., “State Separation for Code-Based Game-Playing Proofs”

[BCK21] Brzuska et al., *Cryptographic Security of the MLS RFC*, Draft 11

[Aba+21] Abate et al., “SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq”

[DKO21] Dupressoir et al., *Bringing State-Separating Proofs to EasyCrypt - A Security Proof for Cryptobox*
1.1.1 WireGuard

In Chapter 3, we present cryptographic proofs of a comprehensive list of se-
curity properties for the WireGuard Virtual Private Network (VPN) protocol.
The WireGuard VPN has quickly seen widespread adoption, because of its
modern and simple design and implementation. This makes it an impor-
tant protocol worth of careful cryptographic analysis. WireGuard's success
continues: In the year 2020, one year after our cryptographic analysis was
published, it has been integrated into the Linux kernel. A hand-written
cryptographic proof of the WireGuard protocol was published before our
work, in a paper by Dowling and Paterson [DP18]. They modify the protocol
slightly to make it amenable for analysis as authenticated key exchange
protocol in an eCK model. We analyse the entire WireGuard protocol as it
is, in an ACCE-like model [Jag+12] as secure authenticated channel proto-
col, including transport data messages that have been excluded by [DP18].
Dowling and Paterson conduct their proof assuming a cyclic group. However,
the elliptic curve employed by WireGuard, Curve25519, does not consti-
tute a cyclic group. For our analysis, we create a detailed model of this
elliptic curve, taking into account its particularities like, for example, that
there are equivalent public keys. Overall, our analysis confirms WireGuard's
cryptographic security and uncovers an attack of theoretical interest, that
underlines the importance of detailed modelling of non-prime-order elliptic
curves.

[DP18] Dowling and Paterson, "A Crypto-graphic Analysis of the WireGuard Protocol"

[Jag+12] Jager et al., "On the Security of TLS-DHE in the Standard Model"

1.1.2 *Hybrid Public Key Encryption*

Chapter 4 and Chapter 5 are concerned with the Hybrid Public Key Encryp-
tion (HPKE) standard that has been published as RFC 9180 in February 2022.
We shaped its development substantially and became an official co-author. In
Chapter 4, we present a detailed analysis of one of HPKE's modes, indicating
and discussing exact security bounds, in the spirit of practice-oriented prov-
able security. Continuing our effort of creating detailed models of elliptic
curves, we introduce the framework of *nominal groups* to capture prime-
order and non-prime-order groups in one single model. In Section 5.1, we
present an analysis we did beforehand on all of HPKE's modes. In Section 5.2,
we summarize the most important contributions that we made to the crypto-
graphic design of the standard. In Section 5.2.5, we describe how we use an
implementation of HPKE developed by us to produce interesting information
that contributed to the standard. During the work on the HPKE standard, a
particular advantage of computer-aided proofs became practically useful:
the models and proofs were easily adaptable to new drafts of the standard,
with the peace-of-mind that the proof assistant checks everything again.
This would be much more tedious and error-prone to do entirely by hand.

1.1.3 *cv2fstar: Linking Computational Proofs and Implementations*

In the second part of the thesis, we consider the problem of obtaining crypto-
graphic guarantees on executable code. This aims to close a gap that is left
open most of the time: both cryptographic proofs and implementations are
usually produced starting from a specification; however, there is no assurance
that both interpretations match, and thus, that the cryptographic guarantees proved for the specification actually hold for the implementation. In the end, it is the implementation of a cryptosystem that matters for practical security, and so it is an important real-world problem to tackle. We chose the approach of linking the CryptoVerif proof assistant with the F\* programming language and proof assistant. To this end, in Chapter 6, we present cv2fstar, a tool that translates CryptoVerif models to executable specifications in F\*. This follows a long line of related work that we summarize in Section 6.2. In short, a link to executable specifications in another proof assistant, from highly-detailed models of complex protocols, written in a proof assistant like CryptoVerif that can prove concrete cryptographic security bounds, has not been done previously. Our case study on the Needham-Schroeder-Lowe protocol shows that our CryptoVerif models can be so detailed that we do not need to fill many gaps when linking to executable code. Notably, gaps that the CryptoVerif models hide using non-cryptographic assumptions like message encoding functions, can be closed by cv2fstar: the compiler generates F\* lemmas as proof obligations for these assumptions, such that they can be proved for the actual implementation. In a more global view, cv2fstar connects CryptoVerif to the large F\* ecosystem including the HACL\* verified cryptographic library.

Finally, in Chapter 7, we conclude, share our thoughts – looking back on the work presented in this thesis – on the placement of mechanized proofs within the cryptographic community, and lay out avenues for future work.

### 1.1.4 *Dependencies between Chapters*

Readers not familiar with game-based proofs or the CryptoVerif proof assistant are advised to read Chapter 2 before the remainder of the thesis. Chapter 3 and Chapter 4 can be read independently from the other chapters. Chapter 5 benefits from the introduction to HPKE and builds upon the formalisation of HPKE presented in Chapter 4, so we advise to read at least Section 4.1 and Section 4.6 before Chapter 5. Chapter 6 can be read independently, although it is advised to read Section 2.5 before, to better understand the case study presented in Section 6.15.

## 1.2 LIST OF PUBLICATIONS

During my time as PhD candidate at Inria, I was involved in the following conference publications, standards, and preprints.

### CONFERENCE PUBLICATIONS

Benjamin Lipp, Bruno Blanchet, and Karthikeyan Bhargavan. "A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol". In: *4th IEEE European Symposium on Security and Privacy*. Full version: https://hal.inria.fr/hal-02100345. Stockholm, Sweden: IEEE Computer Society, June 2019, pp. 231–246. DOI: 10.1109/EuroSP.2019.00026. See Chapter 3.

Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp, and Doreen Riepel. "Analysing the HPKE Standard". In: *EU-
ROCRYPT 2021, Part I. ed. by Anne Canteaut and François-Xavier Standaert. Vol. 12696. LNCS. Springer, Heidelberg, Oct. 2021, pp. 87–116. DOI: 10.1007/978-3-030-77870-5_4, Full version: https://eprint.iacr.org/2020/1499. See Chapter 4.

## REQUEST FOR COMMENTS (RFC)

Richard L. Barnes, Karthik Bhargavan, Benjamin Lipp, and Christopher A. Wood. *Hybrid Public Key Encryption*. RFC 9180. RFC Editor, Feb. 2022, pp. 1–107. URL: https://www.rfc-editor.org/rfc/rfc9180.html. See Section 5.2.

Formally, HPKE is an *Informational Request for Comments (RFC)* published by the IRTF, and only *Standards-Track RFCs* by the IETF can become official *Internet Standards*. Informally, RFCs like HPKE are also called a “standard” within the community. Thus, we use the terms *RFC* and *standard* interchangeably for HPKE, in this thesis. RFC 7418 <fnref n="4" />, and RFC 2014 <fnref n="5" /> provide an overview of how the IRTF and its research groups work. The Crypto Forum Research Group (CFRG) is one of them. <fnref n="6" />

## PREPRINT

Benjamin Lipp. *An Analysis of Hybrid Public Key Encryption*. Cryptology ePrint Archive, Report 2020/243. https://eprint.iacr.org/2020/243. 2020. See Section 5.1.

<footnote n="4">⁴https://www.rfc-editor.org/rfc/rfc7418.html</footnote>

<footnote n="5">⁵https://www.rfc-editor.org/rfc/rfc2014.html</footnote>

<footnote n="6">⁶https://irtf.org/cfrg</footnote>
<figure><img src="image_13.png" /></figure>
CryptoVerif is a proof assistant that formalizes cryptographic proofs by sequences of games, also called game hopping. Before introducing CryptoVerif, we briefly recap this proof methodology.

## 2.1 PROOFS BASED ON SEQUENCES OF GAMES

Game-based security notions model security properties by a game that gives an adversary a challenge to solve – solving the challenge is then interpreted as breaking the security property. We further describe this approach based on the tutorial paper by Victor Shoup [Sho04], and with references to an excerpt [FM21] from the hash book by Mittelbach and Fischlin [MF21] and to the introduction of code-based proofs by Bellare and Rogaway [BR04]. The game exposes oracles to communicate with the adversary, and the oracles might expect some input from the adversary, and might return an output. Shoup begins by saying that the game can be modeled as a probability space because game and adversary are probabilistic processes: oracles perform a possibly probabilistic computation, and their outputs are the random variables that the adversary sees from the probability space. The adversary is equally performing probabilistic computation. We assume that all computation is efficient, i. e., in bounded polynomial time.<fnref n="1" />

**ADVERSARY ADVANTAGE.** We separate two kinds of challenges that the adversary can face: computational tasks, where the adversary has to compute some value that satisfies some condition, e. g., forge a ciphertext, and distinguishing tasks, where the adversary has to decide between several but usually two options, e. g., determine which one of two messages the challenge oracle encrypted, or determine if the adversary is interacting with the left or right version of a game (or the “real” or “ideal” version, or the “real” or “random” version). We call the probability that the adversary solves the challenge, i. e., breaks the security property, the adversary advantage against the challenge. For computational tasks, this is simply the probability that the adversary succeeds to compute a value satisfying the winning condition. For distinguishing tasks between two options, we are interested in how much better the adversary is than guessing: here, we define the advantage as the difference between the probability that the adversary makes the right choice and the probability that uniform guessing wins (which is 1/2 when naively

<footnote>[Sho04] Shoup, *Sequences of games: a tool for taming complexity in security proofs*</footnote>

<footnote>[FM21] Fischlin and Mittelbach, *An Overview of the Hybrid Argument*</footnote>

<footnote>[MF21] Mittelbach and Fischlin, *The Theory of Hash Functions and Random Oracles - An Approach to Modern Cryptography*</footnote>

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

<footnote n="1">¹In this thesis, we do not consider quantum computation nor a quantum adversary.</footnote>
guessing a secret bit).

ASYMPTOTIC AND CONCRETE SECURITY. There are two frameworks for the evaluation of the adversary advantage: asymptotic security and concrete security (sometimes called exact security). In the framework of asymptotic security, the adversary advantage is evaluated only qualitatively. In this framework, the game is parametrized by a security parameter $\lambda \in \mathbb{N}$. Parameters of the game like key sizes and the number of calls that the adversary is allowed to issue to oracles, as well as the length of oracle inputs and outputs are assumed to be polynomial in $\lambda$. Security properties are defined to hold if the adversary advantage is negligible in $\lambda$: a function $\epsilon(\lambda)$ is negligible if for all polynomials $p$, there exists $\lambda_0 \in \mathbb{N}$ such that for all $\lambda \ge \lambda_0$, $\epsilon(\lambda) \le \frac{1}{p(\lambda)}$ [FM21]. A proof that tries to establish that the adversary advantage against the security property of some system is negligible usually assumes that some underlying cryptographic building blocks are secure – specifically, we assume that the adversary advantage against these building blocks is negligible. A result in the asymptotic framework means that there exists a $\lambda$ for which the security property holds, however it does not give an indication on how to select the actual parameters, like key sizes, such that the system is secure. We use this framework in our analysis of WireGuard, see Chapter 3.

In the framework of concrete security, the adversary advantage is evaluated quantitatively: theorems indicate the advantage as a function depending on the adversary advantage of breaking the cryptographic building blocks used in the system, the runtime of the adversary, the number of calls issued to oracles, and the length of oracle inputs and outputs. This framework allows to assess the security of a system for specific parameters. We use it in our analysis of HPKE's authenticated mode, see Chapter 4, where we evaluate the scheme's security level in bits.

In the following, we need a definition of computational indistinguishability. We adapt the definition of [FM21] to the concrete and asymptotic security framework:

**Definition 2.1** (Computational Indistinguishability ([FM21])) . In the concrete security framework, the advantage of a bounded-time probabilistic adversary $\mathcal{A}$ against the computational indistinguishability of two random variables $X, Y$ is

$$ \mathrm{Adv}_{\mathcal{A},X,Y}^{\mathrm{indist}} = |\mathrm{Pr}[\mathcal{A}(X) = 1] - \mathrm{Pr}[\mathcal{A}(Y) = 1]| . $$

In the asymptotic security framework, two random variables $X, Y$ are computationally indistinguishable if for all probabilistic polynomial adversaries $\mathcal{A}$, the advantage

$$ \mathrm{Adv}_{\mathcal{A},X,Y}^{\mathrm{indist}}(\lambda) = |\mathrm{Pr}[\mathcal{A}(\lambda, X(\lambda)) = 1] - \mathrm{Pr}[\mathcal{A}(\lambda, Y(\lambda)) = 1]| $$

is negligible.

For distinguishing tasks, the proof goal is to evaluate the adversary advantage against the computational indistinguishability of the left and the right version of the game (in the concrete security framework), or to

[FM21] Fischlin and Mittelbach, An Overview of the Hybrid Argument
show that the two versions are computationally indistinguishable (in the asymptotic security framework).

For computational tasks, the proof goal is to evaluate the adversary advantage to compute a value satisfying the winning condition (in the concrete security framework), or to show that this advantage is negligible (in the asymptotic security framework).

The de facto standard technique to write proofs for game-based security notions consists in formulating a sequence of games, sometimes called game hopping. Starting from an initial game, transformations are gradually made to the game, producing a sequence of games. For distinguishing tasks, the sequence stops at the other version of the game (the right, the ideal, or the random version of the game). For computational tasks, the sequence stops at a game for which it is straightforward to establish that the adversary advantage is negligible, or for which it is straightforward to quantify the adversary advantage in the concrete security framework. In principle, one could reason directly about the adversary advantage on the initial game. The interest of formulating a sequence of games is to reduce the complexity of the proof, to make it easier to understand.

In the asymptotic security framework, if any two consecutive games in the sequence are computationally indistinguishable, then the initial and the final game are computationally indistinguishable and the security property holds [FM21]. In the concrete security framework, for each two consecutive games, a bound is specified for the adversary advantage to computationally distinguish the distribution of the two game's outputs. An overall advantage can be computed with which the adversary computationally distinguishes the initial and the final game [BR04].

Shoup [Sho04] describes three types of game transformations that we introduce briefly in the following.

**TRANSFORMATIONS BASED ON INDISTINGUISHABILITY.** Transformations of this type from a game $G_0$ to a game $G_1$ rely on the assumption that some other two distributions are computationally indistinguishable. Thus, the proof that the distributions of $G_0$ and $G_1$ are indistinguishable is reduced to this assumption, in a *proof by reduction*: If an adversary can distinguish $G_0$ and $G_1$, this would mean that the adversary could also distinguish the other two distributions that are assumed to be indistinguishable. The adversary advantage to distinguish $G_0$ and $G_1$ has then a bound by the adversary advantage to break the assumption (in the exact security framework), or is negligible (in the asymptotic security framework).

An example for this type of transition is using a Decisional Diffie-Hellman (DDH) assumption to replace a Diffie-Hellman shared secret $g^{ab}$ in a game $G_0$ by a random group element in $G_1$. If the adversary can distinguish $G_0$ and $G_1$, it could be used to construct an adversary against DDH.

**TRANSFORMATIONS BASED ON FAILURE EVENTS.** Here, a game is transformed into a game that has the same output distribution except if a failure event $F$ occurs. The adversary advantage to distinguish the two games is the probability of the failure event $F$. This is backed by the following lemma.

**Definition 2.2** (Difference Lemma [Sho04]). Let A, B, F be events defined

<footnote>[FM21] Fischlin and Mittelbach, *An Overview of the Hybrid Argument*</footnote>

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

<footnote>[Sho04] Shoup, *Sequences of games: a tool for taming complexity in security proofs*</footnote>
in some probability distribution, and suppose that $A \land \neg F \iff B \land \neg F$. Then
$|\Pr[A] - \Pr[B]| \le \Pr[F]$.

For an example of this type of transformation, consider a game $G_0$ where
an AEAD scheme with nonces is used. Many AEAD schemes with nonces
lose at least some security properties in case a nonce is reused. Consider a
second game $G_1$ that is the same as $G_0$ but it does not encrypt if a nonce is
reused and instead aborts with a failure event. The adversary advantage to
distinguish the games is thus the probability that a nonce is reused.

BRIDGING STEPS. These transformations do not change the output distribu-
tions, but serve only to prepare for transformations of the other two types.
They do so by changing computations in an equivalent way, for example by
reordering independent computations, deleting unnecessary computations,
or inlining definitions.

2.2 INTRODUCTION TO CRYPTOVERIF

CryptoVerif is a proof assistant that helps to write game-based proofs. It for-
malizes the proof methodology by sequences of games presented above, and
can be used for analyses in the asymptotic and the concrete security frame-
work. Games are expressed in a well-specified language [Bla17], inspired
mainly by the applied pi-calculus [AF01], using a probabilistic semantics
instead of a non-deterministic one. CryptoVerif provides a high degree of
automation. The user is required to specify the initial game, the proof goals,
and optionally the game transformation steps. The transformation steps
are indicated with concise commands that instruct CryptoVerif to create the
sequence of games itself, writing the intermediary games automatically.

CryptoVerif can use all three types of transformations described in the
previous section, and all transformations applied by CryptoVerif are guar-
anteed to produce a sequence of computationally indistinguishable games.
CryptoVerif has an automatic mode where it can find which transforma-
tions to apply based on a built-in proof strategy. This way, simple protocols
can be proven completely automatically, without indicating any transfor-
mation steps. This is different from EasyCrypt [Bar+11] where the user
has to manually write all intermediary games and the proofs that they are
computationally indistinguishable.

CryptoVerif can prove secrecy, authentication, and indistinguishability
properties. Secrecy corresponds to real-or-random indistinguishability where
CryptoVerif proves that a variable in the game is indistinguishable from a
random value of the same type. Authentication properties are proved by
correspondences between events that are issued in the game. For example,
a correspondence could express that if some event has been executed, then
some other event has been executed before, where events may represent
that a participant A thinks they talk to a participant B, and conversely. For
indistinguishability properties, the user specifies two games, and CryptoVerif
transforms both of them until it can prove that they are indistinguishable.
We discuss these three kinds of properties in more detail in Section 2.4.

[Bla17] Blanchet, CryptoVerif: A Computationally-Sound Security Protocol Verifier

[AF01] Abadi and Fournet, “Mobile Values, New Names, and Secure Communication”

[Bar+11] Barthe et al., "Computer-Aided Security Proofs for the Working Cryptographer"
For each transformation, CryptoVerif keeps track of the adversary advan-
tage to distinguish the two games, and computes the final advantage based
on them. A successful proof and a final advantage are reached when in a
game, all desired properties can be proved. This is then the final game. As
all transformations have an advantage of being detected negligible in the
security parameter, the same holds for the final advantage. This means that
when CryptoVerif concludes with a proof, an asymptotic proof for the security
properties has been found. Furthermore, CryptoVerif indicates the exact
security bound depending on the number of oracle queries, the length of
inputs, the size of types, the execution time of the adversary, and the adver-
sary's advantage to break the security properties of cryptographic building
blocks.

CryptoVerif comes with a pre-defined set of cryptographic assumptions,
and users can also specify their own using CryptoVerif's input language.
There are limitations to the game transformations that can be used with
CryptoVerif. For example, cryptographic assumptions have to be expressed
in multi-instance versions, which means that a proof reducing multi-user
security to two-user security cannot be formalized in CryptoVerif. Further-
more, CryptoVerif cannot express generic hybrid arguments as described
in [FM21]. However, this and other simplifications allow the high degree of
automation in CryptoVerif, that makes the tool fit to handle large real-world
protocols like TLS [BBK17] and WireGuard, see Chapter 3.

In the following, we describe CryptoVerif's syntax and semantics.

2.3 SYNTAX AND SEMANTICS: OVERVIEW

CryptoVerif uses a language mainly inspired by the applied pi-calculus to
represent games [AF01]. This is a process calculus with probabilistic seman-
tics, developed for the purpose of analysing cryptographic protocols [Bla17].
Process calculi are fitted for the use case of interactive protocols because
they permit to model their concurrent nature with parallel executions.

CryptoVerif has two syntax frontends that are functionally equivalent: the
channels frontend that is adapted for users familiar with process calculi, and
the oracles frontend that is adapted for users more familiar with game-based
proofs from cryptographic literature.

CryptoVerif models the adversary as an evaluation context of the game.
[Bla17] shows that any bounded-time probabilistic Turing machine that
communicates with the game via oracles, can be expressed as an evaluation
context.

In the following, we use the oracles frontend to introduce CryptoVerif's
syntax and semantics. Figure 2.1 gives an overview of the most important
syntax elements, and we cover them briefly in this and the following sections.

Parallel execution is modeled via parallel composition of possibly dif-
ferent oracles, for example Q|Q', and replication of one oracle, that is
foreach i ≤ n do Q, which intuitively corresponds to an n times parallel
composition of Q. The value i is called a *replication index*. Interaction with
the adversary is modeled via oracle input parameters and oracle return val-
ues. At the beginning of the game and after each oracle return, the control

[FM21] Fischlin and Mittelbach, *An Overview of the Hybrid Argument*

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

[AF01] Abadi and Fournet, "Mobile Values, New Names, and Secure Communication"

[Bla17] Blanchet, CryptoVerif: A Computationally-Sound Security Protocol Verifier
<table>
  <tbody>
    <tr>
      <td>M, N ::=</td>
      <td>terms</td>
    </tr>
    <tr>
      <td>i</td>
      <td>replication index</td>
    </tr>
    <tr>
      <td>x[M<sub>1</sub>, ..., M<sub>m</sub>]</td>
      <td>variable access</td>
    </tr>
    <tr>
      <td>f(M<sub>1</sub>, ..., M<sub>m</sub>)</td>
      <td>function application</td>
    </tr>
    <tr>
      <td>x &harr; T; N</td>
      <td>random number</td>
    </tr>
    <tr>
      <td>let p = M in N else N'</td>
      <td>assignment (pattern-matching)</td>
    </tr>
    <tr>
      <td>let x : T = M in N</td>
      <td>assignment</td>
    </tr>
    <tr>
      <td>if defined(M<sub>1</sub>, ..., M<sub>l</sub>) &amp; M then N else N'</td>
      <td>conditional</td>
    </tr>
    <tr>
      <td>find[unique?] (&oplus;<sup>m</sup><sub>j=1</sub> u<sub>j1</sub>[i&#x0303;] = i<sub>j1</sub> &le; n<sub>j1</sub>, ..., u<sub>jm<sub>j</sub></sub>[i&#x0303;] = i<sub>jm<sub>j</sub></sub> &le; n<sub>jm<sub>j</sub></sub> suchthat defined(M<sub>j1</sub>, ..., M<sub>j<sub>l<sub>j</sub></sub>) &amp; M'<sub>j</sub> then N<sub>j</sub>) else N'</td>
      <td>array lookup</td>
    </tr>
    <tr>
      <td>insert tbl(M<sub>1</sub>, ..., M<sub>l</sub>); N</td>
      <td>insert in table</td>
    </tr>
    <tr>
      <td>get[unique?] tbl(p<sub>1</sub>, ..., p<sub>l</sub>) suchthat M in N else N'</td>
      <td>get from table</td>
    </tr>
    <tr>
      <td>event e(M<sub>1</sub>, ..., M<sub>l</sub>); N</td>
      <td>event</td>
    </tr>
    <tr>
      <td>event_abort e</td>
      <td>event e and abort</td>
    </tr>
  </tbody>
</table>

<table>
  <tbody>
    <tr>
      <td>p ::=</td>
      <td>pattern</td>
    </tr>
    <tr>
      <td>x : T</td>
      <td>variable assignment</td>
    </tr>
    <tr>
      <td>f(p<sub>1</sub>, ..., p<sub>m</sub>)</td>
      <td>function application</td>
    </tr>
    <tr>
      <td>=M</td>
      <td>comparison with a term</td>
    </tr>
  </tbody>
</table>

<table>
  <tbody>
    <tr>
      <td>Q ::=</td>
      <td>oracle definitions (input process)</td>
    </tr>
    <tr>
      <td>0</td>
      <td>nil</td>
    </tr>
    <tr>
      <td>Q | Q'</td>
      <td>parallel composition</td>
    </tr>
    <tr>
      <td>foreach i &le; n do Q</td>
      <td>replication n times</td>
    </tr>
    <tr>
      <td>O(p<sub>1</sub>, ..., p<sub>l</sub>) := P</td>
      <td>oracle definition</td>
    </tr>
  </tbody>
</table>

<table><caption>FIGURE 2.1: Syntax of CryptoVerif's process calculus in the oracles frontend. Adapted from [Bla17]</caption>
  <tbody>
    <tr>
      <td>P ::=</td>
      <td>oracle body (output process)</td>
    </tr>
    <tr>
      <td>return(M<sub>1</sub>,...,M<sub>l</sub>);Q</td>
      <td>oracle output</td>
    </tr>
    <tr>
      <td>x &harr; T; P</td>
      <td>random number</td>
    </tr>
    <tr>
      <td>let p = M in P else P'</td>
      <td>assignment</td>
    </tr>
    <tr>
      <td>if defined(M<sub>1</sub>,...,M<sub>l</sub>) &amp; M then P else P'</td>
      <td>conditional</td>
    </tr>
    <tr>
      <td>find[unique?] (&oplus;<sup>m</sup><sub>j=1</sub> u<sub>j1</sub>[i&#x0303;] = i<sub>j1</sub> &le; n<sub>j1</sub>,...,u<sub>jm<sub>j</sub></sub>[i&#x0303;] = i<sub>jm<sub>j</sub></sub> &le; n<sub>jm<sub>j</sub></sub> suchthat defined(M<sub>j1</sub>,...,M<sub>j<sub>l<sub>j</sub></sub>) &amp; M<sub>j</sub> then P<sub>j</sub>) else P</td>
      <td>array lookup</td>
    </tr>
    <tr>
      <td>insert tbl(M<sub>1</sub>,...,M<sub>l</sub>);P</td>
      <td>insert in table</td>
    </tr>
    <tr>
      <td>get[unique?] tbl(p<sub>1</sub>,...,p<sub>l</sub>) suchthat M in P else P'</td>
      <td>get from table</td>
    </tr>
    <tr>
      <td>event e(M<sub>1</sub>,...,M<sub>l</sub>);P</td>
      <td>event</td>
    </tr>
    <tr>
      <td>event_abort e</td>
      <td>event e and abort</td>
    </tr>
    <tr>
      <td>yield</td>
      <td>end</td>
    </tr>
  </tbody>
</table>
is given to the adversary, who can decide which oracle to call next. Crypto-Verif works in the computational model, and so, input and return values are bitstrings, and functions are from bitstrings to bitstrings. CryptoVerif allows to declare types that represent a certain subset of the bitstrings, and functions that work on any of the declared types. Security assumptions that express the computational indistinguishability of two processes $Q, Q'$ up to probability $p$ are noted as $Q \approx_p Q'$.

A CryptoVerif input file consists of a list of declarations followed by a structure of oracle definitions. This oracle structure describes the security game. The declarations contain type and function declarations, cryptographic and non-cryptographic assumptions, and queries that specify the security properties to prove.

## 2.4 SECURITY QUERIES

**SECRECY PROPERTIES.** The proof goal of secrecy of a variable $k$ is stated by the query query secret $k$. The meaning of this query is multi-session secrecy of $k$: CryptoVerif proves that the sequence of values of $k$ over all its replications (if $k$ is defined in an oracle under replication) is computationally indistinguishable from a sequence of the same length of randomly sampled values of the same type. Concretely, CryptoVerif proves this query by verifying that the values of $k$ for different replication indices are independent, and that for each replication, no oracle output depends on $k$. For the formal definition, see Definition 7 in [Bla17].

In our analysis of HPKE<sub>Auth</sub>, we use a secrecy query to prove the confidentiality security notions of HPKE displayed in Listing 4.6: a challenge bit $b$ is used by the challenge oracle to choose between two same-length plaintexts submitted by the adversary.

**AUTHENTICATION-LIKE PROPERTIES.** Correspondence queries permit to prove correspondence properties between events. There are three different variants that we want to discuss here. First, queries like “if an event A has been executed, then an event B has been executed before”. These are *non-injective* correspondences. For WireGuard, we use such a query to prove that the first protocol message cannot be forged if no key was compromised. However it can be replayed. Second, queries like “for each occurrence of the event A, there is a distinct occurrence of an event B”. These are called *injective* correspondences and permit to prove authentication properties where replay is not possible. Third, queries like “if an event A and an event B have been executed, then some equation holds”. In WireGuard, we use these to prove correctness of the protocol and resistance against unknown key-share attacks: If two parties have the same view on a protocol transcript, then they calculate the same key; if two parties calculate the same key, then they have the same view on the protocol transcript.

These three are only motivational examples. In fact, a non-injective correspondence is an implication between two logical formulae $\psi \Rightarrow \phi$, and these formulae can contain events. The grammar for logical formulae $\phi$ is the following [Bla07]:

[Bla17] Blanchet, CryptoVerif: A Computationally-Sound Security Protocol Verifier

[Bla07] Blanchet, “Computationally Sound Mechanized Proofs of Correspondence Assertions”
<figure><img src="image_14.png" /></figure>

The formula $M$ holds if the term $M$ evaluates to true, the formula $\text{event}(e(M_1, \dots, M_l))$ holds if the event has been executed, and conjunction and disjunction are defined as usual. For injective correspondences, the grammar for logical formula is extended with $\text{inj-event}(e(M_1, \dots, M_l))$. The left-hand formula $\psi$ is then a conjunction of injective or non-injective events.

The algorithm to check correspondences is much more involved than the one that checks secrecy. We only present the rough idea and refer to [Bla07] for more details. For all program points in a model, CryptoVerif collects true facts, which can be the value a variable is set to, the fact that a variable is defined, and the fact that an event has been executed. For injective events, CryptoVerif also collects information on the replication indices of the events. To prove a non-injective correspondence $\psi \Rightarrow \phi$, CryptoVerif collects all facts that hold at program points of events in $\psi$ and shows that these facts imply $\phi$ using an equational prover. For injective correspondences, it is shown that if the replication indices of two executions of injective events in $\psi$ are different, then the replication indices of the corresponding executions of the considered injective event of $\phi$ are also different [Bla07].

[Bla07] Blanchet, "Computationally Sound Mechanized Proofs of Correspondence As-sertions"

**INDISTINGUISHABILITY BETWEEN TWO GAMES.** For proofs of computational indistinguishability of two games, a CryptoVerif input file consists of a list of declarations followed by two structures of oracle definitions. To prove indistinguishability, CryptoVerif checks whether the two games are equivalent, term-by-term, while allowing variable names to be different. For example, we use this in our analysis of $\text{HPKE}_{\text{Auth}}$ to prove the confidentiality and authentication security notions of the KEM displayed in Listing 4.3, Listing 4.4, and Listing 4.5.

In the following, we explain the remainder of CryptoVerif's language elements based on an example.

## 2.5 EXAMPLE: THE NEEDHAM-SCHROEDER-LOWE PROTOCOL

The Needham-Schroeder and the Needham-Schroeder-Lowe (NSL) protocols have been the “Hello World” of security protocol verification methodologies since many years. We use NSL as an example to introduce CryptoVerif, and also for our first case study on cv2fstar, see Section 6.15.

The Needham-Schroeder shared-key and public-key protocols [NS78] have been presented in the year 1978, based on symmetric encryption and public-key encryption, respectively. The main goal of the protocols is to mutually authenticate two participants. In 1995, Lowe presented an attack on the public-key protocol and proposed an improved version that is called Needham-Schroeder-Lowe protocol [Low95] nowadays.

In the Needham-Schroeder-Lowe protocol, two participants A and B use a trusted key server to retrieve the other participant's public key. The

[NS78] Needham and Schroeder, "Using encryption for authentication in large networks of computers"

[Low95] Lowe, "An attack on the Needham-Schroeder public-key authentication protocol"
<figure><img src="image_15.png" /><figcaption>FIGURE 2.2: The simplified version of the Needham-Schroeder-Lowe protocol that we use. We assume that A and B possess a private key and know the other participant's public key $pk_{B,A}$. We assume that they have an address $addr_{A,B}$ and know the one of the other participant. The events $beginA$, $beginB$, $endA$, and $endB$ are used to express the authentication properties of the protocol.</figcaption></figure>

key server authenticates its messages using a digital signature. In our case study, we use a simplified version of the protocol without communication between key server and participants. Instead, we implement the key server as tables in CryptoVerif, that the two participants can access. This of course constitutes a stronger assumption, but keeps our example simpler.

### 2.5.1 Simplified Version of the Needham-Schroeder-Lowe Protocol

The version of the Needham-Schroeder-Lowe (NSL) protocol that we use is shown in Figure 2.2. The protocol has three messages.

For the first message, the initiator A samples a random nonce $N_A$. The initiator encrypts the nonce along with its identity $addr_A$ under the responder's public key $pk_B$. Successful decryption of this first message marks the event $beginB$ on the responder's side. The responder samples a random nonce $N_B$ and encrypts the two nonces along with its identity $addr_B$ under the initiator's public key $pk_A$. Successful decryption of this second message marks the event $beginA$ on the initiator's side. The initiator encrypts the nonce $N_B$ under the responder's public key and sends this ciphertext as third message. This marks event $endA$ on the initiator's side. Successful decryption of this third message marks the event $endB$ on the responder's side, and the protocol is finished. Both participants now have a guarantee that they are talking to the participant that they think to which they are talking, protected from replay attacks.

### 2.5.2 CryptoVerif Model for NSL

We base the CryptoVerif model for our version of NSL on a model shipped with CryptoVerif<fnref n="2" />. Changes we made include: using the oracle frontend, removing the key server, and adapting the top-level oracle structure. Also, we use a public-key encryption scheme where encryption can fail.

The main process of the model contains four top-level oracles that we outsource in separate process definitions using a syntax feature of Crypto-Verif: With the keyword `let`, we can encapsulate oracle definitions under a process name, and reuse it in the model with the keyword `run`. We use four such process definitions: the setup of the key pairs for the two honest participants A and B, the possibility for the adversary to register key pairs for dishonest participants, and finally the initiator and responder oracles.

<footnote n="2">²The file can be found in `examples/basic/needham-schroeder-pkcorrAuth.pcv`</footnote>
1 process
2 ( 
3 run setup()
4 |
5 run key_register()
6 |
7 run initiator()
8 |
9 run responder()
10 )

These processes are in parallel composition, so the adversary can call the first oracle in any of them in any order. Each of these separate processes begins in the same style. First it is declared using `let`. Then, we declare a replication of the top-level oracle:

1 let setup() =
2 foreach i ≤ Qsetup do
3     setup(addr: address) :=
4     ...
5 }.

The parameter `Qsetup` indicates the upper limit for the number of calls to the setup oracle. It is declared by a line

1 param Qsetup.

### 2.5.3 Types, Constants, Functions, and Equations

Types, constants, and functions in a CryptoVerif model are declared without implementation, it is just assumed that they exist.

**TYPES.** CryptoVerif's language is strongly typed, type conversions need to be done explicitely. Arbitrary type conversion functions can be defined. CryptoVerif defines the built-in types `bitstring`, `bitstringbot`, and `bool`, where `bitstringbot` contains all bitstrings and the special failure symbol `⊥` (bottom in code). A custom type `T` is declared as follows in a CryptoVerif model:

1 type T.

Types correspond to sets of bitstrings or $⊥$. A type can be declared with options `o`:

1 type T [o].

The most common options are fixed or bounded to indicate fixed-length bitstrings, or bitstrings with a maximum length; and `large` to indicate that the number of elements of this type is large enough such that the probability that two randomly sampled elements collide is negligible. If two options are used, they are separated by a comma. For more options, we refer to the CryptoVerif manual that is available in the CryptoVerif download. 3 The options determine from which probability distribution values are randomly sampled with $R \leftarrow (<-R$ in code).

**CONSTANTS.** A constant `c` of type `T` is declared as follows in a CryptoVerif model:

1 const c: T.

<footnote n="3">3 https://cryptoverif.inria.fr</footnote>
**FUNCTIONS.** A function $f$ with parameters of types $T_1, \dots, T_n$ of type $T$ is declared as follows in a CryptoVerif model:

1. `fun f(T<1, ..., T<\dots,n>): T.`

The optional `[data]` keyword can be added at the end. It indicates that $f$ is injective and has an efficiently computable inverse:

1. `fun f(T<1, ..., T<\dots,n>): T [data]`.

**EQUATIONS.** An equation is defined starting with the equation keyword, followed by a list of universally quantified variables with type indication, then a boolean term $M$ encoding the assumption, and optionally, the keyword if followed by a condition $M'$:

1. `equationforall v<1:T<1, ..., v<\dots:T<\dots; M if M'.`

Equations can be used to express non-cryptographic assumptions, like for example disjointness of function outputs, and assumptions about cryptographic building blocks, like for example correctness of an encryption scheme. This introduction does not cover the specification of cryptographic indistinguishability assumptions.

**TYPES, AND SOME CONSTANTS, FUNCTIONS, AND EQUATIONS IN NSL.** In the following, we list the main types used in the CryptoVerif model for NSL, and some constants and functions that go along with them.

We define nonce as a fixed, large type. For key-pair generation, we use a keyseed that is also defined as fixed and large type. Private keys skey and public keys pkey are declared `[bounded]`. The type keypair groups together a secret and public key. The type ciphertext is `[bounded]`. As mentioned earlier, encryption can fail, so we instantiate a CryptoVerif public-key encryption macro so that the return type of the encryption function is ciphertext\_opt. CryptoVerif does not support option types directly, but we can model an option type as follows:

1. `type ciphertext\_opt [bounded]`.

2. `fun ciphertext\_some(input): ciphertext\_opt [data]`.

3. `const ciphertext\_bottom: ciphertext\_opt`.

4. `equationforall x: ciphertext;`

5. `ciphertext\_some(x) <> ciphertext\_bottom.`

The type for plaintext is `[bounded]`. We use probabilistic public-key encryption, and so we need random coins for encryption. They have the `[bounded]` type encseed in our model. Finally, the `[bounded]` type address for the participant's identities.

### 2.5.4 Tables, and Their Use in the Setup and Registration Oracles

In a CryptoVerif model, tables are declared using

1. `table tbl(T<1, ..., T<\dots,n>)`.

where tbl is the table name and $T_1$ to $T_n$ are the types of an entry's fields. In a process, entries can be added to a table by a term

1. `insert tbl(M<1, ..., M<\dots,n>); N`
<caption>Listing 2.1: Code of the setup oracle.</caption>

1 setup(addr: address) :=
2   get[unique] all_keys(=addr, ign1, ign2) in (
3     yield
4   ) else
5     let kp(the_pkA: pkey, the_skA: skey) = keygen() in
6       insert trusted_keys(addr, the_skA, the_pkA);
7       insert all_keys(addr, the_pkA, true);
8     return(the_pkA)

where $M_1$ to $M_l$ must be terms with types matching the types of the table declaration. A table insert always succeeds in CryptoVerif, so there is no branching, and only one next term $M$ that is evaluated. Entries cannot be removed from tables.

A table is queried by a term

1 get tbl(p₁, ..., pᵢ) suchthat M in N' else N''

where $p_1$ to $p_l$ are patterns. We will explain patterns by example when they occur in the following. The query tries to find an entry with fields matching the patterns such that the term $M$ is true. If exactly one matching entry is found, the term evaluates to the result of $N'$. If more than one matching entries are found, one among them is chosen almost uniformly random, and the term evaluates to the result of $N'$. Otherwise, it evaluates to the result of $N''$. The keyword `[unique]` can be added directly after `get` to make it `[unique]`. Then, CryptoVerif tries to prove that there is only ever at most one matching table entry for this query, up to negligible probability.

We use two tables, `trusted_keys` and `all_keys`. Each table entry contains data about a participant. The table `trusted_keys` contains addresses and key pairs of honest participants. The table `all_keys` contains addresses and the public keys of all participants, and a trust bit indicating if this participant is honest.

1 table trusted_keys(address, skey, pkey).

2 table all_keys(address, pkey, bool).

The setup oracle generates a key pair and writes it to both tables, with the trust bit set to true, see Listing 2.1. Before generating and inserting the key pair, the oracle uses a `get[unique]` query to test if a key for the given address exists already. Here, we use an equality test pattern to compare the first field of a table entry with the variable `addr`, by using the `=addr` syntax. We do this check in the key register oracle, as well. This means entries are only added to the tables for a given address, if no entry for this address exists, yet. Thus, CryptoVerif can prove that the `get` queries indeed have at most one matching entry. In case a key pair is already registered for address `addr`, the oracle ends with `yield`, which gives control back to the adversary, letting it know that the oracle terminated with an error. In Line 5, there is an instance of pattern matching. As we describe later in more detail, the `keygen` function returns a key pair. The `kp` function constructs a key pair given a public key and a private key. In the pattern matching, the key pair returned by `keygen` is split into a public key and a private key using the
inverse of the function kp. If this pattern matching fails, the oracle implicitly
ends with `yield`.

The key register oracle writes public keys received from the adversary to
the table `all_keys` with the trust bit set to `false`:

1 register (addr: address, pkX: pkey) :=
2 get[unique] all_keys(=addr, ign1, ign2) in (
3   yield
4 ) else
5   insert all_keys(addr, pkX, false);
6 return ()

The initiator and responder oracles retrieve their own private key from
the table `trusted_keys`, and the public key of their interlocutor from the
table `all_keys`, see Section 2.5.8.

### 2.5.5 Message Encoding Functions

The message encoding functions `msg1`, `msg2`, and `msg3` return a value of type
`plaintext` and are declared `[data]` because we need a parser to retrieve
the message's fields on the recipient's side, respectively:

1 fun msg1(nonce, address): plaintext [data].

2 fun msg2(nonce, nonce, address): plaintext [data].

3 fun msg3(nonce): plaintext [data].

We assume that messages never collide, by using the following three equa-
tions:

1 equationforall z: nonce, t: nonce, u: address, y2: nonce, z2: address;

2 msg2(z, t, u) <> msg1(y2, z2).

3 equationforall y: nonce, y2: nonce, z2: address;

4 msg3(y) <> msg1(y2, z2).

5 equationforall z: nonce, t: nonce, u: address, y2: nonce;

6 msg2(z, t, u) <> msg3(y2).

### 2.5.6 Instantiating Public-Key Encryption

The only cryptographic assumption that we use to prove secure our vari-
ant of NSL is IND-CCA2 security of the probabilistic public-key encryption
scheme. The CryptoVerif library ships a macro that defines such a scheme
and that we instantiate with the types `keyseed`, `pkey`, `skey`, `plaintext",
`ciphertext_opt`, and `encseed`. The instantiation is as follows, and we
explain the other parameters step by step:

1 proba Penc.

2 proba Penccoll.

4 expand IND_CCA2_public_key_enc_all_args(

5 keyseed, pkey, skey, plaintext, ciphertext_opt, encseed,

6 skgen, skgen2, pkgen, pkgen2, enc, enc_r, enc_r2,

7 dec_opt, dec_opt2, injbot, Z, Penc, Penccoll).

The probability function Penc(t, N) stands for the adversary advantage
to break the IND-CCA2 property in time t for a key, using N queries to a
decryption oracle. The collision probability between private or public keys
that are independently generated is denoted by Penccoll.
The macro declares for us the functions skgen and pkgen that model generation of private and public keys. For encryption, it declares a deterministic encryption function enc_r that takes random coins as explicit parameter, and defines a probabilistic encryption function enc that samples random coins internally. Function declarations are always for deterministic functions in CryptoVerif, so enc has to use another language feature: With letfun definitions, CryptoVerif allows to reuse terms under a given name for convenience and better readability of the model; they are immediately inlined during the proof. Thus, enc is a letfun that wraps enc_r, passing the randomness to it:

1 fun enc_r(plaintext, pkey, encseed): ciphertext.

2 letfun enc(m: plaintext, pk: pkey) =

3 r <-R encseed; enc_r(m, pk, r).

For decryption, the macro declares a decryption function dec_opt, and a function injbot that injects the type plaintext into the type bitstringbot. The decryption function dec_opt takes a value of type ciphertext_opt as parameter, to allow it to be called on the failure value ciphertext_bottom. Outside the macro, we define a letfun function dec as a wrapper that can be called with a value of type ciphertext directly. It injects the value into ciphertext_opt using the function ciphertext_some before calling dec_opt:

1 letfun dec(c: ciphertext, sk: skey) =

2 dec_opt(ciphertext_some(c), sk).

The function names ending in 2 in the macro instantiation are not used in the initial game. They will appear in the game after CryptoVerif applies the IND-CCA2 transformation, replacing the occurrences of the function names without 2 by the function names with 2. This is so that the transformation cannot match again and let CryptoVerif end up in an infinite loop.

Finally, the macro declares a function Z that models the leakage of the plaintext length by the encryption scheme. It is used in the definition of the IND-CCA2 transformation.

Outside the macro, we declare a function kp that takes a public and a private key, and returns a keypair. We define a letfun keygen wrapping this function, sampling the key seed internally.

1 fun kp(pkey, skey): keypair [data].

2 letfun keygen() = k <-R keyseed; kp(pkgen(k), skgen(k)).

### 2.5.7 Events and Queries

In a CryptoVerif model, an event can be declared by

1 event e(T₁, ..., Tᵢ).

where e is the name of the event, and T₁ to Tᵢ are the types of its parameters. An event is invoked by a term

1 event e(M₁, ..., Mᵢ); N

where e is the name of an event that has been declared in the model, and M₁ to Mᵢ are terms with types matching the event's declaration. An event cannot fail, so there is no branching, and the return value of the term is
the evaluation of the following term $N$. An event can also be invoked by
`event_abort` in which case the game is stopped after executing the event,
and so there is no following term. CryptoVerif will try to prove that the
probability that this event is invoked is negligible. This is for example used
to prove that nonces are not reused in an AEAD scheme with nonces.

In our NSL model, the four events `beginA`, `beginB`, `endA`, and `endB` are
all declared to take both participants addresses and the two nonces as input:

1. `event beginA(address, address, nonce, nonce)`.

2. `event endA(address, address, nonce, nonce)`.

3. `event beginB(address, address, nonce, nonce)`.

4. `event endB(address, address, nonce, nonce)`.

This way, at the appropriate stages of the protocol, the participants record
what participant they believe to talk to, and based on what nonces.

As a reminder to what was presented when describing Figure 2.2, event `beginB` is issued when the responder successfully decrypted the first protocol message, event `beginA` is issued when the initiator successfully decrypted the second protocol message, event `endA` is issued after the initiator sent the third protocol message, and event `endB` is issued after the responder successfully decrypted the third protocol message. However, the events `endA` and `endB` are only issued if their interlocutor is marked as trusted in the table `all_keys`, respectively. This is because only in this situation, if two honest participants communicate, we want to prove mutual authentication. We ask CryptoVerif to prove the following correspondance queries, and it succeeds to do so in automatic mode:

1. `query x:address, y:address, na:nonce, nb:nonce;`

2. `inj-event(endA(x,y,na,nb)) = inj-eventSCOPESCOPESCOPESCOPESCOPE)(beginB(x,y,na,nb))`.

3. `query x:address, y:address, na:nonce, nb:nonce;`

4. `inj-event(endB(x,y,na,nb)) = inj-eventSCOPESCOPESCOPESCOPESCOPE)(beginA(x,y,na,nb))`.

This means that for two honest participants, for each event `endA`, there is a
unique event `beginB` with the same parameters, and likewise, for each event
`endB`, there is a unique event `beginA` with the same parameters. Intuitively,
this ensures that if an honest participant $P_1$ believes to have concluded the
protocol with another honest participant $P_2$ resulting in two nonces, then
this other participant $P_2$ has actually engaged in the protocol, too, believing
to talk to $P_1$, with the same nonces. Also, it ensures that there is no replay
attack.

### 2.5.8 Honest Participant Oracles

The initiator process exposes three oracles that can be called only in sequence.
This is modeled by defining the following oracles after the return of the
previous oracle, respectively. The first oracle sends the first protocol message,
the second oracle receives the second protocol message and sends the third
protocol message, and the third oracle issues the event `endA` if the responder
is honest. The responder process exposes two oracles that can be called
only in sequence. The first oracle receives the first and sends the second
protocol message, the second oracle receives the third protocol message and
issues the event `endB` if the initiator is honest. We only cover the code of
the initiator in this section, the code of the responder is included in the full
nsl.ocv file in Appendix A.1.
<caption>Listing 2.2: Code of the oracle sending the first protocol message.</caption>

```c
1 initiator_send_msg1(addrA: address, addrX: address) :=
2     (* the gets fail if addrA or addrX have not been
3      setup by the adversary. *)
4 get[unique] trusted_keys(=addrA, skA, pkA) in
5 get[unique] all_keys(=addrX, pkX, trustX) in
6     (* Prepare Message 1 *)
7 Na <-R nonce:
8     let cc1 = enc(msg1(Na, addrA), pkX) in
9     let ciphertext_some(c1: ciphertext) = cc1 in
10    return (c1);
```

The initiator's first oracle, `initiator_send_msg_1`, takes two addresses as parameters, see Listing 2.2. The first one instructs the oracle which identity to use as initiator, the second one is used for the responder. Thus, the adversary can request a communication between any two participants that have previously been set up either using the setup or the key register oracle. The oracle starts by trying to retrieve the private and public key for the initiator identity from the table `trusted_keys`, and the public key and trust bit for the responder identity from table `all_keys`. If any of these get requests fail, the oracle implicitly yields. If the requests are successful, a nonce is sampled, and the first protocol message is prepared and encrypted. Only if the encryption succeeds, tested by a pattern matching, the oracle returns successfully and sends the ciphertext to the adversary. If the pattern matching fails, the oracle implicitly yields.

The second oracle consumes the second protocol message and sends the third protocol messages. It takes only the ciphertext of the supposed second protocol message as parameter. Other variables, like `Na`, `addrX`, and `skA`, are still in scope from the previous oracle, because the oracles are defined in sequence.

```c
1 initiator_send_msg3 (c: ciphertext) :=
2     let injbot(msg2(=Na, Nb, =addrX)) = dec(c, skA) in
3     event beginA(addrA, addrX, Na, Nb);
4     let ciphertext_some(c3) = enc(msg3(Nb), pkX) in
5     return (c3);
```

The ciphertext is decrypted and if it is a valid plaintext, parsed as second message via the inverse of `msg2`, to retrieve the nonce `Nb`. Here, we use all three types of pattern matching shown in Figure 2.1: variable assignment, function application, and comparison with a term. Afterwards, event `beginA` is issued and the third message sent, if the encryption is successful.

The third oracle does not take parameters, its interest is to invoke the event `endA` if the other participant is trusted: we only want to prove authentication between trusted participants.

```c
1 initiator_finished() :=
2     if (trustX) then
3         event endA(addrA, addrX, Na, Nb);
4     return ()
```

The `else` branch of the condition is an implicit `yield`.
### 2.5.9 Elements Not Covered by the Example

**ARRAYS.** An extension of particular interest of CryptoVerif's calculus over other process calculi is the automatic accessibility of variable values via arrays: The value of a variable $x$ in a specific replication of an oracle can be accessed via array indices $x[i]$, where $i$ is the sequence of all replication indices needed to uniquely identify an oracle replication that is possibly nested. If an oracle is under multiple nested replications, the order of the replication indices is from the innermost to the outermost replication.

This is used in the find array lookup, which is useful for case distinctions in proofs. An array lookup find $i <= n$ such that $\text{defined}(x[i]) \wedge M$ then $N$ else $N'$ looks for a replication index $i$ in $n$ such that $x[i]$ is defined and the condition $M$ holds. If it finds one, it evaluates to $N$ with that index set; otherwise, it evaluates to $N'$. This can be extended to several branches by using orfind. The keyword [unique] can be used to specify that the lookup shall only succeed if exactly one index $i$ satisfying the condition is found. As a particular case of find, the built-in function defined can be used in an if conditional, too. An example for the usage of find for case distinctions in proofs is described at the end of Section 3.6.

**TUPLES.** In a CryptoVerif model, tuples can be constructed by wrapping multiple values into parentheses, separated by commas, like in this example: $(a, b, c)$. Tuples are of type bitstring. They do not appear in Figure 2.1 because they are seen as special case of a function application.

**NIL.** The last element from Figure 2.1 that is not yet explained is $\emptyset$. It is an input process that does nothing and can be used to make explicit that no oracles are exposed to the adversary.

This concludes the description of CryptoVerif's syntax and semantics. We are not describing how proofs are done in CryptoVerif. The correspondence queries in our NSL example are proved automatically by CryptoVerif without any proof statements necessary. The proof is done by reducing the security of the authentication property to the IND-CCA2 security of the public-key encryption scheme. A description of a proof with proof steps is included in the chapter about WireGuard, at the end of Section 3.6. A comparison of security notions in the style known from cryptography papers and their implementation in a CryptoVerif model can be found in Appendix C.2.

## 2.6 CONTRIBUTIONS TO CRYPTOVERIF'S USABILITY

During my work with CryptoVerif, I contributed various external scripts and ideas that have improved the usability of the tool. Three of them are highlighted in the following.

### 2.6.1 Referencing Terms in Intermediary Games

For proof guidance, CryptoVerif supports an insert command that is useful for case distinctions in a proof. For example, in the WireGuard proof, we introduce a case distinction in the initiator process, to treat separately the
CryptoVerif. CryptoVerif now indicates the first term in which the games
differ, making such indistinguishability proofs much more accessible.

2.6.3 Autocompletion for CryptoVerif's Interactive Mode

In CryptoVerif's interactive mode, the user has to type commands like crypto
ind_cca(enc) to guide the proof. Unlike many modern terminal emulators,
CryptoVerif's prompt does not provide autocompletion, such that the user
could type cr, press the tab key, and have CryptoVerif complete to crypto.
Also, CryptoVerif does not provide a command history that could be accessed
by the arrow keys, as in modern terminal emulators. I built a wrapper around
CryptoVerif that adds both features. 5 It provides command history across
usages. For autocompletion, it works with a predefined list of keywords
extracted from CryptoVerif's manual and the standard library. Unfortunately,
it cannot provide context-aware completion, as the wrapper has no knowl-
edge of the current game or proof. Building context-aware completion and
command history into CryptoVerif directly could be an interesting avenue
for future work on usability.

<footnote>5https://github.com/blipp/cryptoverif-completion/</footnote>
<figure><img src="image_16.png" /></figure>
Part II

CRYPTOVERIF CASE STUDIES ON REAL-WORLD PROTOCOLS
<figure><img src="image_17.png" /></figure>
This chapter and the appendix belonging to it are based on the long version [LBB19b] of the paper “A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol” published at IEEE’s EuroS&P 2019 with co-authors Bruno Blanchet and Karthikeyan Bhargavan [LBB19a].

ABSTRACT. 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. In this chapter, we present 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.

The traditional distinction between a secure intranet and the untrusted In-
ternet is becoming less relevant as more and more enterprises host internal
services on cloud-based servers distributed across multiple data centres. Sen-
sitive 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

[LBB19b] Lipp et al., *A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol*

[LBB19a] Lipp et al., "A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol"
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.¹

STANDARDS VS. CUSTOM PROTOCOLS. Most popular VPN solutions are based on Internet standards like IPsec [KY05] and TLS [Res18], 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 [BL16] and software flaws [Beu+15]. 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 [Bha+14a].

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 [MP16] used in many secure messaging systems and the Noise protocol framework [Per18].

WireGuard is a VPN protocol that adopts this design philosophy [Don17]. 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 [Don17], 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 [Bla16] and Tamarin [Mei+13] can help find logical flaws, and WireGuard already has been analysed using Tamarin [DM18]. 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. [BL16].)

¹https://cloud.google.com/vpn/doc
s/concepts/overview,
https://docs.aws.amazon.com/vpc/la
test/userguide/vpn-connections.htm
l,
https://azure.microsoft.com/en-us/
services/vpn-gateway/

[KY05] Kent and Yao, *Security Architecture for the Internet Protocol*

[Res18] Rescorla, *The Transport Layer Security (TLS) Protocol Version 1.3*

[BL16] Bhargavan and Leurent, "On the Practical (In-)Security of 64-bit Block Ciphers: Collision Attacks on HTTP over TLS and OpenVPN"

[Beu+15] Beurdouche et al., "A Messy State of the Union: Taming the Composite State Machines of TLS"

[Bha+14a] Bhargavan et al., "Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS"

[MP16] Marlinspike and Perrin, *The X3DH Key Agreement Protocol*

[Per18] Perrin, *The Noise Protocol Framework*

[Don17] Donenfeld, "WireGuard: Next Generation Kernel Network Tunnel"

[Bla16] Blanchet, "Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif"

[Mei+13] Meier et al., "The TAMARIN Prover for the Symbolic Analysis of Security Protocols"

[DM18] Donenfeld and Milner, *Formal Verification of the WireGuard Protocol*
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 [DP18], 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 chapter, we rely on the CryptoVerif protocol verifier [Bla08; Bla07] 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 misbinding, 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 [Don17]. In addition to classic key exchange security for IKpsk2, we examine the identity hiding and denial-of-service protections provided by WireGuard. We

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

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

<footnote>[Bla07] Blanchet, "Computationally Sound Mechanized Proofs of Correspondence Assertions"</footnote>

<footnote>[Don17] Donenfeld, "WireGuard: Next Generation Kernel Network Tunnel"</footnote>
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 Wire-Guard. 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 sev-eral extensions to CryptoVerif that we mention in the rest of the paper when we use them. These extensions are included in CryptoVerif as of version 2.01 available at https://cryptoverif.inria.fr/.

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

## 3.2 WIREGUARD

WireGuard [Don17] 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, in the year 2020, WireGuard has been incorporated into the Linux kernel with version 5.6,² 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 Wire-Guard 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.

[Don17] Donenfeld, "WireGuard: Next Generation Kernel Network Tunnel"

²https://arstechnica.com/gadgets/2020/03/wireguard-vpn-makes-it-to-1-0-0-and-into-the-next-linux-kernel/

### 3.2.1 Secure Channel Protocol: Noise IKpsk2

Noise [Per18] 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 3.1a, and the cryptographic computations are detailed in Figure 3.1b, using notations similar to [Don17]. Before the protocol begins, the initiator *i* and the responder *r* are assumed to have exchanged their long-term *static public keys* ($S_i^{pub}$, $S_r^{pub}$). 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.

[Per18] Perrin, *The Noise Protocol Framework*
<figure><img src="image_18.png" /><figcaption>Figure 3.1a: WireGuard's protocol messages.</figcaption></figure>

<figure><img src="image_19.png" /><figcaption>Figure 3.1c: Cookie mechanism under load.</figcaption></figure>

<figure><img src="image_20.png" /><figcaption>Figure 3.1b: Cryptographic Computations for Protocol Messages.</figcaption></figure>

FIGURE 3.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_{\oplus}$ for a variable containing an encryption of $x$; $x_{\ominus}$ 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_{\alpha}$ refers to all the bytes of a message up to but not including $mac_{1}$, $msg_{\beta}$ is the same but including $mac_{1}$. Session key derivation takes places after the second protocol message, symbolised by $\leftrightarrow$, at which point the initiator can send messages. The end of the handshake is symbolised by $\leftarrow$, 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.
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_i^{pub}$: a fresh ephemeral public key, generated by $i$,

• $S_{i \oplus}^{pub}$: $i$'s static public key, encrypted for $r$,

• $ts_{\oplus}$: a timestamp, encrypted with a key that can be computed only by $i$ and $r$, and

• $mac_1, mac_2$: message authentication codes (see Section 3.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_r^{pub}$: a fresh ephemeral public key, generated by $r$,

• empty$_{\oplus}$: 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 Section 3.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 session-specific 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 \rightarrow, T \leftarrow$) 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^{\rightarrow}$ or $N_j^{\leftarrow}$: the current message counter,

• $P_j$: an IP datagram, encrypted under the traffic key.

CRYPTOGRAPHIC COMPUTATIONS. Figure 3.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, \dots, H_7$) that hashes in all the public data used in the two handshake messages, including:

• protocol_name, prologue: strings identifying the protocol,

• $E_i^{pub}, E_r^{pub}$: both ephemeral public keys,

• $S_r^{pub}, S_{i \oplus}^{pub}$: both static public keys, but with the initiator's key in encrypted form,

• $ts_{\oplus}$, empty$_{\oplus}$: both encrypted handshake payloads, and

• $\pi$: 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, \dots, C_7$) by
mixing in all the key material, including:

*   protocol_name, $E_i^{\text{pub}}$, $E_r^{\text{pub}}$,

*   $\text{dh}(E_i^{\text{priv}}, S_r^{\text{pub}}) = \text{dh}(S_r^{\text{priv}}, E_i^{\text{pub}})$: 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*),

*   $\text{dh}(S_i^{\text{priv}}, S_r^{\text{pub}}) = \text{dh}(S_r^{\text{priv}}, S_i^{\text{pub}})$: the static-static shared secret,

*   $\text{dh}(E_i^{\text{priv}}, E_r^{\text{pub}}) = \text{dh}(E_r^{\text{priv}}, E_i^{\text{pub}})$: the ephemeral-ephemeral shared secret,

*   $\text{dh}(S_i^{\text{priv}}, E_r^{\text{pub}}) = \text{dh}(E_r^{\text{priv}}, S_i^{\text{pub}})$: the static-ephemeral shared secret, and

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

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* [LHT16]. 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 com-
promise of some of these keys. The psk also serves as a defensive coun-
termeasure 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 ($\pi$) for the second
message, and traffic keys ($T \leftarrow, T \rightarrow$) 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 asso-
ciated 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

[LHT16] Langley et al., *Elliptic Curves for Security*
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.

### 3.2.2 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.

To protect more actively against DoS, WireGuard incorporates a cookie-based protocol (depicted in Figure 3.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* ($\tau$) 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 $\tau$ 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 $\tau$ as the MAC key. After verifying this MAC, the responder continues with the standard handshake.

However, to obtain $\tau$, 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₂ 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.

### 3.2.3 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, which uses 32-byte private and public keys [LHT16];

* hash: all hash operations use the BLAKE2s hash function [SA15], which returns a 32-byte hash;

* aenc: authenticated encryption for handshake and traffic message uses the AEAD scheme ChaCha20Poly1305 [NL18], 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 into the standard ChaCha20Poly1305 construction [Ber11];

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

* hkdf<sub>n</sub>: all key derivations use the HKDF construction [KE10], 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<sub>1</sub> computation uses the UTF-8 string "mac1---" as label<sub>mac1</sub>, and the cookie computation uses "cookie-" as label<sub>cookie</sub>.

### 3.2.4 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 [Per18] and extending them with the additional DoS and
stealth goals of WireGuard [Don17]. In the following, we use *honest* to refer

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

<footnote>[SA15] Saarinen and Aumasson, *The BLAKE2 Cryptographic Hash and Message Authentication Code (MAC)*</footnote>

<footnote>[NL18] Nir and Langley, *ChaCha20 and Poly1305 for IETF Protocols*</footnote>

<footnote>[Ber11] Bernstein, *Extending the Salsa20 nonce*</footnote>

<footnote>[KE10] Krawczyk and Eronen, *HMAC-based Extract-and-Expand Key Derivation Function (HKDF)*</footnote>

<footnote>[Per18] Perrin, *The Noise Protocol Framework*</footnote>

<footnote>[Don17] Donenfeld, "WireGuard: Next Generation Kernel Network Tunnel"</footnote>
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 3.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 \leftarrow, T \leftarrow$) 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_i^{\text{priv}}$, $S_r^{\text{priv}}$) 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.

* **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 chapter, we investigate whether WireGuard achieves the goals set out above.

### 3.3 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.

#### 3.3.1 Random Oracle Model

We assume that BLAKE2s is a random oracle [BR93]. This assumption is justified in [LMN16] 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.

#### 3.3.2 IND-CPA and INT-CTXT for AEAD

We assume that the ChaCha20Poly1305 AEAD scheme [NL18] is IND-CPA (indistinguishable under chosen plaintext attacks) and INT-CTXT (ciphertext integrity) [BN00], 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 [Pro14], assuming ChaCha20 is a PRF (pseudo-random function) and Poly1305 is an $\epsilon$-almost-$\Delta$-universal hash function. The latter property is shown to hold in [Ber05].

#### 3.3.3 Curve25519 and Gap Diffie-Hellman

WireGuard uses the elliptic curve Curve25519 [LHT16] for Diffie-Hellman key exchanges. Curve25519, as implemented in WireGuard and as specified by RFC 7748 [LHT16], satisfies the following properties:

<footnote>[BR93] Bellare and Rogaway, "Random Oracles Are Practical: a Paradigm for Designing Efficient Protocols"</footnote>

<footnote>[LMN16] Luykx et al., "Security Analysis of BLAKE2s Modes of Operation"</footnote>

<footnote>[NL18] Nir and Langley, ChaCha20 and Poly1305 for IETF Protocols</footnote>

<footnote>[BN00] Bellare and Namprempre, "Authenticated Encryption: Relations among notions and analysis of the generic composition paradigm"</footnote>

<footnote>[Pro14] Procter, A Security Analysis of the Composition of ChaCha20 and Poly1305</footnote>

<footnote>[Ber05] Bernstein, "The Poly1305-AES Message-Authentication Code"</footnote>

<footnote>[LHT16] Langley et al., Elliptic Curves for Security</footnote>
1. It is an elliptic curve defined by an equation of the form $Y^2 = X^3 + AX^2 + X$ in the field $\mathbb{F}_p$ of non-zero integers modulo a large prime $p$, where $A^2 - 4$ is not a square modulo $p$.

2. 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 $\infty$ 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 $\infty$ 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 [Ber06, Theorem 2.1]: We consider the elliptic curve $E(\mathbb{F}_{p^2})$ defined by the equation $Y^2 = X^3 + AX^2 + X$ in a quadratic extension $\mathbb{F}_{p^2}$ of $\mathbb{F}_p$, we define $X_0 : E(\mathbb{F}_{p^2}) \to \mathbb{F}_{p^2}$ by $X_0(\infty) = 0$ and $X_0(X, Y) = X$, and for $X \in \mathbb{F}_p$ and $y$ an integer, we define $y \cdot X \in \mathbb{F}_p$ as $y \cdot X = X_0(yQ)$ for all $Q \in E(\mathbb{F}_{p^2})$ such that $X_0(Q) = X$.

6. The public keys (bitstrings in a finite set $G$) are mapped to elements of $\mathbb{F}_p$ by the function $decode_pk : G \to \mathbb{F}_p$ and conversely, elements of $\mathbb{F}_p$ are mapped to public keys by the function $encode_pk : \mathbb{F}_p \to G$, such that $decode_pk \circ encode_pk$ is the identity.

7. The Diffie-Hellman "exponentiation" $\exp : G \times \mathbb{Z} \to G$ is defined by

$$ \exp(X, y) = \text{encode\_pk}(y \cdot \text{decode\_pk}(X)) $$

8. The private keys are chosen uniformly in $\{kn | n \in S\}$ where $S \subseteq \{n_{\min}, \dots, 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} + \delta$ with $0 < \delta < 2^{128}$, $q' = 2^{253} - 9 - 2\delta$, $S = \{2^{251}, \dots, 2^{252} - 1\}$.<fnref n="3" />

The set $G$ of public keys consists of bitstrings of 32 bytes, or equivalently $G = \{0, \dots, 2^{256} - 1\}$. The function $decode_pk : G \to \mathbb{F}_p$ is defined by $decode_pk(X) = (X \mod 2^{255}) \mod p$. Conversely, $encode_pk : \mathbb{F}_p \to G$ is such that $encode_pk(X)$ is the representation of $X$ as an element of $\{0, \dots, 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 \cdot X$.

**Lemma 3.1.** 1. We can define $y \cdot X$ for $y$ in $\mathbb{Z}_{qq'}$.

2. $y \cdot (z \cdot X) = (yz) \cdot X$.

[Ber06] Bernstein, “Curve25519: New Diffie-Hellman Speed Records”

<footnote n="3">³The exact value of $\delta$ is $0x14def9dea2f79cd65812631a5cf5d3ed</footnote>
3. Let $Z$ be the set of integers multiple of $k$ and prime to $qq'$ modulo $kqq'$. For any $z \in Z$, for any $X, Y \in \mathbb{F}_p$, we have $z \cdot X = z \cdot Y$ if and only if $k \cdot X = k \cdot Y$.

4. Let $G_{\text{sub}} = \{k \cdot X \mid X \in \mathbb{F}_p\}$. For any $z$ prime to $qq'$, for any $X, Y \in G_{\text{sub}}$, we have $z \cdot X = z \cdot Y$ if and only if $X = Y$.

*Proof.* 1. We have $kqq'Q = \infty$ for any $Q$: if $Q$ is on the curve, then $kqQ = \infty$ since $\infty$ is the neutral element of the curve and its order is $kq$, so $kqq'Q = \infty$; if $Q$ is on the twist, then $k'q'Q = \infty$ since $\infty$ is the neutral element of the twist and its order is $k'q'$, so $kqq'Q = \infty$ since $kqq'$ is a multiple of $k'q'$. Hence, $(y + nkqq')Q = yQ$ for any $n$, so we can define $y \cdot X$ when $y$ is in $\mathbb{Z}_{kqq'}$.

2. We have $y \cdot (z \cdot X) = X_0(yQ')$ for all $Q' \in E(\mathbb{F}_{p^2})$ such that $X_0(Q') = z \cdot X = X_0(zQ)$ for all $Q \in E(\mathbb{F}_{p^2})$ such that $X_0(Q) = X$. Taking $Q' = zQ$, we have $y \cdot (z \cdot X) = X_0(yzQ)$ for all $Q \in E(\mathbb{F}_{p^2})$ such that $X_0(Q) = X$, so $y \cdot (z \cdot X) = (yz) \cdot 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'' \cdot (z \cdot X) = (zz'') \cdot X = (kz'z'') \cdot X = k \cdot X$ and similarly $z'' \cdot (z \cdot Y) = k \cdot Y$.

If $k \cdot X = k \cdot Y$, then $z \cdot X = (kz') \cdot X = z' \cdot (k \cdot X) = z' \cdot (k \cdot Y) = (kz') \cdot Y = z \cdot Y$. Conversely, suppose $z \cdot X = z \cdot Y$. Thus, $z'' \cdot (z \cdot X) = z'' \cdot (z \cdot Y)$, so $k \cdot X = k \cdot Y$.

4. We have $X = k \cdot X'$ and $Y = k \cdot Y'$ for some $X'$ and $Y'$. By 3. applied to $kz, X', Y'$, we have $(kz) \cdot X' = (kz) \cdot Y'$ if and only if $k \cdot X' = k \cdot Y'$. That is exactly $z \cdot X = z \cdot Y$ if and only if $X = Y$. $\square$

Property 2 implies that $\exp(\exp(g, y), z) = \text{encode\_pk}(z \cdot (y \cdot X_0(g_0))) = \text{encode\_pk}((zy) \cdot X_0(g_0))$, where $g = \text{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 \cdot \text{decode\_pk}(X) = k \cdot \text{decode\_pk}(Y)$ are equivalent, because they yield the same Diffie-Hellman shared secrets as shown by Lemma 3.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 \cdot 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 3.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_{\text{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_{\text{sub}}$ represents the set $\{k \cdot X \mid X \in \mathbb{F}_p\} = \{X_0(Q) \mid Q\}$ is 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 3.1. When honest participants choose private keys, they are chosen uniformly in a subset of $Z$, $\{kn \mid n \in S\}$, considered modulo $kqq'$. By hypothesis, $n \in 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_{\text{sub}}$, and so to work as much as possible with elements in $G_{\text{sub}}$. We rewrite the computations in $G$ into computations in $G_{\text{sub}}$ by first mapping the public keys $X \in G$ to $k \cdot \text{decode_pk}(X) \in G_{\text{sub}}$.

We define functions:

fun exp($G$, $Z$) : $G$.

fun mult($Z$, $Z$) : $Z$.

equation builtin commut(mult).

We let $\text{exp}(X, y) = \text{encode_pk}(y \cdot \text{decode_pk}(X))$ and $\text{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 $\text{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_{\text{sub}}$.

fun exp_div_k($G_{\text{sub}}$, $Z$) : $G_{\text{sub}}$.

fun $G_{\text{sub}}2G(G_{\text{sub}})$ : $G$ [data].

equationforall $X$ : $G_{\text{sub}}$, $X'$ : $G_{\text{sub}}$;

$$ (\text{pow}_k(\text{G}_{\text{sub}}2G(X)) = \text{pow}_k(\text{G}_{\text{sub}}2G(X'))) = (X = X'). $$

We have $\text{pow}_k(X) = k \cdot \text{decode_pk}(X)$, and it is in $G_{\text{sub}}$ for all $X$ in $G$. We have $\text{exp_div}_k(X, y) = (y/k) \cdot 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_{\text{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 \in \{0, \dots, k-1\}$, but all representatives yield the same value for $(y/k) \cdot X$: since $X \in G_{\text{sub}}$, there exists $X'$ such that $X = k \cdot X'$, so $(y' + nqq') \cdot X = (y' + nqq') \cdot (k \cdot X') = (ky' + nkqq') \cdot X' = y \cdot X'$. Moreover, this value is equal to $k \cdot (y' \cdot X')$, so it is in $G_{\text{sub}}$. The function $G_{\text{sub}}2G$ is $\text{encode_pk}$ restricted to $G_{\text{sub}}$; it converts elements of type $G_{\text{sub}}$ to type $G$. The annotation data tells CryptoVerif that it is injective. The last equation says that $\text{pow}_k \circ G_{\text{sub}}2G$ is injective. The function $\text{decode_pk} \circ G_{\text{sub}}2G$ is the identity, so $\text{pow}_k(G_{\text{sub}}2G(X)) = k \cdot X$ and similarly $\text{pow}_k(G_{\text{sub}}2G(X')) = k \cdot X'$. By Lemma 3.1, property 4, $k \cdot X = k \cdot X'$ if and only if $X = X'$.
We also define constants:

const zero : G.

const zero<sub>sub</sub> : G<sub>sub</sub>.

equation zero = G<sub>sub</sub>2G(zero<sub>sub</sub>).

const g : G.

const g_k : G<sub>sub</sub>.

equation pow_k(g) = g_k.

equation g_k ≠ zero<sub>sub</sub>.

The constant 0 is zero as an element of G and zero<sub>sub</sub> as an element of G<sub>sub</sub>. The constant g = encode_pk(X<sub>0</sub>(g<sub>0</sub>)) represents the base point, and g_k = k · decode_pk(g).

We also state equations that hold on these functions:

equation for all X : G, y : Z;

$$
\begin{align}
& \exp(X, y) \tag{3.1} \\
& = G_{\text{sub}} 2G(\exp_{\text{div}} k(\text{pow}_k(X), y)). \nonumber
\end{align}
$$

equation for all X : G<sub>sub</sub>, y : Z, z : Z;

$$
\begin{align}
& \exp_{\text{div}} k(\text{pow}_k(G_{\text{sub}} 2G(\exp_{\text{div}} k(X, y))), z) \tag{3.2} \\
& = \exp_{\text{div}} k(X, \text{mult}(y, z)). \nonumber
\end{align}
$$

Equation (3.1) follows from $y \cdot \text{decode_pk}(X) = (y/k) \cdot (k \cdot \text{decode_pk}(X))$ and Equation (3.2) from $(z/k) \cdot k \cdot (y/k) \cdot X = (yz/k) \cdot X$. Equation (3.2) applies in particular to simplify $\exp(\exp(X, y), z)$ after applying (3.1):

$$
\begin{align*}
\exp(\exp(X, y), z) \\
&= G_{\text{sub}} 2G(\exp_{\text{div}} k(\text{pow}_k(G_{\text{sub}} 2G(\exp_{\text{div}} k(\text{pow}_k(X), y))), z)) \\
&= G_{\text{sub}} 2G(\exp_{\text{div}} k(\text{pow}_k(X), \text{mult}(y, z)))
\end{align*}
$$

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_{\text{sub}}$, after mapping the public keys $X \in G$ to $k \cdot \text{decode_pk}(X) \in G_{\text{sub}}$. In particular, $\exp(g, y) = G_{\text{sub}} 2G(\exp_{\text{div}} k(g_k, y))$ and $\exp(\exp(g, y), z) = G_{\text{sub}} 2G(\exp_{\text{div}} k(g_k, \text{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 for all X : G<sub>sub</sub>, y : Z; (exp_div_k(X, y) = zero<sub>sub</sub>) = (X = zero<sub>sub</sub>).

equation for all X : G<sub>sub</sub>, y : Z; (exp_div_k(X, y) ≠ zero<sub>sub</sub>) = (X ≠ zero<sub>sub</sub>).

equation for all X : G<sub>sub</sub>; (pow_k(G<sub>sub</sub>2G(X)) = zero<sub>sub</sub>) = (X = zero<sub>sub</sub>).

equation for all X : G<sub>sub</sub>; (pow_k(G<sub>sub</sub>2G(X)) ≠ zero<sub>sub</sub>) = (X ≠ zero<sub>sub</sub>).

When $y \in Z$, $y = ky'$ for some $y'$ prime to $qq'$. Moreover, $y' \cdot 0 = 0$. Therefore, $(y/k) \cdot X = 0$ if and only if $y' \cdot X = y' \cdot 0$ if and only if $X = 0$ by Lemma 3.1, property 4. We have `pow_k(G<sub>sub</sub>2G(X)) = k \cdot X` and $k$ is
prime to $qq'$, so $k \cdot X = 0$ if and only if $k \cdot X = k \cdot 0$ if and only if $X = 0$ by Lemma 3.1, property 4.

Other properties serve to simplify equalities between Diffie-Hellman values in $G_{\text{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.

$$ \begin{array}{l} \text{equation for all } X: G_{\text{sub}}, X': G_{\text{sub}}, y: Z; \\ \qquad (\exp_{\text{div}}_k(X, y) = \exp_{\text{div}}_k(X', y)) = (X = X'). \end{array} \qquad (3.3) $$

$$ \begin{array}{l} \text{equation for all } X: G_{\text{sub}}, x': Z, y: Z; \\ \qquad (\exp_{\text{div}}_k(X, y) = \exp_{\text{div}}_k(\text{g}_k, \text{mult}(x', y))) = \\ \qquad (X = \text{pow}_k(G_{\text{sub}}2G(\exp_{\text{div}}_k(\text{g}_k, x')))). \end{array} \qquad (3.4) $$

$$ \begin{array}{l} \text{collision } y \stackrel{R}{\leftarrow} Z; z \stackrel{R}{\leftarrow} Z; [\text{random\_choices\_may\_be\_equal}] \text{forall } X: G_{\text{sub}}; \\ \qquad \text{return}(\exp_{\text{div}}_k(X, y) = \exp_{\text{div}}_k(X, z)) \\ \qquad \approx_{\text{Pcoll1rand}(Z)} \text{return}((X = \text{zero}_{\text{sub}}) \lor (y = z)). \end{array} \qquad (3.5) $$

$$ \begin{array}{l} \text{collision } x \stackrel{R}{\leftarrow} Z; \text{forall } X: G_{\text{sub}}, Y: G_{\text{sub}}; \\ \qquad \text{return}(\exp_{\text{div}}_k(X, x) = Y) \\ \qquad \approx_{2 \times \text{Pcoll1rand}(Z)} \text{return}((X = \text{zero}_{\text{sub}}) \land (Y = \text{zero}_{\text{sub}})) \\ \qquad \text{if } X \text{ independent-of } x \land Y \text{ independent-of } x. \end{array} \qquad (3.6) $$

$$ \begin{array}{l} \text{collision } x \stackrel{R}{\leftarrow} Z; \text{forall } y: Z, X: G_{\text{sub}}; \\ \qquad \text{return}(\exp_{\text{div}}_k(\text{g}_k, \text{mult}(x, y)) = X) \approx_{2 \times \text{Pcoll1rand}(Z)} \text{return}(\text{false}) \\ \qquad \text{if } y \text{ independent-of } x \land X \text{ independent-of } x. \end{array} \qquad (3.7) $$

$$ \begin{array}{l} \text{collision } x \stackrel{R}{\leftarrow} Z; y \stackrel{R}{\leftarrow} Z; [\text{random\_choices\_may\_be\_equal}] \text{forall } X: G_{\text{sub}}; \\ \qquad \text{return}(\exp_{\text{div}}_k(\text{g}_k, \text{mult}(x, y)) = X) \approx_{4 \times \text{Pcoll1rand}(Z)} \text{return}(\text{false}) \\ \qquad \text{if } X \text{ independent-of } x \lor X \text{ independent-of } y. \end{array} \qquad (3.8) $$

$$ \begin{array}{l} \text{collision } x \stackrel{R}{\leftarrow} Z; y \stackrel{R}{\leftarrow} Z; y' \stackrel{R}{\leftarrow} Z; [\text{random\_choices\_may\_be\_equal}] \\ \qquad \text{return}(\exp_{\text{div}}_k(\text{g}_k, \text{mult}(x, y)) = \exp_{\text{div}}_k(\text{g}_k, \text{mult}(x, y'))) \\ \qquad \approx_{\text{Pcoll1rand}(Z)} \text{return}(y = y'). \end{array} \qquad (3.9) $$

Equation (3.3) follows from Lemma 3.1, property 4 because $y = ky'$ for some $y'$ prime to $qq'$. In particular, using (3.1), injectivity of $G_{\text{sub}}2G$, and (3.3), $\exp(X, y) = \exp(X', y)$ simplifies into $\text{pow}_k(X) = \text{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 3.6, we fail to prove equality of the public keys $X = X'$ and can only prove $\text{pow}_k(X) = \text{pow}_k(X')$.

Equation (3.4) is a particular case of (3.3) when $X' = x' \cdot g_k = \text{pow}_k(G_{\text{sub}}2G(\exp_{\text{div}}_k(\text{g}_k, x')))$). However, CryptoVerif would not apply (3.3) to a term of the form $\exp_{\text{div}}_k(X, y) = \exp_{\text{div}}_k(\text{g}_k, \text{mult}(x', y))$).
Let us solve the equation $y \cdot X = z \cdot X$ for $X \in G_{\text{sub}}$. If $X = 0$, then $y \cdot X = 0 = z \cdot 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 \neq 0$, $Q \neq \infty$, so $Q$ is a generator of either of these subgroups. The equation $y \cdot X = z \cdot X$ means $X_0(yQ) = X_0(zQ)$, that is, $yQ = zQ$ or $yQ = -zQ$. If $Q$ is on the curve, this means $y \equiv z \pmod q$ or $y \equiv -z \pmod q$. If $Q$ is on the twist, this means $y \equiv z \pmod {q'}$ or $y \equiv -z \pmod {q'}$. In other words, $z + mq$ and $-z + mq$ are equivalent private keys for all $m$ and all public keys in $G_{\text{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_{\text{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 \in \{2^{251}, \dots, 2^{251} + \delta\}$ can both be honestly generated since $q-n \in \{2^{251}, \dots, 2^{251} + \delta\}$ in this case. Similarly, $kn$ and $k(q'-n)$ for $n \in \{2^{252}-8-2\delta, \dots, 2^{252}-1\}$ can both be honestly generated since $q'-n \in \{2^{252}-8-2\delta, \dots, 2^{252}-1\}.$)

In the collision statement (3.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 (3.5) means that the probability of distinguishing $\text{exp\_div\_k}(X, y) = \text{exp\_div\_k}(X, z)$ from $(X = \text{zero}_{\text{sub}}) \lor (y = z)$ is at most Pcoll1rand(Z), assuming y and z are chosen randomly in Z ($y \stackrel{R}{\leftarrow} Z; z \stackrel{R}{\leftarrow} Z$). The annotation $[\text{random\_choices\_may\_be\_equal}]$ means that the random choices $y \stackrel{R}{\leftarrow} Z$ and $z \stackrel{R}{\leftarrow} 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 (3.5), when $X = 0$ or $y = z$, both sides are true. Suppose now that $X \neq 0$ and $y \neq 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) \cdot X = (z/k) \cdot X$, so $y/k \equiv z/k \pmod q$ or $y/k \equiv -z/k \pmod q$ when $X = X_0(Q)$ for $Q$ on the curve and $y/k \equiv z/k \pmod {q'}$ or $y/k \equiv -z/k \pmod {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 \subseteq \{n_{\min}, \dots, n_{\max}\}$, the only possibility for $y/k \equiv z/k \pmod q$ or $y/k \equiv z/k \pmod {q'}$ is $y = z$, which is excluded, and the equations $y/k \equiv -z/k \pmod q$ and $y/k \equiv -z/k \pmod {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 (3.6) means that the probability of distinguishing $\text{exp\_div\_k}(X, x) = Y$ from $(X = \text{zero}_{\text{sub}}) \land (Y = \text{zero}_{\text{sub}})$ is at most $2 \times \text{Pcoll1rand}(Z)$ assuming x is chosen randomly in Z ($x \stackrel{R}{\leftarrow} Z$) and X and Y are independent of x. Indeed, suppose that $\text{exp\_div\_k}(X, x) = Y$ differs from $(X = \text{zero}_{\text{sub}}) \land (Y = \text{zero}_{\text{sub}})$. If $X = 0$, then $(x/k) \cdot X = 0$, so both expressions reduce to $Y = 0$, so they cannot differ. Therefore, $X \neq 0$. The second expression is then false. If $(x/k) \cdot X = Y$, then $Y = y \cdot X$ for some
y independent of x. Moreover $x = kn$ for $n \in S$ chosen randomly, and y is independent of n. The equality $(x/k) \cdot X = n \cdot X = Y = y \cdot X$ holds if and only if $n \equiv y \pmod q$ or $n \equiv -y \pmod q$ when $X = X_0(Q)$ for Q on the curve and $n \equiv y \pmod {q'}$ or $n \equiv -y \pmod {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 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) \cdot X = Y$ is true with probability at most $2 \times \text{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 (3.7), when the equality $\text{exp\_div\_k}(g_k, \text{mult}(x, y)) = X$ holds, we have $X = \text{exp\_div\_k}(g_k, z)$ for some $z \in Z$ independent of x. Hence, since $g_k$ corresponds to a point on the curve, $xy/k \equiv z/k \pmod q$ or $xy/k \equiv -z/k \pmod q$. Since $y/k$ is prime to $qq'$, so prime to $q$, $y/k$ is invertible modulo $q$, so $x \equiv z/y \pmod q$ or $x \equiv -z/y \pmod q$, and $z/y$ is independent of $x$, so these equalities happen with probability at most $2 \times \text{Pcoll1rand}(Z)$.

When x and y are independent, statement (3.8) is a consequence of statement (3.7). Suppose that x and y are the same random choice: $x = y$. When the equality $\text{exp\_div\_k}(g_k, \text{mult}(x, x)) = X$ holds, we have $X = \text{exp\_div\_k}(g_k, z)$ for some $z \in Z$ independent of x. Hence, since $g_k$ corresponds to a point on the curve, $x^2/k \equiv z/k \pmod q$ or $x^2/k \equiv -z/k \pmod q$, that is, $x^2 \equiv z \pmod q$ or $x^2 \equiv -z \pmod 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 \times \text{Pcoll1rand}(Z)$. (Furthermore, for Curve25519, $q \equiv 1 \pmod 4$, so $-1$ is a square modulo $q$, hence both z and $-z$ are squares simultaneously, so $x^2 \equiv z \pmod q$ or $x^2 \equiv -z \pmod q$ may have 4 solutions for x in total.)

Statement (3.9) holds when y and y' are the same random choice. When y and y' are independent random choices and $\text{exp\_div\_k}(g_k, \text{mult}(x, y)) = \text{exp\_div\_k}(g_k, \text{mult}(x, y'))$, since $g_k$ corresponds to a point on the curve, we have $xy/k \equiv xy'/k \pmod q$ or $xy/k \equiv -xy'/k \pmod q$. Since x is prime to $qq'$, so prime to $q$, x is invertible modulo $q$, so $y/k \equiv y'/k \pmod q$ or $y/k \equiv -y'/k \pmod q$. In the first case, since $q$ is greater than $n_{max} - n_{min}$ and $y/k$ and $y'/k$ are in $S \subseteq \{n_{min}, \dots, n_{max}\}$, we have $y = y'$. Hence the two sides of (3.9) differ only in the second case, which happens with probability less than $\text{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 $\text{exp\_div\_k}$ into $\text{exp\_div\_k'}$, in order to prevent the repeated application of the same game transformation. Hence, we define a symbol $\text{exp\_div\_k'}$ with the same equations and collision statements as $\text{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 [LHT16], which

<footnote>[LHT16] Langley et al., *Elliptic Curves for Security*</footnote>
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} - \delta$ with $0 < \delta < 2^{220}$, $q' = 2^{446} + \delta$, and the private keys are $kn$ for $n \in \{2^{445}, \dots, 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}, \dots, 2^{446} - 1\}$ are not all prime to $qq'$: $q$ is in $\{2^{445}, \dots, 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) \cdot 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}, \dots, 2^{446} - 1\} \setminus \{q\}$.

* $q \equiv -1 \pmod 4$, so $-1$ is not a square modulo $q$. Hence, in the proof of (3.8), the equalities $x^2 \equiv z \pmod q$ and $x^2 \equiv -z \pmod 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 (3.8) can be strengthened by reducing the probability difference to $2 \times \text{Pcoll1rand}(Z)$ instead of $4 \times \text{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 \equiv -1 \pmod 4$. The latter model is sound for both Curve25519 and Curve448.

We assume that $G_{\text{sub}}$ satisfies the gap Diffie-Hellman (GDH) assumption [OP01], in the following sense:

**Definition 3.1 (Gap Diffie-Hellman).** Given $g$ that corresponds to a generator of the subgroup of order $q$ of the curve and $\mathcal{E}_U = \{kn \mid n \in [(q+1)/2, q-1]\}$ considered modulo $kqq'$, $a \cdot g$, and $b \cdot g$ for random $a, b \in \mathcal{E}_U$, the adversary has a negligible probability to compute $(ab) \cdot g$ (computational Diffie-Hellman assumption), even when the adversary has access to decisional Diffie-Hellman oracles, which tell it

* given $U, V, W \in G_{\text{sub}}$, whether there exist $\beta \in \mathcal{E}_U$ such that $U = \beta \cdot g$, and $W = \beta \cdot V$;

* given $G, U, V, W \in G_{\text{sub}}$, whether there exist $\alpha, \beta \in \mathcal{E}_U$ such that $G = \alpha \cdot g$, $U = \beta \cdot g$, and $\alpha \cdot W = \beta \cdot V$.

Choosing the exponents in $\mathcal{E}_U$ guarantees the unicity of $\beta$ such that $U = \beta \cdot g$ ($\mathcal{E}$ stands for exponent, $U$ for unique). Moreover, $\mathcal{E}_U$ is close to the set of honestly generated exponents $\{kn \mid n \in S\}$: the statistical distance between the uniform distributions on these two sets is bounded by $2^{-126}$ (see Lemma 4.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 $\alpha \in \mathcal{E}_U$ such that $\alpha \cdot W = W$ for all $W \in G_{\text{sub}}$. We use the formulation of Definition 3.1 for the decisional Diffie-Hellman oracles to

[OP01] Okamoto and Pointcheval, “The Gap-Problems: a New Class of Problems for the Security of Cryptographic Schemes”
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 \cdot g$ for $u = \beta, V = v \cdot g$ for some $v$ so $W = (uv) \cdot g$; and for the second oracle $U = u \cdot G$ for $u = \beta/\alpha$ (since $\alpha$ is invertible modulo $q$) and $V = v \cdot G$ for some $v$, so $\alpha \cdot W = \beta \cdot V = (v\beta) \cdot G = (uv\alpha) \cdot G$ so $W = (uv) \cdot G$, hence there exist $u$ and $v$ such that $U = u \cdot G, V = v \cdot G$, and $W = (uv) \cdot 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 $\beta \cdot V$ corresponds to a point on the curve and $\alpha \cdot 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 \cdot X$ is point multiplication, the functions decode_pk and encode_pk are the identity. Then we have properties similar to Lemma 3.1, replacing $qq'$ with $q$: $y \cdot X$ is defined for $y \in \mathbb{Z}_{kq}$; $y \cdot (z \cdot X) = (yz) \cdot X$; for any $z \in Z$, $X, Y \in G$, we have $z \cdot X = z \cdot Y$ if and only if $k \cdot X = k \cdot Y$ (because $z = kz'$ for some $z'$ invertible modulo $q$); for any $z$ prime to $q$, for any $X, Y \in G_{sub}$, we have $z \cdot X = z \cdot Y$ if and only if $X = Y$ (because $z$ is invertible modulo $q$). Public keys $X$ and $Y$ are equivalent when $k \cdot X = k \cdot Y$, so each public key has $k$ equivalent public keys, including itself. Similarly to the previous model, $\exp(X, y) = y \cdot X$, mult is the product modulo $kq$ in $Z$, $\text{pow}_k(X) = k \cdot X$, and $\exp\_\text{div}_k(X, y) = (y/k) \cdot 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 $G_{sub}$ represent the neutral element of $G$, that is, the point at infinity $\infty$. The properties of these functions and constants until (3.4) are proved similarly to the previous model, replacing $qq'$ with $q$. Let us solve the equation $y \cdot X = z \cdot X$ for $X \in G_{sub}$. If $X = \infty$, then $y \cdot X = \infty = z \cdot X$ for all $y$ and $z$. Otherwise, $X$ is a generator of $G_{sub}$, so $y \cdot X = z \cdot X$ if and only if $y \equiv z \mod q$. As a result, we can strengthen (3.5) as follows:

$$ \text{equation for all } X : G_{\text{sub}}, y : Z, z : Z; \\ (\exp_{\text{div}_k}(X, y) = \exp_{\text{div}_k}(X, z)) = ((y = z) \lor (X = \text{zero}_{\text{sub}})). $$

In the proof of (3.6), $(x/k) \cdot X = n \cdot X = Y = y \cdot X$ holds if and only if $n \equiv y \mod q$, and the probability that the expressions differ is at most $\text{Pcoll1rand}(Z)$ instead of $2 \times \text{Pcoll1rand}(Z)$. Due to the strengthened form of (3.5), equalities $\exp_{\text{div}_k}(g_k, y) = \exp_{\text{div}_k}(g_k, z)$ are replaced with $y = z$. For this reason, we replace (3.7), (3.8), and (3.9) with properties
on private keys. Statement (3.7) becomes:

collision $x \stackrel{R}{\leftarrow} Z$; $\forall y: Z, z: Z$;
return(mult($x, y$) = $z$) $\approx_{\text{Pcoll1rand}(Z)}$ return(false)
if $y$ independent-of $x \land z$ independent-of $x$

since mult($x, y$) = $z$ means $xy \equiv z \mod kq$, so $xy/k \equiv z/k \mod q$ and $y$ is invertible modulo $q$, so $x/k \equiv z/ky \mod q$, so $x \equiv z/y \mod kq$. Since $z/y$ is independent of $x$, the equality $x \equiv z/y \mod kq$ has probability at most Pcoll1rand($Z$) to happen. Statement (3.8) becomes:

collision $x \stackrel{R}{\leftarrow} Z$; $y \stackrel{R}{\leftarrow} Z$; $[\text{random\_choices\_may\_be\_equal}]$ $\forall z: Z$;
return(mult($x, y$) = $z$) $\approx_{2 \times \text{Pcoll1rand}(Z)}$ return(false)
if $z$ independent-of $x \lor 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 \equiv z \mod kq$, so $x^2/k \equiv z/k \mod q$ so $(x/k)^2 \equiv z/k^2 \mod q$ since $k$ is invertible modulo $q$, and the probability that the expressions differ is at most $2 \times \text{Pcoll1rand}(Z)$ instead of $4 \times \text{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 (3.9) becomes

equation $\forall x: Z, y: Z, y': Z$; $(\text{mult}(x, y) = \text{mult}(x, y')) = (y = y')$

since mult($x, y$) = mult($x, y'$) means $xy \equiv xy' \mod kq$, so $xy/k \equiv xy'/k \mod q$, so $y/k \equiv y'/k \mod q$ since $x$ is invertible modulo $q$, so $y \equiv y'$ mod $kq$, that is, $y = y'$ in $Z$. Finally, the GDH assumption is needed only in the subgroup $G_{\text{sub}}$, so the twist is excluded. This model is presented in the conference version of this work [LBB19a], 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 [DP18] 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, Fischlin, Günther, and Janson [Bre+17] show that it is implausible to instantiate the PRF-ODH assumption without a random oracle, so our assumptions and the one of [DP18] are in fact fairly similar.

## 3.4 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,

<footnote>[LBB19a] Lipp et al., “A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol”</footnote>

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

<footnote>[Bre+17] Brendel et al., “PRF-ODH: Relations, Instantiations, and Impossibility Results”</footnote>
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 [MP16]. 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:

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

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:

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

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: [DP18] relies on the PRF-ODH assumption, [DM18] uses the symbolic model.

### 3.4.1 Definition of Indifferentiability

Indifferentiability can be defined as follows. This definition is an extension of [Cor+05] to several independent oracles.

**Definition 3.2 (Indifferentiability).** Functions $(F_i)_{1 \le i \le n}$ with oracle access to independent random oracles $(H_j)_{1 \le j \le m}$ are $(t_D, t_S, (q_{H_j})_{1 \le j \le m}, (q_{F_i})_{1 \le i \le n}, (q_{H'_i})_{1 \le i \le n}, \epsilon$)-indifferentiable from independent random oracles $(H'_i)_{1 \le i \le n}$ if there exists a simulator $S$ such that for any distinguisher $D$

$$| \Pr[D^{(F_i)_{1 \le i \le n}, (H_j)_{1 \le j \le m}} = 1] - \Pr[D^{(H'_i)_{1 \le i \le n}, S} = 1] | \le \epsilon$$

[MP16] Marlinspike and Perrin, The X3DH Key Agreement Protocol

[DP18] Dowling and Paterson, “A Cryptographic Analysis of the WireGuard Protocol”

[DM18] Donenfeld and Milner, Formal Verification of the WireGuard Protocol

[Cor+05] Coron et al., “Merkle-Damgård Revisited: How to Construct a Hash Function”
The simulator $S$ has oracle access to $(H'_i)_{1\le i\le 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_{H_j}$ queries to $H_j$ for $1 \le j \le m$ and $q_{F_i}$ queries to $F_i$ for $1 \le i \le n$.

In the game $G_0 = D^{(F_i)_{1\le i\le n}, (H_j)_{1\le j\le 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\le i\le 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 \le i \le n$; these simulators share a common
state.) Indifferentiability means that these two games are indistinguishable.

3.4.2 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 3.2 shows that random oracle calls
with disjoint domains are indifferentiable from calls to independent random
oracles.

**Lemma 3.2** (Version of [KBB17, Lemma 2] with more precise evaluation of numbers of oracle calls). If $H$ is a random oracle, then the functions $H_1, \dots, H_n$ defined as $H$ on disjoint subsets $D_1, \dots, D_n$ of the domain $D$ of $H$ are $(t_D, t_S, q_H, (q_{H_i})_{1\le i\le n}, (q'_{H_i})_{1\le i\le 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'_{H_i}$ is the number of requests to $H$ in domain $D_i$ made by the distinguisher. Hence $q'_{H_1} + \dots + q'_{H_n} \le q_H$, so in the worst case $q'_{H_i}$ is bounded by $q_H$.

Lemma 3.3 shows that the concatenation of two independent random
oracle calls is indifferentiable from a random oracle.

**Lemma 3.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 concate-
nation $H'$ of $H_1$ and $H_2$ is $(t_D, t_S, (q_{H_1}, q_{H_2}), q_{H'}, q_{H_1} + q_{H_2}, 0)$-indifferentiable
from a random oracle, where $t_S = O(q_{H_1} + q_{H_2})$.

Conversely, Lemma 3.4 shows that splitting the output of a random oracle
into two fixed length outputs yields independent random oracles.

**Lemma 3.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'}, q_{H'_2}), (q_H, q_H), 0)$-indifferentiable from independent random oracles, where $t_S = O(q_H)$.

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

**Lemma 3.5** (Already stated in [KBB17, 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 3.6 and 3.7 deal with the composition of two random oracle
calls in sequence. We extended CryptoVerif to be able to prove indistin-
guishability 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 3.4.1, which implies the indifferentiability result. We present the
proof of Lemma 3.6 as an illustration.

**Lemma 3.6.** If $H_1: S_1 \to S'_1$ and $H_2: S'_1 \times S_2 \to 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_{H_1}, q_{H_2}), q_{H_3}, q_{H_2}, \epsilon)$-indifferentiable from a random oracle, where $t_S = O(q_{H_1}q_{H_2})$ and $\epsilon = (2q_{H_2}q_{H_1} + q_{H_1}^2 + q_{H_2}q_{H_3} + q_{H_3}^2)/|S'_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) \in 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) \in L_1$ for some $x$, otherwise returns $u$ if $((y, z), u) \in 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 $\epsilon$. □

**Lemma 3.7.** If $H_1: S_1 \to S'_1$ and $H_2: S'_1 \times S_2 \to S'_2$ are independent random oracles, then $H'_1 = H_1$ and $H'_2$ defined by $H'_2(x) = H_2(H_1(x), x)$ are $(t_D, t_S, (q_{H_1}, q_{H_2}), (q_{H'_1}, q_{H'_2}), (q_{H_1} + q_{H_2}, q_{H_2}), \epsilon)$-indifferentiable from independent random oracles, where $t_S = O(q_{H_2})$ and $\epsilon = q_{H_2}(2q_{H_1} + 2q_{H'_1} + q_{H'_2} + 1)/|S'_1|$.

### 3.4.3 Indifferentiability of HKDF

The hkdf key derivation function is defined as follows [KE10]:

$$
\begin{align*}
\text{hkdf-extract}(\text{salt}, \text{key}) &= \text{hmac}(\text{salt}, \text{key}) \\
\text{hkdf-expand}_n(\text{prk}, \text{info}) &= k_1 \| \dots \| k_n \text{ where} \\
& \quad k_1 = \text{hmac}(\text{prk}, \text{info} \| i_0) \\
& \quad k_{i+1} = \text{hmac}(\text{prk}, k_i \| \text{info} \| i + i_0) \text{ for } 1 \le i < n \\
\text{hkdf-n}(\text{salt}, \text{key}, \text{info}) &= \text{hkdf-expand}_n(\text{hkdf-extract}(\text{salt}, \text{key}), \text{info})
\end{align*}
$$

where $n \le 255$, and $i_0 = 0x01$ and $i$ are of size 1 byte. In WireGuard, info is always empty, so we omit it in Section 3.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 3.8.** If `hmac` is a random oracle, then `hkdf-expand_n` is $(t_D, t_S, q_{hmac}, q_{hkdf-expand_n}, q_{hmac}, \epsilon)$-indifferentiable from a random oracle, where $t_S = O(q_{hmac})$ and $\epsilon = (3q_{hkdf-expand_n}q_{hmac} + q_{hmac}^2)/|M|$.

[KE10] Krawczyk and Eronen, HMAC-based Extract-and-Expand Key Derivation Function (HKDF)
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 Appendix B.)

**Lemma 3.9.** If `hmac` is a random oracle and $\mathcal{K} \cap (\mathcal{I}\|i_0 \cup \bigcup_{i=1}^{n-1} \mathcal{M}\|\mathcal{I}\|i + i_0) = \emptyset$, then $hkdf_n$ with domain $\mathcal{S} \times \mathcal{K} \times \mathcal{I}$ is $(t_D, t_S, q_{hmac}, q_{hkdf_n}, q_{hmac}, \epsilon)$-indifferentiable from a random oracle, where $t_S = O(q_{hmac}^2)$ and $\epsilon = (q_{hkdf_n}^2 + 4q_{hkdf_n}q_{hmac} + q_{hmac}^2)/|\mathcal{M}|$.

This result extends the proof given for $hkdf_2$ in [KBB17, Lemma 1]. Moreover, our proof is modular and partly made using CryptoVerif, thanks to the basic lemmas of Section 3.4.2.

*Proof sketch.* Since the domains are disjoint, by Lemma 3.2, the $(n+1)$ calls to `hmac` are indifferentiable from independent random oracles $H_0, \dots, 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 3.7, the computation of $k_2 = H_2(H_1(\text{prk}, \text{info}), \text{prk}, \text{info})$ is indifferentiable from a random oracle $k_2 = H'_2(\text{prk}, \text{info})$. Applying this reasoning $n$ times, the computation of $k_i$ for $1 \le i \le n$ is indifferentiable from independent random oracles $k_i = H'_i(\text{prk}, \text{info})$. By Lemma 3.3, concatenation of $H'_i$ for $1 \le i \le n$ is indifferentiable from a random oracle $H$, so $hkdf_n(\text{salt}, \text{key}, \text{info}) = k_1 \| \dots \| k_n = H(\text{prk}, \text{info})$, where $\text{prk} = H_0(\text{salt}, \text{key})$. By Lemma 3.6, we conclude that $hkdf_n$ is indifferentiable from a random oracle. $\square$

[KBB17] Kobeissi et al., “Automated Verification for Secure Messaging Protocols and their Implementations: A Symbolic and Computational Approach”

### 3.4.4 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.3 (Chain).** Let $m \ge 1$ be a fixed integer, let $C$ and $C_j$ with $0 \le j \le m+1$ be bitstrings of length $l'$, let $v_j$ with $0 \le j \le 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 \le j \le m$ be bitstrings of length $(l-l')$. We define the functions $\text{chain}_n, 0 \le n < m$ and the function $\text{chain}_m$ in the following way:

$$ \begin{array}{l} \text{chain}_n(v_0, \dots, v_n) = \\ \qquad C_0 = \text{const} \\ \qquad \text{for } j = 0 \text{ to } n \text{ do } C_{j+1} \| r_j = H(C_j, v_j) \\ \qquad \text{return } r_n \end{array} \qquad (3.11) $$

$$ \begin{array}{l} \text{chain}_m(v_0, \dots, v_m) = \\ \qquad C_0 = \text{const} \\ \qquad \text{for } j = 0 \text{ to } m \text{ do } C_{j+1} \| r_j = H(C_j, v_j) \\ \qquad \text{return } C_{m+1} \| r_m \end{array} \qquad (3.12) $$

The functions $\text{chain}_n, n < m$, have an output of length $(l-l')$, and the output length of $\text{chain}_m$ is $l$.

**Lemma 3.10.** If $H$ is a random oracle, then $\text{chain}_n$, for $n \le m$, are $(t_D, t_S, q_H, (q_{\text{chain}_n})_{0 \le n \le m}, (q_H)_{0 \le n \le m}, \epsilon)$-indifferentiable from independent random oracles, where $t_S = O(q_H^2)$ and $\epsilon = ((\sum_{n=0}^m n \cdot q_{\text{chain}_n}) \cdot q_H + q_H^2)/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.

### 3.4.5 Application to WireGuard

WireGuard employs BLAKE2s [Aum+13] 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 collision-resistant 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_r^{pub})$, $hash(H_1||E_i^{pub})$, $hash(H_4||E_r^{pub})$, and $hash(H_5||\pi)$, 80 bytes for $hash(H_2||S_{i\_\text{empty}}^{pub})$, 60 bytes for $hash(H_3||ts_{\_\text{empty}})$, 48 bytes for $hash(H_6||\text{empty}_{\_\text{key}})$, 40 bytes for $hash label_{\text{mac1}}||S_r^{pub})$, $hash label_{\text{mac1}}||S_i^{pub})$, and $hash label_{\text{cookie}}||S_m^{pub})$. In contrast, the length of the argument of BLAKE2s in HMAC(*k*, *m*) is 96 bytes or $64 + \text{length}(*m*)$, and in the computation of HKDF, *info* is empty in WireGuard, so the length of *m* is 32 bytes (key), 1 byte ($\text{info}||i_0$) or 33 bytes ($k_i||\text{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 3.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 [Dod+12, Theorem 3].

Moreover, the domains of the calls to HMAC in HKDF$_n$ are disjoint. Indeed, $\mathcal{K}$ consists of bitstrings of length 32 bytes, $\mathcal{I}||i_0$ consists of bitstrings of length 1 byte, and $\mathcal{M}||\mathcal{I}||i + i_0$ consists of bitstrings of length 33 bytes. By Lemma 3.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 3.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:

<table><tr><td>C<sub>0</sub></td><td>← const</td></tr><tr><td>C<sub>1</sub>||_||_</td><td>← HKDF<sub>3</sub>(C<sub>0</sub>, v<sub>0</sub>)</td></tr><tr><td>C<sub>2</sub>||k<sub>1</sub>||_</td><td>← HKDF<sub>3</sub>(C<sub>1</sub>, v<sub>1</sub>)</td></tr><tr><td>C<sub>3</sub>||k<sub>2</sub>||_</td><td>← HKDF<sub>3</sub>(C<sub>2</sub>, v<sub>2</sub>)</td></tr><tr><td>C<sub>4</sub>||_||_</td><td>← HKDF<sub>3</sub>(C<sub>3</sub>, v<sub>3</sub>)</td></tr><tr><td>C<sub>5</sub>||_||_</td><td>← HKDF<sub>3</sub>(C<sub>4</sub>, v<sub>4</sub>)</td></tr><tr><td>C<sub>6</sub>||_||_</td><td>← HKDF<sub>3</sub>(C<sub>5</sub>, v<sub>5</sub>)</td></tr><tr><td>C<sub>7</sub>||π||k<sub>3</sub></td><td>← HKDF<sub>3</sub>(C<sub>6</sub>, v<sub>6</sub>)</td></tr><tr><td>T'→||T'←||_</td><td>← HKDF<sub>3</sub>(C<sub>7</sub>, v<sub>7</sub>)</td></tr></table>

Because of the way HKDF$_n$ is constructed, this is actually the same computation.

<footnote>[Aum+13] Aumasson et al., “BLAKE2: Simpler, Smaller, Fast as MD5”</footnote>

<footnote>[Dod+12] Dodis et al., “To Hash or Not to Hash Again? (In)Differentiability Results for $H^2$ and HMAC”</footnote>
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 3.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 Section 3.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 Section 3.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) [Jag+12] 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.

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.

### 3.5.2 Modelling Tricks

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

[Jag+12] Jager et al., "On the Security of TLS-DHE in the Standard Model"