A Systematic Design Methodology of Formally Proven Side-Channel-Resistant Cryptographic Hardware

Research output: Contribution to journalArticlepeer-review

3 Citations (Scopus)


This article proposes a formal design system for automatically generating provably secure register transfer level description of cryptographic hardware based on generalized masking scheme. To address the above problems, we propose a formal design and verification method for generalized masking schem (GMS)-based Galois-field (GF) arithmetic circuits. The proposed method is based on a formal approach to describing and verifying GF arithmetic circuits. The basic ideas revolve around the description of GF arithmetic circuits using a high-level mathematical graph called GF arithmetic circuit graph (GF-ACG) and its verification using an algebraic procedure based on a GroÄbner basis (GB) and a polynomial reduction technique. The proposed methodology automatically generates the GMS-based GF arithmetic circuits from circuit function and GMS order, and then its functionality is verified on the basis of GF-ACG.

Original languageEnglish
Article number9367223
Pages (from-to)84-92
Number of pages9
JournalIEEE Design and Test
Issue number3
Publication statusPublished - 2021 Jun


  • and Side-channel attack
  • Cryptographic hardware
  • Differential power analysis
  • Formal verification
  • Galois-field arithmetic circuit
  • Masking


Dive into the research topics of 'A Systematic Design Methodology of Formally Proven Side-Channel-Resistant Cryptographic Hardware'. Together they form a unique fingerprint.

Cite this