:: Public-Key Cryptography and Pepin's Test for the Primality of
:: Fermat Numbers
:: by Yoshinori Fujisawa , Yasushi Fuwa and Hidetaka Shimizu
::
:: Received December 21, 1998
:: Copyright (c) 1998-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, INT_1, XXREAL_0, RELAT_1, ARYTM_3, CARD_1,
NEWTON, ARYTM_1, INT_2, SUBSET_1, SQUARE_1, ORDINAL1, ABIAN, POWER,
EULER_1, TARSKI, SETWOP_2, FINSET_1, XBOOLE_0, PEPIN, REAL_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0,
XREAL_0, INT_1, INT_2, NAT_1, NAT_D, SETWOP_2, POWER, ABIAN, SQUARE_1,
NEWTON, EULER_1, FINSET_1, XXREAL_0;
constructors SQUARE_1, NAT_1, NAT_D, SETWOP_2, NEWTON, SERIES_1, BINARITH,
EULER_1, ABIAN, VALUED_1, XXREAL_2;
registrations ORDINAL1, FINSET_1, FINSUB_1, XXREAL_0, XREAL_0, NAT_1, INT_1,
NEWTON, ABIAN, SERIES_1, POWER, CARD_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin :: Some selected Basic Theorems
reserve d,i,j,k,m,n,p,q,x,k1,k2 for Nat,
a,c,i1,i2,i3,i5 for Integer;
theorem :: PEPIN:1
for i being Nat holds i,i+1 are_coprime;
theorem :: PEPIN:2
for p being Nat holds p is prime implies m,p are_coprime
or m gcd p = p;
theorem :: PEPIN:3
for k,m,n being Nat holds k divides n*m & n,k are_coprime
implies k divides m;
theorem :: PEPIN:4
n divides m & k divides m & n,k are_coprime implies (n*k) divides m;
registration
let i be Integer;
cluster i^2 -> natural;
end;
theorem :: PEPIN:5
c > 1 implies 1 mod c = 1;
theorem :: PEPIN:6
for i,n be Nat st i <> 0 holds i divides n iff n mod i = 0;
theorem :: PEPIN:7
for m,n being Nat holds m <> 0 & m divides n mod m implies m divides n;
theorem :: PEPIN:8
for m,n,k being Nat holds 0 < n & m mod n = k implies n divides (m - k);
theorem :: PEPIN:9
i*p <> 0 & 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_coprime 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
for p being Nat holds 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
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;
theorem :: PEPIN:25
m > 1 & n > 0 implies m |^ n > 1;
theorem :: PEPIN:26
n <> 0 & p <> 0 implies n |^ p = n*(n |^ (p -'1));
theorem :: PEPIN:27
for n,m st m mod 2 = 0 holds (n |^ (m div 2))^2 = n |^ m;
theorem :: PEPIN:28
n <> 0 & 1 <= k implies (n |^ k) div n = n |^ (k -'1);
theorem :: PEPIN:29
2 |^ (n + 1) = (2 |^ n)+(2 |^ n);
theorem :: PEPIN:30
k > 1 & k |^ n = k |^ m implies n = m;
theorem :: PEPIN:31
m <= n iff 2 |^ m divides 2 |^ n;
theorem :: PEPIN:32
p is prime & i divides p |^ n implies i = 1 or ex k being
Element of NAT st i = p*k;
theorem :: PEPIN:33
for n st p is prime & n < p |^ (k+1) holds n divides p |^ (k+1)
iff n divides p |^ k;
theorem :: PEPIN:34
for k holds p is prime & d divides (p |^ k) implies ex t being
Element of NAT st d = p |^ t & t <= k;
theorem :: PEPIN:35
p > 1 & i mod p = 1 implies (i |^ n) mod p = 1;
theorem :: PEPIN:36
for m,n being Nat holds m > 0 implies (n |^ m) mod n = 0;
theorem :: PEPIN:37
for p being Nat holds p is prime & n,p are_coprime
implies (n |^ (p -'1)) mod p = 1;
theorem :: PEPIN:38
p is prime & d > 1 & d divides (p |^ k) & not d divides ((p |^ k
) div p) implies d = p |^ k;
definition
let i be Integer;
redefine func i^2 -> Element of NAT;
end;
theorem :: PEPIN:39
for n st n > 1 holds m mod n = 1 iff m,1 are_congruent_mod n;
theorem :: PEPIN:40
i1,i2 are_congruent_mod i5 & i1,i3 are_congruent_mod i5 implies
i2,i3 are_congruent_mod i5;
theorem :: PEPIN:41
3 is prime;
theorem :: PEPIN:42
n <> 0 implies Euler n <> 0;
theorem :: PEPIN:43
n <> 0 implies -n < n;
theorem :: PEPIN:44
n <> 0 implies n div n = 1;
begin :: Public Key Cryptography
definition
let k,m,n;
func Crypto(m,n,k) -> Element of NAT equals
:: PEPIN:def 1
(m |^ k) mod n;
end;
theorem :: PEPIN:45
p is prime & q is prime & p <> q & n = p*q & k1,Euler(n)
are_coprime & (k1*k2) mod Euler(n) = 1 implies for m be Element of NAT
st m < n holds Crypto(Crypto(m,n,k1),n,k2) = m;
begin :: Order
definition
let i,p;
assume that
p > 1 and
i,p are_coprime;
func order(i,p) -> Element of 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:46
p > 1 implies order(1,p) = 1;
theorem :: PEPIN:47
p > 1 & (i |^ n) mod p = 1 & i,p are_coprime implies
order(i,p) divides n;
theorem :: PEPIN:48
p > 1 & i,p are_coprime & order(i,p) divides n implies (i
|^ n) mod p = 1;
theorem :: PEPIN:49
p is prime & i,p are_coprime implies order(i,p) divides ( p -'1);
begin :: Fermat Number
definition
let n be Nat;
func Fermat(n) -> Element of NAT equals
:: PEPIN:def 3
2 |^ (2 |^ n) + 1;
end;
theorem :: PEPIN:50
Fermat(0) = 3;
theorem :: PEPIN:51
Fermat(1) = 5;
theorem :: PEPIN:52
Fermat(2) = 17;
theorem :: PEPIN:53
Fermat(3) = 257;
theorem :: PEPIN:54
Fermat(4) = 256*256+1;
theorem :: PEPIN:55
Fermat(n) > 2;
theorem :: PEPIN:56
p is prime & p > 2 & p divides Fermat(n) implies ex k being
Element of NAT st p = k*(2 |^ (n + 1)) + 1;
theorem :: PEPIN:57
n <> 0 implies 3,Fermat(n) are_coprime;
begin :: Pepin's Test
::$N Pepin's test
theorem :: PEPIN:58
(3 |^ ((Fermat(n)-'1) div 2)),(-1) are_congruent_mod Fermat(n)
implies Fermat(n) is prime;
theorem :: PEPIN:59
5 is prime;
theorem :: PEPIN:60
17 is prime;
theorem :: PEPIN:61
257 is prime;
theorem :: PEPIN:62
256*256+1 is prime;
:: Moved from JORDAN1A, AK, 21.02.2006
theorem :: PEPIN:63
for i,j being Integer holds j <> 0 & i mod j = 0 implies i div j = i / j;
theorem :: PEPIN:64
for i,n being Nat st n > 0 holds i |^ n div i = i |^ n / i;
reserve r for Real;
theorem :: PEPIN:65
for n being Nat holds 0 < n & 1 < r implies 1 < r|^n;
theorem :: PEPIN:66
for m,n being Nat holds r > 1 & m > n implies r|^m > r|^n;