A formal approach to designing cryptographic processors based on GF(2 m) arithmetic circuits

Research output: Contribution to journalArticlepeer-review

20 Citations (Scopus)


This paper proposes a formal approach to designing Galois-field (GF) arithmetic circuits, which are widely used in modern cryptographic processors. Our method describes GF arithmetic circuits in a hierarchical manner with high-level directed graphs associated with specific GFs and arithmetic functions. The proposed circuit description can be effectively verified by symbolic computations based on polynomial reduction using Grbner bases. The verified description is then translated into the equivalent hardware description language (HDL) codes, which are available for the conventional design flow. We first describe the proposed graph representation and present an example of the description and verification. The significant advantage of the proposed approach is demonstrated through experimental designs of parallel multipliers over GF(2 m) for different word lengths and irreducible polynomials. The result shows that the proposed approach has a definite capability of formally verifying practical GF arithmetic circuits for which the conventional techniques fail. We also propose an application of this approach to cryptographic processor design. The target considered here is a 128-bit advanced encryption standard (AES) data path with a loop architecture. To the best of the authors' knowledge, this is the first verification of this type of practical AES data path. We present a detailed description of the AES data path and its verification. The proposed approach successfully verifies the AES data path description within 800 s.

Original languageEnglish
Article number5773490
Pages (from-to)3-13
Number of pages11
JournalIEEE Transactions on Information Forensics and Security
Issue number1 PART 1
Publication statusPublished - 2012 Feb


  • Advanced encryption standard (AES) processors
  • computer aided design
  • computer algebra
  • cryptographic processors
  • formal design
  • Galois-field (GF) arithmetic


Dive into the research topics of 'A formal approach to designing cryptographic processors based on GF(2 m) arithmetic circuits'. Together they form a unique fingerprint.

Cite this