Automatic generation of formally-proven tamper-resistant Galois-field multipliers based on generalized masking scheme

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

In this study, we propose a formal design system for tamper-resistant cryptographic hardwares based on Generalized Masking Scheme (GMS). The masking scheme, which is a state-of-the-art masking-based countermeasure against higher-order differential power analyses (DPAs), can securely construct any kind of Galois-field (GF) arithmetic circuits at the register transfer level (RTL) description, while most other ones require specific physical design. In this study, 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. In addition, we propose an automatic generation system for GMS-based GF multipliers, which can synthesize a fifth-order 256-bit multiplier (whose input bit-length is 256 × 77) within 15 min.

Original languageEnglish
Title of host publicationProceedings of the 2017 Design, Automation and Test in Europe, DATE 2017
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages978-983
Number of pages6
ISBN (Electronic)9783981537093
DOIs
Publication statusPublished - 2017 May 11
Event20th Design, Automation and Test in Europe, DATE 2017 - Swisstech, Lausanne, Switzerland
Duration: 2017 Mar 272017 Mar 31

Publication series

NameProceedings of the 2017 Design, Automation and Test in Europe, DATE 2017

Other

Other20th Design, Automation and Test in Europe, DATE 2017
CountrySwitzerland
CitySwisstech, Lausanne
Period17/3/2717/3/31

Keywords

  • Arithmetic circuits
  • Formal verification
  • Galois-field
  • Side-channel attack
  • Threshold implementation

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Hardware and Architecture
  • Safety, Risk, Reliability and Quality

Fingerprint Dive into the research topics of 'Automatic generation of formally-proven tamper-resistant Galois-field multipliers based on generalized masking scheme'. Together they form a unique fingerprint.

Cite this