Toward formal design of practical cryptographic hardware based on galois field arithmetic

Research output: Contribution to journalArticlepeer-review

14 Citations (Scopus)


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 GF(pm) (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.Wethen 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 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.

Original languageEnglish
Article number6532293
Pages (from-to)2604-2613
Number of pages10
JournalIEEE Transactions on Computers
Issue number10
Publication statusPublished - 2014 Oct 1


  • AES processors
  • Computer algebra
  • Computer-aided design
  • Cryptographic processors
  • Formal method
  • Formal verification
  • Galois-field arithmetic

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Hardware and Architecture
  • Computational Theory and Mathematics


Dive into the research topics of 'Toward formal design of practical cryptographic hardware based on galois field arithmetic'. Together they form a unique fingerprint.

Cite this