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

Research output: Contribution to journalArticlepeer-review


In this study, we propose a formal design system for automatically generating provably-secure register transfer level (RTL) description of cryptographic hardwares based on Generalized Masking Scheme (GMS). We first present a formal design methodology of GMS-based GF arithmetic circuits based on a hierarchical dataflow graph, called GF arithmetic circuit graph (GF-ACG), and present a formal verification method for both functionality and security property based on Gröbner basis. The proposed automatic generation system for GMS-based GF multipliers can synthesize a fifth-order 256-bit multiplier (whose input bit-length is 256 × 77) within 15 min.

Original languageEnglish
JournalIEEE Design and Test
Publication statusAccepted/In press - 2021


  • Adders
  • Cryptographic hardware
  • Cryptography
  • Design methodology
  • Differential power analysis
  • Formal verification
  • Galois-field arithmetic circuit
  • Hardware
  • Masking
  • Registers
  • Resistance
  • Side-channel attacks
  • and Side-channel attack

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture
  • Electrical and Electronic Engineering

Fingerprint 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