Volume 10, 1998

University of Bialystok

Copyright (c) 1998 Association of Mizar Users

**Yasushi Fuwa**- Shinshu University, Nagano
**Yoshinori Fujisawa**- Shinshu University, Nagano

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

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

- [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.

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