Paper 2017/879 Original: eprint.iacr.org/2017/879 ↗
Formal Verification of Side-channel Countermeasures via Elementary Circuit Transformations
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
- Preprint.
- History
- 2018-04-09: last updated
- 2017-09-13: published
- Short URL
- https://ia.cr/2017/879
- License
- https://creativecommons.org/licenses/by/4.0/
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}
}