作者
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub
发表日期
2015/4/14
图书
Annual International Conference on the Theory and Applications of Cryptographic Techniques
页码范围
457-485
出版商
Springer Berlin Heidelberg
简介
In this paper, we study the problem of automatically verifying higher-order masking countermeasures. This problem is important in practice, since weaknesses have been discovered in schemes that were thought secure, but is inherently exponential: for -order masking, it involves proving that every subset of intermediate variables is distributed independently of the secrets. Some tools have been proposed to help cryptographers check their proofs, but are often limited in scope.
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 all valid adversary observations. The …
学术搜索中的文章
G Barthe, S Belaïd, F Dupressoir, PA Fouque… - Annual International Conference on the Theory and …, 2015