This paper presents an automatic hierarchical formal verification method for arithmetic circuits over Galois fields (GFs) which are dedicated digital circuits for GF arithmetic operations used in cryptographic processors. The proposed verification method is based on a combination of a word-level computer algebra procedure with a bit-level PPRM (Positive Polarity Reed-Muller) expansion procedure. While the application of the proposed verification method is not limited to cryptographic processors, these processors are our important targets because complicated implementation techniques, such as field conversions, are frequently used for side-channel resistant, compact and low power design. In the proposed method, the correctness of entire datapath is verified over GF(2m) level, or word-level. A datapath implementation is represented hierarchically as a set of components' functional descriptions over GF(2m) and their wiring connections. We verify that the implementation satisfies a given total-functional specification over GF(2m), by using an automatic algebraic method based on the Gröbner basis and a polynomial reduction. Then, in order to verify whether each component circuit is correctly implemented by combination of GF(2) operations, i.e. logic gates in bit-level, we use our fast PPRM expansion procedure which is customized for handling large-scale Boolean expressions with many variables. We have applied the proposed method to a complicated AES (Advanced Encryption Standard) circuit with a masking countermeasure against side-channel attack. The results show that the proposed method can verify such practical circuit automatically within 4 minutes, while any single conventional verification methods fail within a day or even more.

Tweakable block cipher (TBC) is an extension of conventional block cipher. We study how to build a TBC based on generalized Feistel structure (GFS), a classical block cipher construction. While known dedicated TBC proposals are based on substitution-permutation network (SPN), GFS has not been used for building TBC. In particular, we take 64-bit GFS block cipher TWINE and try to make it tweakable with a minimum change. To find a best one from a large number of candidates, we performed a comprehensive search with a help of mixed integer linear programming (MILP) solver. As a result, our proposal TWINE is quite efficient, has the same number of rounds as TWINE with extremely simple tweak schedule.