[KBB17] Nadim Kobeissi, Karthikeyan Bhargavan, and Bruno Blanchet. "Automated Verification for Secure Messaging Protocols and their Implementations: A Symbolic and Computational Approach". In: *2nd IEEE European Symposium on Security and Privacy*. IEEE, Apr. 2017, pp. 435-450 (cit. on pp. 5, 55, 57, 74, 82, 126, 204).

[Kob07] Neal Koblitz. "Another look at automated theorem-proving". In: *Journal of Mathematical Cryptology* 1.4 (2007), pp. 385-403. DOI: doi:10.1515/jmc.2007.020. URL: https://doi.org/10.1515/jmc.2007.020 (cit. on pp. 182, 184).

[Kob12] Neal Koblitz. "Another look at automated theorem-proving II". In: *Journal of Mathematical Cryptology* 5.3-4 (2012), pp. 205-224. DOI: doi:10.1515/jmc-2011-0014. URL: https://doi.org/10.1515/jmc-2011-0014 (cit. on p. 182).

[KBC97] H. Krawczyk, M. Bellare, and R. Canetti. *HMAC: Keyed-Hashing for Message Authentication*. RFC 2104. RFC Editor, Feb. 1997, pp. 1-11. URL: https://www.rfc-editor.org/rfc/rfc2104.html (cit. on p. 107).

[KE10] H. Krawczyk and P. Eronen. *HMAC-based Extract-and-Expand Key Derivation Function (HKDF)*. RFC 5869. RFC Editor, May 2010, pp. 1-14. URL: https://www.rfc-editor.org/rfc/rfc5869.html (cit. on pp. 41, 56, 107).

[KTG12] Ralf Küsters, Tomasz Truderung, and Juergen Graf. "A Framework for the Cryptographic Verification of Java-Like Programs". In: *25th IEEE Computer Security Foundations Symposium, CSF 2012, Cambridge, MA, USA, June 25-27, 2012*. Ed. by Stephen Chong. IEEE Computer Society, 2012, pp. 198-212. DOI: 10.1109/CSF.2012.9. URL: https://doi.org/10.1109/CSF.2012.9 (cit. on p. 128).

[LHT16] A. Langley, M. Hamburg, and S. Turner. *Elliptic Curves for Security*. RFC 7748. RFC Editor, Jan. 2016, pp. 1-22. URL: https://www.rfc-editor.org/rfc/rfc7748.html (cit. on pp. 39, 41, 43, 50, 79, 84, 87, 88).

[LGR21] Julia Len, Paul Grubbs, and Thomas Ristenpart. "Partitioning Oracle Attacks". In: *30th USENIX Security Symposium (USENIX Security 21)*. USENIX Association, Aug. 2021, pp. 195-212. ISBN: 978-1-939133-24-3. URL: https://www.usenix.org/conference/usenixsecurity21/presentation/len (cit. on p. 119).

[Lip20] Benjamin Lipp. *An Analysis of Hybrid Public Key Encryption*. Cryptology ePrint Archive, Report 2020/243. https://eprint.iacr.org/2020/243. 2020 (cit. on pp. 9, 112).

[LBB19a] 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 (cit. on pp. 8, 33, 53).

[LBB19b] Benjamin Lipp, Bruno Blanchet, and Karthikeyan Bhargavan. *A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol*. Research Report RR-9269. Inria Paris, Apr. 2019, p. 49. URL: https://hal.inria.fr/hal-02100345 (cit. on p. 33).

[Low95] Gavin Lowe. "An attack on the Needham-Schroeder public-key authentication protocol". In: *Information Processing Letters* 56.3 (1995), pp. 131-133. ISSN: 0020-0190. DOI: https://doi.org/10.1016/0020-0190(95)00144-2. URL: https://www.sciencedirect.com/science/article/pii/0020019095001442 (cit. on pp. 4, 18).

[Low96] Gavin Lowe. "Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR". In: *Tools and Algorithms for the Construction and Analysis of Systems*. Ed. by Tiziana Margaria and Bernhard Steffen. Berlin, Heidelberg: Springer Berlin Heidelberg, 1996, pp. 147-166. ISBN: 978-3-540-49874-2 (cit. on p. 4).

[LMN16] Atul Luykx, Bart Mennink, and Samuel Neves. "Security Analysis of BLAKE2s Modes of Operation". In: *IACR Transactions on Symmetric Cryptology* 2016.1 (Dec. 2016), pp. 158-176 (cit. on p. 43).

[MP16] Moxie Marlinspike and Trevor Perrin. *The X3DH Key Agreement Protocol*. Available at https://signal.org/docs/specifications/x3dh/. Nov. 2016 (cit. on pp. 34, 54).

[Mei+13] Simon Meier, Benedikt Schmidt, Cas Cremers, and David A. Basin. "The TAMARIN Prover for the Symbolic Analysis of Security Protocols". In: *Computer Aided Verification, CAV'13*. Vol. 8044. LNCS. Springer, 2013, pp. 696-701 (cit. on pp. 5, 34).

[MF21] Arno Mittelbach and Marc Fischlin. *The Theory of Hash Functions and Random Oracles - An Approach to Modern Cryptography*. Information Security and Cryptography. Springer, 2021. ISBN: 978-3-030-63286-1. DOI: 10.1007/978-3-030-63287-8 (cit. on p. 11).

[Nat13] National Institute of Standards and Technology. *Digital Signature Standard (DSS)*. FIPS Publication 186-4. July 2013. URL: https://doi.org/10.6028/nist.fips.186-4 (cit. on pp. 79, 84, 87, 88).

[NS78] Roger M. Needham and Michael D. Schroeder. "Using encryption for authentication in large networks of computers". In: *Communications of the Association for Computing Machinery* 21.21 (Dec. 1978), pp. 993-999 (cit. on pp. 4, 18).
[NL18] Yoav Nir and Adam Langley. ChaCha20 and Poly1305 for IETF Protocols. IETF RFC 8439. June 2018 (cit. on pp. 41, 43).

[OP01] Tatsuaki Okamoto and David Pointcheval. "The Gap-Problems: a New Class of Problems for the Security of Cryptographic Schemes". In: PKC 2001. Vol. 1992. LNCS. Springer, Feb. 2001, pp. 104–118 (cit. on pp. 51, 116).

[Oma+20] E. Omara, Benjamin Beurdouche, E. Rescorla, S. Inguva, A. Kwon, and A. Duric. The Messaging Layer Security (MLS) Architecture. Internet-Draft draft-ietf-mls-architecture-05. IETF Secretariat, July 2020. URL: https://tools.ietf.org/html/draft-ietf-mls-architecture-05 (cit. on p. 80).

[Per18] Trevor Perrin. The Noise Protocol Framework. https://noiseprotocol.org/noise.html. July 2018 (cit. on pp. 34, 36, 41).

[PM15] Adam Petcher and Greg Morrisett. "The Foundational Cryptography Framework". In: Principles of Security and Trust. Ed. by Riccardo Focardi and Andrew Myers. Berlin, Heidelberg: Springer Berlin Heidelberg, 2015, pp. 53–72 (cit. on pp. 6, 128).

[PS10] Alfredo Pironti and Riccardo Sisto. "Provably correct Java implementations of Spi Calculus security protocols specifications". In: Computers & Security 29.3 (2010). Special issue on software engineering for secure systems, pp. 302–314. ISSN: 0167-4048. DOI: https://doi.org/10.1016/j.cose.2009.08.001. URL: https://www.sciencedirect.com/science/article/pii/S0167404809000832 (cit. on p. 128).

[Pol+20] Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, and Santiago Zanella-Béguelin. "HACLxN: Verified Generic SIMD Crypto (for All Your Favourite Platforms)". In: Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security. New York, NY, USA: Association for Computing Machinery, 2020, pp. 899918. ISBN: 9781450370899. URL: https://doi.org/10.1145/3372297.3423352 (cit. on pp. 119, 126).

[Pro14] Gordon Procter. A Security Analysis of the Composition of ChaCha20 and Poly1305. Cryptology ePrint Archive, Report 2014/613. https://eprint.iacr.org/2014/613. 2014 (cit. on pp. 43, 68).

[Pro+19] Jonathan Protzenko, Benjamin Beurdouche, Denis Merigoux, and Karthikeyan Bhargavan. "Formally Verified Cryptographic Web Applications in WebAssembly". In: 2019 IEEE Symposium on Security and Privacy, SP 2019, San Francisco, CA, USA, May 19-23, 2019. IEEE, 2019, pp. 1256–1274. DOI: 10.1109/SP.2019.00064 (cit. on p. 126).

[Pro+17] Jonathan Protzenko, Jean Karim Zinzindohoue, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Ctlin Hricu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy. "Verified Low-Level Programming Embedded in F*". In: 22nd International Conference on Functional Programming (ICFP 2017). ACM SIGPLAN, 2017. URL: https://www.microsoft.com/en-us/research/publication/verified-low-level-programming-embedded-f/ (cit. on pp. 126, 167).

[RBS20] Leonie Reichert, Samuel Brack, and Björn Scheuermann. A Survey of Automatic Contact Tracing Approaches Using Bluetooth Low Energy. Cryptology ePrint Archive, Report 2020/672. https://eprint.iacr.org/2020/672. 2020 (cit. on p. 3).

[Res18] E. Rescorla. The Transport Layer Security (TLS) Protocol Version 1.3. IETF RFC 8446. 2018 (cit. on pp. 4, 34).

[Res+20] E. Rescorla, K. Oku, N. Sullivan, and C. A. Wood. TLS Encrypted Client Hello. Internet-Draft draft-ietf-tls-esni-07. IETF Secretariat, June 2020. URL: https://tools.ietf.org/html/draft-ietf-tls-esni-07 (cit. on p. 79).

[Rog15] Phillip Rogaway. The Moral Character of Cryptographic Work. Cryptology ePrint Archive, Report 2015/1162. https://eprint.iacr.org/2015/1162. 2015 (cit. on pp. 3, 182).

[SA15] M-J. Saarinen and J-P Aumasson. The BLAKE2 Cryptographic Hash and Message Authentication Code (MAC). IETF RFC 7693. 2015 (cit. on p. 41).

[SSW20] Peter Schwabe, Douglas Stebila, and Thom Wiggers. "Post-Quantum TLS Without Handshake Signatures". In: ACM CCS 2020. Ed. by Jay Ligatti, Xinming Ou, Jonathan Katz, and Giovanni Vigna. ACM Press, Nov. 2020, pp. 1461–1480. DOI: 10.1145/3372297.3423350 (cit. on p. 185).

[Sho04] Victor Shoup. Sequences of games: a tool for taming complexity in security proofs. Cryptology ePrint Archive, Report 2004/332. https://eprint.iacr.org/2004/332. 2004 (cit. on pp. 4, 11, 13).

[Sis+11] Riccardo Sisto, Matteo Avalle, Alfredo Pironti, and Davide Pozza. "JavaSPI: A Framework for Security Protocol Implementation". In: Int. J. Secur. Softw. Eng. 2.4 (2011), pp. 3448. ISSN: 1947-3036. DOI: 10.4018/jsse.2011100103. URL: https://doi.org/10.4018/jsse.2011100103 (cit. on p. 128).

[SD18] A. Suter-Dörig. "Formalizing and verifying the security protocols from the Noise framework". Available at https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/noise_suter-doerig.pdf. Bachelor's thesis. ETH Zürich, Nov. 2018 (cit. on pp. 75, 76).
[Swa+16] Nikhil Swamy, Ctlin Hricu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, and Santiago Zanella-Béguelin. "Dependent Types and Multi-Monadic Effects in F*". In: *POPL '16 Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*. 2016, pp. 256–270.
ISBN: 978-1-4503-3549-2. URL: https://www.microsoft.com/en-us/research/publication/dependent-types-multi-monadic-effects-f/ (cit. on pp. 119, 126).

[Val+22] Henry de Valence, Jack Grigg, Mike Hamburg, Isis Lovecruft, George Tankersley, and Filippo Valsorda. *The ristretto255 and decaf448 Groups*. Internet-Draft draft-irtf-cfrg-ristretto255-decaf448-03. Work in Progress. Internet Engineering Task Force, Feb. 2022. 27 pp. URL: https://datatracker.ietf.org/doc/html/draft-irtf-cfrg-ristretto255-decaf448-03 (cit. on p. 181).

[Zhe97] Yuliang Zheng. "Digital Signcryption or How to Achieve Cost(Signature & Encryption) ≪ Cost(Signature) + Cost(Encryption)". In: *CRYPTO '97*. Ed. by Burton S. Kaliski Jr. Vol. 1294. LNCS. Springer, Heidelberg, Aug. 1997, pp. 165–179. DOI: 10.1007/BFb0052234 (cit. on pp. 79, 83).
<figure><img src="image_37.png" /></figure>
Part V

APPENDIX
<figure><img src="image_38.png" /></figure>
# A

## Appendices to the CryptoVerif Introduction

### A.1 CRYPTOVERIF MODEL NSL.OCV

1. (* Needham Schroeder public key protocol, fixed by Lowe.
2. The user identity in this model is just an arbitrary
3. address. An implementation could use an user@hostname
4. construction.
5. *)
6.
7. param Qsetup.
8. param Qkey_reg.
9. param Qinit.
10. param Qresp.
11.
12. def OptionType₁ option, option_Some, option_None, input) {
13. fun option_Some(input): option [data].
14. const option_None: option.
15. equationforall x: input;
16. option_Some(x) <> option_None.
17. }
18.
19. type nonce [fixed,large].
20. type pkey [bounded].
21. type skey [bounded].
22. type keyseed [fixed,large].
23. type encseed [bounded].
24. type plaintext [bounded].
25. type address [bounded].
26. type keypair [bounded].
27. fun kp(pkey, skey): keypair [data].
28.
29. type ciphertext [bounded].
30. type ciphertext_opt [bounded].
31. expand OptionType₁(ciphertext_opt, ciphertext_some, ciphertext_bottom, ciphertext).
32.
33. table trusted_keys(address, skey, pkey).
34. table all_keys(address, pkey, bool).
35.
36. set diffConstants = false.
37.
38. fun msg1(nonce, address): plaintext [data].
39. fun msg2(nonce, nonce, address): plaintext [data].
40. fun msg3(nonce): plaintext [data].
41.
42.
43.
equation **forall** z:nonce,t:nonce,u:address,y2:nonce,z2:address;
msg2(z,t,u) <> msg1(y2,z2).
equation **forall** y:nonce,y2:nonce,z2:address;
msg3(y) <> msg1(y2,z2).
equation **forall** z:nonce,t:nonce,u:address,y2:nonce;
msg2(z,t,u) <> msg3(y2).

(* Public-key encryption (IND-CCA2) *)

proba Penc.
proba Pencoll.

expand IND_CCA2_public_key_enc_all_args(
keyseed, pkey, skey, plaintext, ciphertext_opt, encseed,
skgen, skgen2, pkgen, pkgen2, enc, enc_r, enc_r2, dec_opt, dec_opt2, injbot,
Z, Penc, Penccoll).

(* Not needed because the in processes receive ciphertext, not ciphertext_opt *)
equation **forall** sk: skey; dec_opt(ciphertext_bottom, sk) = bottom.

letfun dec(c: ciphertext, sk: skey) =
dec_opt(ciphertext_some(c), sk).

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

const Zplaintext: plaintext.
equation **forall** x: plaintext; Z(x) = Zplaintext.

(* Queries *)
event beginA(address, address, nonce, nonce).
event endA(address, address, nonce, nonce).
event beginB(address, address, nonce, nonce).
event endB(address, address, nonce, nonce).

query x:address, y:address, na:nonce, nb:nonce;
event(endA(x,y,na,nb)) = eventSCOPE eventSCOPE (beginB(x,y,na,nb)).
query x:address, y:address, na:nonce, nb:nonce;
event(endB(x,y,na,nb)) = eventSCOPE eventSCOPE (beginA(x,y,na,nb)).
query x:address, y:address, na:nonce, nb:nonce;
inj-event(endA(x,y,na,nb)) = inj-eventSCOPE eventSCOPE (beginB(x,y,na,nb)).
query x:address, y:address, na:nonce, nb:nonce;
inj-event(endB(x,y,na,nb)) = inj-eventSCOPE eventSCOPE (beginA(x,y,na,nb)).

let initiator() =
Initiator {
  foreach i_init ≤ Qinit do
    initiator_sendMsg1(addrA: address, addrX: address) :=
      (* the gets fail if addrA or addrX have not been
       setup by the adversary. *)
      get[unique] trusted_keys(=addrA, skA, pkA) in
      get[unique] all_keys(=addrX, pkX, trustX) in
      (* Prepare Message 1 *)
      Na <-R nonce;
      let cc1 = enc(msg1(Na, addrA), pkX) in
      let ciphertext_some(c1: ciphertext) = cc1 in
      return (c1);
      (* Receive Message 2 *)
```c
106 initiator_send_msg3 (c: ciphertext) :=
107         let injbot(msg2(=Na, Nb, =addrX)) = dec(c, skA) in
108         event beginA(addrA, addrX, Na, Nb);
109         (* Prepare Message 3 *)
110         let ciphertext_some(c3) = enc(msg3(Nb), pkX) in
111         return (c3);
112
113 (* OK *)
114 initiator_finished() :=
115         if (trustX) then
116         event endA(addrA, addrX, Na, Nb);
117         return ()
118     }.
119
120 let responder() =
121
122 Responder {
123
124     foreach iresp ≤ Qresp do
125
126         (* Receive Message 1 *)
127         responder_send_msg2(addrB: address, m: ciphertext) :=
128             (* the get fails if addrB has not been setup by
129              the adversary *)
130             get[unique] trusted_keys(=addrB, skB, pkB) in
131             let injbot(msg1(Na, addrY)) = dec(m, skB) in
132             get[unique] all_keys(=addrY, pkY, trustY) in
133             (* Send Message 2 *)
134             Nb <-R nonce;
135             event beginB(addrY, addrB, Na, Nb);
136             let ciphertext_some(c2) = enc(msg2(Na, Nb, addrB), pkY) in
137             return (c2);
138
139         (* Receive Message 3 *)
140         responder_received msg3 (m3: ciphertext) :=
141             let injbot(msg3(=Nb)) = dec(m3, skB) in
142             if (trustY) then (
143                 event endB(addrY, addrB, Na, Nb); return ()
144             else return ()
145         ).
146
147 let key_register() =
148
149 KeyRegister {
150
151     foreach i ≤ Qkey_reg do
152
153         register (addr: address, pkX: pkey) :=
154             get[unique] all_keys(=addr, ign1, ign2) in (
155             yield
156         ) else
157             insert all_keys(addr, pkX, false);
158             return ()
159         ).
160
161 let setup() =
162
163 Setup {
164
165     foreach i ≤ Qsetup do
166         setup(addr: address) :=
167             get[unique] all_keys(=addr, ign1, ign2) in (
```
168         yield
169     ) else
170         let kp(the_pkA: pkey, the_skA: skey) = keygen() in
171             insert trusted_keys(addr, the_skA, the_pkA);
172             insert all_keys(addr, the_pkA, true);
173         return(the_pkA)
174     }.
175 }
176
177 process
178     (
179         run setup()
180     |
181         run key_register()
182     |
183         run initiator()
184     |
185         run responder()
186     )
# B

# Appendices to the WireGuard Analysis

## B.1 INDIFFERENTIABILITY RESULTS

### B.1.1 Basic Lemmas

*Proof of Lemma 3.2.* Consider

* the game $G_0$ in which $H$ is a random oracle, and $H_i(x) = H(x)$ for each $x \in D_i$ and $i \le n$, and

* the game $G_1$ in which $H_1, \dots, H_n$ are independent random oracles defined on $D_1, \dots, D_n$ respectively, and $H(x) = H_i(x)$ if $x \in D_i$ for some $i \le n$, and $H(x) = H_0(x)$ otherwise, where $H_0$ is a random oracle of domain $D \setminus (D_1 \cup \dots \cup D_n)$.

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

*Proof of Lemma 3.3.* Consider

* the game $G_0$ in which $H_1$ and $H_2$ are independent random oracles, and $H'(x) = H_1(x) \parallel H_2(x)$, and

* the game $G_1$ in which $H'$ is a random oracle that returns bitstrings of length $l_1 + l_2$, $H_1(x)$ is the $l_1$ first bits of $H'(x)$ and $H_2(x)$ is the $l_2$ last bits of $H'(x)$.

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

*Proof of Lemma 3.4.* Consider

* the game $G_0$ in which $H$ is a random oracle, $H'_1(x)$ is the first $l_1$ bits of $H(x)$, and $H'_2(x)$ is the last $l-l_1$ bits of $H(x)$, and

* the game $G_1$ in which $H'_1$ and $H'_2$ are independent random oracles that return bitstrings of length $l_1$ and $l-l_1$ respectively, and $H(x) = H'_1(x) \parallel H'_2(x)$.

It is easy to see that these two games are perfectly indistinguishable, which proves indifferentiability. (It is the same indistinguishability result as in Lemma 3.3, swapping $G_0$ and $G_1$.) □

*Proof of Lemma 3.5.* This is a consequence of Lemma 3.4, by not giving access to oracle $H'_2$ to the distinguisher (so $q_{H'_2} = 0$). $H'_2$ is then included in the simulator. We assume that random oracles answer in constant time. □
Proof of Lemma 3.7. Consider

* the game $G_0$ in which $H_1$ and $H_2$ are independent random oracles, $H'_1(x) = H_1(x)$, and $H'_2(x) = H_2(H_1(x), x)$, and

* the game $G_1$ in which $H'_1$ and $H'_2$ are independent random oracles; $H_1(x) = H'_1(x)$; $H_2(y, z)$ returns $H'_2(z)$ if $y = H'_1(z)$ and $H_3(y, z)$ otherwise, where $H_3$ is a random oracle (independent of $H'_1$ and $H'_2$).

CryptoVerif shows that these two games are indistinguishable, up to probability $\epsilon$. (The oracles $H_1$ and $H'_1$ are considered as a single oracle, which receives $q_{H_1} + q_{H'_1}$ queries in total.) □

### B.1.2 Indifferentiability of HKDF

Much like for HMAC in [Dod+12] and as mentioned in [KBB17], $hkdf_n$ is not indifferentiable from a random oracle in general. Intuitively, the problem comes from a confusion between the first and the second (or third) call to `hmac`, which makes it possible to generate PRK by calling $hkdf_2$ rather than `hmac`. In more detail, let

$$ 
\begin{align*}
\mathrm{PRK} \|_{\_} &= \mathrm{hkdf}_2(s, k, \mathrm{info}) \\
\mathrm{salt} &= \mathrm{hmac}(s, k) \\
x &= \mathrm{hmac}(\mathrm{PRK}, \mathrm{info} \| \| i_0) \\
x' \|_{\_} &= \mathrm{hkdf}_2(\mathrm{salt}, \mathrm{info} \| i_0, \mathrm{info}')
\end{align*}
$$

where the notation $x_1 \| x_2 = \mathrm{hkdf}_2(s, k, \mathrm{info})$ denotes that $x_1$ consists of the first 256 bits of $\mathrm{hkdf}_2(s, k, \mathrm{info})$ and $x_2$ its last 256 bits.

When $hkdf_2$ is defined from `hmac` as above, we have $PRK = \mathrm{hmac}(\mathrm{PRK}', \mathrm{info} \| i_0)$ where $PRK' = \mathrm{hmac}(s, k) = \mathrm{salt}$, so $PRK = \mathrm{hmac}(\mathrm{salt}, \mathrm{info} \| i_0)$. Hence, $x' = \mathrm{hmac}(\mathrm{PRK}, \mathrm{info}' \| i_0) = x$. However, when $hkdf_2$ is a random oracle and `hmac` is defined from $hkdf_2$, the simulator that computes `hmac` sees what seems to be two unrelated calls to `hmac`. (It is unable to see that $PRK$ is in fact related to the previous call $\mathrm{salt} = \mathrm{hmac}(s, k)$: we have $PRK \|_{\_} = \mathrm{hkdf}_2(s, k, \mathrm{info})$ but the simulator does not know which value of $\mathrm{info}$ it should use.) Therefore, the simulator can only return fresh random values for $\mathrm{salt}$ and $x$, and $x \neq x'$ in general.

**Proof of Lemma 3.8.** In this proof, we write $S[H_1, \dots, H_n]$ instead of $S^{H_1, \dots, H_n}$ for a system $S$ with oracle access to $H_1, \dots, H_n$, because we need to write systems in which the oracles are themselves systems that access other oracles. Consider the game $G_0$ in which `hmac` is a random oracle and $hkdf-expand_n$ is defined as above.

The different calls to `hmac` in the definition of $hkdf-expand_n$ use disjoint domains (the last byte differs among the calls to `hmac`), so by Lemma 3.2, there exists a simulator $S_1$ for `hmac` such that $G_0$ is perfectly indistinguishable from $G_1$ in which `hmac` = $S_1[H_1, \dots, H_n]$ and $hkdf-expand_n$ is defined by

$$ 
\begin{align*}
\mathrm{hkdf}-\mathrm{expand}_n^1(\mathrm{PRK}, \mathrm{info}) &= k_1 \| \dots \| k_n \text{ where} \\
k_1 &= H_1(\mathrm{PRK}, \mathrm{info}) \\
k_{i+1} &= H_{i+1}(\mathrm{PRK}, k_i \| \mathrm{info}) \text{ for } 1 \le i < n
\end{align*}
$$

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

<footnote>[KBB17] Kobeissi et al., “Automated Verification for Secure Messaging Protocols and their Implementations: A Symbolic and Computational Approach”</footnote>
where $H_1, \dots, H_n$ are independent random oracles and the simulator $S_1$ calls $H_i$ at most $q_{H_i}$ times, with $q_{H_1} + \dots + q_{H_n} \le q_{hmac}$, and runs in time $O(q_{hmac})$.

Slightly reorganising the arguments of $H_i$, there exists a simulator $S_2$ for $hmac$ such that $G_1$ is perfectly indistinguishable from $G_2$ in which $hmac = S_2[H_1, \dots, H_n]$ and $hkdf-expand_n$ is defined by

$$hkdf-expand_n^2(\text{PRK, info}) = k_1 \| \dots \| k_n \text{ where} $$

$$ k_1 = H_1(\text{PRK, info}) $$

$$ k_{i+1} = H_{i+1}(k_i, \text{PRK, info}) \text{ for } 1 \le i < n $$

where $H_1, \dots, H_n$ are independent random oracles and the simulator $S_2$ calls $H_i$ at most $q_{H_i}$ times, with $q_{H_1} + \dots + q_{H_n} \le q_{hmac}$, and runs in time $O(q_{hmac})$.

By Lemma 3.7, there exists a simulator $S_{3,2}$ for $H_2$ ($H_1$ is simulated by $H'_1 = H_1$ itself) such that $G_2 = G_{3,1}$ is indistinguishable up to probability $\epsilon_2$ from $G_{3,2}$ in which $hmac = S_2[H'_1, S_{3,2}[H'_1, H'_2], H_3, \dots, H_n]$ and $hkdf-expand_n$ is defined by

$$ hkdf-expand_n^{3,2}(\text{PRK, info}) = k_1 \| \dots \| k_n \text{ where} $$

$$ k_1 = H'_1(\text{PRK, info}) $$

$$ k_2 = H'_2(\text{PRK, info}) $$

$$ k_{i+1} = H_{i+1}(k_i, \text{PRK, info}) \text{ for } 2 \le i < n $$

where $H'_1, H'_2, H_3, \dots, H_n$ are independent random oracles; the simulator for $hmac$ calls $H'_1$ at most $q_{H_1} + q_{H_2}$ times, $H'_2$ at most $q_{H_2}$ times, $H_i$ at most $q_{H_i}$ times for $i \ge 3$, with $q_{H_1} + \dots + q_{H_n} \le q_{hmac}$, and runs in time $O(q_{hmac} + q_{H_2})$; and $\epsilon_2 = q_{H_2}(2q_{H_1} + 3q_{hkdf-expand_n} + 1)/|M|$. Furthermore, by definition of the simulator in the proof of Lemma 3.7, $H'_1$ is called at most $q_{H_1}$ times via the first hole of $S_2$ and $H'_1$ and $H'_2$ are called with the same arguments at most $q_{H_2}$ times via the second hole of $S_2$.

Repeating the same reasoning inductively, there exists a simulator $S_{3,j}$ for $H_j$ such that $G_{3,j-1}$ is indistinguishable up to probability $\epsilon_j$ from $G_{3,j}$ in which $hmac = S_2[H'_1, S_{3,2}[H'_1, H'_2], \dots, S_{3,j}[H'_{j-1}, H'_j], H_{j+1}, \dots, H_n]$ and $hkdf-expand_n$ is defined by

$$ hkdf-expand_n^{3,j}(\text{PRK, info}) = k_1 \| \dots \| k_n \text{ where} $$

$$ k_i = H'_i(\text{PRK, info}) \text{ for } 1 \le i \le j $$

$$ k_{i+1} = H_{i+1}(k_i, \text{PRK, info}) \text{ for } j \le i < n $$

where $H'_1, \dots, H'_j, H_{j+1}, \dots, H_n$ are independent random oracles; the simulator for $hmac$ calls $H'_1$ at most $q_{H_1}$ times via the first hole of $S_2$, $H'_{i-1}$ and $H'_i$ with the same arguments at most $q_{H_i}$ times via the $i$-th hole of $S_2$ for $1 < i \le j$, $H_i$ at most $q_{H_i}$ times for $i > j$, with $q_{H_0} + \dots + q_{H_n} \le q_{hmac}$, and runs in time $O(q_{hmac} + q_{H_2} + \dots + q_{H_j})$; and $\epsilon_j = q_{H_j}(2q_{H_{j-1}} + 3q_{hkdf-expand_n} + 1)/|M|$.

For $j=n$, we obtain a game $G_{3,n}$ in which $hmac = S_2[H'_1, S_{3,2}[H'_1, H'_2], \dots, S_{3,n}[H'_{n-1}, H'_n]]$ and $hkdf-expand_n$ is defined by

$$ hkdf-expand_n^{3,n}(\text{PRK, info}) = k_1 \| \dots \| k_n \text{ where} $$

$$ k_i = H'_i(\text{PRK, info}) \text{ for } 1 \le i \le n $$

where $H'_1, \dots, H'_n$ are independent random oracles; the simulator for $hmac$ calls $H'_1$ at most $q_{H_1}$ times via the first hole of $S_2$, $H'_{i-1}$ and $H'_i$ with the
same arguments at most $q_{H_i}$ times via the $i$-th hole of $S_2$ for $1 < i \le n$, with $q_{H_1} + \cdots + q_{H_n} \le q_{hmac}$, and runs in time $O(q_{hmac}+q_{H_2}+\cdots+q_{H_n}) = O(q_{hmac})$.

By Lemma 3.3, there exist simulators $S_{4,j}$ ($1 \le j \le n$) for $H'_j$ such that $G_{3,n}$ is perfectly indistinguishable from $G_4$ in which $hmac = S_2[S_{4,1}[H], S_{3,2}[S_{4,1}[H], S_{4,2}[H]], \dots, S_{3,n}[S_{4,n-1}[H], S_{4,n}[H]]]$ and $hkdf-expand_n$ is a random oracle $H$ where the simulator for $hmac$ calls $H$ at most $q_{H_1} + \cdots + q_{H_n} \le q_{hmac}$ times, and runs in time $O(q_{hmac})$. (Since $H$ is the concatenation of the $H'_i$ for $1 \le i \le n$ and, for $i > 1$, the calls to $H'_{i-1}$ and $H'_i$ via the $i$-th hole of $S_2$ have the same arguments, these two calls can be implemented by a single call to $H$, and hence there are at most $q_{H_i}$ calls to $H$ via the $i$-th hole of $S_2$.)

The probability of distinguishing $G_0$ from $G_4$ is then at most

$$ 
\begin{align*}
\epsilon &= \sum_{j=2}^{n} \epsilon_j \\
&= \sum_{j=2}^{n} \frac{q_{H_j}(2q_{H_{j-1}} + 3q_{hkdf-expand_n} + 1)}{|\mathcal{M}|} \\
&= \frac{1}{|\mathcal{M}|} \left( 3q_{hkdf-expand_n}(\sum_{j=2}^{n} q_{H_j}) + 2\sum_{j=2}^{n} q_{H_j}q_{H_{j-1}} + \sum_{j=2}^{n} q_{H_j} \right) \\
&\le \frac{1}{|\mathcal{M}|} \left( 3q_{hkdf-expand_n}q_{hmac} + 2\sum_{j=2}^{n} q_{H_j}q_{H_{j-1}} + \sum_{j=2}^{n} q_{H_j}^2 \right) \\
&\le \frac{3q_{hkdf-expand_n}q_{hmac} + q_{hmac}^2}{|\mathcal{M}|} \quad \square
\end{align*}
$$

*Proof of Lemma 3.9.* As in the previous proof, we write $S[H_1, \dots, H_n]$ instead of $S^{H_1, \dots, H_n}$ for a system $S$ with oracle access to $H_1, \dots, H_n$. Consider the game $G_0$ in which $hmac$ is a random oracle and $hkdf_n$ is defined as above.

By hypothesis, the calls to $hmac$ in $hkdf-extract$ and $hkdf-expand_n$ use disjoint domains, so by Lemma 3.2, there exists a simulator $S_1$ for $hmac$ such that $G_0$ is perfectly indistinguishable from $G_1$ in which $hmac = S_1[H_0, H_1]$ and $hkdf_n$ is defined by $hkdf_n^1(\text{salt}, k, \text{info}) = \text{hkdf-expand}_n^1(H_0(\text{salt}, k), \text{info})$, where $hkdf_n^1$ is defined from the random oracle $H_1$ instead of $hmac$ and the simulator $S_1$ calls $H_i$ at most $q_{H_i}$ times, with $q_{H_0} + q_{H_1} \le q_{hmac}$ and runs in time $O(q_{hmac})$.

By Lemma 3.8, there exists a simulator $S_2$ for $H_1$ such that $G_1$ is indistinguishable up to probability $\epsilon$ from $G_2$ in which $hmac = S_1[H_0, S_2[H]]$, and $hkdf_n$ is defined by $hkdf_n^1(\text{salt}, k, \text{info}) = H(H_0(\text{salt}, k), \text{info})$, where $H$ is a random oracle, $S_2$ calls $H$ at most $q_H \le q_{H_1}$ times, runs in time $O(q_{H_1}) = O(q_{hmac})$, and $\epsilon = (3q_{hkdf_n}q_{H_1} + q_{H_1}^2)/|\mathcal{M}|$. So the simulator for $hmac$ calls $H_0$ at most $q_{H_0}$ times and $H$ at most $q_H \le q_{H_1}$ times and runs in time $O(q_{hmac})$.

By Lemma 3.6, there exist simulators $S_{3,1}$ for $H_0$ and $S_{3,2}$ for $H$ such that $G_2$ is indistinguishable up to probability $\epsilon'$ from $G_3$ in which $hmac = S_2[H_0, S_2[H]]$ with $H_0 = S_{3,1}[hkdf_n^3]$ and $H = S_{3,2}[hkdf_n^3]$ and $hkdf_n^3$ is a random oracle, where the simulator for $hmac$ calls $hkdf_n$ at most $q_H \le q_{H_1} \le q_{hmac}$ times, runs in time $O(q_{hmac} + q_{H_0}q_H) = O(q_{hmac}^2)$, and $\epsilon' = (2q_Hq_{H_0} + q_{H_0}^2 + q_Hq_{hkdf_n} + q_{hkdf_n}^2)/|\mathcal{M}|$.
The probability of distinguishing $G_0$ from $G_3$ is then at most

$$ \epsilon = \epsilon' + \epsilon \\ = \frac{2q_H q_{H_0} + q_{H_0}^2 + q_H q_{hkdf_n} + q_{hkdf_n}^2 + \frac{3q_{hkdf_n} q_{H_1} + q_{H_1}^2}{|M|}}{|M|} \\ = \frac{1}{|M|} \left( q_{hkdf_n}^2 + q_{hkdf_n} (q_H + 3q_{H_1}) + q_{H_1}^2 + 2q_H q_{H_0} + q_{H_0}^2 \right) \\ \le \frac{q_{hkdf_n}^2 + 4q_{hkdf_n} q_{hmac} + q_{hmac}^2}{|M|} \quad \square \\ \quad \square $$

### B.1.3 Chain of Random Oracle Calls

*Proof of Lemma 3.10.* We consider the following two games $G_0$ and $G_1$.

* The game $G_0$ in which $H$ is a random oracle and the functions $chain_n$ with $0 \le n \le m$ are defined from $H$ by (3.11) and (3.12).

* The game $G_1$ in which the functions $chain_n$ with $0 \le n \le m$ are independent random oracles and $H$ is defined from them in Figure B.1. In this figure, $L$ is a list of triples $((C, v), (C_{j+1}, r_j), j)$ such that $C_{j+1} \parallel r_j$ is the result of a previous call to $H(C, v)$ and $j$ indicates the index of this $H$ call in a chain of calls to $H$. If a call to $H$ was not coming from a chain of calls, the index $j = -2$ is used.

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

We name *direct* oracle calls to $chain_n$ or $H$ calls that are done directly by the distinguisher, and *indirect* oracle calls the calls to $H$ done from inside $chain_n$ in $G_0$ and the calls to $chain_n$ done from inside $H$ in $G_1$. Note for clarification that in $G_0$ there are no indirect calls to $chain_n$ and in $G_1$ there are no indirect calls to $H$.

We show that the two games $G_0$ and $G_1$ are indistinguishable as long as the following hypotheses hold. In game $G_0$:

H1. Consider $C_{j+1} \parallel r_j = H(C_j, v_j), j \le n < m$ that gets called from inside a direct call to $chain_n(v_1, \dots, v_j, \dots, v_n)$. If the distinguisher calls $H(C_{j+1}, v_{j+1})$ before or after the call to $chain_n$, then $H(C_j, v_j)$ has been called directly by the distinguisher before $H(C_{j+1}, v_{j+1})$.
<table><caption>FIGURE B.1: Simulator for H</caption><tr><td>H(C, v) =</td></tr><tr><td>1) if ((C, v), (C<sub>j+1</sub>, r<sub>j</sub>), j) ∈ L for some C<sub>j+1</sub>, r<sub>j</sub>, j then<br> return C<sub>j+1</sub>||r<sub>j</sub></td></tr><tr><td>2) else if C = const then<br> C<sub>1</sub> ← $\{0, 1\}^{l'}<br> r<sub>0</sub> ← chain<sub>0</sub>(v)<br> add ((C, v), (C<sub>1</sub>, r<sub>0</sub>), 0) to L<br> return C<sub>1</sub>||r<sub>0</sub></td></tr><tr><td>3) else if ((C<sub>j</sub>, v<sub>j</sub>), (C, r<sub>j</sub>), j) ∈ L for some C<sub>j</sub>, v<sub>j</sub>, r<sub>j</sub> and j with 0 ≤ j &lt; m then<br> for k = j − 1 to 0 do<br> find ((C<sub>k</sub>, v<sub>k</sub>), (C<sub>k+1</sub>, r<sub>k</sub>), k) ∈ L for some C<sub>k</sub>, v<sub>k</sub>, r<sub>k</sub><br> set C<sub>k</sub> and v<sub>k</sub> to the found values<br> endfor<br> if j + 1 = m then<br> C<sub>j+2</sub>||r<sub>j+1</sub> = chain<sub>m</sub>(v<sub>0</sub>, ..., v<sub>j</sub>, v)<br> else<br> C<sub>j+2</sub> ← $\{0, 1\}^{l'}<br> r<sub>j+1</sub> ← chain<sub>j+1</sub>(v<sub>0</sub>, ..., v<sub>j</sub>, v)<br> endif<br> add ((C, v), (C<sub>j+2</sub>, r<sub>j+1</sub>), j + 1) to L<br> return C<sub>j+2</sub>||r<sub>j+1</sub></td></tr><tr><td>4) else<br> C<sub>−1</sub> ← $\{0, 1\}^{l'}<br> r<sub>−2</sub> ← $\{0, 1\}^{l−l'}<br> add ((C, v), (C<sub>−1</sub>, r<sub>−2</sub>), −2) to L<br> return C<sub>−1</sub>||r<sub>−2</sub></td></tr><tr><td>endif</td></tr></table>

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

In game $G_1$:

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

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

H3. There are no collisions between the fresh $C_j$.

We have the following invariants:

P1. Given C, v, there is at most one pair ((C<sub>j+1</sub>, r<sub>j</sub>), j) such that

$$((C, v), (C_{j+1}, r_j), j) \in L.$$

Indeed, when L contains such an element, calls to H(C, v) immediately return $C_{j+1}||r_j$ in case 1, and never add another element (((C, v), (C<sub>j+1</sub>, r<sub>j</sub>), j) to L.
P2. Given $((C_j, v_j), (C, r_j), j) \in L$, for some $C_j, v_j, r_j$ and $j$ with $0 \le j < m$ then there is, for each $k = j - 1$ to 0, a single matching element $((C_k, v_k), (C_{k+1}, r_k), k)$ in $L$.

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

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

Moreover, the uniqueness of $((C_k, v_k), (C_{k+1}, r_k), k)$ comes from H3: when an element $((C_k, v_k), (C_{k+1}, r_k), k)$ is added to $L$, $C_{k+1}$ is always a fresh $C_j$, so by H3, there is a single element in $L$ with a given $C_{k+1}$.

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

CASE 1 Suppose the distinguisher makes a direct oracle call to $H$ or $\text{chain}_n$ with the same arguments as a previous direct call to the same oracle. Both $G_0$ and $G_1$ return the same result as in the previous call.

CASE 2 Suppose the distinguisher makes a direct call to $\text{chain}_n$ that has not been done before as a direct call.

CASE 2. A) In $G_0$, the last $H(C, v_n)$ in the chain that simulates $\text{chain}_n(v_0, \dots, v_n)$ has already been called directly. Then by H1 the distinguisher did all $H$ calls in the chain that simulates $\text{chain}_n(v_0, \dots, v_n)$ directly.

The result in $G_0$ is

$$ \_\|\text{chain}_n(v_0, \dots, v_n) = H(C, v_n) $$

which is the last part of the result of the previous call to $H$, or in the case of $n = m$

$$ \text{chain}_m(v_0, \dots, v_m) = H(C, v_m). $$

In $G_1$, because the whole chain of $H$ calls was made in the right order, $\text{chain}_n(v_0, \dots, v_n)$ has already been invoked indirectly by the call to $H(C, v_n)$. Thus, this current call to $\text{chain}_n$ returns a previously fixed value, fulfilling the following equation:

$$ H(C, v_n) = C_{j+1} \| \text{chain}_n(v_0, \dots, v_n) $$

or in the case of $n = m$

$$ H(C, v_m) = \text{chain}_m(v_0, \dots, v_m). $$

This is the same result as in $G_0$.
CASE 2. B) In $G_0$, the last $H(C, v_n)$ in the chain that simulates $chain_n(v_0, \dots, v_n)$ has not already been called directly. Like in the previous case, the result is

$$ \|\text{chain}_n(v_0, \dots, v_n)\| = H(C, v_n) $$

or in the case of $n = m$

$$ \text{chain}_m(v_0, \dots, v_m) = H(C, v_m), $$

but as $H(C, v_n)$ and $chain_n(v_1, \dots, v_n)$ have not been called before directly, the result is independent of previously returned values and thus looks like a fresh random value to the distinguisher.

In $G_1$, $chain_n(v_0, \dots, v_n)$ has not been invoked before and thus returns a fresh random value.

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

### CASE 3. A)
In $G_0$, this call to $H(C, v_i)$ has already been done from inside a $chain_n(v_0, \dots, v_n)$ call. Hence all other $H$ calls belonging to this chain have also been done from inside said $chain_n$ call, in particular the call $H(C_{i-1}, v_{i-1})$ directly before the current call (except for $C = \text{const}$, thus if the current call is the beginning of a chain). **H1** implies that the distinguisher has then made a direct call to $H(C_{i-1}, v_{i-1})$ before the current $H$ call. By recursively applying **H1**, the distinguisher has then directly made all $H$ calls in the chain up to the current one, in the right order.

### CASE 3. A) I)
In $G_0$, the current direct call to $H(C, v_n)$ has already been done as the last one of the chain of calls indirectly invoked from inside a $chain_n(v_0, \dots, v_n)$ call.

In $G_0$, the result fulfils the following equation:

$$ C_{n+1} \| \text{chain}_n(v_0, \dots, v_n) = H(C, v_n), $$

and in the case of $n = m$:

$$ \text{chain}_m(v_0, \dots, v_m) = H(C, v_m). $$

This is similar to case 2. a) just that the order of the calls is inverted and the following small difference: the parts of $H$'s result coming from chain are already known by the distinguisher, while $C_{n+1}$ looks like a fresh random value.

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

$$ H(C, v_n) = C_{n+1} \| \text{chain}_n(v_0, \dots, v_n) $$

or in the case of $n = m$:

$$ H(C, v_m) = \text{chain}_m(v_0, \dots, v_m). $$

The parts of $H$'s result coming from chain are already known by the distinguisher, while $C_{n+1}$ is a fresh random value. This is indistinguishable from the result in $G_0$.
CASE 3. A) II) In $G_0$, the current direct call to $H(C, v_i)$ has already been done from inside a chain$_n(v_0, \dots, v_n)$ call, but not as the last one. This implies that said chain$_n$ call was not chain$_0$ – this is covered by case 3. a) i).

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

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

CASE 3. B) In $G_0$, this call to $H(C, v_i)$ has not been done before, neither directly nor indirectly.<fnref n="1" /> Hence, H returns a fresh random value.

In $G_1$, the simulator's case 1 is not relevant because this call has not been done before. Simulator's case 2: If $C = \text{const}$, then H returns a fresh random $C_1$ and a fresh random $r_0$ via chain$_0$. This call to chain$_0$ has not been done before because this would have invoked the H call in $G_0$, which is excluded by the hypothesis. Simulator's case 3: If $((C_j, v_j), (C, r_j), j) \in L$ for some $C_j, v_j, r_j$ and $0 \le j < m$, then the current call to $H(C, v_i)$ appends to a chain. Thus, a fresh random $C_{j+2} \parallel r_{j+1}$ is returned. The involved chain$_{j+1}$ or chain$_m$ has not been called before for the same reason as chain$_0$ above. Simulator's case 4: A fresh random $C_{-1} \parallel r_{-2}$ is returned. To conclude, a fresh random value is returned in every case in $G_1$.

The previous proof shows that the games $G_0$ and $G_1$ are indistinguishable assuming the hypotheses H1, H2, and H3 hold. We will now bound the probability that they do not hold. Suppose that there are at most $q_H$ direct queries to H and $q_{\text{chain}_n}$ direct queries to chain$_n$.

* When H1 does not hold, the distinguisher does an H call from a chain corresponding to an earlier or later chain$_n$ call without having done the H calls starting from the beginning of the chain, by using the matching $C$ value. There are at most $(\sum_{n=0}^m n \cdot q_{\text{chain}_n})$ different $C$ values from H, and the distinguisher has $q_H$ attempts to hit a matching one, so the probability that H1 does not hold is at most $(\sum_{n=0}^m n \cdot q_{\text{chain}_n}) \cdot q_H / 2^{l'}$.

* The probability that H2 does not hold at the $q$-th call to H is at most the probability that a fresh random value in $\{0, 1\}^{l'}$ collides with $q$ values in $\{0, 1\}^{l'}$, hence $q/2^{l'}$. So in total, the probability that H2 does not hold is $\sum_{q=1}^{q_H} q/2^{l'} = q_H(q_H + 1)/2^{l'+1}$.

* The probability that H3 does not hold is at most the probability that among $q_H$ random values in $\{0, 1\}^{l'}$, two of them collide, so it is at most $q_H(q_H - 1)/2^{l'+1}$.

Hence, the probability that $G_0$ and $G_1$ are distinguished is at most

$$ \frac{(\sum_{n=0}^{m} n \cdot q_{\text{chain}_n}) \cdot q_H + q_H^2}{2^{l'}} $$

□

<footnote n="1">¹This means that there is no involvement of previous calls to chain$_n$, but the distinguisher can build an H chain with direct calls.</footnote>
<figure><img src="image_39.png" /></figure>
# C

## Appendices to the Analysis of HPKE's
Authenticated Mode

### C.1 SINGLE- AND TWO-USER DEFINITIONS FOR AKEM

In this section, we give simplified variants of AKEM security notions which only consider a single user (insider security) or two users (outsider security). We show that these notions non-tightly imply their corresponding n-user notion given in Section 4.5.1.

As in Section 4.5.1, we distinguish between Outsider-CCA, Insider-CCA and Outsider-Auth. In all notions, we have a dedicated challenge oracle CHALL, whereas AENCAP and ADECAP always reveal the real key (provided that ADECAP is not queried on a challenge ciphertext).

We give games ($q_e, q_d, q_c$)-2-Outsider-CCA$_ℓ$ and ($q_e, q_d, q_c$)-2-Outsider-CCA$_r$ in Listing C.1 and games ($q_e, q_d, q_c$)-2-Outsider-Auth$_ℓ$ and ($q_e, q_d, q_c$)-2-Outsider-Auth$_r$ in Listing C.3. We also provide the ($q_e, q_d, q_c$)-1-Insider-CCA games in Listing C.2, where compared to the ($n, q_e, q_d, q_c$)-Insider-CCA games we omit the key generation oracle GEN since we need to generate only one challenge key and w.l.o.g. we can do this at the beginning of the game. In all games, adversary $\mathcal{A}$ is allowed to make $q_e$ queries to AENCAP, $q_d$ queries to ADECAP and $q_c$ queries to CHALL. We define the advantage of $\mathcal{A}$ in each game as

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

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

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

For each security notion, we prove that the corresponding single- or two-user notion with one challenge query implies the n-user notion of Section 4.5.1 with multiple challenge queries. This is captured in Theorems C.1 to C.3. The proofs are given in Appendices C.1.1 to C.1.3.
<caption>Listing C.1: Games $(q_e, q_d, q_c)$-2-Outsider-CCA$_\ell$ and $(q_e, q_d, q_c)$-2-Outsider-CCA$_r$ for AKEM. Adversary $\mathcal{A}$ makes at most $q_e$ queries to $\mathcal{A}ENCAP$, at most $q_d$ queries to $\mathcal{A}DECAP$ and at most $q_c$ queries to $\mathcal{C}HALL$.</caption>

$$
\begin{array}{l@{\quad}l}
(q_e, q_d, q_c)\text{-2-Outsider-CCA}_\ell \text{ and} & \text{Oracle } \mathcal{C}HALL(i \in [2], j \in [2]) \\[1.5ex]
\text{---------------------------} & \textcircled{08} (c, K) \stackrel{\mathcal{S}}{\leftarrow} \text{AuthEncap}(\text{sk}_i, \text{pk}_j) \\[1.5ex]
\text{---------------------------} & \textcircled{09} K \stackrel{\mathcal{S}}{\leftarrow} \mathcal{K} \\[1.5ex]
\text{---------------------------} & \textcircled{10} \bar{C} \leftarrow \bar{C} \cup \{(\text{pk}_i, \text{pk}_j, c, K)\} \\[1.5ex]
\text{---------------------------} & \textcircled{11} \textbf{return} (c, K) \\[1.5ex]
\text{---------------------------} & \text{Oracle } \mathcal{A}DECAP(j \in [2], \text{pk}, c) \\[1.5ex]
\text{---------------------------} & \textcircled{12} \textbf{if} \exists K : (\text{pk}, \text{pk}_j, c, K) \in \mathcal{C} \\[1.5ex]
\text{---------------------------} & \textcircled{13} \textbf{return} \perp \\[1.5ex]
\text{---------------------------} & \textcircled{14} K \leftarrow \text{AuthDecap}(\text{sk}_j, \text{pk}, c) \\[1.5ex]
\text{---------------------------} & \textcircled{15} \textbf{return} K
\end{array}
$$

<caption>Listing C.2: Games $(q_e, q_d, q_c)$-1-Insider-CCA$_\ell$ and $(q_e, q_d, q_c)$-1-Insider-CCA$_r$ for AKEM. Adversary $\mathcal{A}$ makes at most $q_e$ queries to $\mathcal{A}ENCAP$, at most $q_d$ queries to $\mathcal{A}DECAP$ and at most $q_c$ queries to $\mathcal{C}HALL$.</caption>

$$
\begin{array}{l@{\quad}l}
(q_e, q_d, q_c)\text{-1-Insider-CCA}_\ell \text{ and} & \text{Oracle } \mathcal{C}HALL(\text{sk}) \\[1.5ex]
\text{---------------------------} & \textcircled{07} (c_2, K) \stackrel{\mathcal{S}}{\leftarrow} \text{AuthEncap}(\text{sk}, \text{pk}^*) \\[1.5ex]
\text{---------------------------} & \textcircled{08} K \stackrel{\mathcal{S}}{\leftarrow} \mathcal{K} \\[1.5ex]
\text{---------------------------} & \textcircled{09} C \leftarrow C \cup \{(\mu(\text{sk}), c, K)\} \\[1.5ex]
\text{---------------------------} & \textcircled{10} \textbf{return} (c, K) \\[1.5ex]
\text{---------------------------} & \text{Oracle } \mathcal{A}DECAP(\text{pk}, c) \\[1.5ex]
\text{---------------------------} & \textcircled{11} \textbf{if} \exists K : (\text{pk}, c, K) \in \mathcal{C} \\[1.5ex]
\text{---------------------------} & \textcircled{12} \textbf{return} \perp \\[1.5ex]
\text{---------------------------} & \textcircled{13} K \leftarrow \text{AuthDecap}(\text{sk}^*, \text{pk}, c) \\[1.5ex]
\text{---------------------------} & \textcircled{14} \textbf{return} K
\end{array}
$$

<caption>Listing C.3: Games $(q_e, q_d, q_c)$-2-Outsider-Auth$_\ell$ and $(q_e, q_d, q_c)$-2-Outsider-Auth$_r$ for AKEM. Adversary $\mathcal{A}$ makes at most $q_e$ queries to $\mathcal{A}ENCAP$, at most $q_d$ queries to $\mathcal{A}DECAP$ and at most $q_c$ queries to $\mathcal{C}HALL$.</caption>

$$
\begin{array}{l@{\quad}l}
(q_e, q_d, q_c)\text{-2-Outsider-Auth}_\ell \text{ and} & \text{Oracle } \mathcal{A}DECAP(j \in [2], \text{pk}, c) \\[1.5ex]
\text{---------------------------} & \textcircled{09} \textbf{if} \exists K : (\text{pk}, \text{pk}_j, c, K) \in \mathcal{E} \\[1.5ex]
\text{---------------------------} & \textcircled{10} \textbf{return} \perp \\[1.5ex]
\text{---------------------------} & \textcircled{11} K \leftarrow \text{AuthDecap}(\text{sk}_j, \text{pk}, c) \\[1.5ex]
\text{---------------------------} & \textcircled{12} \mathcal{E} \leftarrow \mathcal{E} \cup \{(\text{pk}, \text{pk}_j, c, K)\} \\[1.5ex]
\text{---------------------------} & \textcircled{13} \textbf{return} K \\[1.5ex]
\text{---------------------------} & \text{Oracle } \mathcal{C}HALL(i \in [2], j \in [2], c) \\[1.5ex]
\text{---------------------------} & \textcircled{14} \textbf{if} \exists K : (\text{pk}_i, \text{pk}_j, c, K) \in \mathcal{E} \\[1.5ex]
\text{---------------------------} & \textcircled{15} \textbf{return} \perp \\[1.5ex]
\text{---------------------------} & \textcircled{16} K \leftarrow \text{AuthDecap}(\text{sk}_j, \text{pk}_i, c) \\[1.5ex]
\text{---------------------------} & \textcircled{17} \textbf{if} K \neq \perp \\[1.5ex]
\text{---------------------------} & \textcircled{18} K \stackrel{\mathcal{S}}{\leftarrow} \mathcal{K} \\[1.5ex]
\text{---------------------------} & \textcircled{19} \mathcal{E} \leftarrow \mathcal{E} \cup \{(\text{pk}_i, \text{pk}_j, c, K)\} \\[1.5ex]
\text{---------------------------} & \textcircled{20} \textbf{return} K
\end{array}
$$
**Theorem C.1** (($q_e, q_d, 1$)-2-Outsider-CCA $\implies$ ($n, q_e, q_d$)-Outsider-CCA). For any adversary $\mathcal{A}$ against the ($n, q_e, q_d$)-Outsider-CCA security experiment, there exists an adversary $\mathcal{B}$ against the ($q_e, q_d, 1$)-2-Outsider-CCA security experiment such that $t_B \approx t_A$ and

$$ \mathrm{Adv}_{\mathcal{A}, \mathrm{AKEM}}^{(n,q_e,q_d)\text{-Outsider-CCA}} \le n^2 q_e \cdot \mathrm{Adv}_{\mathcal{B}, \mathrm{AKEM}}^{(q_e,q_d,1)\text{-2-Outsider-CCA}} + n^2 \cdot P_{\mathrm{AKEM}}. $$

**Theorem C.2** (($q_e, q_d, 1$)-1-Insider-CCA $\implies$ ($n, q_e, q_d, q_c$)-Insider-CCA). For any adversary $\mathcal{A}$ against the ($n, q_e, q_d, q_c$)-Insider-CCA security experiment, there exists an adversary $\mathcal{B}$ against the ($q_e, q_d, 1$)-1-Insider-CCA security experiment such that $t_B \approx t_A$ and

$$ \mathrm{Adv}_{\mathcal{A}, \mathrm{AKEM}}^{(n,q_e,q_d,q_c)\text{-Insider-CCA}} \le n q_c \cdot \mathrm{Adv}_{\mathcal{B}, \mathrm{AKEM}}^{(q_e,q_d,1)\text{-1-Insider-CCA}}. $$

**Theorem C.3** (($q_e, q_d, 1$)-2-Outsider-Auth $\implies$ ($n, q_e, q_d$)-Outsider-Auth). For any adversary $\mathcal{A}$ against ($n, q_e, q_d$)-Outsider-Auth security of AKEM, there exists an adversary $\mathcal{B}$ against ($q_e, q_d, 1$)-2-Outsider-Auth security of AKEM such that $t_B \approx t_A$ and

$$ \mathrm{Adv}_{\mathcal{A}, \mathrm{AKEM}}^{(n,q_e,q_d)\text{-Outsider-Auth}} \le n^2 q_d \cdot \mathrm{Adv}_{\mathcal{B}, \mathrm{AKEM}}^{(q_e,q_d,1)\text{-2-Outsider-Auth}} + n^2 \cdot P_{\mathrm{AKEM}}. $$

### C.1.1 Proof of Theorem C.1

*Proof.* Let $\mathcal{A}$ be an adversary against ($n, q_e, q_d$)-Outsider-CCA security of AKEM that makes at most $n$ queries to $\mathrm{GEN}$, at most $q_e$ queries to $\mathrm{AENCAP}$ and $q_d$ queries to $\mathrm{ADECAP}$. Consider the games $G_0-G_4$ in Listing C.4.

<table><caption>Listing C.4: Games $G_0-G_4$ for the proof of Theorem C.1.</caption><thead><tr><th></th><th></th><th></th></tr></thead><tbody><tr><td>G<sub>0</sub>, G<sub>1</sub>, (G<sub>2,u,v,q</sub>)<sub>u,v&isin;[n,q]&isin;[q<sub>e</sub>,0]</sub>, G<sub>3</sub>, G<sub>4</sub></td><td></td><td>Oracle AENCAP(i &isin; [l], pk)</td></tr><tr><td>01 ctr &larr; 0</td><td rowspan="4">//G<sub>2,u,v,q</sub></td><td>16 (c, K) &larr; <sup>s</sup> AuthEncap(sk<sub>i</sub>, pk)</td></tr><tr><td>02 l &larr; 0</td><td>17 if pk &isin; {pk<sub>1</sub>, ..., pk<sub>t</sub>}</td></tr><tr><td>03 E &larr; &empty;</td><td>18 find j such that pk = pk<sub>j</sub> //G<sub>2,u,v,q</sub></td></tr><tr><td>04 COLL<sub>pk</sub> &larr; false</td><td>19 if i &larr; u or (i = u &and; j &larr; v) //G<sub>2,u,v,q</sub></td></tr><tr><td>05 b &larr; <sup>s</sup> A<sup>GEN,AENCAP,ADECAP</sup></td><td></td><td>20 K &larr; <sup>s</sup> K //G<sub>2,u,v,q</sub></td></tr><tr><td>06 return b</td><td></td><td>21 if i = u and j = v //G<sub>2,u,v,q</sub></td></tr><tr><td></td><td></td><td>22 ctr &larr; ctr + 1 //G<sub>2,u,v,q</sub></td></tr><tr><td></td><td></td><td>23 if ctr &le; q //G<sub>2,u,v,q</sub></td></tr><tr><td></td><td></td><td>24 K &larr; <sup>s</sup> K //G<sub>2,u,v,q</sub></td></tr><tr><td>Oracle GEN</td><td></td><td>25 K &larr; <sup>s</sup> K //G<sub>3-G<sub>4</sub></sub></td></tr><tr><td>07 l &larr; l + 1</td><td></td><td>26 E &larr; E &oplus; {(pk<sub>i</sub>, pk, c, K)}</td></tr><tr><td>08 (sk<sub>i</sub>, pk<sub>i</sub>) &larr; <sup>s</sup> Gen</td><td>//G<sub>1-G<sub>3</sub></sub></td><td>27 return (c, K)</td></tr><tr><td>09 if pk<sub>i</sub> &isin; {pk<sub>1</sub>, ..., pk<sub>i-1</sub>}</td><td>//G<sub>1-G<sub>3</sub></sub></td><td></td></tr><tr><td>10 COLL<sub>pk</sub> &larr; true; abort</td><td></td><td></td></tr><tr><td>11 return (pk<sub>i</sub>, l)</td><td></td><td></td></tr><tr><td>Oracle ADECAP(j &isin; [l], pk, c)</td><td></td><td></td></tr><tr><td>12 try get K s.t. (pk, pk<sub>j</sub>, c, K) &isin; E</td><td></td><td></td></tr><tr><td>13 then return K</td><td></td><td></td></tr><tr><td>14 K &larr; AuthDecap(sk<sub>j</sub>, pk, c)</td><td></td><td></td></tr><tr><td>15 return K</td><td></td><td></td></tr></tbody></table>

### GAME G<sub>0</sub>
Note that this game is the ($n, q_e, q_d$)-Outsider-CCA<sub>l</sub> game. We already initialise multiset $\mathcal{E}$ and boolean flag COLL<sub>pk</sub>, which we will need in the following games to exclude collisions. In $G_0$, we model $\mathcal{E}$ as a multiset to store all challenge queries to AENCAP and to already match the syntax of the ($n, q_e, q_d$)-Outsider-CCA<sub>r</sub> game. If a challenge is queried to the decapsulation oracle ADECAP, then the challenge key stored in $\mathcal{E}$ is directly returned. Due to perfect correctness, this is only a conceptual change. We have

$$ \mathrm{Pr}[G_0 \Rightarrow 1] = \mathrm{Pr}[(n, q_e, q_d)\text{-Outsider-CCA}_l(\mathcal{A}) \Rightarrow 1]. $$
### GAME $G_1$
In this game, we raise flag $COLL_{pk}$ and abort, whenever a query to $GEN$ generates a public key that was already generated in a previous query to $GEN$. Due to the difference lemma,

$$|\Pr[G_0 \Rightarrow 1] - \Pr[G_1 \Rightarrow 1]| \le \Pr[COLL_{pk}],$$

which we can bound by

$$\Pr[COLL_{pk}] \le \binom{n}{2} \cdot P_{AKEM} \le \frac{n^2}{2} \cdot P_{AKEM}.$$

In the following we want to iterate over all pairs of honest users using indices $u, v \in [n]$ and all their challenges using index $q \in [q_e]_0$ and replace the corresponding challenge key by a random key. We capture each iteration in an intermediate game $G_{2,u,v,q}$, where the key of the $q$-th query to $AENCAP$ for sender public key $pk_u$ and receiver public key $pk_v$ is replaced by random.

At this point we want to remark that $q_e$ is the number of queries for all users and regardless whether it is a challenge query or not. In particular, the actual number of challenge queries for a specific user pair might be lower. However, in our following analysis we cannot easily use this fact to achieve a better bound because we have to cover all cases, which explains the tightness loss of $n^2 \cdot q_e$.

### GAMES ($G_{2,u,v,q}$)
As each public key generated by the game is unique, we can now find a unique index $j$ for queries to $AENCAP$ such that the public key $pk$ provided by $\mathcal{A}$ matches exactly one $pk_j$. To identify the corresponding challenge query, we use a counter $ctr$. Each time, a challenge query for sender public key $pk_u$ and receiver public key $pk_v$ is issued, the counter is increased. Note that the first intermediate game $G_{2,1,1,0}$ is exactly game $G_1$, thus

$$\Pr[G_{2,1,1,0} \Rightarrow 1] = \Pr[G_1 \Rightarrow 1].$$

Also note that whenever $q$ reaches $q_e$, there will be no change in the next step. In particular, for all $u \in [n], v \in [n-1], G_{2,u,v,q_e}$ is the same as $G_{2,u,v+1,0}$, as well as for all $u \in [n-1], G_{2,u,n,q_e}$ is the same as $G_{2,u+1,1,0}$ and thus

$$\Pr[G_{2,u,v,q_e} \Rightarrow 1] = \Pr[G_{2,u,v+1,0} \Rightarrow 1],$$

$$\Pr[G_{2,u,n,q_e} \Rightarrow 1] = \Pr[G_{2,u+1,1,0} \Rightarrow 1].$$

On a high level each game $G_{2,u,v,q}$ separates the output of $AENCAP$ on a query $(i, pk_j)$, where $pk_j \in \{pk_1, \dots, pk_l\}$ is one of the public keys generated by the game so far, into two sets. The game outputs 1) a random key if $i < u$ or if $i = u$ and $j < v$ as well as if $i = u$ and $j = v$ and $ctr \le q$, and 2) the real key otherwise.

We now need to bound the difference between games $G_{2,u,v,q-1}$ and $G_{2,u,v,q}$ for all $u, v \in [n], q \in [q_e]$. Therefore, we construct adversary $\mathcal{B}_{u,v,q}$ against $(q_e, q_d, 1)$-2-Outsider-CCA in Listing C.5.

Adversary $\mathcal{B}_{u,v,q}$ has access to oracles $AEncap$, $ADecap$ and $Chall$. It inputs two public keys which we denote by $pk'_1$ and $pk'_2$ in order to avoid confusion with public keys $pk_1$ and $pk_2$ which will be the first two public keys that $\mathcal{B}_{u,v,q}$ outputs to $\mathcal{A}$ when $\mathcal{A}$ queries $GEN$. On the $u$-th query to $GEN$, $\mathcal{B}_{u,v,q}$ will then output $pk'_1$ and on the $v$-th query it will output $pk'_2$. Note that when $u = v$, $\mathcal{B}_{u,v,q}$ will only use $pk'_1$. This captures queries to $AENCAP$
<table><caption>Listing C.5: Adversary $\mathcal{B}_{u,v,q}$ against $(q_e, q_d, 1)$-2-Outsider-CCA, where $u, v \in [n]$, $q \in [q_e]$ and $f: \{u, v\} \to \{1, 2\}$ is a function such that, when $u = v$, $f(u) = f(v) = 1$, and when $u \neq v$, $f(u) = 1$ and $f(v) = 2$.</caption><thead><tr><th></th><th>Oracle AEncAP(i &isin; [l], pk)</th><th>Oracle ADecAP(j &isin; [l], pk, c)</th></tr></thead><tbody><tr><td>01 ctr &larr; 0</td><td>23 if i &notin; {u, v}</td><td>16 try get K s.t. (pk, pk<sub>j</sub>, c, K) &isin; E</td></tr><tr><td>02 l &larr; 0</td><td>24 (c, K) &larr; AuthEncap(sk<sub>i</sub>, pk)</td><td>17 then return K</td></tr><tr><td>03 E &larr; &empty;</td><td>25 else if i = u and pk = pk<sub>v</sub></td><td>18 if j &isin; {u, v}</td></tr><tr><td>04 b &larr; <sup>s</sup>&frasl;<sub>E</sub> A<sup>GEN,AEncAP,ADecAP</sup></td><td>26 ctr &larr; ctr + 1</td><td>19 K &larr; ADecap(f(j), pk, c)</td></tr><tr><td>05 return b</td><td>27 if ctr = q</td><td>20 else</td></tr><tr><td><u>Oracle GEN</u></td><td>28 (c, K) &larr; Chall(f(i), f(v))</td><td>21 K &larr; AuthDecap(sk<sub>j</sub>, pk, c)</td></tr><tr><td>06 l &larr; l + 1</td><td>29 else</td><td>22 return K</td></tr><tr><td>07 if l = u</td><td>30 (c, K) &larr; AEncap(f(i), pk)</td><td></td></tr><tr><td>08 pk<sub>u</sub> &larr; pk'<sub>1</sub></td><td>31 else</td><td></td></tr><tr><td>09 else if l = v</td><td>32 (c, K) &larr; AEncap(f(i), pk)</td><td></td></tr><tr><td>10 pk<sub>v</sub> &larr; pk'<sub>2</sub></td><td>33 if pk &isin; {pk<sub>1</sub>, ..., pk<sub>l</sub>}</td><td></td></tr><tr><td>11 else</td><td>34 find j such that pk = pk<sub>j</sub></td><td></td></tr><tr><td>12 (sk<sub>l</sub>, pk<sub>l</sub>) &larr; <sup>s</sup>&frasl;<sub>E</sub> Gen</td><td>35 if i &lt; u or (i = u &amp; j &lt; v)</td><td></td></tr><tr><td>13 if pk<sub>l</sub> &isin; {pk<sub>1</sub>, ..., pk<sub>l-1</sub>}</td><td>36 or (i = u &amp; j = v &amp; ctr &lt; q)</td><td></td></tr><tr><td>14 abort</td><td>37 K &larr; K</td><td></td></tr><tr><td>15 return (pk<sub>l</sub>, l)</td><td>38 E &larr; E &oslash; {(pk<sub>i</sub>, pk, c, K)}</td><td></td></tr><tr><td><u>Oracle ADecAP(j &isin; [l], pk, c)</u></td><td>39 return (c, K)</td><td></td></tr></tbody></table>

of the form $(i, pk_i)$. All remaining key pairs will be honestly generated with the condition that $\mathcal{B}_{u,v,q}$ aborts whenever the same key is generated twice, as introduced in game $G_1$. In order to avoid convoluted case distinctions in Listing C.5, we define a function $f: \{u, v\} \to \{1, 2\}$ such that, when $u = v$, $f(u) = f(v) = 1$, and when $u \neq v$, $f(u) = 1$ and $f(v) = 2$. This ensures that oracles AEncap, ADecap and Chall are queried on the correct indices.

Queries to ADecap are simulated using the ADecap oracle whenever $\mathcal{A}$ makes a query on $u$ or $v$. Otherwise, $\mathcal{B}_{u,v,q}$ can run the AuthDecap algorithm, since it knows the secret key $sk_j$.

Queries to AEncap are simulated as follows: We first want to run the AuthEncap algorithm for all queries, except for the $q$-th challenge query of sender $pk_u$ and receiver $pk_v$. Thus, if the index $i$ supplied by $\mathcal{A}$ is not $u$ or $v$, $\mathcal{B}_{u,v,q}$ can run the AuthEncap algorithm itself, since it knows the secret key $sk_i$. For all other queries, $\mathcal{B}_{u,v,q}$ needs to calls its AEncap oracle. However, if this is the $q$-th challenge query of sender $pk_u$ and receiver $pk_v$, $\mathcal{B}_{u,v,q}$ calls the challenge oracle Chall instead, after incrementing $ctr$. At this point note that $\mathcal{B}_{u,v,q}$ makes at most $q_e$ queries to the AEncap oracle and only a single query to Chall.

We check for public key collisions and $\mathcal{B}_{u,v,q}$ aborts whenever $G_{2,u,v,q}$ would abort. Now we can proceed to replacing all challenge keys which were considered in previous games. In particular, if $i < u$ or $i = u$ and $j < v$, where $pk = pk_j$ for some index $j \in [l]$, we choose a random key. We do the same in case $i = u$ and $j = v$ and $ctr < q$. Note that if $\mathcal{B}_{u,v,q}$ is in the $(q_e, q_d, 1)$-2-Outsider-CCA$_l$ game, it perfectly simulates $G_{2,u,v,q-1}$. Otherwise, if $\mathcal{B}_{u,v,q}$ is in the $(q_e, q_d, 1)$-2-Outsider-CCA$_r$ game, it perfectly
simulates $G_{2,u,v,q}$. Thus for all $q \in [q_e]$,

$$|\Pr[G_{2,u,v,q-1} \Rightarrow 1] - \Pr[G_{2,u,v,q} \Rightarrow 1]| \le \mathrm{Adv}_{B_{u,v,q}, \mathrm{AKEM}}^{(q_e, q_d, 1)-2-\mathrm{Outsider-CCA}}.$$

### GAME $G_3$
In this game, all challenge keys output by $\mathrm{AENCAP}$ are random keys. Note that this game is the same as $G_{2,u,v,q_e}$, hence

$$\Pr[G_3 \Rightarrow 1] = \Pr[G_{2,n,n,q_e} \Rightarrow 1].$$

### GAME $G_4$
In game $G_4$ we undo the change introduced in game $G_1$ and do not abort if a public key collision happens. Thus, we get

$$|\Pr[G_3 \Rightarrow 1] - \Pr[G_4 \Rightarrow 1]| \le \frac{n^2}{2} \cdot P_{\mathrm{AKEM}}.$$

Finally note that $G_4$ is exactly the same as the $(n, q_e, q_d)$-Outsider-CCA$_r$ game and

$$\Pr[G_4 \Rightarrow 1] = \Pr[(n, q_e, q_d)\text{-Outsider-CCA}_r(\mathcal{A}) \Rightarrow 1].$$

Folding adversaries $B_{u,v,q}$ into a single adversary $\mathcal{B}$ and collecting the probabilities yields the bound claimed in Theorem C.1. $\square$

### C.1.2 Proof of Theorem C.2

*Proof.* Let $\mathcal{A}$ be an adversary in the $(n, q_e, q_d, q_c)$-Insider-CCA security experiment that makes at most $n$ queries to $\mathrm{GEN}$, at most $q_e$ queries to $\mathrm{AENCAP}$, $q_d$ queries to $\mathrm{ADECAP}$ and $q_c$ queries to $\mathrm{CHALL}$. Consider the sequence of games $G_0-G_2$ in Listing C.6.

<table><caption>Listing C.6: Games $G_0-G_2$ for the proof of Theorem C.2.</caption><tr><td>G<sub>0</sub>, (G<sub>1,u,q</sub>)<sub>u∈[n], q∈[q<sub>e</sub>], G<sub>2</sub></sub></td><td>Oracle AENCAP(i ∈ [l], pk)</td></tr><tr><td>01 ctr ← 0</td><td>13 (c, K) ← AuthEncap(sk<sub>i</sub>, pk)</td></tr><tr><td>02 l ← 0</td><td>14 return (c, K)</td></tr><tr><td>03 C ← ∅</td><td>Oracle CHALL(j ∈ [l], sk)</td></tr><tr><td>04 b <sup>s</sup> A<sup>GEN,AENCAP,ADECAP,CHALL</sup></td><td>15 (c, K) ← AuthEncap(sk, pk<sub>j</sub>)</td></tr><tr><td>05 return b</td><td>16 if j &lt; u //G<sub>1,u,q</sub></td></tr><tr><td>Oracle GEN</td><td>17 K <sup>s</sup> K //G<sub>1,u,q</sub></td></tr><tr><td>06 l ← l + 1</td><td>18 if j = u //G<sub>1,u,q</sub></td></tr><tr><td>07 (sk<sub>l</sub>, pk<sub>l</sub>) <sup>s</sup> Gen</td><td>19 ctr ← ctr + 1 //G<sub>1,u,q</sub></td></tr><tr><td>08 return (pk<sub>l</sub>, l)</td><td>20 if ctr ≤ q //G<sub>1,u,q</sub></td></tr><tr><td>Oracle ADECAP(j ∈ [l], pk, c)</td><td>21 K <sup>s</sup> K //G<sub>1,u,q</sub></td></tr><tr><td>09 try get K s.t. (pk, pk<sub>j</sub>, c, K) ∈ C</td><td>22 K <sup>s</sup> K //G<sub>2</sub></td></tr><tr><td>10 then return K</td><td>23 C ← C ∪ {(μ(sk), pk<sub>j</sub>, c, K)}</td></tr><tr><td>11 K ← AuthDecap(sk<sub>j</sub>, pk, c)</td><td>24 return (c, K)</td></tr><tr><td>12 return K</td><td></td></tr></table>

### GAME $G_0$
This is the original $(n, q_e, q_d, q_c)$-Insider-CCA$_l$ game. The set $\mathcal{C}$ is used to store all queries to the challenge oracle $\mathrm{CHALL}$. If a challenge is queried to the decapsulation oracle $\mathrm{ADECAP}$, then the challenge key is directly returned. Due to perfect correctness, this is only a conceptual change. Thus,

$$\Pr[G_0 \Rightarrow 1] = \Pr[(n, q_e, q_d, q_c)\text{-Insider-CCA}_l(\mathcal{A}) \Rightarrow 1].$$
In the following, we want to replace all real challenge keys by random keys, iterating over all users (indicated by index $u$) and their challenges (indicated by index $q$). We capture each iteration in an intermediate game $G_{1,u,q}$, where the key of the $q$-th query to CHALL for receiver public key $pk_u$ is replaced by random.

At this point we want to remark that $q_c$ is the total number of challenge queries for all users. In particular, the actual number of challenge queries for a specific user might be lower. However, in our following analysis we cannot easily use this fact to achieve a better bound because we have to cover all cases, which explains the tightness loss of $n \cdot q_c$.

GAMES ($G_{1,u,q}$)$_{u \in [n], q \in [q_c]}$. To identify the corresponding challenge query, we use a counter $ctr$. Each time, a challenge query for receiver public key $pk_u$ is issued, the counter is increased. Note that the first intermediate game $G_{1,1,0}$ is the same as $G_0$ as well as $G_{1,u,q_c}$ is the same as $G_{1,u+1,0}$ for all $u \in [n-1]$. Hence,

$$ \Pr[G_{1,1,0} \Rightarrow 1] = \Pr[G_0 \Rightarrow 1], $$

and

$$ \Pr[G_{1,u,q_c} \Rightarrow 1] = \Pr[G_{1,u+1,0} \Rightarrow 1]. $$

In order to bound the difference between $G_{1,u,q-1}$ and $G_{1,u,q}$ for $u \in [n]$, $q \in [q_c]$, we construct an adversary $\mathcal{B}_{u,q}$ against $(q_e, q_d, 1)$-1-Insider-CCA in Listing C.7.

<table><caption>Listing C.7: Adversary $\mathcal{B}_{u,q}$ against $(q_e, q_d, 1)$-1-Insider-CCA, where $u \in [n]$ and $q \in [q_c]$.</caption><tr><td><b>B</b><sup>AEncap,ADecap,Chall</sup><sub>u,q</sub></td><td><b>Oracle AEncap</b>(i &isin; [&ell;], pk)</td></tr><tr><td>01 &ctri; &larr; 0</td><td>19 if i = u</td></tr><tr><td>02 &ell; &larr; 0</td><td>20 (c, K) &larr; AEncap(pk)</td></tr><tr><td>03 C &larr; &emptyset;</td><td>21 else</td></tr><tr><td>04 b &csub; A<sup>GEN,AEncap,ADecap,Chall</sup></td><td>22 (c, K) &larr; AuthEncap(sk<sub>i</sub>, pk)</td></tr><tr><td>05 <b>return</b> b</td><td>23 <b>return</b> (c, K)</td></tr><tr><td><b>Oracle GEN</b></td><td><b>Oracle CHALL</b>(j &isin; [&ell;], sk)</td></tr><tr><td>06 &ell; &larr; &ell; + 1</td><td>24 (c, K) &larr; AuthEncap(sk, pk<sub>j</sub>)</td></tr><tr><td>07 if &ell; = u</td><td>25 if j = u</td></tr><tr><td>08 pk<sub>u</sub> &larr; pk<sup>*</sup></td><td>26 &ctri; &larr; &ctri; + 1</td></tr><tr><td>09 else</td><td>27 if &ctri; = q</td></tr><tr><td>10 (sk<sub>t</sub>, pk<sub>t</sub>) &larr; <sup>s</sup><sub>&emptyset;</sub> Gen</td><td>28 (c, K) &larr; Chall(sk)</td></tr><tr><td>11 <b>return</b> (pk<sub>t</sub>, &ell;)</td><td>29 if j &lt; u or (j = u &and; &ctri; &lt; q)</td></tr><tr><td><b>Oracle ADecap</b>(j &isin; [&ell;], pk, c)</td><td>30 K &csub; K</td></tr><tr><td>12 <b>try get</b> K s.t. (pk, pk<sub>j</sub>, c, K) &isin; C</td><td>31 C &larr; C &割; {&mu;(sk), pk<sub>j</sub>, c, K}</td></tr><tr><td>13 <b>then return</b> K</td><td>32 <b>return</b> (c, K)</td></tr><tr><td>14 if j = u</td><td></td></tr><tr><td>15 K &larr; ADecap(pk, c)</td><td></td></tr><tr><td>16 else</td><td></td></tr><tr><td>17 K &larr; AuthDecap(sk<sub>j</sub>, pk, c)</td><td></td></tr><tr><td>18 <b>return</b> K</td><td></td></tr></table>

$\mathcal{B}_{u,q}$ inputs a challenge public key $pk^*$ and has access to oracles AEncap, ADecap, Chall. It initialises counters $ctr$ for the number of challenge queries and $\ell$ for the number of users. On the $u$-th query to $GEN$, $\mathcal{B}_{u,q}$ outputs $pk^*$ to $\mathcal{A}$. On all other queries, it samples a new key pair. If $\mathcal{A}$ queries AEncap on index $u$, $\mathcal{B}_{u,q}$ uses its AEncap oracle to answer the query. For all other indices, it knows the corresponding secret key and can run the AuthEncap algorithm on its own. The same applies for queries to the ADecap oracle.
If $\mathcal{A}$ issues a challenge query on an index $j$ and a secret key $sk$, $\mathcal{B}_{u,q}$ first
runs the AuthEncap algorithm itself. If $j = u$, the counter $ctr$ is incremented
and if this is the $q$-th query, $\mathcal{B}_{u,q}$ queries the challenge oracle $Chall$. It then
checks whether the challenge key needs to be replaced by a random key,
that means in case $j < u$ or in case $j = u$ and $ctr < q$.

If $\mathcal{B}_{u,q}$ is in the $(q_e, q_d, 1)$-Insider-CCA$_\ell$ game, it perfectly simulates $G_{1,u,q-1}$. Otherwise, if $\mathcal{B}_{u,q}$ is in the $(q_e, q_d, 1)$-Insider-CCA$_r$ game, it perfectly simulates $G_{1,u,q}$, hence

$$
|\Pr[G_{1,u,q-1} \Rightarrow 1] - \Pr[G_{1,u,q} \Rightarrow 1]| \le \text{Adv}_{\mathcal{B}_{u,q}, \text{AKEM}}^{(q_e, q_d, 1)-\text{Insider-CCA}}.
$$

GAME $G_2$. In this game, all keys output by the challenge oracle CHALL are random keys. Note that this game is the same as $G_{1,n,q_c}$, hence

$$
\Pr[G_2 \Rightarrow 1] = \Pr[G_{1,n,q_c} \Rightarrow 1].
$$

Finally note that $G_2$ is exactly the same as the $(n, q_e, q_d, q_c)$-Insider-CCA$_r$ game and

$$
\Pr[G_2 \Rightarrow 1] = \Pr[(n, q_e, q_d, q_c)\text{-Insider-CCA}_r(\mathcal{A}) \Rightarrow 1].
$$

Folding adversaries $\mathcal{B}_{u,q}$ into a single adversary $\mathcal{B}$ and collecting the probabilities yields the bound claimed in Theorem C.2. $\square$

C.1.3 Proof of Theorem C.3

Proof. Let $\mathcal{A}$ be an adversary against $(n, q_e, q_d)$-Outsider-Auth security of AKEM that makes at most $n$ queries to $\text{GEN}$, at most $q_e$ queries to $\text{AENCAP}$ and $q_d$ queries to $\text{ADECAP}$. Consider the games $G_0-G_4$ in Listing C.8. We proceed similarly to the proof of Theorem C.1.

<table><caption>Listing C.8: Games $G_0-G_4$ for the proof of Theorem C.3, where $u \in [n]$, $v \in [n]_0$.</caption>
  <tbody>
    <tr>
      <td>G<sub>0</sub>, G<sub>1</sub>, (G<sub>2,u,v</sub>)<sub>u&isin;[n],v&isin;[n]₀</sub>, G<sub>3</sub>, G<sub>4</sub></td>
      <td>Oracle ADECAP(j &isin; [l], pk, c)</td>
    </tr>
    <tr>
      <td>01 ctr &larr; 0</td>
      <td>15 try get K s.t. (pk, pk<sub>j</sub>, c, K) &isin; E</td>
    </tr>
    <tr>
      <td>02 l &larr; 0</td>
      <td>16 then return K</td>
    </tr>
    <tr>
      <td>03 E &larr; &empty;</td>
      <td>17 K &larr; AuthDecap(sk<sub>j</sub>, pk, c)</td>
    </tr>
    <tr>
      <td>04 COLL<sub>pk</sub> &larr; false</td>
      <td>18 if pk &isin; {pk<sub>1</sub>, ..., pk<sub>j</sub>} and K &ne; &perp;</td>
    </tr>
    <tr>
      <td>05 b &larr; A<sup>GEN,AENCAP,ADECAP</sup></td>
      <td>19 find i such that pk = pk<sub>i</sub></td>
    </tr>
    <tr>
      <td>06 return b</td>
      <td>20 if j &lt; u or (j = u &and; i &lt; v)</td>
    </tr>
    <tr>
      <td>Oracle GEN</td>
      <td>21 K &larr; K</td>
    </tr>
    <tr>
      <td>07 l &larr; l + 1</td>
      <td>22 if j = u &and; i = v</td>
    </tr>
    <tr>
      <td>08 (sk<sub>l</sub>, pk<sub>l</sub>) &larr; Gen</td>
      <td>23 ctr &larr; ctr + 1</td>
    </tr>
    <tr>
      <td>09 if pk<sub>l</sub> &isin; {pk<sub>1</sub>, ..., pk<sub>l&minus;1</sub>}</td>
      <td>24 if ctr &le; q</td>
    </tr>
    <tr>
      <td>10 COLL<sub>pk</sub> &larr; true; abort</td>
      <td>25 K &larr; K</td>
    </tr>
    <tr>
      <td>11 return (pk<sub>l</sub>, l)</td>
      <td>26 K &larr; K</td>
    </tr>
    <tr>
      <td>Oracle AENCAP(i &isin; [l], pk)</td>
      <td>27 E &larr; E &or; {pk<sub>i</sub>, pk<sub>j</sub>, c, K}</td>
    </tr>
    <tr>
      <td>12 (c, K) &larr; AuthEncap(sk<sub>i</sub>, pk)</td>
      <td>28 return K</td>
    </tr>
    <tr>
      <td>13 E &larr; E &or; {pk<sub>i</sub>, pk, c, K}</td>
      <td></td>
    </tr>
    <tr>
      <td>14 return (c, K)</td>
      <td></td>
    </tr>
  </tbody>
</table>

GAME $G_0$. Note that this game is the $(n, q_e, q_d)$-Outsider-Auth$_\ell$ game. We already initialise the multiset $\mathcal{E}$ and boolean flag $\text{COLL}_{\text{pk}}$, which we will need in the following games. In $G_0$, $\mathcal{E}$ is used to store all queries to the encapsulation oracle $\text{AENCAP}$ and all queries to the decapsulation oracle
ADECAP, which correspond to challenge queries, that is all queries where pk supplied by A is one of the public keys generated by the game. If a challenge or a previous AENCAP query is queried to ADECAP again, then the corresponding key is directly returned. Due to perfect correctness, this is only a conceptual change. Thus,

$$ \Pr[G_0 \Rightarrow 1] = \Pr[(n, q_e, q_d)\text{-Outsider}-\text{Auth}_\ell(A) \Rightarrow 1]. $$

### GAME G₁.
In this game, we raise flag COLL<sub>pk</sub> and abort, whenever a query to GEN generates a public key that was already generated in a previous query to GEN. Due to the difference lemma,

$$ |\Pr[G_0 \Rightarrow 1] - \Pr[G_1 \Rightarrow 1]| \le \Pr[\text{COLL}_{\text{pk}}], $$

which we can bound by

$$ \Pr[\text{COLL}_{\text{pk}}] \le \binom{n}{2} \cdot P_{\text{AKEM}} \le \frac{n^2}{2} \cdot P_{\text{AKEM}}. $$

In the following we want to iterate over all pairs of honest users using indices $u, v \in [n]$ and all their challenges using index $q \in [q_d]_0$ and replace the corresponding challenge key by a random key. We capture each iteration in an intermediate game $G_{2,u,v,q}$, where the key of the q-th query to ADECAP for sender public key $pk_u$ and receiver public key $pk_v$ is replaced by random.

At this point we want to remark that $q_d$ is the number of queries for all users and regardless whether it is a challenge query or not. In particular, the actual number of challenge queries for a specific user pair might be lower. However, in our following analysis we cannot easily use this fact to achieve a better bound because we have to cover all cases, which explains the tightness loss of $n^2 \cdot q_d$.

### GAMES (G<sub>2,u,v,q</sub>)<sub>u,v \in [n]</sub>, q<sub>u,v \in [q_d]</sub>.
To identify the corresponding challenge query, we use a counter ctr. Each time a challenge query for receiver public key $pk_u$ and sender public key $pk_v$ is issued, the counter is increased. Note that the first intermediate game G<sub>2,1,1,0</sub> is exactly game G<sub>1</sub>, thus

$$ \Pr[G_{2,1,1,0} \Rightarrow 1] = \Pr[G_1 \Rightarrow 1]. $$

Also note that whenever $q$ reaches $q_d$, there will be no change in the next step. In particular, for all $u \in [n]$, $v \in [n-1]$, $G_{2,u,v,q_d}$ is the same as $G_{2,u,v+1,0}$, as well as for all $u \in [n-1]$, $G_{2,u,n,q_e}$ is the same as $G_{2,u+1,1,0}$ and thus

$$ \Pr[G_{2,u,v,q_d} \Rightarrow 1] = \Pr[G_{2,u,v+1,0} \Rightarrow 1], $$

$$ \Pr[G_{2,u,n,q_d} \Rightarrow 1] = \Pr[G_{2,u+1,1,0} \Rightarrow 1]. $$

On a high level each game $G_{2,u,v,q}$ separates the output of ADECAP on a query ($j, pk_i$), where $pk_i \in \{pk_1, \dots, pk_\ell\}$ is one of the public keys generated by the game so far, into two sets. The game outputs 1) a random key if $j < u$ or if $j = u$ and $i < v$ as well as if $j = u$ and $i = v$ and ctr $\le q$, and 2) the real key otherwise.

At this point note that for challenges the index $i$ is uniquely defined as each public key generated by the game is unique. Also, each entry in the multiset $\mathcal{E}$ is unique.
Listing C.9: Adversary $\mathcal{B}_{u,v,q}$ against $(q_e, q_d, 1)$-2-Outsider-Auth, where $f: \{u, v\} \to \{1, 2\}$ is a function such that, when $u = v, f(u) = f(v) = 1$, and when $u \neq v, f(u) = 1$ and $f(v) = 2$.

$$ \mathcal{B}_{u,v,q}^{\text{AEncap,ADecap,Chall}}(\text{pk}'_1, \text{pk}'_2) $$

$$ 01 \quad \text{ctr} \leftarrow 0 $$

$$ 02 \quad \ell \leftarrow 0 $$

$$ 03 \quad \mathcal{E} \leftarrow \emptyset $$

$$ 04 \quad b \stackrel{\S}{\leftarrow} \mathcal{A}^{\text{GEN,AEncAP,ADECAP}} $$

$$ 05 \quad \text{return } b $$

Oracle GEN

$$ 06 \quad \ell \leftarrow \ell + 1 $$

$$ 07 \quad \text{if } \ell = u $$

$$ 08 \quad \text{pk}_u \leftarrow \text{pk}'_1 $$

$$ 09 \quad \text{else if } \ell = v $$

$$ 10 \quad \text{pk}_v \leftarrow \text{pk}'_2 $$

$$ 11 \quad \text{else} $$

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

$$ 13 \quad \text{if } \text{pk}_\ell \in \{\text{pk}_1, \dots, \text{pk}_{\ell-1}\} $$

$$ 14 \quad \text{abort} $$

$$ 15 \quad \text{return } (\text{pk}_\ell, \ell) $$

Oracle AEncAP

$$ 16 \quad \text{if } i \in \{u, v\} $$

$$ 17 \quad (c, K) \leftarrow \text{AEncap}(f(i), \text{pk}) $$

$$ 18 \quad \text{else} $$

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

$$ 20 \quad \mathcal{E} \leftarrow \mathcal{E}^* \{(\text{pk}_i, \text{pk}, c, K)\} $$

$$ 21 \quad \text{return } (c, K) $$

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

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

$$ 23 \quad \text{then return } K $$

$$ 24 \quad \text{if } \text{pk} \notin \{\text{pk}_1, \dots, \text{pk}_\ell\} $$

$$ 25 \quad \text{if } j \in \{u, v\} $$

$$ 26 \quad K \leftarrow \text{ADecap}(f(j), \text{pk}, c) $$

$$ 27 \quad \text{else} $$

$$ 28 \quad K \leftarrow \text{AuthDecap}(\text{sk}_j, \text{pk}, c) $$

$$ 29 \quad \text{return } K $$

$$ 30 \quad \text{find } i \text{ such that } \text{pk} = \text{pk}_i $$

$$ 31 \quad \text{if } j \notin \{u, v\} $$

$$ 32 \quad K \leftarrow \text{AuthDecap}(\text{sk}_j, \text{pk}, c) $$

$$ 33 \quad \text{else if } j = u \text{ and } i = v $$

$$ 34 \quad \text{ctr} \leftarrow \text{ctr} + 1 $$

$$ 35 \quad \text{if } \text{ctr} = q $$

$$ 36 \quad K \leftarrow \text{Chall}(f(j), f(i), c) $$

$$ 37 \quad \text{else} $$

$$ 38 \quad K \leftarrow \text{ADecap}(f(j), \text{pk}_i, c) $$

$$ 39 \quad \text{else} $$

$$ 40 \quad K \leftarrow \text{ADecap}(f(j), \text{pk}_i, c) $$

$$ 41 \quad \text{if } j < u \text{ or } (j = u \land i < v) $$

$$ \text{or } (j = u \land i = v \land \text{ctr} < q) $$

$$ 42 \quad \text{if } K \neq \bot $$

$$ 43 \quad K \stackrel{\S}{\leftarrow} K $$

$$ 44 \quad \text{if } K \neq \bot $$

$$ 45 \quad \mathcal{E} \leftarrow \mathcal{E}^* \{(\text{pk}, \text{pk}_j, c, K)\} $$

$$ 46 \quad \text{return } K $$

We now need to bound the difference between games $G_{2,u,v,q-1}$ and $G_{2,u,v,q}$ for all $u, v \in [n], q \in [q_d]$. Therefore, we construct adversary $\mathcal{B}_{u,v,q}$ against $(q_e, q_d, 1)$-2-Outsider-Auth in Listing C.9.

Adversary $\mathcal{B}_{u,v,q}$ has access to oracles AEncap, ADecap and Chall. It inputs two public keys which we denote by $\text{pk}'_1$ and $\text{pk}'_2$ in order to avoid confusion with public keys $\text{pk}_1$ and $\text{pk}_2$ which will be the first two public keys that $\mathcal{B}_{u,v,q}$ outputs to $\mathcal{A}$ when $\mathcal{A}$ queries GEN. On the $u$-th query to GEN, $\mathcal{B}_{u,v,q}$ will then output $\text{pk}'_1$ and on the $v$-the query it will output $\text{pk}'_2$. Note that when $u = v, \mathcal{B}_{u,v,q}$ will only use $\text{pk}'_1$. This captures queries to ADECAP of the form $(j, \text{pk}_j)$. All remaining key pairs will be honestly generated with the condition that $\mathcal{B}_{u,v,q}$ aborts whenever the same key is generated twice, as introduced in game $G_1$. As in the proof of Theorem C.1, we define a function $f: \{u, v\} \to \{1, 2\}$ such that, when $u = v, f(u) = f(v) = 1$, and when $u \neq v, f(u) = 1$ and $f(v) = 2$. This ensures that oracles AEncap, ADecap and Chall are queried on the correct indices.

Queries to AEncap are simulated using the AEncap oracle whenever $\mathcal{A}$ makes a query on $u$ or $v$. Otherwise, $\mathcal{B}_{u,v,q}$ can run the AuthEncap algorithm, since it knows the secret key $\text{sk}_i$.

Queries to ADECAP are simulated as follows: We first take care of non-challenges, that means where the public key supplied by $\mathcal{A}$ is not one of the public keys generated by $\mathcal{B}_{u,v,q}$ so far. If the index $j$ supplied by $\mathcal{A}$ is either $u$ or $v$, $\mathcal{B}_{u,v,q}$ queries its ADecap oracle. Otherwise, it knows the corresponding secret key and can run the AuthDecap algorithm itself. The result will then returned to $\mathcal{A}$. If the query was a challenge query, then $\text{pk}$ must be $\text{pk}_i$ for some unique $i \in [\ell]$. Before we can replace any challenge keys, we first need to compute the output of AuthDecap using the algorithm itself or the correct
oracle. If $j \notin \{u, v\}$, $\mathcal{B}_{u,v,q}$ knows the secret key and can thus compute the output on its own. If $j = u$ and $i = v$, we need to increment the counter $ctr$ and if this is the $q$-th query, $\mathcal{B}_{u,v,q}$ calls the challenge oracle $\text{Chall}$. In all other cases, it calls $\text{ADecap}$. At this point note that $\mathcal{B}_{u,v,q}$ makes at most $q_d$ queries to the $\text{ADecap}$ oracle and only a single query to $\text{Chall}$.

Now we can proceed to replacing all challenge keys which were considered in previous games. In particular, if $j < u$ or $j = u$ and $i < v$, we choose a random key. We do the same in case $j = u$ and $i = v$ and $ctr < q$. Note that if $\mathcal{B}_{u,v,q}$ is in the $(q_e, q_d, 1)$-2-Outsider-Auth$_\ell$ game, it perfectly simulates $G_{2,u,v,q-1}$. Otherwise, if $\mathcal{B}_{u,v,q}$ is in the $(q_e, q_d, 1)$-2-Outsider-Auth$_r$ game, it perfectly simulates $G_{2,u,v,q}$. Thus for all $q \in [q_d]$,

$$|\Pr[G_{2,u,v,q-1} \Rightarrow 1] - \Pr[G_{2,u,v,q} \Rightarrow 1]| \le \text{Adv}_{\mathcal{B}_{u,v,q}, \text{AKEM}}^{(q_e, q_d, 1)-2-\text{Outsider-Auth}}.$$

### GAME $G_3$
In this game, all challenge keys output by the oracle $\text{ADECAP}$ are random keys. Note that this game is the same as $G_{2,n,n,q_d}$, hence

$$\Pr[G_3 \Rightarrow 1] = \Pr[G_{2,n,n,q_d} \Rightarrow 1].$$

### GAME $G_4$
In game $G_4$ we undo the change introduced in game $G_1$ and do not abort if a public key collision happens. Thus, we get

$$|\Pr[G_3 \Rightarrow 1] - \Pr[G_4 \Rightarrow 1]| \le \frac{n^2}{2} \cdot P_{\text{AKEM}}.$$

Finally note that $G_4$ is exactly the same as the $(n, q_e, q_d)$-Outsider-Auth$_r$ game. We get

$$\Pr[G_4 \Rightarrow 1] = \Pr[(n, q_e, q_d)-\text{Outsider-Auth}_r(A) \Rightarrow 1].$$

Folding adversaries $\mathcal{B}_{u,v,q}$ into a single adversary $\mathcal{B}$ and collecting the probabilities yields the bound claimed in Theorem C.3. □

## C.2 COMPARISON OF PSEUDOCODE DEFINITIONS AND THEIR IMPLEMENTATION IN CRYPTOVERIF

The goal of this section is to convince the readers that the CryptoVerif models provided as supplementary material actually prove the theorems presented in the main body of Chapter 4. Rather than explaining syntax and semantics of CryptoVerif on an abstract level, we take one of the chapter's security notions and explain by example how the pseudocode presented in the main body relates to the code written in CryptoVerif. The security notion we use as example is $(n, q_e, q_d)$-Outsider-CCA of AKEM, presented in Listing 4.3. This notion appears in Theorem 4.7, where we show that DH-AKEM satisfies it, and it appears in the composition theorems 4.3 and 4.5, where we use it as an assumption. In Listing C.10, we display the pseudocode definition of $(n, q_e, q_d)$-Outsider-CCA from Listing 4.3 in the left column next to its implementation as an assumption in CryptoVerif in the right column. The modelling of assumptions and proof goals in CryptoVerif has only some slight syntactical differences. Both columns contain line numbers, and we will use Lxy to refer to line number xy in the left column, and Rxy to refer to line number xy in the right column. As with all the listings throughout the paper
so far, the game of the real version of the notion contains only the non-boxed
lines, and the game of the ideal version additionally contains the boxed
lines. The complete rolled-out version of CryptoVerif code for the (n, q_e, q_d)-
Outsider-CCA notion as assumption can be found in lib.authkem.ocvl, from
lines 102 to 143. The CryptoVerif files are available at [Alw+].

<figure><img src="image_40.png" /><figcaption>Listing C.10: Games $(n, q_e, q_d)$-Outsider-CCA$_\ell$ and $(n, q_e, q_d)$-Outsider-CCA$_r$ for AKEM, with their modelling in CryptoVerif shown on the right side.</figcaption></figure>

[Alw+] Alwen et al., Analysing the HPKE
Standard Supplementary Material

In pseudocode, L01 to L04 constitute the *main procedure* of the game;
they set up the experiment and call the adversary, giving it the oracles GEN,
AENCAP and ADECAP. AENCAP and ADECAP explicitly take the indices
i and j as parameter, by which the adversary chooses the private key upon
which it wants to act. These indices are assigned by GEN.

In CryptoVerif code, the first line R01 states that everything below will
be executed in parallel N times. In CryptoVerif, this is called a *replication*. A
replication index i is assigned to each of the parallel executions. Continuing
to R02, in each of these parallel processes, a key pair will be generated. In
our CryptoVerif model, we chose to represent key pairs in a general way
by a key pair seed s, the private key computed from it by skgen(s) and
the public key by pkgen(s). This allows to cover a broad range of KEM
constructions with one model. The type of key pair seed elements in our
models is called **keypairseed**. The operator $<-R$ denotes that the variable
on the left is sampled randomly from the type given on the right. These keys
can be dynamically generated, that is, line R02 implicitly defines an oracle
GENCV which generates a key pair seed s.

Line R03 begins a block of oracle definitions, and it ends with line R29.
In CryptoVerif, all oracles are implicitly accessible by the adversary. The
three oracles that are defined are Opk in R04, OAEncap in R09, and OADecap
in R24. Lines R06 and R22 define that these oracles are accessible by the
adversary in parallel, in any order it chooses to call them.

The oracles GENCV, Opk, OAEncap, and OADecap are located inside the N
times replication started in R01. This means that these oracles are available
once for each i ∈ [1,N], and they are defined with this index as implicit
argument. Thus, the adversary has access to N oracles GENCV[i] for
1 ≤ i ≤ N, and the variable defined in GENCV[i] is s[i]. All variables in
CryptoVerif are implicitly stored in arrays indexed by the replication indices
above their definition. Similarly, the adversary has access to N oracles Opk[i]
for 1 ≤ i ≤ N, and the variable accessed inside Opk[i] is s[i]. A call to
GENCV[i] immediately followed by a call to Opk[i] is equivalent to a
call to GEN, up to the renumbering of keys. (In pseudocode, the keys are
indexed in increasing order. In CryptoVerif, the keys can be generated in
any order. The renumbering just consists in applying a bijection known to
the adversary to the indices of keys.) CryptoVerif separates generating keys
by GENCV[i] from acquiring the public key by Opk[i], while pseudocode
groups these two actions in one oracle call GEN. However, a call to Opk[i]
can be added immediately after GENCV[i] and all other calls to Opk[i]
removed without changing the state of the system, so this separation leaves
the security notion unchanged.

The main procedure in the pseudocode (lines L01-L04) is essentially absent in CryptoVerif. Line L01 initializes the index for the last generated key $\ell$. There is no such index in CryptoVerif, since the adversary provides the index of the key it generates at generation time, as argument to oracle GENCV. Line L02 initialises the multiset $\mathcal{E}$. In the CryptoVerif model, $\mathcal{E}$ is represented by a table E, which is implicitly empty at the beginning. Line L03 calls the adversary and line L04 returns its result. The adversary is not explicitly called in CryptoVerif: the adversary is implicit and is allowed to call all oracles provided by the CryptoVerif code.

Lines R07 and R23 define a replication, indicating that the adversary can
call OAEncap[i] (pk_R) for each key pair Qeperuser times, and OADecap[i]
(pk_S, cd) for each key pair Qdperuser times. The oracle Opk has no
replication in front of it, which means the adversary can call it only once
per key pair (which is sufficient to acquire the public key).

In the real version of the security notion, the oracle AENCAP directly
returns the result of the probabilistic AuthEncap function, see line L08. This
corresponds to R21. In CryptoVerif, all functions are deterministic; to model
a probabilistic function, one has to provide randomness to a function. For
AuthEncap_r this is done with the ks parameter. It is chosen randomly
by the oracle OAEncap independently for each call; the CryptoVerif syntax
requires that this statement is located directly after the replication definition
in R08, and thus before the oracle definition.

The public key given as parameter to 0AEncap has the role of the recipient public key, which is why it is called pk_R. We proceed to explain how the ideal version of the security notion is formalised in CryptoVerif. The if statement in L09 corresponds to the find statement started in lines R10 and R11. This find implements a lookup in the set of honest public keys pkᵢ: it looks for an index i2 ∈ [1, N], and tests if the public key pk_R given as argument to the oracle is equal to the public key pkgen(s[i2]) corresponding to the key pair seed s[i2], that is, the value of s generated within the replicated copy indexed by i2. (The operator && is the logical and.)

The syntax let (...) = ... in R13 denotes a pattern matching; it is used here to split up the tuple that the function AuthEncap_r returns. The actual pattern matching used in the CryptoVerif model is let AuthEncap_tuple(k: key, ce: ciphertext) = ..., but we abbreviated it to let (k, ce) = ... such that it fits into one line in the listing. In general, a pattern matching can fail in CryptoVerif, which is why we need to include an else case with lines R17 and R18; we return an error symbol AuthEncap_None, which corresponds to ⊥. The actual AuthEncap does not fail; we model this with a simple game transformation eliminate_failing that expresses that AuthEncap_r always returns a pair and results in removing the else branch during the proofs. Lines R14 and R16 are executed if the pattern matching and thus the call to AuthEncap_r succeeded: A random KEM key k' is generated, a new element is added to the table E, which represents the multiset $\mathcal{E}$, and a new tuple is constructed from k' and the KEM ciphertext ce, and returned.

The difference remaining to be explained is that on the left side, there is only one call to AuthEncap, at the beginning of the oracle in line L08, but two calls to AuthEncap_r on the right side, in lines R13 and R21. These two calls are in disjoint branches of the code and thus both variants are equivalent. The reason we do not call AuthEncap_r once at the beginning of the oracle is purely technical: The proof is easier if we assign unique variable names per branch from the start (here: (k, ce) and no variable assignment in R21).

Oracle 0ADecap takes a sender public key pk_S and a KEM ciphertext cd as arguments. In the real version, the result of the actual AuthDecap function is returned, see lines L15 and R28.

The **try get** statement with the lookup in multiset $\mathcal{E}$ in L13 has its counterpart in the get statement in line R25, which looks up in table E. In E(=pk_S, =pkgen(s), =cd, k''), the equality tests =pk_S, =pkgen(s), and =cd indicate that we look for an element in E whose first 3 components are equal to the given values. The fourth component is a variable k''', which is bound to the fourth component of the found element of E, if such an element is found. If an element is found, 0ADecap returns the random key k'' found in the table E (R26). In case several elements match, the get statement chooses one at random, like the **try get** statement.

The CryptoVerif property expresses a bound on the probability that the adversary distinguishes the real from the ideal game; it leaves implicit the return of the bit b by which the adversary says with which of the two games it thinks it interacts.
If CryptoVerif concludes a proof, it displays the probability bound it could
prove. In CryptoVerif's output, this bound is indicated in the line that starts
with RESULT Proved. The proof output for Chapter 4's theorems can be
found in the files with filenames ending in .proof [Alw+]. The probabil-
ity bound depends on replication parameters (for example N, Qeperuser,
Qdperuser), total number of calls to oracles, written #0 for oracle 0 (for
example #0AEncap, #0ADecap), probability bounds of the assumptions used
in the proof (for example Adv_PRF_KeySchedule and Adv_Outsider_CCA),
and collision probabilities (for example P_pk_coll, which corresponds to
P<sub>AKEM</sub>, for AKEM public keys in our composition proofs, and P_hashcoll
for the collision resistant hash function in the key schedule proof). Probabil-
ity bounds like Adv_Outsider_CCA are expressed as functions with several
arguments: the execution time of the adversary (indicated by time_*) and
the numbers of queries. The execution time of the adversary is detailed in
the lines below RESULT Proved.

[Alw+] Alwen et al., *Analysing the HPKE*
*Standard Supplementary Material*
<figure><img src="image_41.png" /></figure>
# D

## cv2fstar Case Study: CryptoVerif Model and Generated Code

### D.1 CRYPTOVERIF MODEL NSL.OCV

```c
1 (* Needham Schroeder public key protocol, fixed by Lowe.
2 The user identity in this model is just an arbitrary
3 address. An implementation could use an user@hostname
4 construction.
5 *)
6
7 param Qsetup.
8 param Qkey_reg.
9 param Qinit.
10 param Qresp.
11
12 def OptionType1 (option, option_Some, option_None, input) {
13 fun option_Some (input): option [data].
14 const option_None: option.
15 equationforall x: input;
16 option_Some(x) <> option_None.
17 }
18
19 type nonce [fixed,large].
20 type pkey [bounded].
21 type skey [bounded].
22 type keyseed [fixed,large].
23 type encseed [bounded].
24 type plaintext [bounded].
25 type address [bounded].
26 type keypair [bounded].
27 fun kp (pkey, skey): keypair [data].
28
29 type ciphertext [bounded].
30 type ciphertext_opt [bounded].
31 expand OptionType1 (ciphertext_opt, ciphertext_some, ciphertext_bottom, ciphertext).
32
33 table trusted_keys (address, skey, pkey).
34 table all_keys (address, pkey, bool).
35
36 set diffConstants = false.
37
38 fun msg1 (nonce, address): plaintext [data].
39 fun msg2 (nonce, nonce, address): plaintext [data].
40 fun msg3 (nonce): plaintext [data].
41
```
42
43
44 equationforall z:nonce,t:nonce,u:address,y2:nonce,z2:address;
45 msg2(z,t,u) <> msg1(y2,z2).
46 equationforall y:nonce,y2:nonce,z2:address;
47 msg3(y) <> msg1(y2,z2).
48 equationforall z:nonce,t:nonce,u:address,y2:nonce;
49 msg2(z,t,u) <> msg3(y2).
50
51 (* Public-key encryption (IND-CCA2) *)
52
53 proba Penc.
54 proba Penccoll.
55
56 expand IND_CCA2_public_key_enc_all_args(
57 keyseed, pkey, skey, plaintext, ciphertext_opt, encseed,
58 skgen, skgen2, pkgen, pkgen2, enc, enc_r, enc_r2, dec_opt, dec_opt2, injbot,
59 Z, Penc, Penccoll).
60
61 (* Not needed because the in processes receive ciphertext, not ciphertext_opt *)
62 equationforall sk: skey; dec_opt(ciphertext_bottom, sk) = bottom.
63
64 letfun dec(c: ciphertext, sk: skey) =
65 dec_opt(ciphertext_some(c), sk).
66
67 letfun keygen() = k <-R keyseed; kp(pkgen(k), skgen(k)).
68
69 const Z plaintext: plaintext.
70 equationforall x: plaintext; Z(x) = Z plaintext.
71
72 (* Queries *)
73
74 event beginA(address, address, nonce, nonce).
75 event endA(address, address, nonce, nonce).
76 event beginB(address, address, nonce, nonce).
77 event endB(address, address, nonce, nonce).
78
79 query x:address, y:address, na:nonce, nb:nonce;
80 event(endA(x,y,na,nb)) = eventnings(x,y,na,nb)).
81 query x:address, y:address, na:nonce, nb:nonce;
82 event(endB(x,y,na,nb)) = event(nmns(x,y,na,nb)).
83 query x:address, y:address, na:nonce, nb:nonce;
84 inj-event(endA(x,y,na,nb)) = inj-event(begins(x,y,na,nb)).
85 query x:address, y:address, na:nonce, nb:nonce;
86 inj-event(endB(x,y,na,nb)) = inj-event(begins(x,y,na,nb)).
87
88 type msg1res_t.
89 fun msg1succ(skey, pkey, bool, nonce, ciphertext): msg1res_t [data].
90 const msg1fail: msg1res_t.
91 equationforall x1: skey, x2: pkey, x3: bool, x4: nonce, x5: ciphertext;
92 msg1succ(x1,x2,x3,x4,x5) <> msg1fail.
93
94 implementation
95 type keyseed=256;
96 type nonce=64;
97 type ciphertext="ciphertext"
98 [serial = " serialize_ciphertext ", " deserialze_ciphertext "; equal = "eq_ciphertext"];
99 type ciphertext_opt="ciphertext_opt"
100 [equal = "eq_ciphertext_opt"; serial = "ciphertext_opt_to ", "ciphertext_opt_from"];
101 fun ciphertext_some="ciphertext_some" [inverse = "inv_ciphertext_some"];
102 const ciphertext_bottom="ciphertext_bottom";
103 type pkey="pkey" [serial = " serialize_pkey ", " deserialze_pkey "; equal = "eq_pkey"];

42

43

44

45

46

47

48

49

50

51

52

53

54

55

56

57

58

59

60

61

62

63

64

65

66

67

68

69

70

71

72

73

74

75

76

77

78

79

80

81

82

83

84

85

86

87

88

89

90

91

92

93

94

95

96

97

98

99

100

101

102

103
```c
104 type skey="skey" [serial = " serialize_skey", " deserialze_skey"; equal = "eq_skey"];
105 type encseed=256;
106 table trusted_keys="trusted_keys";
107 table all_keys="all_keys";
108 type keypair="keypair" [equal = "eq_keypair"];
109 type plaintext=" plaintext" [equal = "eq plaintext"];
110 fun msg1="msg1" [inverse = "inv msg1"];
111 fun msg2="msg2" [inverse = "inv msg2"];
112 fun kp = "kp" [inverse = "inv kp"];
113 fun skgen = "skgen";
114 fun pkgen = "pkgen";
115 type address="address"
116 [serial = " serialize_address", " deserialze_address"; equal = "eq_addr"];
117 fun enc_r="enc";
118 fun dec="dec";
119 fun injbot="injbot" [inverse = "inv injbot"];
120 fun msg3="msg3" [inverse = "inv msg3"];
121 fun msg1succ="msg1succ" [inverse = "inv msg1succ"];
122 const msg1fail="msg1fail";
123 type msg1res_t="msg1res" [equal = "eq msg1res"].
124
125 letfun initiator_send msg1_inner(addrA: address, addrX: address) =
126 (* the gets fail if addrA or addrX have not been
127 setup by the adversary. *)
128 get[unique] trusted_keys(=addrA, skA, pkA) in (
129 get[unique] all_keys(=addrX, pkX, trustX) in (
130 (* Prepare Message 1 *)
131 Na <-R nonce;
132 let cc1 = enc(msg1(Na, addrA), pkX) in
133 let ciphertext_some(c1: ciphertext) = cc1 in (
134 msg1succ(skA, pkX, trustX, Na, c1)
135 ) else msg1fail
136 ) else msg1fail
137 ) else msg1fail.
138
139 let initiator() =
140
141 Initiator {
142     foreach i_init ≤ Qinit do
143         initiator_send msg1 (addrA: address, addrX: address) :=
144             let msg1succ(skA, pkX, trustX, Na, c1) = initiator_send msg1_inner(addrA, addrX) in
145             return (c1);
146         (* Receive Message 2 *)
147         initiator_send msg3 (c: ciphertext) :=
148             let injbot(msg2(=Na, Nb, =addrX)) = dec(c, skA) in
149             event beginA(addrA, addrX, Na, Nb);
150             (* Prepare Message 3 *)
151             let ciphertext_some(c3) = enc(msg3(Nb), pkX) in
152             return (c3);
153         (* OK *)
154         initiator_finished() :=
155             if (trustX) then
156                 event endA(addrA, addrX, Na, Nb);
157             return ()
158         }.
159     let responder() =
160```
166 Responder {
167
168 foreach iresp & Qresp do
169
170 (* Receive Message 1 *)
171 responder_send msg2 (addrB: address, m: ciphertext) :=
172 (* the get fails if addrB has not been setup by
173 the adversary *)
174 get[unique] trusted_keys(=addrB, skB, pkB) in
175 let injbot(msg1(Na, addrY)) = dec(m, skB) in
176 get[unique] all_keys(=addrY, pkY, trustY) in
177 (* Send Message 2 *)
178 Nb <-R nonce;
179 event beginB(addrY, addrB, Na, Nb);
180 let ciphertext_some(c2) = enc(msg2(Na, Nb, addrB), pkY) in
181 return (c2);
182
183 (* Receive Message 3 *)
184 responder_received msg3 (m3: ciphertext) :=
185 let injbot(msg3(=Nb)) = dec(m3, skB) in
186 if (trustY) then (
187 event endB(addrY, addrB, Na, Nb); return ()
188 else return ()
189 else return ()
190
191 }.
192
193 let key_register() =
194 Key Register {
195
196 foreach i & Qkey_reg do
197
198 register (addr: address, pkX: pkey) :=
199 get[unique] all_keys(=addr, ign1, ign2) in (
200 yield
201 ) else
202 insert all_keys(addr, pkX, false);
203 return ()
204 }.
205
206 let setup() =
207 Setup {
208
209 foreach i & Qsetup do
210 setup(addr: address) :=
211 get[unique] all_keys(=addr, ign1, ign2) in (
212 yield
213 ) else
214 let kp(the_pkA: pkey, the_skA: skey) = keygen() in
215 insert trusted_keys(addr, the_skA, the_pkA);
216 insert all_keys(addr, the_pkA, true);
217 return(the_pkA)
218
219 }.
220
221 process
222 (
223 run setup()
224 |
225 run key_register()
226 |
227 run initiator()
228 |  
229   run responder()  
230 )

D.2 NSL.INITIATOR.FSTI, GENERATED BY CV2FSTAR

1 module NSL.Initiator
2
3 open CVTypes
4 open State
5 open Helper
6 open NSL Types
7 open NSL Functions
8 open NSL Tables
9 open NSL Sessions
10 open NSL Events
11 open NSL Protocol
12
13 val oracle_initiator_finished: nsl_state → nat → Tot (nsl_state * option (unit))
14
15 val oracle_initiator_send_msg_1: nsl_state → address → address
16 → Tot (nsl_state * option (nat * ciphertext))
17
18 val oracle_initiator_send_msg_3: nsl_state → nat → ciphertext
19 → Tot (nsl_state * option (ciphertext))

D.3 NSL.INITIATOR.FST, GENERATED BY CV2FSTAR

1 module NSL.Initiator
2
3 open CVTypes
4 open State
5 open Helper
6 open NSL Types
7 open NSL Functions
8 open NSL Tables
9 open NSL Sessions
10 open NSL Events
11 open NSL Protocol
12
13
14 let oracle_initiator_finished state sid =
15 match get_and_remove_session_entry state Oracle_initiator_finished sid with
16 | state, None → state, None
17 | state, Some (se: nsl_session_entry) →
18 match se with
19 | R1_initiator_finished var_Na_3 var_Nb_1 var_addrA_1 var_addrX_1 var_trustX_2 →
20 if var_trustX_2
21 then
22 let ev = Event_endA var_addrA_1 var_addrX_1 var_Na_3 var_Nb_1 in
23 let state = state_add_event state ev in
24 (state, Some ())
else state, None

let oracle_initiator_sendMsg1 state input_43 input_42 =
  let state, sid = state_reserve_session_id state in
  let var_addrA_1 = input_43 in
  let var_addrX_1 = input_42 in
  let state, v44 = NSL.Letfun.fun_initiator_sendMsg1_inner state var_addrA_1 var_addrX_1 in
  let bvar_45 = v44 in
  match inv_msg1succ bvar_45 with
    | None -> state, None
    | Some (var_skA_2, var_pkX_4, var_trustX_2, var_Na_3, var_c1_3) ->
      let sel =
        [R1_initiator_sendMsg3 var_Na_3 var_addrA_1 var_addrX_1 var_pkX_4 var_skA_2 var_trustX_2]
      in
    let state = state_add_to_session state sid sel in
    (state, Some (sid, var_c1_3))

let oracle_initiator_sendMsg3 state sid input_46 =
  match get_and_remove_session_entry state Oracle_initiator_sendMsg3 sid with
    | state, None -> state, None
    | state, Some (se: nsl_session_entry) ->
      match se with
        | R1_initiator_sendMsg3 var_Na_3 var_addrA_1 var_addrX_1 var_pkX_4 var_skA_2 var_trustX_2 ->
          let var_c_3 = input_46 in
          let bvar_47 = (dec var_c_3 var_skA_2) in
          match inv_injbot bvar_47 with
            | None -> state, None
            | Some bvar_48 ->
              match inv_msg2 bvar_48 with
                | None -> state, None
                | Some (bvar_49, var_Nb_1, bvar_50) ->
                  if eq_lbytes bvar_49 var_Na_3 && eq_addr bvar_50 var_addrX_1
                    then
                      let ev = Event_beginA var_addrA_1 var_addrX_1 var_Na_3 var_Nb_1 in
                      let state = state_add_event state ev in
                      let state, v51 = NSL.Letfun.fun_enc state (msg3 var_Nb_1) var_pkX_4 in
                      let bvar_52 = v51 in
                      match inv_cipherText some bvar_52 with
                        | None -> state, None
                        | Some var_c3_0 ->
                          let sel =
                            [R1_initiator_finished var_Na_3 var_Nb_1 var_addrA_1 var_addrX_1 var_trustX_2]
                          in
                        let state = state_add_to_session state sid sel in
                        (state, Some (var_c3_0))
                      else state, None
                      2
                    3
                  4
                5
              6
            7
        8
      9
    10
  11
  12
  13
  14
  15
  16
  17
  18
  19
  20
  21
  22
  23
  24
  25
  26
  27
  28
  29
  30
  31
  32
  33
  34
  35
  36
  37
  38
  39
  40
  41
  42
  43
  44
  45
  46
  47
  48
  49
  50
  51
  52
  53
  54
  55
  56
  57
  58
  59
  60
  61
  62
  63
  64
  65
  66
  67
  68
  69
  70
  71
  72

## D.4 NSL.RESPONDER.FSTI, GENERATED BY CV2FSTAR

1. module NSL.Responder

2.

3. open CVTypes

4. open State

5. open Helper

6. open NSLireTypes
7 open NSL Functions

8 open NSL Tables

9 open NSL Sessions

10 open NSL Events

11 open NSL Protocol

12

13 val oracle_responder_received msg 3: nsl_state → nat → ciphertext

14 → Tot (nsl_state * option (unit))

15

16 val oracle_responder_send msg 2: nsl_state → address → ciphertext

17 → Tot (nsl_state * option (nat * ciphertext))

## D.5 NSL.RESPONDER.FST, GENERATED BY CV2FSTAR

1 module NSL.Responder

2

3 open CVTypes

4 open State

5 open Helper

6 open NSL Types

7 open NSL Functions

8 open NSL Tables

9 open NSL Sessions

10 open NSL Events

11 open NSL Protocol

12

13

14 let oracle_responder_received msg 3 state sid input_18 =

15 match get_and_remove_session_entry state Oracle_responder_received msg 3 sid with

16 | state, None → state, None

17 | state, Some (se: nsl_session_entry) →

18 match se with

19 | R1_responder_received msg 3 var_Na_4 var_Nb_2 var_addrB_0 var_addrY_0 var_skB_0 var_trustY_0 →

20 let var_m3_0 = input_18 in

21 let bvar_19 = (dec var_m3_0 var_skB_0) in

22 match inv_injbot bvar_19 with

23 | None → state, None

24 | Some bvar_20 →

25 match inv_msg3 bvar_20 with

26 | None → state, None

27 | Some bvar_21 →

28 if eq_lbytes bvar_21 var_Nb_2

29 then

30 if var_trustY_0

31 then

32 let ev = Event_endB var_addrY_0 var_addrB_0 var_Na_4 var_Nb_2 in

33 let state = state_add_event state ev in

34 (state, Some ( ))

35 else (state, Some ( ))

36 else state, None

37

38

39 let oracle_responder_send msg 2 state input_23 input_22 =

40 let state, sid = state_reserve_session_id state in

41 let var_addrB_0 = input_23 in

42 let var_m_0 = input_22 in

43 match
get_unique state
Table_trusted_keys
 fun (te: nsl_table_entry Table_trusted_keys) →
  let TableEntry_trusted_keys tvar_26 tvar_25 tvar_24 = te in
  let bvar_27 = tvar_26 in
  let var_skB_0 = tvar_25 in
  let var_pkB_0 = tvar_24 in
  if eq_addr bvar_27 var_addrB_0 then Some (var_skB_0) else None)
with
 None → state, None
Some var_skB_0 →
let bvar_28 = (dec var_m_0 var_skB_0) in
match inv_injbot bvar_28 with
 None → state, None
Some bvar_29 →
match inv_msg1 bvar_29 with
 None → state, None
Some (var_Na_4, var_addrY_0) →
match
  get_unique state
  Table_all_keys
  (fun (te: nsl_table_entry Table_all_keys) →
   let TableEntry_all_keys tvar_32 tvar_31 tvar_30 = te in
   let bvar_33 = tvar_32 in
   let var_pkY_0 = tvar_31 in
   let var_trustY_0 = tvar_30 in
   if eq_addr bvar_33 var_addrY_0 then Some (var_trustY_0, var_pkY_0) else None)
with
 None → state, None
Some (var_trustY_0, var_pkY_0) →
let state, var_Nb_2 = call_with_entropy state (gen_lbytes 8) in
let ev = Event_beginB var_addrY_0 var_addrB_0 var_Na_4 var_Nb_2 in
let state = state_add_event state ev in
let state, v34 =
  NSL.Letfun.fun_enc state (msg2 var_Na_4 var_Nb_2 var_addrB_0) var_pkY_0
in
let bvar_35 = v34 in
match inv_ciphertext_some bvar_35 with
 None → state, None
Some var_c2_0 →
let sel =
  [
    R1_responder_received msg_3 var_Na_4
    var_Nb_2
    var_addrB_0
    var_addrY_0
    var_skB_0
    var_trustY_0
  ]
in
let state = state_add_to_session state sid sel in
(state, Some (sid, var_c2_0))

D.6 EXCERPT OF APPLICATION.FST, MANUALLY WRITTEN

1 val add_honest_parties: nsl_state → Tot (nsl_state * bool)

2 let add_honest_parties st =
```s
match oracle_setup st addrA with
  | st, None -> st, false
  | st, Some pkA ->
    match oracle_setup st addrB with
      | st, None -> st, false
      | st, Some pkB -> st, true

val initialize: Lib.RandomSequence.entropy -> Tot (nsl_state * bool)
let initialize ent =
  let st = init_state nsl_state_type ent in
  add_honest_parties st

val testrun: Lib.RandomSequence.entropy -> FStar.All.ML Lib.RandomSequence.entropy
let testrun ent =
  match initialize ent with
    | st0, false ->
      IO.print_string "fail";
    finalize_state st0
    | st0, true ->
      IO.print_string "##_Tables_After_Calling_Setup\n\n";
      nsl_print_tables st0;
      IO.print_string "\n";
    match oracle_initiator_send_msg_1 st0 addrA addrB with
      | st1, None ->
        IO.print_string "init_send_1_fail";
      finalize_state st1
      | st1, Some (id_init, c1) ->
        IO.print_string "##_Sessions_After_init_send_msg_1\n\n";
        nsl_print_session st1 id_init;
        IO.print_string "\n\n";
        IO.print_string "##_Protocol_Message_1\n\n";
        print_label_bytes "ct" ( serialize_ciphertext c1) true;
        IO.print_string "\n\n";
    match oracle_responder_send_msg_2 st1 addrB c1 with
      | st2, None ->
        nsl_print_session st2 id_init;
        IO.print_string "resp_send_2_fail";
      finalize_state st2
      | st2, Some (idresp, c2) ->
        IO.print_string "##_Sessions_Afterresp_send_msg_2\n\n";
        nsl_print_session st2 id_init;
        nsl_print_session st2 idResponse;
        IO.print_string "\n\n";
        IO.print_string "##_Protocol_Message_2\n\n";
        print_label_bytes "ct" ( serialize_ciphertext c2) true;
        IO.print_string "\n\n";
    match oracle_initiator_send_msg_3 st2 id_init c2 with
      | st3, None ->
        nsl_print_session st3 id_init;
        IO.print_string "init_send_3_fail";
      finalize_state st3
      | st3, Some c3 ->
        IO.print_string "##_Sessions_After_init_send_msg_3\n\n";
        nsl_print_session st3 id_init;
        nsl_print_session st3 idResponse;
        IO.print_string "\n\n";
        IO.print_string "##_Protocol_Message_3\n\n";
        print_label_bytes "ct" ( serialize_ciphertext c3) true;
        IO.print_string "\n\n";
    match oracle_responder_received msg_3 st3 idResponse c3 with
      | st4, None ->
        nsl_print_session st4 idResponse;
```
```python
65 IO.print_string "resp_recv_3_fail";
66 finalize_state st4
67 | st4, Some () ->
68 IO.print_string "##_Sessions_After resp_recv_msg_3\n\n";
69 nsl_print_session st4 id_init;
70 nsl_print_session st4 idresp;
71 IO.print_string "\n\n";
72 match oracle_initiator_finished st4 id_init with
73 | st5, None ->
74 IO.print_string "initiator_finished_fail";
75 finalize_state st5
76 | st5, Some () ->
77 IO.print_string "##_Sessions_After_init_finished\n\n";
78 nsl_print_session st5 id_init;
79 nsl_print_session st5 idresp;
80 IO.print_string "\n\n";
81 IO.print_string "##_Event_List_at the End of Protocol Execution\n\n";
82 print_events st5 nsl_print_event;
83 IO.print_string "\n\n";
84 IO.print_string "success\n";
85 finalize_state st5
86
87 let main =
88   let entropy = testrun Lib.RandomSequence.entropy0 in
89   ()
```

## D.7 OUTPUT OF APPLICATION.FST

```python
1 ## Tables After Calling Setup
2
3 trusted_keys [
4 {
5   address: 41406c6f63616c686f7374,
6   skey: 53cb277a99b5cb5e5415c70cba5253608e094fe241b30ab85b2d4c6a8f7eb12b,
7   pkey: 6d7c8fe400c016674e62d84fab09ce7fd61b83d32324bf2825fd337d9d71a301,
8 }
9 {
10  address: 42406c6f63616c686f7374,
11  skey: d9f3f877c463f5a73615880de60f73dfe46df8a6dccc088306f602b1255a0141,
12  pkey: fd91a8ca37dac95a1c17a766a4ee2461de2bb7f4da628cffe99e926eca380060,
13 }
14 ]
15
16 all_keys [
17 {
18   address: 41406c6f63616c686f7374,
19   pkey: 6d7c8fe400c016674e62d84fab09ce7fd61b83d32324bf2825fd337d9d71a301,
20   bool: ff,
21 }
22 {
23   address: 42406c6f63616c686f7374,
24   pkey: fd91a8ca37dac95a1c17a766a4ee2461de2bb7f4da628cffe99e926eca380060,
25   bool: ff,
26 }
27 ]
28
29
```
30 ## Sessions After init_send_msg_1

31

32 0.R1_initiator_send_msg_3: {

33 var_Na_3: 9bcae7aeb3fb1085,

34 var_addrA_1: 41406c6f63616c686f7374,

35 var_addrX_1: 42406c6f63616c686f7374,

36 var_pkX_4: fd91a8ca37dac95a1c17a766a4ee2461de2bb7f4da628cffe99e926eca380060,

37 var_skA_2: 53cb277a99b5cb5e5415c70cba5253608e094fe241b30ab85b2d4c6a8f7eb12b,

38 var_trustX_2: ff,

39 }

40

41

42 ## Protocol Message 1

43

44 ct: adf4368b100ff6675c80ee04ed4667c5c88f489b72a3ddd50402b3089eccbe250cf857

45 491f27ea9614bc0c5e326cb52f4f82703b6d5996df8643a75ada69bd7dcca06f43883,

46

47

48 ## Sessions After resp_send_msg_2

49

50 0.R1_initiator_send_msg_3: {

51 var_Na_3: 9bcae7aeb3fb1085,

52 var_addrA_1: 41406c6f63616c686f7374,

53 var_addrX_1: 42406c6f63616c686f7374,

54 var_pkX_4: fd91a8ca37dac95a1c17a766a4ee2461de2bb7f4da628cffe99e926eca380060,

55 var_skA_2: 53cb277a99b5cb5e5415c70cba5253608e094fe241b30ab85b2d4c6a8f7eb12b,

56 var_trustX_2: ff,

57 }

58 1.R1_responder_received msg_3: {

59 var_Na_4: 9bcae7aeb3fb1085,

60 var_Nb_2: 3ac19b9d052e94f5,

61 var_addrB_0: 42406c6f63616c686f7374,

62 var_addrY_0: 41406c6f63616c686f7374,

63 var_skB_0: d9f3f877c463f5a73615880de60f73dfe46df8a6dccc088306f602b1255a0141,

64 var_trustY_0: ff,

65 }

66

67

68 ## Protocol Message 2

69

70 ct: d83c39ad7d4701a4d2462f9423667a32d88d64c31b27d8e326f325c5d5f89f09b67676a8494a80

71 eaedf17e5741d01b619992fd27e0153980c6bad1f8277c43cb834c70391d0c697adde9f7a2acaf,

72

73

74 ## Sessions After init_send msg_3

75

76 0.R1_initiator_finished: {

77 var_Na_3: 9bcae7aeb3fb1085,

78 var_Nb_1: 3ac19b9d052e94f5,

79 var_addrA_1: 41406c6f63616c686f7374,

80 var_addrX_1: 42406c6f63616c686f7374,

81 var_trustX_2: ff,

82 }

83 1.R1_responder_received msg_3: {

84 var_Na_4: 9bcae7aeb3fb1085,

85 var_Nb_2: 3ac19b9d052e94f5,

86 var_addrB_0: 42406c6f63616c686f7374,

87 var_addrY_0: 41406c6f63616c686f7374,

88 var_skB_0: d9f3f877c463f5a73615880de60f73dfe46df8a6dccc088306f602b1255a0141,

89 var_trustY_0: ff,

90 }

91
92
93 ## Protocol Message 3
94
95 ct: 48730c365da9350e69da4230e91bfb12db40b444177ada11ecdf8ef64
96 93b985557bd1cd4b3e99e647e0d82be740ed11e0c6771ead7ab9d0560,
97
98
99 ## Sessions After resp_recv msg_3
100
101 0.R1_initiator_finished: {
102 var_Na_3: 9bcae7aeb3fb1085,
103 var_Nb_1: 3ac19b9d052e94f5,
104 var_addrA_1: 41406c6f63616c686f7374,
105 var_addrX_1: 42406c6f63616c686f7374,
106 var_trustX_2: ff,
107 }
108 1.session does not exist
109
110
111 ## Sessions After init_finished
112
113 0.session does not exist
114 1.session does not exist
115
116
117 ## Event List at the End of Protocol Execution
118
119 Events: [
120 beginB: { address: 41406c6f63616c686f7374,
121 address: 42406c6f63616c686f7374,
122 lbytes 8: 9bcae7aeb3fb1085,
123 lbytes 8: 3ac19b9d052e94f5,
124 }
125 beginA: { address: 41406c6f63616c686f7374,
126 address: 42406c6f63616c686f7374,
127 lbytes 8: 9bcae7aeb3fb1085,
128 lbytes 8: 3ac19b9d052e94f5,
129 }
130 endB: { address: 41406c6f63616c686f7374,
131 address: 42406c6f63616c686f7374,
132 lbytes 8: 9bcae7aeb3fb1085,
133 lbytes 8: 3ac19b9d052e94f5,
134 }
135 endA: { address: 41406c6f63616c686f7374,
136 address: 42406c6f63616c686f7374,
137 lbytes 8: 9bcae7aeb3fb1085,
138 lbytes 8: 3ac19b9d052e94f5,
139 }
140 ]
141
142 success
<figure><img src="image_42.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 combmons 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é.

# MOTS CLÉS

protocoles cryptographiques, sécurité prouvée, méthodes formelles, implémentations vérifiées

# 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 computational 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 requires 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 cryptographic 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 Public Key Encryption (HPKE), that has already been picked up for use in a privacy-enhancing extension of the TLS protocol (ECH), and in the Messaging 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 connects CryptoVerif to the large F* ecosystem, eventually allowing to formally guarantee cryptographic properties on verified, efficient low-level code.

# KEYWORDS

cryptographic protocols, provable security, formal methods, verified implementations