International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

Gilles Barthe

Publications

Year
Venue
Title
2021
TCHES
Masking in Fine-Grained Leakage Models: Construction, Implementation and Verification 📺
We propose a new approach for building efficient, provably secure, and practically hardened implementations of masked algorithms. Our approach is based on a Domain Specific Language in which users can write efficient assembly implementations and fine-grained leakage models. The latter are then used as a basis for formal verification, allowing for the first time formal guarantees for a broad range of device-specific leakage effects not addressed by prior work. The practical benefits of our approach are demonstrated through a case study of the PRESENT S-Box: we develop a highly optimized and provably secure masked implementation, and show through practical evaluation based on TVLA that our implementation is practically resilient. Our approach significantly narrows the gap between formal verification of masking and practical security.
2019
JOFC
Automated Analysis of Cryptographic Assumptions in Generic Group Models
We initiate the study of principled, automated methods for analyzing hardness assumptions in generic group models, following the approach of symbolic cryptography. We start by defining a broad class of generic and symbolic group models for different settings—symmetric or asymmetric (leveled) k -linear groups—and by proving “computational soundness” theorems for the symbolic models. Based on this result, we formulate a very general master theorem that formally relates the hardness of a (possibly interactive) assumption in these models to solving problems in polynomial algebra. Then, we systematically analyze these problems. We identify different classes of assumptions and obtain decidability and undecidability results. Next, we develop and implement automated procedures for verifying the conditions of master theorems, and thus the validity of hardness assumptions in generic group models. The concrete outcome of this work is an automated tool which takes as input the statement of an assumption and outputs either a proof of its generic hardness or shows an algebraic attack against the assumption.
2018
EUROCRYPT
2017
EUROCRYPT
2017
CRYPTO
2017
EUROCRYPT
2016
EUROCRYPT
2016
FSE
2015
PKC
2015
EUROCRYPT
2015
EUROCRYPT
2015
ASIACRYPT
2014
CRYPTO
2014
CHES
2011
CRYPTO

Program Committees

Crypto 2018
Eurocrypt 2015