Algebraic Group on Fixed-length Bit Integer and its Adaptation to IDEA Cryptography

Journal of Formalized Mathematics
Volume 10, 1998
University of Bialystok
Copyright (c) 1998 Association of Mizar Users

Algebraic Group on Fixed-length Bit Integer and its Adaptation to IDEA Cryptography

Yasushi Fuwa: Shinshu University, Nagano
Yoshinori Fujisawa: Shinshu University, Nagano

Summary.

In this article, an algebraic group on fixed-length bit integer is constructed and its adaptation to IDEA cryptography is discussed. In the first section, we present some selected theorems on integers. In the continuous section, we construct an algebraic group on fixed-length integer. In the third section, operations of IDEA Cryptograms are defined and some theorems on these operations are proved. In the fourth section, we define sequences of IDEA Cryptogram's operations and discuss their nature. Finally, we make a model of IDEA Cryptogram and prove that the ciphertext that is encrypted by IDEA encryption algorithm can be decrypted by the IDEA decryption algorithm.

MML Identifier: IDEA_1

The terminology and notation used in this paper have been introduced in the following articles [17] [21] [18] [19] [12] [1] [23] [22] [5] [10] [13] [7] [6] [2] [4] [16] [8] [3] [9] [20] [15] [14] [11]

Contents (PDF format)

Some Selected Theorems on Integers
Basic Operators of IDEA Cryptograms
Operations of IDEA Cryptograms
Sequences of IDEA Cryptogram's Operations
Modeling of IDEA Cryptogram

Bibliography

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.

[2] Grzegorz Bancerek. Curried and uncurried functions. Journal of Formalized Mathematics, 2, 1990.

[3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.

[4] Grzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. Journal of Formalized Mathematics, 8, 1996.

[5] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[6] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.

[7] Czeslaw Bylinski. Partial functions. Journal of Formalized Mathematics, 1, 1989.

[8] Czeslaw Bylinski. A classical first order language. Journal of Formalized Mathematics, 2, 1990.

[9] Czeslaw Bylinski. Finite sequences and tuples of elements of a non-empty sets. Journal of Formalized Mathematics, 2, 1990.

[10] Katarzyna Jankowska. Matrices. Abelian group of matrices. Journal of Formalized Mathematics, 3, 1991.

[11] Andrzej Kondracki. The Chinese Remainder Theorem. Journal of Formalized Mathematics, 9, 1997.

[12] Rafal Kwiatek and Grzegorz Zwara. The divisibility of integers and integer relatively primes. Journal of Formalized Mathematics, 2, 1990.

[13] Beata Madras. Product of family of universal algebras. Journal of Formalized Mathematics, 5, 1993.

[14] Robert Milewski. Binary arithmetics. Binary sequences. Journal of Formalized Mathematics, 10, 1998.

[15] Takaya Nishiyama and Yasuho Mizuhara. Binary arithmetics. Journal of Formalized Mathematics, 5, 1993.

[16] Konrad Raczkowski and Andrzej Nedzusiak. Series. Journal of Formalized Mathematics, 3, 1991.

[17] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[18] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

[19] Michal J. Trybulec. Integers. Journal of Formalized Mathematics, 2, 1990.

[20] Wojciech A. Trybulec. Pigeon hole principle. Journal of Formalized Mathematics, 2, 1990.

[21] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

[22] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[23] Edmund Woronowicz. Many-argument relations. Journal of Formalized Mathematics, 2, 1990.

Received September 7, 1998

[ Download a postscript version, MML identifier index, Mizar home page]