Paper 2017/879
Formal Verification of Side-channel Countermeasures via Elementary Circuit Transformations
Jean-Sebastien Coron
Abstract
We describe a technique to formally verify the security of masked implementations against side-channel attacks, based on elementary circuit transforms. We describe two complementary approaches: a generic approach for the formal verification of any circuit, but for small attack orders only, and a specialized approach for the verification of specific circuits, but at any order. We also show how to generate security proofs automatically, for simple circuits. We describe the implementation of CheckMasks, a formal verification tool for side-channel countermeasures. Using this tool, we formally verify the security of the Rivain-Prouff countermeasure for AES, and also the recent Boolean to arithmetic conversion algorithm from CHES 2017.
Metadata
- Available format(s)
-
PDF
- Category
- Implementation
- Publication info
- Published elsewhere. Major revision. ACNS 2018
- Keywords
- Side-channel countermeasuresmaskingformal verification.
- Contact author(s)
- jean-sebastien coron @ uni lu
- History
- 2018-04-09: last of 4 revisions
- 2017-09-13: received
- See all versions
- Short URL
- https://ia.cr/2017/879
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2017/879,
author = {Jean-Sebastien Coron},
title = {Formal Verification of Side-channel Countermeasures via Elementary Circuit Transformations},
howpublished = {Cryptology {ePrint} Archive, Paper 2017/879},
year = {2017},
url = {https://eprint.iacr.org/2017/879}
}
