The abstract of the Mizar article:

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

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;