Formal design of multiple-valued arithmetic algorithms over galois fields and its application to cryptographic processor

Naofumi Homma; Kazuya Saito; Takafumi Aoki

doi:10.1109/ISMVL.2012.24

Formal design of multiple-valued arithmetic algorithms over galois fields and its application to cryptographic processor

Naofumi Homma, Kazuya Saito, Takafumi Aoki

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

7 Citations (Scopus)

Abstract

This paper presents a formal description of multiple-valued arithmetic algorithms over Galois Fields (GFs). Our graph-based method can be applied to any multiple-valued arithmetic circuit over GF(2 ^m). The proposed circuit description is formally verified by formula manipulation based on polynomial reduction using Groebner basis. In this paper, we first present the graph representation and its extension. We also present an application of the proposed method to cryptographic processor consisting of GF(2 ^m) arithmetic circuits. The target architecture considered here is a round-per-cycle loop architecture commonly used in the design of cryptographic processors. The proposed approach successfully describes the 128-bit data path and verifies it within 4 minutes.

Original language	English
Title of host publication	Proceedings - IEEE 42nd International Symposium on Multiple-Valued Logic, ISMVL 2012
Pages	110-115
Number of pages	6
DOIs	https://doi.org/10.1109/ISMVL.2012.24
Publication status	Published - 2012
Event	42nd IEEE International Symposium on Multiple-Valued Logic, ISMVL 2012 - Victoria, BC, Canada Duration: 2012 May 14 → 2012 May 16

Publication series

Name	Proceedings of The International Symposium on Multiple-Valued Logic
ISSN (Print)	0195-623X

Other

Other	42nd IEEE International Symposium on Multiple-Valued Logic, ISMVL 2012
Country/Territory	Canada
City	Victoria, BC
Period	12/5/14 → 12/5/16

Keywords

arithmetic algorithms
computer algebra
formal verification
multiple-valued logic

ASJC Scopus subject areas

Computer Science(all)
Mathematics(all)

Access to Document

10.1109/ISMVL.2012.24

Cite this

Homma, N., Saito, K., & Aoki, T. (2012). Formal design of multiple-valued arithmetic algorithms over galois fields and its application to cryptographic processor. In Proceedings - IEEE 42nd International Symposium on Multiple-Valued Logic, ISMVL 2012 (pp. 110-115). [6214793] (Proceedings of The International Symposium on Multiple-Valued Logic). https://doi.org/10.1109/ISMVL.2012.24

Formal design of multiple-valued arithmetic algorithms over galois fields and its application to cryptographic processor. / Homma, Naofumi; Saito, Kazuya; Aoki, Takafumi.
Proceedings - IEEE 42nd International Symposium on Multiple-Valued Logic, ISMVL 2012. 2012. p. 110-115 6214793 (Proceedings of The International Symposium on Multiple-Valued Logic).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Homma, N, Saito, K & Aoki, T 2012, Formal design of multiple-valued arithmetic algorithms over galois fields and its application to cryptographic processor. in Proceedings - IEEE 42nd International Symposium on Multiple-Valued Logic, ISMVL 2012., 6214793, Proceedings of The International Symposium on Multiple-Valued Logic, pp. 110-115, 42nd IEEE International Symposium on Multiple-Valued Logic, ISMVL 2012, Victoria, BC, Canada, 12/5/14. https://doi.org/10.1109/ISMVL.2012.24

@inproceedings{a57f3c1d77c6463ea894f54ff59c4709,

title = "Formal design of multiple-valued arithmetic algorithms over galois fields and its application to cryptographic processor",

abstract = "This paper presents a formal description of multiple-valued arithmetic algorithms over Galois Fields (GFs). Our graph-based method can be applied to any multiple-valued arithmetic circuit over GF(2 m). The proposed circuit description is formally verified by formula manipulation based on polynomial reduction using Groebner basis. In this paper, we first present the graph representation and its extension. We also present an application of the proposed method to cryptographic processor consisting of GF(2 m) arithmetic circuits. The target architecture considered here is a round-per-cycle loop architecture commonly used in the design of cryptographic processors. The proposed approach successfully describes the 128-bit data path and verifies it within 4 minutes.",

keywords = "arithmetic algorithms, computer algebra, formal verification, multiple-valued logic",

author = "Naofumi Homma and Kazuya Saito and Takafumi Aoki",

year = "2012",

doi = "10.1109/ISMVL.2012.24",

language = "English",

isbn = "9780769546735",

series = "Proceedings of The International Symposium on Multiple-Valued Logic",

pages = "110--115",

booktitle = "Proceedings - IEEE 42nd International Symposium on Multiple-Valued Logic, ISMVL 2012",

note = "42nd IEEE International Symposium on Multiple-Valued Logic, ISMVL 2012 ; Conference date: 14-05-2012 Through 16-05-2012",

}

TY - GEN

T1 - Formal design of multiple-valued arithmetic algorithms over galois fields and its application to cryptographic processor

AU - Homma, Naofumi

AU - Saito, Kazuya

AU - Aoki, Takafumi

PY - 2012

Y1 - 2012

N2 - This paper presents a formal description of multiple-valued arithmetic algorithms over Galois Fields (GFs). Our graph-based method can be applied to any multiple-valued arithmetic circuit over GF(2 m). The proposed circuit description is formally verified by formula manipulation based on polynomial reduction using Groebner basis. In this paper, we first present the graph representation and its extension. We also present an application of the proposed method to cryptographic processor consisting of GF(2 m) arithmetic circuits. The target architecture considered here is a round-per-cycle loop architecture commonly used in the design of cryptographic processors. The proposed approach successfully describes the 128-bit data path and verifies it within 4 minutes.

AB - This paper presents a formal description of multiple-valued arithmetic algorithms over Galois Fields (GFs). Our graph-based method can be applied to any multiple-valued arithmetic circuit over GF(2 m). The proposed circuit description is formally verified by formula manipulation based on polynomial reduction using Groebner basis. In this paper, we first present the graph representation and its extension. We also present an application of the proposed method to cryptographic processor consisting of GF(2 m) arithmetic circuits. The target architecture considered here is a round-per-cycle loop architecture commonly used in the design of cryptographic processors. The proposed approach successfully describes the 128-bit data path and verifies it within 4 minutes.

KW - arithmetic algorithms

KW - computer algebra

KW - formal verification

KW - multiple-valued logic

UR - http://www.scopus.com/inward/record.url?scp=84864260000&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84864260000&partnerID=8YFLogxK

U2 - 10.1109/ISMVL.2012.24

DO - 10.1109/ISMVL.2012.24

M3 - Conference contribution

AN - SCOPUS:84864260000

SN - 9780769546735

T3 - Proceedings of The International Symposium on Multiple-Valued Logic

SP - 110

EP - 115

BT - Proceedings - IEEE 42nd International Symposium on Multiple-Valued Logic, ISMVL 2012

T2 - 42nd IEEE International Symposium on Multiple-Valued Logic, ISMVL 2012

Y2 - 14 May 2012 through 16 May 2012

ER -

Formal design of multiple-valued arithmetic algorithms over galois fields and its application to cryptographic processor

Abstract

Publication series

Other

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this