Automatic Generation of Formally-Proven Temper-Resistant Galois-Field Multipliers Based on Generalized Masking Scheme

被引：0

作者：

Ueno, Rei ^{[1
]}

Homma, Naofumi ^{[1
]}

Morioka, Sumio ^{[2
]}

Aoki, Takafumi ^{[1
]}

机构：

[1] Tohoku Univ, Aramaki Aza Aoba 6-6-05, Sendai, Miyagi 9808579, Japan

[2] Interstellar Technol Inc, 690-4 Memu, Taiki, Hokkaido 0892113, Japan

来源：

PROCEEDINGS OF THE 2017 DESIGN, AUTOMATION & TEST IN EUROPE CONFERENCE & EXHIBITION (DATE) | 2017年

关键词：

formal verification; arithmetic circuits; Galois-field; threshold implementation; side-channel attack; HARDWARE; DESIGN;

D O I：

暂无

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

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 specifiic physical design. In this study, we first present a formal design methodology of GMS-based GF arithmetic circuits based on a hierarchical data flow graph, called GF arithmetic circuit graph (GF-ACG), and present a formal verification method for both functionality and security property based on Grobner 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 x 77) within 15 min.

引用

页码：978 / 983

页数：6