I am a researcher in the
SPLiTS team at Sophia Antipolis.
My research focuses on compilers, formal methods, and the certification of cryptographic algorithms and implementations,
with a strong emphasis on proof assistants.
I am deeply involved in the
Formosa Crypto project, as well as
in the development of the
Jasmin programming language
and the
EasyCrypt proof assistant.
Publications
News
- Distinguished Paper Award for our paper
"Jazzline: Composable CryptoLine Functional Correctness Proofs for Jasmin Programs" at CCS 2025
- Distinguished Paper Award for our paper
"Typing High-Speed Cryptography against Spectre v1" at S&P 2023
- Distinguished Paper Award for our paper
"Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic "Constant-Time" at CSF 2018
- Best Paper Award for our paper
"Computer-Aided Security Proofs for the Working Cryptographer" at CRYPTO 2011
Activities
Recent Program committees
Jury
Current Projects
- ANR Higher-Order Probabilistic and resource-aware Reasoning HOPR (2024–2028)
- PEPR Cybersecurity Security Verification Protocol SVP (2022-2028)
Students
Current Students
Former Students
- Swarn Priya
- Mohamad El Laz
- Cécile Baritel-Ruet
- Sylvain Heraud
- Jorge-Luis Sacchini
- Santiago Zanella Béguelin
- César Kunz
Contact
| E-mail: |
Benjamin.Gregoire@sophia.inria.fr |
| Snail mail: | Projet Marelle, INRIA Sophia Antipolis, |
| 2004 route des Lucioles, B.P. 93, |
| 06902 Sophia Antipolis Cedex |
| Phone: | 04 92 38 75 59 (from France),
+33 4 92 38 75 59 (from abroad) |
| Fax: | 04 92 38 50 29 (from France),
+33 4 92 38 50 29 (from abroad) |
