Paper 2015/060

Verified Proofs of Higher-Order Masking

Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, and Pierre-Yves Strub

Abstract

In this paper, we study the problem of automatically verifying higher-order masking countermeasures. This problem is important in practice (weaknesses have been discovered in schemes that were thought secure), but is inherently exponential: for $t$-order masking, it involves proving that every subset of $t$ intermediate variables is distributed independently of the secrets. Some type systems have been proposed to help cryptographers check their proofs, but many of these approaches are insufficient for higher-order implementations. We propose a new method, based on program verification techniques, to check the independence of sets of intermediate variables from some secrets. Our new language-based characterization of the problem also allows us to design and implement several algorithms that greatly reduce the number of sets of variables that need to be considered to prove this independence property on \emph{all} valid adversary observations. The result of these algorithms is either a proof of security or a set of observations on which the independence property cannot be proved. We focus on AES implementations to check the validity of our algorithms. We also confirm the tool's ability to give useful information when proofs fail, by rediscovering existing attacks and discovering new ones.

Note: IACR copyright agreement

Metadata
Available format(s)
PDF
Category
Secret-key cryptography
Publication info
A minor revision of an IACR publication in EUROCRYPT 2015
Keywords
MaskingAutomatic toolsEasyCryptHigher-Order Masking
Contact author(s)
sonia belaid @ live fr
History
2015-02-06: last of 4 revisions
2015-01-27: received
See all versions
Short URL
https://ia.cr/2015/060
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2015/060,
      author = {Gilles Barthe and Sonia Belaïd and François Dupressoir and Pierre-Alain Fouque and Benjamin Grégoire and Pierre-Yves Strub},
      title = {Verified Proofs of Higher-Order Masking},
      howpublished = {Cryptology ePrint Archive, Paper 2015/060},
      year = {2015},
      note = {\url{https://eprint.iacr.org/2015/060}},
      url = {https://eprint.iacr.org/2015/060}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.