Skip to Main content Skip to Navigation


...
hal-01410216v1  Conference papers
Gilles BartheSonia BelaïdFrançois DupressoirPierre-Alain FouqueBenjamin Grégoire et al.  Strong Non-Interference and Type-Directed Higher-Order Masking
CCS 2016 - 23rd ACM Conference on Computer and Communications Security, Oct 2016, Vienne, Austria. pp.116 - 129, ⟨10.1145/2976749.2978427⟩
...
hal-01959322v1  Journal articles
Gilles BartheThomas EspitauBenjamin GrégoireJustin HsuPierre-Yves Strub. Proving expected sensitivity of probabilistic programs
Proceedings of the ACM on Programming Languages, ACM, 2017, 2 (POPL), pp.1-29. ⟨10.1145/3158145⟩
hal-02470965v1  Conference papers
Gilles BartheSonia BelaïdGaëtan CassiersPierre-Alain FouqueBenjamin Grégoire et al.  MaskVerif: Automated Verification of Higher-Order Masking in Presence of Physical Defaults.
ESORICS 2019 The European Symposium on Research in Computer Security, Sep 2019, Luxembourg, Luxembourg. pp.300-318
hal-02975012v1  Journal articles
Gilles BartheSandrine BlazyBenjamin GrégoireRémi HutinVincent Laporte et al.  Formal verification of a constant-time preserving C compiler
Proceedings of the ACM on Programming Languages, ACM, 2020, 4 (POPL), pp.1-30. ⟨10.1145/3371075⟩
hal-01112084v1  Conference papers
Gilles BartheBenjamin GrégoireYassine LakhnechSantiago Zanella-Béguelin. Beyond Provable Security Verifiable IND-CCA Security of OAEP
Topics in Cryptology - 2011 - The Cryptographers' Track at the Conference 2011, San Francisco, CA, USA, February 14-18, 2011. Proceedings, 2011, San Francisco, United States. ⟨10.1007/978-3-642-19074-2_13⟩
...
hal-00765883v1  Conference papers
Michael BackesGilles BartheMatthias BergBenjamin GrégoireCesar Kunz et al.  Verified Security of Merkle-Damgaard
25th IEEE Computer Security Foundations Symposium, CSF 2012, Jun 2012, Cambridge, MA, United States. pp.354-368, ⟨10.1109/CSF.2012.14⟩
...
hal-00639130v1  Conference papers
Michaël ArmandGermain FaureBenjamin GrégoireChantal KellerLaurent Théry et al.  A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
CPP - Certified Programs and Proofs - First International Conference - 2011, Dec 2011, Kenting, Taiwan. pp.135-150, ⟨10.1007/978-3-642-25379-9_12⟩
...
hal-00537104v1  Conference papers
Benjamin GrégoireJorge Sacchini. On Strong Normalization of the Calculus of Constructions with Type-Based Termination
17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Oct 2010, Yogyakarta, Indonesia. pp.333-347, ⟨10.1007/978-3-642-16242-8_24⟩
hal-01112767v1  Book sections
Benjamin GrégoireLoïc PottierLaurent Théry. Proof Certificates for Algebra and their Application to Automatic Geometry Theorem Proving
Thomas Sturm; Christoph Zengler. Automated Deduction in Geometry, 6301, Springer, pp.42-59, 2011, Lecture Notes in Computer Science, 978-3-642-21045-7. ⟨10.1007/978-3-642-21046-4_3⟩
...
hal-02404755v1  Conference papers
Sunjay CauligiGary SoellerBrian JohannesmeyerFraser BrownRiad Wahby et al.  FaCT: A DSL for Timing-Sensitive Computation
PLDI 2019 - 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, Jun 2019, Phoenix, United States. ⟨10.1145/3314221.3314605⟩
...
hal-00765874v1  Conference papers
Gilles BartheBenjamin GrégoireSylvain HeraudFederico OlmedoSantiago Zanella-Béguelin. Verified Indifferentiable Hashing into Elliptic Curves
Principles of Security and Trust - First International Conference, POST 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Mar 2012, Tallinn, Estonia. pp.209-228, ⟨10.1007/978-3-642-28641-4_12⟩
hal-01112075v1  Conference papers
Gilles BartheBenjamin GrégoireSantiago Zanella-BéguelinSylvain Heraud. Computer-Aided Security Proofs for the Working Cryptographer
Advances in Cryptology - 2011 - 31st Annual Cryptology Conference, 2011, Santa Barbara, United States. ⟨10.1007/978-3-642-22792-9_5⟩
hal-01246713v1  Conference papers
Gilles BartheBenjamin GrégoireBenedikt Schmidt. Automated Proofs of Pairing-Based Cryptography
Proceedings of the 22nd Conference on Computer and Communications Security, Oct 2015, Denver, United States. ⟨10.1145/2810103.2813697⟩
...
hal-00765864v1  Conference papers
Gilles BartheBenjamin GrégoireSantiago Zanella-Béguelin. Probabilistic relational Hoare logics for computer-aided security proofs
Mathematics of Program Construction - 11th International Conference, MPC 2012, Jun 2012, Madrid, Spain. pp.1-6, ⟨10.1007/978-3-642-31113-0_1⟩
...
hal-00765869v1  Conference papers
Gilles BartheBenjamin GrégoireSantiago Zanella-Béguelin. Computer-Aided Cryptographic Proofs
Static Analysis - 19th International Symposium, SAS 2012, Sep 2012, Deauville, France. ⟨10.1007/978-3-642-33125-1_1⟩
...
hal-01410196v1  Conference papers
Gilles BartheNoémie FongMarco GaboardiBenjamin GrégoireJustin Hsu et al.  Advanced Probabilistic Couplings for Differential Privacy
23rd ACM Conference on Computer and Communications Security , Oct 2016, Vienne, Austria. pp.55 - 67, ⟨10.1145/2976749.2978391⟩
...
hal-01649104v1  Conference papers
José AlmeidaManuel BarbosaGilles BartheFrancois DupressoirBenjamin Grégoire et al.  A Fast and Verified Software Stack for Secure Function Evaluation
CCS 2017 - ACM SIGSAC Conference on Computer and Communications Security, Oct 2017, Dallas, United States. pp.1-18
hal-00935736v1  Conference papers
Gilles BartheGeorge DanezisBenjamin GrégoireCésar KunzSantiago Zanella-Béguelin. Verified Computational Differential Privacy with Applications to Smart Metering
2013 IEEE 26th Computer Security Foundations Symposium, Jun 2013, New Orleans, United States. pp.287-301, ⟨10.1109/CSF.2013.26⟩
...
hal-00765842v1  Conference papers
Gilles BartheJuan Manuel CrespoBenjamin GrégoireCesar KunzSantiago Zanella-Béguelin. Computer-Aided Cryptographic Proofs
ITP 2012 - Third International Conference on Interactive Theorem Proving, Aug 2012, Princeton N.J., United States. ⟨10.1007/978-3-642-32347-8_2⟩
...
hal-01411097v1  Conference papers
Gilles BartheMarco GaboardiBenjamin GrégoireJustin HsuPierre-Yves Strub. Proving Differential Privacy via Probabilistic Couplings
Thirty-First Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jul 2016, New York, United States. pp.749 - 758, ⟨10.1145/2933575.2934554⟩
hal-01094565v1  Conference papers
Joseph A. AkinyeleGilles BartheBenjamin GrégoireBenedikt SchmidtPierre-Yves Strub. Certified Synthesis of Efficient Batch Verifiers
CSF 2014 - IEEE 27th Computer Security Foundations Symposium, Jul 2014, Vienna, Austria. pp.153 - 165, ⟨10.1109/CSF.2014.19⟩
...
hal-02404540v1  Conference papers
José Bacelar AlmeidaManuel BarbosaGilles BartheMatthew CampagnaErnie Cohen et al.  A Machine-Checked Proof of Security for AWS Key Management Service
ACM CCS 2019 - 26th ACM Conference on Computer and Communications Security, Nov 2019, London, United Kingdom. pp.63-78, ⟨10.1145/3319535.3354228⟩