During his PhD studies, Lasse Letager Hansen researched how to build provably secure and correct software. Bugs and oversights in code can be very costly and even threaten the security of banks, computers, and elections. Lasse Letager Hansen studied how to prove security and correctness in Rocq of efficient and realistic software written in Rust.

The frameworks developed were tested on the Advanced Encryption Standard (AES), the Transport Layer Security (TLS) protocol, and a voting smart contract.

The PhD study was completed at Department of Computer Science, Faculty of Natural Sciences, Aarhus University.

This summary was prepared by the PhD student.

Time: Monday 17 November 2025
Place: Department of Computer Science, Aarhus University, Åbogade 34, 8200 Aarhus N
Title of PhD thesis: High Assurance Cryptographic Software using Rust and Rocq
Contact information: Lasse Letager Hansen, e-mail: letager@cs.au.dk , tel.: +45 60 46 45 94
Members of the assessment committee:
Senior Principal Researcher Nik Swamy, Microsoft Research Lab, Redmond, Washington, USA
Professor Carsten Schürmann, Center for Information Security and Trust, IT University of Copenhagen, Denmark
Associate Professor Amin Timany (chair), Department of Computer Science, Aarhus University, Denmark
Main supervisor: Associate professor Bas Spitters, Department of Computer Science, Aarhus University, Denmark
Language: The PhD dissertation will be defended in Englis

 

The defence is public.
The PhD thesis is available for reading at the Graduate School of Natural Sciences/GSNS, Ny Munkegade 120, building 1521, 8000 Aarhus C.