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

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.