Benjamin Gregoire
Benjamin Gregoire
Inria Sophia-Antipolis
Verified email at inria.fr
Title
Cited by
Cited by
Year
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
3412009
Computer-aided security proofs for the working cryptographer
G Barthe, B Grégoire, S Heraud, SZ Béguelin
Annual Cryptology Conference, 71-90, 2011
2712011
A compiled implementation of strong reduction
B Grégoire, X Leroy
Proceedings of the seventh ACM SIGPLAN international conference on …, 2002
2262002
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
1742011
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
1352005
EasyCrypt: A Tutorial
G Barthe, F Dupressoir, B Grégoire, C Kunz, B Schmidt, PY Strub
Foundations of security analysis and design vii, 146-166, 2013
1232013
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
1212015
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
1182016
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
992014
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
892010
Parallel implementations of masking schemes and the bounded moment leakage model
G Barthe, F Dupressoir, S Faust, B Grégoire, FX Standaert, PY Strub
Annual International Conference on the Theory and Applications of …, 2017
842017
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
722013
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
712017
JACK—a tool for validation of security and behaviour of Java applications
G Barthe, L Burdy, J Charles, B Grégoire, M Huisman, JL Lanet, ...
International Symposium on Formal Methods for Components and Objects, 152-174, 2006
632006
Proving differential privacy via probabilistic couplings
G Barthe, M Gaboardi, B Grégoire, J Hsu, PY Strub
2016 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1-10, 2016
592016
A structured approach to proving compiler optimizations based on dataflow analysis
Y Bertot, B Grégoire, X Leroy
International Workshop on Types for Proofs and Programs, 66-81, 2004
582004
Beyond provable security verifiable IND-CCA security of OAEP
G Barthe, B Grégoire, Y Lakhnech, SZ Béguelin
Cryptographers’ Track at the RSA Conference, 180-196, 2011
512011
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
482018
Fully automated analysis of padding-based encryption in the computational model
G Barthe, JM Crespo, B Grégoire, C Kunz, Y Lakhnech, B Schmidt, ...
Proceedings of the 2013 ACM SIGSAC conference on Computer & communications …, 2013
472013
Full reduction at full throttle
M Boespflug, M Dénès, B Grégoire
International Conference on Certified Programs and Proofs, 362-377, 2011
462011
The system can't perform the operation now. Try again later.
Articles 1–20