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

## Public-Key Cryptography and Pepin's Test for the Primality of Fermat Numbers

Yoshinori Fujisawa
Shinshu University, Nagano
Yasushi Fuwa
Shinshu University, Nagano
Hidetaka Shimizu
Information Technology Research Institute, of Nagano Prefecture

### Summary.

In this article, we have proved the correctness of the Public-Key Cryptography and the Pepin's Test for the Primality of Fermat Numbers (\$F(n) = 2^{2^n}+1\$). It is a very important result in the IDEA Cryptography that F(4) is a prime number. At first, we prepared some useful theorems. Then, we proved the correctness of the Public-Key Cryptography. Next, we defined the Order's function and proved some properties. This function is very important in the proof of the Pepin's Test. Next, we proved some theorems about the Fermat Number. And finally, we proved the Pepin's Test using some properties of the Order's Function. And using the obtained result we have proved that F(1), F(2), F(3) and F(4) are prime number.

#### MML Identifier: PEPIN

The terminology and notation used in this paper have been introduced in the following articles [10] [14] [11] [13] [6] [2] [1] [8] [7] [9] [12] [4] [5] [3]

#### Contents (PDF format)

1. Some Useful Theorems
2. Public-Key Cryptography
3. Order's Function
4. Fermat Number
5. Pepin's Test

#### Bibliography

[1] Grzegorz Bancerek. Cardinal numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.
[3] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.
[4] Yoshinori Fujisawa and Yasushi Fuwa. The Euler's function. Journal of Formalized Mathematics, 9, 1997.
[5] Yoshinori Fujisawa, Yasushi Fuwa, and Hidetaka Shimizu. Euler's Theorem and small Fermat's Theorem. Journal of Formalized Mathematics, 10, 1998.
[6] Rafal Kwiatek and Grzegorz Zwara. The divisibility of integers and integer relatively primes. Journal of Formalized Mathematics, 2, 1990.
[7] Takaya Nishiyama and Yasuho Mizuhara. Binary arithmetics. Journal of Formalized Mathematics, 5, 1993.
[8] Konrad Raczkowski and Andrzej Nedzusiak. Series. Journal of Formalized Mathematics, 3, 1991.
[9] Piotr Rudnicki and Andrzej Trybulec. Abian's fixed point theorem. Journal of Formalized Mathematics, 9, 1997.
[10] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[11] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[12] Andrzej Trybulec and Czeslaw Bylinski. Some properties of real numbers operations: min, max, square, and square root. Journal of Formalized Mathematics, 1, 1989.
[13] Michal J. Trybulec. Integers. Journal of Formalized Mathematics, 2, 1990.
[14] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

Received December 21, 1998