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
Creative Commons Attribution
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},
      note = {\url{https://eprint.iacr.org/2017/879}},
      url = {https://eprint.iacr.org/2017/879}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.