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 transformations. 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 describe the implementation of CheckMasks, a formal verification tool for side-channel countermeasures, using the Common Lisp programming language. Using this tool, we show how to formally verify the security of the Rivain-Prouff countermeasure for AES.

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

Date: received 10 Sep 2017, last revised 18 Sep 2017

Contact author: jean-sebastien coron at uni lu

Available format(s): PDF | BibTeX Citation

Version: 20170918:090436 (All versions of this report)

Short URL: ia.cr/2017/879

Discussion forum: Show discussion | Start new discussion


[ Cryptology ePrint archive ]