Cryptology ePrint Archive: Report 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.

Category / Keywords: implementation / Side-channel countermeasures, masking, formal verification.

Original Publication (with major differences): ACNS 2018

Date: received 10 Sep 2017, last revised 9 Apr 2018

Contact author: jean-sebastien coron at uni lu

Available format(s): PDF | BibTeX Citation

Version: 20180409:120046 (All versions of this report)

Short URL:

[ Cryptology ePrint archive ]