[18] Gilles Barthe, Sunjay Cauligi, Benjamin Grégoire, Adrien Koutsos, Kevin Liao, Tiago Oliveira, Swarn Priya, Tamara Rezk, and Peter Schwabe. 2021. High-Assurance Cryptography in the Spectre Era. In *42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24-27 May 2021*. IEEE, 1884–1901. https://doi.org/10.1109/SP40001.2021.00046

[19] Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Benedikt Schmidt, and Santiago Zanella Béguelin. 2013. Fully automated analysis of padding-based encryption in the computational model. In *CCS’13*. ACM, 1247–1260. https://doi.org/10.1145/2508859.2516663

[20] Gilles Barthe, Marion Daubignard, Bruce M. Kapron, and Yassine Lakhnech. 2010. Computational indistinguishability logic. In *Proceedings of the 17th ACM Conference on Computer and Communications Security, CCS 2010, Chicago, Illinois, USA, October 4-8, 2010*, Ehab Al-Shaer, Angelos D. Keromytis, and Vitaly Shmatikov (Eds.). ACM, 375–386. https://doi.org/10.1145/1866307.1866350

[21] Gilles Barthe, François Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, and Pierre-Yves Strub. 2013. EasyCrypt: A Tutorial. In *Foundations of Security Analysis and Design VII - FOSAD 2012/2013 Tutorial Lectures (Lecture Notes in Computer Science, Vol. 8604)*. Springer, 146–166. https://doi.org/10.1007/978-3-319-10082-1_6

[22] Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, and Pierre-Yves Strub. 2015. Relational Reasoning via Probabilistic Coupling. In *LPAR-20*. 387–401. https://doi.org/10.1007/978-3-662-48899-7_27

[23] Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2016. A Program Logic for Union Bounds. In *43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy (LIPIcs, Vol. 55)*, Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 107:1–107:15. https://doi.org/10.4230/LIPIcs.ICALP.2016.107

[24] Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, and Santiago Zanella Béguelin. 2011. Computer-Aided Security Proofs for the Working Cryptographer. In *CRYPTO (Lecture Notes in Computer Science, Vol. 6841)*. Springer, 71–90. https://doi.org/10.1007/978-3-642-22792-9_5

[25] Gilles Barthe, Benjamin Grégoire, and Benedikt Schmidt. 2015. Automated Proofs of Pairing-Based Cryptography. In *CCS’15*. ACM, 1156–1168. https://doi.org/10.1145/2810103.2813697

[26] Gilles Barthe, Benjamin Grégoire, and Santiago Zanella-Béguelin. 2009. Formal certification of code-based cryptographic proofs. In *Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009*. 90–101. https://doi.org/10.1145/1480881.1480894

[27] David A. Basin, Andreas Lochbihler, and S. Reza Sefidgar. 2020. CryptHOL: Game-Based Proofs in Higher-Order Logic. *J. Cryptol*. 33, 2 (2020), 494–566. https://doi.org/10.1007/s00145-019-09341-z

[28] Andrej Bauer and Matija Pretnar. 2015. Programming with algebraic effects and handlers. *J. Log. Algebr. Meth. Program*. 84, 1 (2015), 108–123. https://doi.org/10.1016/j.jlamp.2014.02.001

[29] Mihir Bellare, Dennis Hofheinz, and Eike Kiltz. 2015. Subtleties in the Definition of IND-CCA: When and How Should Challenge Decryption Be Disallowed? *J. Cryptol*. 28, 1 (2015), 29–48. https://doi.org/10.1007/s00145-013-9167-4

[30] Mihir Bellare and Phillip Rogaway. 2006. The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs. In *Advances in Cryptology - EUROCRYPT 2006, 25th Annual International Conference on the Theory and Applications of Cryptographic Techniques, St. Petersburg, Russia, May 28 - June 1, 2006, Proceedings (Lecture Notes in Computer Science, Vol. 4004)*, Serge Vaudenay (Ed.). Springer, 409–426. https://doi.org/10.1007/11761679_25

[31] Lennart Beringer, Adam Petcher, Katherine Q. Ye, and Andrew W. Appel. 2015. Verified Correctness and Security of OpenSSL HMAC. In *24th USENIX Security Symposium. USENIX Association, 207–221*. https://www.usenix.org/conference/usenixsecurity15/technical-sessions/presentation/beringer

[32] Daniel J. Bernstein. 2009. Cryptography in NaCl. https://cr.yp.to/highspeed/naclcrypto-20090310.pdf

[33] Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jianyang Pan, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella Béguelin, and Jean Karim Zinzindohoue. 2017. Implementing and Proving the TLS 1.3 Record Layer. *IEEE S&P* (2017).

[34] Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, and Santiago Zanella Béguelin. 2014. Proving the TLS Handshake Secure (As It Is). In *CRYPTO’14 (Lecture Notes in Computer Science, Vol. 8617)*. Springer, 235–255. https://doi.org/10.1007/978-3-662-44381-1_14

[35] Bruno Blanchet. 2006. A Computationally Sound Mechanized Prover for Security Protocols. In *IEEE S&P. IEEE Computer Society, 140–154*. https://doi.org/10.1109/SP.2006.1

[36] Ioana Boureanu, Constantin Catalin Dragan, François Dupressoir, David Gérault, and Pascal Lafourcade. 2021. Mechanised Models and Proofs for Distance-Bounding. In *34th IEEE Computer Security Foundations Symposium, CSF 2021, Dubrovnik, Croatia, June 21-25, 2021*. IEEE, 1–16. https://doi.org/10.1109/CSF51468.2021.00049

[37] Anne Broadbent and Martti Karvonen. 2022. Categorical composable cryptography. In *25th International Conference on Foundations of Software Science and Computation Structures, FOSSACS (Lecture Notes in Computer Science, Vol. 13242)*,
Patricia Bouyer and Lutz Schröder (Eds.). Springer, 161-183. https://doi.org/10.1007/978-3-030-99253-8_9

[38] Chris Brzuska, Eric Cornelissen, and Konrad Kohbrok. 2022. Security Analysis of the MLS Key Derivation. In *43rd IEEE Symposium on Security and Privacy, SP 2022, San Francisco, CA, USA, May 22-26, 2022*. IEEE, 2535-2553. https://doi.org/10.1109/SP46214.2022.9833678

[39] Chris Brzuska, Antoine Delignat-Lavaud, Christoph Egger, Cédric Fournet, Konrad Kohbrok, and Markulf Kohlweiss. 2021. Key-schedule Security for the TLS 1.3 Standard. Cryptology ePrint Archive, Paper 2021/467; to appear at Asiacrypt 2022. https://eprint.iacr.org/2021/467

[40] Chris Brzuska, Antoine Delignat-Lavaud, Cédric Fournet, Konrad Kohbrok, and Markulf Kohlweiss. 2018. State Separation for Code-Based Game-Playing Proofs. In *ASIACRYPT*. Springer International Publishing, Cham, 222-249. https://eprint.iacr.org/2018/306

[41] Chris Brzuska and Sabine Oechsner. 2021. A State-Separating Proof for Yao's Garbling Scheme. Cryptology ePrint Archive, Paper 2021/1453; To appear at CSF'2023. https://eprint.iacr.org/2021/1453

[42] D. Butler, A. Lochbihler, D. Aspinall, and A. Gascón. 2021. Formalising Σ-Protocols and Commitment Schemes Using CryptHOL. 65, 4 (2021), 521-567. https://doi.org/10.1007/s10817-020-09581-w

[43] Ran Canetti. 2020. Universally Composable Security. J. ACM 67, 5 (2020), 28:1-28:94. https://doi.org/10.1145/3402457

[44] Ran Canetti, Assaf Kfoury, Alley Stoughton, Mayank Varia, Gollamudi Tarakaram, and Tomislav Petrovic. 2021. UC Domain Specific Language. unpublished. https://github.com/easyuc/EasyUC/tree/master/uc-dsl

[45] Ran Canetti, Alley Stoughton, and Mayank Varia. 2019. EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security. In *CSF*. IEEE, 167-183.

[46] Bob Coecke, Tobias Fritz, and Robert W. Spekkens. 2016. A mathematical theory of resources. Inf. Comput. 250 (2016), 59-86. https://doi.org/10.1016/j.ic.2016.02.008

[47] Pierre Corbineau, Mathilde Duclos, and Yassine Lakhnech. 2011. Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience. In *Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings (Lecture Notes in Computer Science, Vol. 7086)*, Jean-Pierre Jouannaud and Zhong Shao (Eds.). Springer, 378-393. https://doi.org/10.1007/978-3-642-25379-9_27

[48] Ronald Cramer and Victor Shoup. 2003. Design and Analysis of Practical Public-Key Encryption Schemes Secure against Adaptive Chosen Ciphertext Attack. SIAM J. Comput. 33, 1 (2003), 167-226. https://doi.org/10.1137/S0097539702403773

[49] Lukasz Czajka and Cezary Kaliszyk. 2018. Hammer for Coq: Automation for Dependent Type Theory. J. Autom. Reason. 61, 1-4 (2018), 423-453. https://doi.org/10.1007/s10817-018-9458-4

[50] Ivan Damgaard. 2011. On Sigma-Protocols. lecture notes, Aarhus University. https://cs.au.dk/~ivan/Sigma.pdf

[51] Constantin Catalin Dragan, François Dupressoir, Ehsan Estaji, Kristian Gjøsteen, Thomas Haines, Peter Y. A. Ryan, Peter B. Rønne, and Morten Rotvold Solberg. 2022. Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co. In *35th IEEE Computer Security Foundations Symposium, CSF 2022, Haifa, Israel, August 7-10, 2022*. IEEE, 335-347. https://doi.org/10.1109/CSF54842.2022.9919663

[52] François Dupressoir, Konrad Kohbrok, and Sabine Oechsner. 2022. Bringing State-Separating Proofs to EasyCrypt - A Security Proof for Cryptobox. In *To appear in 35th IEEE Computer Security Foundations Symposium*. IEEE. https://eprint.iacr.org/2021/326

[53] A. Erbsen, J. Philipoom, J. Gross, R. Sloan, and A. Chlipala. 2019. Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises. In *IEEE S&P*. https://doi.org/10.1109/SP.2019.000005

[54] Denis Firsov and Dominique Unruh. 2022. Zero-Knowledge in EasyCrypt. Cryptology ePrint Archive, Paper 2022/926. https://eprint.iacr.org/2022/926 https://eprint.iacr.org/2022/926.

[55] Cédric Fournet, Markulf Kohlweiss, and Pierre-Yves Strub. 2011. Modular code-based cryptographic verification. In *Proceedings of the 18th ACM Conference on Computer and Communications Security*, Yan Chen, George Danezis, and Vitaly Shmatikov (Eds.). ACM, 341-350. https://doi.org/10.1145/2046707.2046746

[56] Joshua Gancher, Kristina Sojakova, Xiong Fan, Elaine Shi, and Greg Morrisett. 2023. A Core Calculus for Equational Proofs of Cryptographic Protocols. To appear at POPL 2023. https://github.com/ipdl/submission/raw/main/main.pdf

[57] Jeremy Gibbons and Ralf Hinze. 2011. Just do it: simple monadic equational reasoning. In *Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011*. 2-14. https://doi.org/10.1145/2034773.2034777

[58] Michèle Giry. 1982. A categorical approach to probability theory. In *Categorical Aspects of Topology and Analysis*, B. Banaschewski (Ed.). Springer, 68-85. https://www.chrisstucchio.com/blog_media/2016/probability_the-monad/categoricalProbability_giry.pdf
[59] Shai Halevi. 2005. A plausible approach to computer-aided cryptographic proofs. *IACR Cryptol. ePrint Arch.* (2005), 181. http://eprint.iacr.org/2005/181

[60] Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Catalin Hritcu, and Bas Spitters. 2023. The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography. *Cryptology ePrint* Archive, Paper 2023/185. https://eprint.iacr.org/2023/185 https://eprint.iacr.org/2023/185.

[61] Carmit Hazay and Yehuda Lindell. 2010. *Efficient Secure Two-Party Protocols - Techniques and Constructions*. Springer. https://doi.org/10.1007/978-3-642-14303-8

[62] Shin-ya Katsumata and Tetsuya Sato. 2013. Preorders on Monads and Coalgebraic Simulations. In *Foundations of Software Science and Computation Structures - 16th International Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings*. 145–160. https://doi.org/10.1007/978-3-642-37075-5_10

[63] G M Kelly. 1982. *Basic Concepts of Enriched Category Theory*. 143 pages. Reprint of the 1982 original [Cambridge Univ. Press, Cambridge; MR0651714].

[64] Konrad Kohbrok, Markulf Kohlweiss, Tahina Ramananandro, and Nikhil Swamy. 2020. Relational F\* for State Separating Cryptographic Proofs. F\* wiki article. https://github.com/FStarLang/FStar/wiki/Relational-F\*-for-State-Separating-Cryptographic-Proofs

[65] Sheng Liang, Paul Hudak, and Mark P. Jones. 1995. Monad Transformers and Modular Interpreters. In *Conference Record of POPL '95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, January 23-25, 1995*, Ron K. Cytron and Peter Lee (Eds.). ACM Press, 333–343. https://doi.org/10.1145/199448.199528

[66] Kevin Liao, Matthew A. Hammer, and Andrew Miller. 2019. ILC: a calculus for composable, computational cryptography. In *PLDI*. ACM, 640–654.

[67] Andreas Lochbihler, S. Reza Sefidgar, David A. Basin, and Ueli Maurer. 2019. Formalizing Constructive Cryptography using CryptHOL. In *CSF. IEEE, 152–166*. https://doi.org/10.1109/CSF.2019.00018

[68] Saunders Mac Lane. 1978. *Categories for the Working Mathematician* (2 ed.). Graduate Texts in Mathematics, Vol. 5. Springer, New York, NY.

[69] Assia Mahboubi and Enrico Tassi. 2021. Mathematical components. Online book. https://math-comp.github.io/mcb/

[70] Kenji Maillard, Câtălin Hrițcu, Exequiel Rivas, and Antoine Van Muylder. 2020. The next 700 relational program logics. *Proc. ACM Program. Lang.* 4, POPL (2020), 4:1–4:33. https://doi.org/10.1145/3371072

[71] Ueli Maurer. 2011. Constructive Cryptography - A New Paradigm for Security Definitions and Proofs. In *Theory of Security and Applications - Joint Workshop, TOSCA'11 (Lecture Notes in Computer Science, Vol. 6993)*. Springer, 33–56. https://doi.org/10.1007/978-3-642-27375-9_3

[72] Ueli Maurer and Renato Renner. 2011. Abstract Cryptography. In *Innovations in Computer Science - ICS'11*. Tsinghua University Press, 1–21. http://conference.iiis.tsinghua.edu.cn/ICS2011/content/papers/14.html

[73] Roberto Metere and Changyu Dong. 2017. Automated Cryptographic Analysis of the Pedersen Commitment Scheme. In *Computer Network Security*, Jacek Rak, John Bay, Igor Kotenko, Leonard Popyack, Victor Skormin, and Krzysztof Szczypiorski (Eds.). Springer, 275–287.

[74] Robin Milner, Joachim Parrow, and David Walker. 1992. A Calculus of Mobile Processes, I. *Inf. Comput.* 100, 1 (1992), 1–40. https://doi.org/10.1016/0890-5401(92)90008-4

[75] Robin Milner, Mads Tofte, and Robert Harper. 1990. *The Definition of Standard ML*. MIT Press.

[76] Eugenio Moggi. 1989. Computational Lambda-Calculus and Monads. In *Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89)*, Pacific Grove, California, USA, June 5-8, 1989. IEEE Computer Society, 14–23. https://doi.org/10.1109/LICS.1989.39155

[77] Christine Paulin-Mohring, David Baelde, and Pierre Courtieu. 2009. ALEA Coq Library. https://github.com/coq-community/alea

[78] Adam Petcher and Greg Morrisett. 2015. The Foundational Cryptography Framework. In *Principles of Security and Trust - 4th International Conference, POST 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings (Lecture Notes in Computer Science, Vol. 9036)*, Riccardo Focardi and Andrew C. Myers (Eds.). Springer, 53–72. https://doi.org/10.1007/978-3-662-46666-7_4

[79] Gordon D. Plotkin and John Power. 2003. Algebraic Operations and Generic Effects. *Applied Categorical Structures* 11, 1 (2003), 69–94. https://doi.org/10.1023/A:1023064908962

[80] Gordon D. Plotkin and John Power. 2003. Algebraic Operations and Generic Effects. *Appl. Categorical Struct.* 11, 1 (2003), 69–94. https://doi.org/10.1023/A:1023064908962

[81] Gordon D. Plotkin and Matija Pretnar. 2009. Handlers of Algebraic Effects. In *Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings (Lecture Notes in Computer Science, Vol. 5502)*,
Giuseppe Castagna (Ed.). Springer, 80-94. https://doi.org/10.1007/978-3-642-00590-9_7

[82] Christoph Rauch, Sergey Goncharov, and Lutz Schröder. 2016. Generic Hoare Logic for Order-Enriched Effects with Exceptions. In *Recent Trends in Algebraic Development Techniques - 23rd IFIP WG 1.3 International Workshop, WADT 2016, Gregynog, UK, September 21-24, 2016, Revised Selected Papers*. 208-222. https://doi.org/10.1007/978-3-319-72044-9_14

[83] Eric Rescorla. 2018. The Transport Layer Security (TLS) Protocol Version 1.3. IETF RFC 5246. https://tools.ietf.org/html/rfc8446

[84] Phillip Rogaway and Yusi Zhang. 2018. Simplifying Game-Based Definitions - Indistinguishability up to Correctness and Its Application to Stateful AE. In *Advances in Cryptology - CRYPTO 2018 - 38th Annual International Cryptology Conference, Santa Barbara, CA, USA, August 19-23, 2018, Proceedings, Part II (Lecture Notes in Computer Science, Vol. 10992)*, Hovav Shacham and Alexandra Boldyreva (Eds.). Springer, 3-32. https://doi.org/10.1007/978-3-319-96881-0_1

[85] Andreas Rossberg, Claudio V. Russo, and Derek Dreyer. 2014. F-ing modules. *J. Funct. Program*. 24, 5 (2014), 529-607. https://doi.org/10.1017/S0956796814000264

[86] Mike Rosulek. 2021. The Joy of Cryptography. Online textbook. http://web engr oregonstate.edu/~rosulekm/ crypto/

[87] Claus Schnorr. 1991. Efficient signature generation by smart cards. *Journal of Cryptology* 4 (01 1991), 161-174. https://doi.org/10.1007/BF00196725

[88] Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, and Swarn Priya. 2022. Enforcing Fine-grained Constant-time Policies. In *Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, CCS 2022, Los Angeles, CA, USA, November 7-11, 2022*, Heng Yin, Angelos Stavrou, Cas Cremers, and Elaine Shi (Eds.). ACM, 83-96. https://doi.org/10.1145/3548606.3560689

[89] Victor Shoup. 2004. Sequences of games: a tool for taming complexity in security proofs. *IACR Cryptol. ePrint Arch*. (2004), 332. http://eprint.iacr.org/2004/332

[90] Nikolaj Sidorenco, Sabine Oechsner, and Bas Spitters. 2021. Formal security analysis of MPC-in-the-head zero-knowledge protocols. In *2021 IEEE 34th Computer Security Foundations Symposium (CSF)*. 1-14. https://doi.org/10.1109/CSF51468.2021.00050

[91] Nikolaj Sidorenco and Bas Spitters. 2022. A formal security analysis of Blockchain voting. preprint. https://www.cs.au.dk/~spitters/ovn.pdf

[92] Jonathan Sterling and Robert Harper. 2021. Logical relations as types: Proof-relevant parametricity for program modules. *Journal of the ACM (JACM)* 68, 6 (2021), 1-47.

[93] Alley Stoughton, François Dupressoir, Pierre-Yves Strub, César Kunz, Juan Manuel Crespo, Benjamin Grégoire, Gilles Barthe, and Benedikt Schmidt. 2018. *EasyCrypt Reference Manual*. Technical Report. 206 pages.

[94] Pierre-Yves Strub. 2020. XHL. https://github.com/strub/xhl

[95] Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoué, and Santiago Zanella-Béguélin. 2016. Dependent Types and Multi-Monadic Effects in F*. In *43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)*. ACM, 256-270. https://www.fstar-lang.org/papers/mumon/

[96] Christian Urban. 2008. Nominal Techniques in Isabelle/HOL. *J. Autom. Reason*. 40, 4 (2008), 327-356. https://doi.org/10.1007/s10817-008-9097-2

[97] Philip Wadler. 1990. Comprehending Monads. In *LFP'90 (Nice, France). ACM, New York, NY, USA, 61-78*. https://doi.org/10.1145/91556.91592

[98] Katherine Q. Ye, Matthew Green, Naphat Sanguansin, Lennart Beringer, Adam Petcher, and Andrew W. Appel. 2017. Verified Correctness and Security of mbedTLS HMAC-DRBG. In *CCS'17. ACM, 2007-2020*. https://doi.org/10.1145/3133956.3133974