Benjamin Gregoire
Benjamin Gregoire
Inria Sophia-Antipolis
Adresse e-mail validée de
Citée par
Citée par
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
Advances in Cryptology–CRYPTO 2011: 31st Annual Cryptology Conference, Santa …, 2011
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
Certified Programs and Proofs: First International Conference, CPP 2011 …, 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
EasyCrypt: A Tutorial
G Barthe, F Dupressoir, B Grégoire, C Kunz, B Schmidt, PY Strub
Foundations of Security Analysis and Design VII: FOSAD 2012/2013 Tutorial …, 2014
Verified proofs of higher-order masking
G Barthe, S Belaïd, F Dupressoir, PA Fouque, B Grégoire, PY Strub
Advances in Cryptology--EUROCRYPT 2015: 34th Annual International Conference …, 2015
Proving equalities in a commutative ring done right in Coq
B Grégoire, A Mahboubi
Theorem Proving in Higher Order Logics: 18th International Conference …, 2005
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
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
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
Extending Coq with imperative features and its application to SAT verification.
M Armand, B Grégoire, A Spiwack, L Théry
ITP 6172, 83-98, 2010
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
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
Formal verification of a constant-time preserving C compiler
G Barthe, S Blazy, B Grégoire, R Hutin, V Laporte, D Pichardie, A Trieu
Cryptology ePrint Archive, 2019
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
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, ...
Formal Methods for Components and Objects: 5th International Symposium, FMCO …, 2007
Masking the GLP lattice-based signature scheme at any order
G Barthe, S Belaïd, T Espitau, PA Fouque, B Grégoire, M Rossi, ...
Advances in Cryptology–EUROCRYPT 2018: 37th Annual International Conference …, 2018
Le système ne peut pas réaliser cette opération maintenant. Veuillez réessayer plus tard.
Articles 1–20