Benjamin Gregoire
Benjamin Gregoire
Inria Sophia-Antipolis
Adresse e-mail validée de inria.fr
Titre
Citée par
Citée par
Année
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
3612009
Computer-aided security proofs for the working cryptographer
G Barthe, B Grégoire, S Heraud, SZ Béguelin
Annual Cryptology Conference, 71-90, 2011
2852011
A compiled implementation of strong reduction
B Grégoire, X Leroy
Proceedings of the seventh ACM SIGPLAN international conference on …, 2002
2372002
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
1952011
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
1432016
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
1402013
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
1382005
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
1362015
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
1052014
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
1032017
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
942010
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
822017
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
782013
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
702016
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
672018
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
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
602004
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
542011
Full reduction at full throttle
M Boespflug, M Dénès, B Grégoire
International Conference on Certified Programs and Proofs, 362-377, 2011
502011
Advanced probabilistic couplings for differential privacy
G Barthe, N Fong, M Gaboardi, B Grégoire, J Hsu, PY Strub
Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications …, 2016
492016
Le système ne peut pas réaliser cette opération maintenant. Veuillez réessayer plus tard.
Articles 1–20