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

by
Yoshinori Fujisawa,
Yasushi Fuwa, and
Hidetaka Shimizu

MML identifier: PEPIN
[ Mizar article, MML identifier index ]

```environ

vocabulary EULER_1, NAT_1, SQUARE_1, ARYTM_3, INT_1, FINSET_1, ARYTM_1,
ABSVALUE, FILTER_0, MATRIX_2, CARD_1, POWER, FINSEQ_1, PEPIN, RELAT_1,
GROUP_1;
notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, INT_1, INT_2,
NAT_1, CARD_1, SETWOP_2, SERIES_1, BINARITH, ABIAN, SQUARE_1, EULER_1,
EULER_2, FINSET_1, GROUP_1;
constructors REAL_1, SERIES_1, BINARITH, ABIAN, SQUARE_1, EULER_1, EULER_2,
SETWOP_2, GROUP_1, INT_2, MEMBERED;
clusters INT_1, XREAL_0, ABIAN, FINSET_1, FINSUB_1, SQUARE_1, MEMBERED,
NUMBERS, ORDINAL2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;

begin :: Some selected Basic Theorems

reserve d,i,j,k,m,n,p,q,x,y,n1,n2,k1,k2 for Nat,
a,b,c,i1,i2,i3,i5 for Integer;

theorem :: PEPIN:1
for i holds i,i+1 are_relative_prime;

theorem :: PEPIN:2
for p holds p is prime implies m,p are_relative_prime or m hcf p = p;

theorem :: PEPIN:3
k divides n*m & n,k are_relative_prime implies k divides m;

theorem :: PEPIN:4
n divides m & k divides m & n,k are_relative_prime implies (n*k) divides m;

definition let n be Nat;
redefine func n^2 -> Nat;
end;

theorem :: PEPIN:5
c > 1 implies 1 mod c = 1;

theorem :: PEPIN:6
for i st i <> 0 holds i divides n iff n mod i = 0;

theorem :: PEPIN:7
m <> 0 & m divides n mod m implies m divides n;

theorem :: PEPIN:8
0 < n & m mod n = k implies n divides (m - k);

theorem :: PEPIN:9
i*p <> 0 & p is prime & k mod i*p < p
implies k mod i*p = k mod p;

theorem :: PEPIN:10
(a*p + 1) mod p = 1 mod p;

theorem :: PEPIN:11
1 < m & (n*k) mod m = k mod m & k,m are_relative_prime
implies n mod m = 1;

theorem :: PEPIN:12
(p |^ k) mod m = ((p mod m) |^ k) mod m;

theorem :: PEPIN:13
i <> 0 implies i^2 mod (i+1) = 1;

theorem :: PEPIN:14
k^2 < j & i mod j = k implies i^2 mod j = k^2;

theorem :: PEPIN:15
p is prime & i mod p = -1 implies i^2 mod p = 1;

theorem :: PEPIN:16
n is even implies n + 1 is odd;

theorem :: PEPIN:17
p > 2 & p is prime implies p is odd;

theorem :: PEPIN:18
n > 0 implies 2 to_power(n) is even;

theorem :: PEPIN:19
i is odd & j is odd implies i*j is odd;

theorem :: PEPIN:20
for k holds i is odd implies i |^ k is odd;

theorem :: PEPIN:21
k > 0 & i is even implies i |^ k is even;

theorem :: PEPIN:22
2 divides n iff n is even;

theorem :: PEPIN:23
m*n is even implies m is even or n is even;

theorem :: PEPIN:24
n |^ 2 = n^2;

canceled;

theorem :: PEPIN:26
m > 1 & n > 0 implies m |^ n > 1;

theorem :: PEPIN:27
n <> 0 & p <> 0 implies n |^ p = n*(n |^ (p -'1));

theorem :: PEPIN:28
for n,m st m mod 2 = 0 holds (n |^ (m div 2))^2 = n |^ m;

theorem :: PEPIN:29
n <> 0 & 1 <= k implies (n |^ k) div n = n |^ (k -'1);

theorem :: PEPIN:30
2 |^ (n + 1) = (2 |^ n)+(2 |^ n);

theorem :: PEPIN:31
k > 1 & k |^ n = k |^ m implies n = m;

theorem :: PEPIN:32
m <= n iff 2 |^ m divides 2 |^ n;

theorem :: PEPIN:33
p is prime & i divides p |^ n implies i = 1 or (ex k being Nat st i = p*k);

theorem :: PEPIN:34
for n st n <> 0 & p is prime & n < p |^ (k+1) holds
n divides p |^ (k+1) iff n divides p |^ k;

theorem :: PEPIN:35
for k holds p is prime & d divides (p |^ k) & d <> 0
implies ex t being Nat st d = p |^ t & t <= k;

theorem :: PEPIN:36
p > 1 & i mod p = 1 implies (i |^ n) mod p = 1;

theorem :: PEPIN:37
m > 0 implies (n |^ m) mod n = 0;

theorem :: PEPIN:38
p is prime & n,p are_relative_prime
implies (n |^ (p -'1)) mod p = 1;

theorem :: PEPIN:39
p is prime & d > 1 & d divides (p |^ k) & not d divides ((p |^ k) div p)
implies d = p |^ k;

definition let a be Integer;
redefine func a^2 -> Nat;
end;

theorem :: PEPIN:40
for n st n > 1 holds m mod n = 1 iff m,1 are_congruent_mod n;

theorem :: PEPIN:41
a,b are_congruent_mod c implies a^2,b^2 are_congruent_mod c;

canceled;

theorem :: PEPIN:43
i1,i2 are_congruent_mod i5 & i1,i3 are_congruent_mod i5
implies i2,i3 are_congruent_mod i5;

theorem :: PEPIN:44
3 is prime;

theorem :: PEPIN:45
n <> 0 implies Euler n <> 0;

theorem :: PEPIN:46
n <> 0 implies -n < n;

canceled;

theorem :: PEPIN:48
n <> 0 implies n div n = 1;

begin :: Public Key Cryptography

definition
let k,m,n;
func Crypto(m,n,k) -> Nat equals
:: PEPIN:def 1
(m |^ k) mod n;
end;

theorem :: PEPIN:49
p is prime & q is prime & p <> q & n = p*q &
k1,Euler(n) are_relative_prime & (k1*k2) mod Euler(n) = 1
implies for m be Nat st m < n holds Crypto(Crypto(m,n,k1),n,k2) = m;

begin :: Order

definition
let i,p;
assume p > 1 & i,p are_relative_prime;
func order(i,p) -> Nat means
:: PEPIN:def 2

it > 0 & (i |^ it) mod p = 1 & for k st k > 0 & (i |^ k) mod p = 1
holds 0 < it & it <= k;
end;

theorem :: PEPIN:50
p > 1 implies order(1,p) = 1;

canceled;

theorem :: PEPIN:52
p > 1 & n > 0 & (i |^ n) mod p = 1 & i,p are_relative_prime
implies order(i,p) divides n;

theorem :: PEPIN:53
p > 1 & i,p are_relative_prime & order(i,p) divides n implies
(i |^ n) mod p = 1;

theorem :: PEPIN:54
p is prime & i,p are_relative_prime implies order(i,p) divides (p -'1);

begin :: Fermat Number

definition
let n be Nat;
func Fermat(n) -> Nat equals
:: PEPIN:def 3

2 |^ (2 |^ n) + 1;
end;

theorem :: PEPIN:55
Fermat(0) = 3;

theorem :: PEPIN:56
Fermat(1) = 5;

theorem :: PEPIN:57
Fermat(2) = 17;

theorem :: PEPIN:58
Fermat(3) = 257;

theorem :: PEPIN:59
Fermat(4) = 256*256+1;

theorem :: PEPIN:60
Fermat(n) > 2;

theorem :: PEPIN:61
p is prime & p > 2 & p divides Fermat(n) implies
ex k being Nat st p = k*(2 |^ (n + 1)) + 1;

theorem :: PEPIN:62
n <> 0 implies 3,Fermat(n) are_relative_prime;

begin :: Pepin's Test

theorem :: PEPIN:63
(3 |^ ((Fermat(n)-'1) div 2)),(-1) are_congruent_mod Fermat(n)
implies Fermat(n) is prime;

theorem :: PEPIN:64
5 is prime;

theorem :: PEPIN:65
17 is prime;

theorem :: PEPIN:66
257 is prime;

theorem :: PEPIN:67
256*256+1 is prime;
```