Formal design of pipelined GF arithmetic circuits and its application to cryptographic processors

Rei Ueno, Yukihiro Sugawara, Naofumi Homma, Takafumi Aoki

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

Abstract

This study presents a formal approach to designing pipelined arithmetic circuits over Galois fields (GFs). The proposed method extends a graph-based circuit description known as a Galois-field arithmetic circuit graph (GF-ACG) to Linear-time Temporal Logic (LTL) in order to represent the timing property of pipelined circuits. We first present the extension of GF-ACG and its formal verification using computer algebra. We then demonstrate the efficiency of the proposed method through an experimental design of a lightweight cryptographic processor. In particular, we design a tamper-resistant datapath with threshold Implementation (TI) based on pipelining and multi-party computation. The proposed method can verify the processor within 1 h, whereas conventional methods would fail.

Original languageEnglish
Title of host publicationProceedings - 2016 IEEE 46th International Symposium on Multiple-Valued Logic, ISMVL 2016
PublisherIEEE Computer Society
Pages217-222
Number of pages6
ISBN (Electronic)9781467394888
DOIs
Publication statusPublished - 2016 Jul 18
Event46th IEEE International Symposium on Multiple-Valued Logic, ISMVL 2016 - Sapporo, Hokkaido, Japan
Duration: 2016 May 182016 May 20

Publication series

NameProceedings of The International Symposium on Multiple-Valued Logic
Volume2016-July
ISSN (Print)0195-623X

Other

Other46th IEEE International Symposium on Multiple-Valued Logic, ISMVL 2016
Country/TerritoryJapan
CitySapporo, Hokkaido
Period16/5/1816/5/20

Keywords

  • Galois-field
  • Threshold Implementation
  • arithmetic circuits
  • computer algebra
  • formal verification

ASJC Scopus subject areas

  • Computer Science(all)
  • Mathematics(all)

Fingerprint

Dive into the research topics of 'Formal design of pipelined GF arithmetic circuits and its application to cryptographic processors'. Together they form a unique fingerprint.

Cite this