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]
-
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]