Email: miguelquaresma DOT w AT gmail DOT com Full CV: PDF (07/2025)
LinkedIn | Google Scholar | GitHub

I am a Security and Cryptography Researcher and Engineer at Least Authority, performing security audits of cryptographic and distributed applications, from design to implementation.

I am also a Doctoral Candidate at the Max-Planck Institute for Security and Privacy jointly supervised by Gilles Barthe and Peter Schwabe. My research focuses on high-performance, high-assurance post-quantum cryptographic implementations.

Previously I worked at Goldman Sachs as a Cybersecurity Analyst.

Between 2015 and 2020 I completed my BSc and MSc degrees in Computer Engineering at the University of Minho, where I specialized in Cryptography, Information Security, Parallel and Distributed Computing. I wrote my Master’s thesis at the High-Assurance Software Laboratory (HASLab) as part of the REASSURE project.

     Thesis: TrustZone based Attestation in Secure Runtime Verification for Embedded Systems [PDF]

During my studies I completed two internships as a Software Engineer at Closer Consulting in 2018 and as a Security Engineer at Aptoide in 2019.

Publications

• Jazzline: Composable CryptoLine functional correctness proofs for Jasmin programs
  ACM CCS 2025
  [code]

• Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt
  CRYPTO 2024
  [code] [paper] [talk]

• Swoosh: Efficient Lattice-Based Non-Interactive Key Exchange
  USENIX Security 2024
  [code] [paper] [talk - RWC] [talk - Usenix Security 24]

• Formally verifying Kyber Episode IV: Implementation Correctness
  TCHES 2023
  [code] [paper] [talk]

GPG Key: 0175 939D F826 0A21 67CA 77C3 02AB 8675 9274 E038

Other

I am a competitive endurance athlete focused on ultra trail running. Here are some of my best times on the road:

• 5K: 18:16 (2024)
• 10K: 37:43 (2024)