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-02552287v2  Reports
Gilles BartheCharlie JacommeSteve Kremer. Universal equivalence and majority of probabilistic programs over finite fields
[Research Report] MPI SP; LSV, ENS Cachan, CNRS, INRIA, Université Paris-Saclay, Cachan (France); LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2020
hal-01599851v1  Conference papers
Miguel AmbronaGilles BartheRomain GayHoeteck Wee. Attribute-Based Encryption in the Generic Group Model: Automated Proofs and New Constructions
ACM Conference on Computer and Communications Security (CCS) 2017, Oct 2017, Dallas, United States
hal-00764871v1  Conference papers
Gilles BartheDavid PointchevalSantiago Zanella-Béguelin. Verified security of redundancy-free encryption from Rabin and RSA
CCS '12 - ACM conference on Computer and communications security, Oct 2012, Raleigh, NC, United States. pp.724-735, ⟨10.1145/2382196.2382272⟩
hal-01101950v1  Conference papers
Gilles BartheGustavo BetarteJuan Diego CampoCarlos LunaDavid Pichardie. System-level Non-interference for Constant-time Cryptography
ACM SIGSAC Conference on Computer and Communications Security, CCS'14, Nov 2014, Scottsdale, United States. pp.1267 - 1279, ⟨10.1145/2660267.2660283⟩
hal-01948334v1  Conference papers
Patrick BaillotGilles BartheUgo Dal Lago. Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs.
Logic for Programming, Artificial Intelligence, and Reasoning - 20thInternational Conference, LPAR-20, Nov 2015, Suva, Fiji. pp.203-218
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-01110783v1  Conference papers
Gilles BartheDelphine DemangeDavid Pichardie. A Formally Verified SSA-based Middle-end
21th European Symposium on Programming, ESOP 2012, Mar 2012, Tallin, Estonia. pp.47-66, ⟨10.1007/978-3-642-28869-2_3⟩
hal-01097677v1  Journal articles
Gilles BartheDelphine DemangeDavid Pichardie. Formal Verification of an SSA-based Middle-end for CompCert
ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2014, 36 (1), pp.35. ⟨10.1145/2579080⟩
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-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⟩