Gilles Barthe

Google Scholar
63 publications in security and cryptology related venues
Year
Venue
Title
2025
journals/tches
Let's DOIT: Using Intel's Extended HW/SW Contract for Secure Compilation of Crypto Code.
Santiago Arranz-Olmos Gilles Barthe Benjamin Grégoire Jan Jancar Vincent Laporte Tiago Oliveira Peter Schwabe
2025
conf/sp
Faster Verification of Faster Implementations: Combining Deductive and Circuit-Based Reasoning in EasyCrypt.
José Bacelar Almeida Gustavo Xavier Delerue Marinho Alves Manuel Barbosa Gilles Barthe Luís Esquível Vincent Hwang Tiago Oliveira Hugo Pacheco Peter Schwabe Pierre-Yves Strub
2024
journals/tches
High-assurance zeroization.
Santiago Arranz-Olmos Gilles Barthe Ruben Gonzalez Benjamin Grégoire Vincent Laporte Jean-Christophe Léchenet Tiago Oliveira Peter Schwabe
2024
journals/joc
Masking the GLP Lattice-Based Signature Scheme at Any Order.
Gilles Barthe Sonia Belaïd Thomas Espitau Pierre-Alain Fouque Benjamin Grégoire Mélissa Rossi Mehdi Tibouchi
2024
conf/ccs
Testing Side-channel Security of Cryptographic Implementations against Future Microarchitectures.
Gilles Barthe Marcel Böhme Sunjay Cauligi Chitchanok Chuengsatiansup Daniel Genkin Marco Guarnieri David Mateos Romero Peter Schwabe David Wu Yuval Yarom
2024
conf/uss
"These results must be false": A usability evaluation of constant-time analysis tools.
Marcel Fourné Daniel De Almeida Braga Jan Jancar Mohamed Sabt Peter Schwabe Gilles Barthe Pierre-Alain Fouque Yasemin Acar
2024
conf/crypto
Formally Verifying Kyber - Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt.
José Bacelar Almeida Santiago Arranz-Olmos Manuel Barbosa Gilles Barthe François Dupressoir Benjamin Grégoire Vincent Laporte Jean-Christophe Léchenet Cameron Low Tiago Oliveira Hugo Pacheco Miguel Quaresma Peter Schwabe Pierre-Yves Strub
2023
journals/tches
Formally verifying Kyber Episode IV: Implementation correctness.
José Bacelar Almeida Manuel Barbosa Gilles Barthe Benjamin Grégoire Vincent Laporte Jean-Christophe Léchenet Tiago Oliveira Hugo Pacheco Miguel Quaresma Peter Schwabe Antoine Séré Pierre-Yves Strub
2023
conf/uss
Ultimate SLH: Taking Speculative Load Hardening to the Next Level.
Zhiyuan Zhang Gilles Barthe Chitchanok Chuengsatiansup Peter Schwabe Yuval Yarom
2023
conf/crypto
Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium.
Manuel Barbosa Gilles Barthe Christian Doczkal Jelle Don Serge Fehr Benjamin Grégoire Yu-Hsuan Huang Andreas Hülsing Yi Lee Xiaodi Wu
2023
conf/sp
Spectre Declassified: Reading from the Right Place at the Wrong Time.
Basavesh Ammanaghatta Shivakumar Jack Barnes Gilles Barthe Sunjay Cauligi Chitchanok Chuengsatiansup Daniel Genkin Sioli O'Connell Peter Schwabe Rui Qi Sim Yuval Yarom
2023
conf/sp
Typing High-Speed Cryptography against Spectre v1.
Basavesh Ammanaghatta Shivakumar Gilles Barthe Benjamin Grégoire Vincent Laporte Tiago Oliveira Swarn Priya Peter Schwabe Lucas Tabary-Maujean
2022
conf/ccs
Enforcing Fine-grained Constant-time Policies.
Basavesh Ammanaghatta Shivakumar Gilles Barthe Benjamin Grégoire Vincent Laporte Swarn Priya
2022
conf/ccs
Tidy: Symbolic Verification of Timed Cryptographic Protocols.
Gilles Barthe Ugo Dal Lago Giulio Malavolta Itsaka Rakotonirina
2022
conf/sp
SoK: Practical Foundations for Software Spectre Defenses.
Sunjay Cauligi Craig Disselkoen Daniel Moghimi Gilles Barthe Deian Stefan
2022
conf/sp
"They're not that hard to mitigate": What Cryptographic Library Developers Think About Timing Attacks.
Jan Jancar Marcel Fourné Daniel De Almeida Braga Mohamed Sabt Peter Schwabe Gilles Barthe Pierre-Alain Fouque Yasemin Acar
2022
conf/asiaccs
Symbolic Synthesis of Indifferentiability Attacks.
Itsaka Rakotonirina Miguel Ambrona Alejandro Aguirre Gilles Barthe
2021
journals/tches
Masking in Fine-Grained Leakage Models: Construction, Implementation and Verification.
Gilles Barthe Marc Gourjon Benjamin Grégoire Maximilian Orlt Clara Paglialonga Lars Porth
2021
conf/ccs
EasyPQC: Verifying Post-Quantum Cryptography.
Manuel Barbosa Gilles Barthe Xiong Fan Benjamin Grégoire Shih-Han Hung Jonathan Katz Pierre-Yves Strub Xiaodi Wu Li Zhou
2021
conf/ccs
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability.
Manuel Barbosa Gilles Barthe Benjamin Grégoire Adrien Koutsos Pierre-Yves Strub
2021
conf/ccs
Structured Leakage and Applications to Cryptographic Constant-Time and Cost.
Gilles Barthe Benjamin Grégoire Vincent Laporte Swarn Priya
2021
conf/sp
SoK: Computer-Aided Cryptography.
Manuel Barbosa Gilles Barthe Karthik Bhargavan Bruno Blanchet Cas Cremers Kevin Liao Bryan Parno
2021
conf/sp
High-Assurance Cryptography in the Spectre Era.
Gilles Barthe Sunjay Cauligi Benjamin Grégoire Adrien Koutsos Kevin Liao Tiago Oliveira Swarn Priya Tamara Rezk Peter Schwabe
2020
conf/sp
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations.
José Bacelar Almeida Manuel Barbosa Gilles Barthe Benjamin Grégoire Adrien Koutsos Vincent Laporte Tiago Oliveira Pierre-Yves Strub
2019
journals/joc
Automated Analysis of Cryptographic Assumptions in Generic Group Models.
Gilles Barthe Edvard Fagerholm Dario Fiore John C. Mitchell Andre Scedrov Benedikt Schmidt
2019
conf/ccs
Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3.
José Bacelar Almeida Cécile Baritel-Ruet Manuel Barbosa Gilles Barthe François Dupressoir Benjamin Grégoire Vincent Laporte Tiago Oliveira Alley Stoughton Pierre-Yves Strub
2019
conf/ccs
A Machine-Checked Proof of Security for AWS Key Management Service.
José Bacelar Almeida Manuel Barbosa Gilles Barthe Matthew Campagna Ernie Cohen Benjamin Grégoire Vitor Pereira Bernardo Portela Pierre-Yves Strub Serdar Tasiran
2019
conf/ccs
GALACTICS: Gaussian Sampling for Lattice-Based Constant- Time Implementation of Cryptographic Signatures, Revisited.
Gilles Barthe Sonia Belaïd Thomas Espitau Pierre-Alain Fouque Mélissa Rossi Mehdi Tibouchi
2019
conf/esorics
maskVerif: Automated Verification of Higher-Order Masking in Presence of Physical Defaults.
Gilles Barthe Sonia Belaïd Gaëtan Cassiers Pierre-Alain Fouque Benjamin Grégoire François-Xavier Standaert
2018
conf/ccs
Symbolic Proofs for Lattice-Based Cryptography.
Gilles Barthe Xiong Fan Joshua Gancher Benjamin Grégoire Charlie Jacomme Elaine Shi
2018
conf/eurocrypt
Masking the GLP Lattice-Based Signature Scheme at Any Order.
Gilles Barthe Sonia Belaïd Thomas Espitau Pierre-Alain Fouque Benjamin Grégoire Mélissa Rossi Mehdi Tibouchi
2017
conf/ccs
A Fast and Verified Software Stack for Secure Function Evaluation.
José Bacelar Almeida Manuel Barbosa Gilles Barthe François Dupressoir Benjamin Grégoire Vincent Laporte Vitor Pereira
2017
conf/ccs
Jasmin: High-Assurance and High-Speed Cryptography.
José Bacelar Almeida Manuel Barbosa Gilles Barthe Arthur Blot Benjamin Grégoire Vincent Laporte Tiago Oliveira Hugo Pacheco Benedikt Schmidt Pierre-Yves Strub
2017
conf/ccs
Attribute-Based Encryption in the Generic Group Model: Automated Proofs and New Constructions.
Miguel Ambrona Gilles Barthe Romain Gay Hoeteck Wee
2017
conf/crypto
Generic Transformations of Predicate Encodings: Constructions and Applications.
Miguel Ambrona Gilles Barthe Benedikt Schmidt
2017
conf/eurosp
Reasoning about Probabilistic Defense Mechanisms against Remote Attacks.
Martín Ochoa Sebastian Banescu Cynthia Disenfeld Gilles Barthe Vijay Ganesh
2017
conf/eurocrypt
Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model.
Gilles Barthe François Dupressoir Sebastian Faust Benjamin Grégoire François-Xavier Standaert Pierre-Yves Strub
2016
conf/fse
Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC.
José Bacelar Almeida Manuel Barbosa Gilles Barthe François Dupressoir
2016
conf/ccs
Advanced Probabilistic Couplings for Differential Privacy.
Gilles Barthe Noémie Fong Marco Gaboardi Benjamin Grégoire Justin Hsu Pierre-Yves Strub
2016
conf/ccs
Strong Non-Interference and Type-Directed Higher-Order Masking.
Gilles Barthe Sonia Belaïd François Dupressoir Pierre-Alain Fouque Benjamin Grégoire Pierre-Yves Strub Rébecca Zucchini
2016
conf/ccs
Differentially Private Bayesian Programming.
Gilles Barthe Gian Pietro Farina Marco Gaboardi Emilio Jesús Gallego Arias Andy Gordon Justin Hsu Pierre-Yves Strub
2016
conf/uss
Verifying Constant-Time Implementations.
José Bacelar Almeida Manuel Barbosa Gilles Barthe François Dupressoir Michael Emmi
2016
conf/eurocrypt
Automated Unbounded Analysis of Cryptographic Constructions in the Generic Group Model.
Miguel Ambrona Gilles Barthe Benedikt Schmidt
2015
conf/ccs
Automated Proofs of Pairing-Based Cryptography.
Gilles Barthe Benjamin Grégoire Benedikt Schmidt
2015
conf/pkc
Strongly-Optimal Structure Preserving Signatures from Type II Pairings: Synthesis and Lower Bounds.
Gilles Barthe Edvard Fagerholm Dario Fiore Andre Scedrov Benedikt Schmidt Mehdi Tibouchi
2015
conf/eurocrypt
Mind the Gap: Modular Machine-Checked Proofs of One-Round Key Exchange Protocols.
Gilles Barthe Juan Manuel Crespo Yassine Lakhnech Benedikt Schmidt
2015
conf/eurocrypt
Verified Proofs of Higher-Order Masking.
Gilles Barthe Sonia Belaïd François Dupressoir Pierre-Alain Fouque Benjamin Grégoire Pierre-Yves Strub
2014
conf/ccs
System-level Non-interference for Constant-time Cryptography.
Gilles Barthe Gustavo Betarte Juan Diego Campo Carlos Daniel Luna David Pichardie
2014
conf/ccs
Synthesis of Fault Attacks on Cryptographic Implementations.
Gilles Barthe François Dupressoir Pierre-Alain Fouque Benjamin Grégoire Jean-Christophe Zapalowicz
2014
conf/crypto
Automated Analysis of Cryptographic Assumptions in Generic Group Models.
Gilles Barthe Edvard Fagerholm Dario Fiore John C. Mitchell Andre Scedrov Benedikt Schmidt
2014
conf/ches
Making RSA-PSS Provably Secure against Non-random Faults.
Gilles Barthe François Dupressoir Pierre-Alain Fouque Benjamin Grégoire Mehdi Tibouchi Jean-Christophe Zapalowicz
2013
conf/ccs
Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations.
José Bacelar Almeida Manuel Barbosa Gilles Barthe François Dupressoir
2013
conf/ccs
Fully automated analysis of padding-based encryption in the computational model.
Gilles Barthe Juan Manuel Crespo Benjamin Grégoire César Kunz Yassine Lakhnech Benedikt Schmidt Santiago Zanella-Béguelin
2012
conf/ccs
Verified security of redundancy-free encryption from Rabin and RSA.
Gilles Barthe David Pointcheval Santiago Zanella-Béguelin
2012
conf/ccs
Full proof cryptography: verifiable compilation of efficient zero-knowledge protocols.
José Bacelar Almeida Manuel Barbosa Endre Bangerter Gilles Barthe Stephan Krenn Santiago Zanella-Béguelin
2011
conf/crypto
Computer-Aided Security Proofs for the Working Cryptographer.
Gilles Barthe Benjamin Grégoire Sylvain Heraud Santiago Zanella-Béguelin
2011
conf/provsec
Verifiable Security of Boneh-Franklin Identity-Based Encryption.
Gilles Barthe Federico Olmedo Santiago Zanella-Béguelin
2011
conf/ctrsa
Beyond Provable Security Verifiable IND-CCA Security of OAEP.
Gilles Barthe Benjamin Grégoire Yassine Lakhnech Santiago Zanella-Béguelin
2010
conf/ccs
Computational indistinguishability logic.
Gilles Barthe Marion Daubignard Bruce M. Kapron Yassine Lakhnech
2009
conf/sp
Formally Certifying the Security of Digital Signature Schemes.
Santiago Zanella-Béguelin Gilles Barthe Benjamin Grégoire Federico Olmedo
2007
conf/esorics
Security of Multithreaded Programs by Compilation.
Gilles Barthe Tamara Rezk Alejandro Russo Andrei Sabelfeld
2006
conf/sp
Deriving an Information Flow Checker and Certifying Compiler for Java.
Gilles Barthe Tamara Rezk David A. Naumann
2004
conf/ccs
Formally verifying information flow type systems for concurrent and thread systems.
Gilles Barthe Leonor Prensa Nieto

Coauthors

Adrien Koutsos (3)
Alejandro Aguirre (1)
Alejandro Russo (1)
Alley Stoughton (1)
Andre Scedrov (3)
Andreas Hülsing (1)
Andrei Sabelfeld (1)
Andy Gordon (1)
Antoine Séré (1)
Arthur Blot (1)
Basavesh Ammanaghatta Shivakumar (3)
Benedikt Schmidt (9)
Benjamin Grégoire (32)
Bernardo Portela (1)
Bruce M. Kapron (1)
Bruno Blanchet (1)
Bryan Parno (1)
Cameron Low (1)
Carlos Daniel Luna (1)
Cas Cremers (1)
Cécile Baritel-Ruet (1)
César Kunz (1)
Charlie Jacomme (1)
Chitchanok Chuengsatiansup (3)
Christian Doczkal (1)
Clara Paglialonga (1)
Craig Disselkoen (1)
Cynthia Disenfeld (1)
Daniel De Almeida Braga (2)
Daniel Genkin (2)
Daniel Moghimi (1)
Dario Fiore (3)
David A. Naumann (1)
David Mateos Romero (1)
David Pichardie (1)
David Pointcheval (1)
David Wu (1)
Deian Stefan (1)
Edvard Fagerholm (3)
Elaine Shi (1)
Emilio Jesús Gallego Arias (1)
Endre Bangerter (1)
Ernie Cohen (1)
Federico Olmedo (2)
François Dupressoir (11)
François-Xavier Standaert (2)
Gaëtan Cassiers (1)
Gian Pietro Farina (1)
Gilles Barthe (63)
Giulio Malavolta (1)
Gustavo Betarte (1)
Gustavo Xavier Delerue Marinho Alves (1)
Hoeteck Wee (1)
Hugo Pacheco (4)
Itsaka Rakotonirina (2)
Jack Barnes (1)
Jan Jancar (3)
Jean-Christophe Léchenet (3)
Jean-Christophe Zapalowicz (2)
Jelle Don (1)
John C. Mitchell (2)
Jonathan Katz (1)
José Bacelar Almeida (12)
Joshua Gancher (1)
Juan Diego Campo (1)
Juan Manuel Crespo (2)
Justin Hsu (2)
Karthik Bhargavan (1)
Kevin Liao (2)
Lars Porth (1)
Leonor Prensa Nieto (1)
Li Zhou (1)
Lucas Tabary-Maujean (1)
Luís Esquível (1)
Manuel Barbosa (16)
Marc Gourjon (1)
Marcel Böhme (1)
Marcel Fourné (2)
Marco Gaboardi (2)
Marco Guarnieri (1)
Marion Daubignard (1)
Martín Ochoa (1)
Matthew Campagna (1)
Maximilian Orlt (1)
Mehdi Tibouchi (5)
Mélissa Rossi (3)
Michael Emmi (1)
Miguel Ambrona (4)
Miguel Quaresma (2)
Mohamed Sabt (2)
Noémie Fong (1)
Peter Schwabe (12)
Pierre-Alain Fouque (10)
Pierre-Yves Strub (14)
Rébecca Zucchini (1)
Romain Gay (1)
Ruben Gonzalez (1)
Rui Qi Sim (1)
Santiago Arranz-Olmos (3)
Santiago Zanella-Béguelin (7)
Sebastian Banescu (1)
Sebastian Faust (1)
Serdar Tasiran (1)
Serge Fehr (1)
Shih-Han Hung (1)
Sioli O'Connell (1)
Sonia Belaïd (6)
Stephan Krenn (1)
Sunjay Cauligi (4)
Swarn Priya (4)
Sylvain Heraud (1)
Tamara Rezk (3)
Thomas Espitau (3)
Tiago Oliveira (10)
Ugo Dal Lago (1)
Vijay Ganesh (1)
Vincent Hwang (1)
Vincent Laporte (11)
Vitor Pereira (2)
Xiaodi Wu (2)
Xiong Fan (2)
Yasemin Acar (2)
Yassine Lakhnech (4)
Yi Lee (1)
Yu-Hsuan Huang (1)
Yuval Yarom (3)
Zhiyuan Zhang (1)
Filters
Select all Unselect all
Years:  to