Toward Formal Design of Practical Cryptographic Hardware Based on Galois Field Arithmetic

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 p^{mbi 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(((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.