By Professor Manuel Barbosa
On 20 October at 2:30 pm, in FC6 0.28, Manuel Barbosa will give a lecture entitled "The Formosa Crypto Approach to Formally Verified Cryptography".
Title:
The Formosa Crypto Approach to Formally Verified Cryptography
Abstract:
In this talk I will present EasyCrypt and Jasmin, and how they are used to formally verify high-speed cryptographic implementations and relate their security to that of high-level provably secure specifications.
As use cases I will use the NIST postquantum standards.
Ongoing and future work on these Formosa Crypto tools will also be briefly discussed.
Bio:
Manuel Barbosa is a lecturer at the Department of Computer Science in the Faculty of Sciences of the University of Porto (DCC-FCUP) and a researcher at INESC TEC. His research interests lie in Cryptography, Information Security, and Formal Verification. He holds a Ph.D. in Electrical and Electronic Engineering from Newcastle University, an M.Sc. from the same University, and a degree in Electrical and Computer Engineering from the Faculty of Engineering of the University of Porto. In the past, he has been a visiting researcher at the University of Bristol, École Normale Supérieure, Inria Sophia-Antipolis, and Bar-Ilan University. Between 2023 and 2025, he was a research fellow at the Max Planck Institute for Security and Privacy. He has been working on the development of high-assurance cryptographic implementations for more than 15 years, bridging the gap between theoretical security and real-world security. His main interests include provable security and its interplay with the formal verification of cryptographic proofs and software implementations. He is also a member of the steering committee of Formosa Crypto (formosa-crypto.org), where the EasyCrypt and Jasmin formal verification frameworks are developed and promoted.