Paper Info
Title
Automatic generation of formally-proven tamper-resistant Galois-field multipliers based on generalized masking scheme.
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.
Year
Venue
Keywords
2017
DATE
formal verification, arithmetic circuits, Galois-field, threshold implementation, side-channel attack
Field
DocType
ISSN
Adder,Computer science,Theoretical computer science,Multiplier (economics),Dataflow,Side channel attack,Physical design,Register-transfer level,Galois theory,Formal verification
Conference
1530-1591
Citations 
PageRank 
References 
0
0.34
14
Authors
4
Name
Order
Citations
PageRank
Ueno, R.121.40
Naofumi Homma237753.81
Sumio Morioka349345.23
Takafumi Aoki4915125.99