TY - GEN
T1 - Automatic generation of formally-proven tamper-resistant Galois-field multipliers based on generalized masking scheme
AU - Ueno, Rei
AU - Homma, Naofumi
AU - Morioka, Sumio
AU - Aoki, Takafumi
N1 - Publisher Copyright:
© 2017 IEEE.
PY - 2017/5/11
Y1 - 2017/5/11
N2 - 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.
AB - 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.
KW - Arithmetic circuits
KW - Formal verification
KW - Galois-field
KW - Side-channel attack
KW - Threshold implementation
UR - http://www.scopus.com/inward/record.url?scp=85020228146&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85020228146&partnerID=8YFLogxK
U2 - 10.23919/DATE.2017.7927133
DO - 10.23919/DATE.2017.7927133
M3 - Conference contribution
AN - SCOPUS:85020228146
T3 - Proceedings of the 2017 Design, Automation and Test in Europe, DATE 2017
SP - 978
EP - 983
BT - Proceedings of the 2017 Design, Automation and Test in Europe, DATE 2017
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 20th Design, Automation and Test in Europe, DATE 2017
Y2 - 27 March 2017 through 31 March 2017
ER -