Title :
Toward Formal Design of Practical Cryptographic Hardware Based on Galois Field Arithmetic
Author :
Homma, Noriyasu ; Saito, Kazuyuki ; Aoki, Toyohiro
Author_Institution :
Dept. of Comput. & Math. Sci., Tohoku Univ., Sendai, Japan
Abstract :
This paper presents a formal method for designing cryptographic processor datapaths on the basis of arithmetic circuits over Galois fields (GFs). The proposed method describes GF arithmetic circuits in the form of hierarchical graph structures, where nodes represent sub-circuits whose functions are defined by arithmetic formulae over GFs, and edges represent data dependency between nodes. In this paper, we first introduce the application of graph representation to arithmetic circuits over extension fields of mbi GF(mbi pmbi m) (mbi p ≥ 2) and composite fields, which are commonly used in the design of cryptographic processors. The newly proposed graph representation can be formally verified through symbolic computation techniques based on polynomial reduction and Gröbner basis. We then demonstrate the capabilities of the proposed approach through an experimental design of a 128-bit AES (Advanced Encryption Standard) datapath including multiplicative inversion circuits over the composite field mbi GF(((22)2)2). The results show that the proposed method can describe such practical datapaths, as well as that complete verification of such a datapath can be carried out within a short period of time.
Keywords :
Galois fields; cryptography; graph theory; symbol manipulation; 128-bit AES datapath; GF arithmetic circuits; Galois field; Grobner basis; advanced encryption standard; arithmetic circuits; cryptographic hardware; cryptographic processors; graph representation; hierarchical graph structures; multiplicative inversion circuits; polynomial reduction; symbolic computation techniques; Cryptography; Encoding; Galois fields; Hardware; Mathematical model; Polynomials; AES processors; Cryptographic processors; Galois-field arithmetic; computer algebra; computer-aided design; formal method; formal verification;
Journal_Title :
Computers, IEEE Transactions on
DOI :
10.1109/TC.2013.131