Benjamin Gregoire
Benjamin Gregoire
Inria Sophia-Antipolis
Verified email at
Cited by
Cited by
Formal certification of code-based cryptographic proofs
G Barthe, B Grégoire, S Zanella Béguelin
Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2009
Computer-aided security proofs for the working cryptographer
G Barthe, B Grégoire, S Heraud, SZ Béguelin
Annual Cryptology Conference, 71-90, 2011
Strong non-interference and type-directed higher-order masking
G Barthe, S Belaïd, F Dupressoir, PA Fouque, B Grégoire, PY Strub, ...
Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications …, 2016
A compiled implementation of strong reduction
B Grégoire, X Leroy
Proceedings of the seventh ACM SIGPLAN international conference on …, 2002
A modular integration of SAT/SMT solvers to Coq through proof witnesses
M Armand, G Faure, B Grégoire, C Keller, L Théry, B Werner
International Conference on Certified Programs and Proofs, 135-150, 2011
Easycrypt: A tutorial
G Barthe, F Dupressoir, B Grégoire, C Kunz, B Schmidt, PY Strub
International School on Foundations of Security Analysis and Design, 146-166, 2012
Verified proofs of higher-order masking
G Barthe, S Belaïd, F Dupressoir, PA Fouque, B Grégoire, PY Strub
Annual International Conference on the Theory and Applications of …, 2015
Jasmin: High-assurance and high-speed cryptography
JB Almeida, M Barbosa, G Barthe, A Blot, B Grégoire, V Laporte, ...
Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications …, 2017
Parallel implementations of masking schemes and the bounded moment leakage model
G Barthe, F Dupressoir, S Faust, B Grégoire, FX Standaert, PY Strub
Advances in Cryptology–EUROCRYPT 2017: 36th Annual International Conference …, 2017
Proving equalities in a commutative ring done right in Coq
B Grégoire, A Mahboubi
International Conference on Theorem Proving in Higher Order Logics, 98-113, 2005
Probabilistic relational verification for cryptographic implementations
G Barthe, C Fournet, B Grégoire, PY Strub, N Swamy, S Zanella-Béguelin
ACM SIGPLAN Notices 49 (1), 193-205, 2014
Secure compilation of side-channel countermeasures: the case of cryptographic “constant-time”
G Barthe, B Grégoire, V Laporte
2018 IEEE 31st Computer Security Foundations Symposium (CSF), 328-343, 2018
Formal verification of a constant-time preserving C compiler
G Barthe, S Blazy, B Grégoire, R Hutin, V Laporte, D Pichardie, A Trieu
Proceedings of the ACM on Programming Languages 4 (POPL), 1-30, 2019
Proving differential privacy via probabilistic couplings
G Barthe, M Gaboardi, B Grégoire, J Hsu, PY Strub
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer …, 2016
Hardware private circuits: From trivial composition to full verification
G Cassiers, B Grégoire, I Levi, FX Standaert
IEEE Transactions on Computers 70 (10), 1677-1690, 2020
Verified computational differential privacy with applications to smart metering
G Barthe, G Danezis, B Grégoire, C Kunz, S Zanella-Beguelin
2013 IEEE 26th Computer Security Foundations Symposium, 287-301, 2013
maskverif: Automated verification of higher-order masking in presence of physical defaults
G Barthe, S Belaïd, G Cassiers, PA Fouque, B Grégoire, FX Standaert
Computer Security–ESORICS 2019: 24th European Symposium on Research in …, 2019
Extending Coq with Imperative Features and Its Application to SAT Verification
M Armand, B Grégoire, A Spiwack, L Théry
International Conference on Interactive Theorem Proving, 83-98, 2010
FaCT: a DSL for timing-sensitive computation
S Cauligi, G Soeller, B Johannesmeyer, F Brown, RS Wahby, J Renner, ...
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language …, 2019
The last mile: High-assurance and high-speed cryptographic implementations
JB Almeida, M Barbosa, G Barthe, B Grégoire, A Koutsos, V Laporte, ...
2020 IEEE Symposium on Security and Privacy (SP), 965-982, 2020
The system can't perform the operation now. Try again later.
Articles 1–20