Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000 Association of Mizar Users

### High-Speed Algorithms for RSA Cryptograms

by
Yasushi Fuwa, and
Yoshinori Fujisawa

[ Mizar article, MML identifier index ]

```environ

vocabulary ARYTM_1, NAT_1, INT_1, ARYTM_3, FINSEQ_1, RADIX_1, POWER, MIDSP_3,
RELAT_1, FUNCT_1, RLVECT_1, RADIX_2, FINSEQ_4, GROUP_1;
notation TARSKI, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, INT_1, NAT_1,
FUNCT_1, POWER, FINSEQ_1, FINSEQ_4, BINARITH, EULER_2, RVSUM_1, TREES_4,
constructors REAL_1, POWER, BINARITH, FINSEQ_4, EULER_2, RADIX_1, SEQ_1,
MEMBERED, RAT_1;
clusters INT_1, RELSET_1, XREAL_0, WSIERP_1, NAT_1, MEMBERED, ORDINAL2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;

begin :: Some Useful Theorems

reserve k for Nat;

for a be Nat holds a mod 1 = 0;

for a,b be Integer, n be Nat st n>0 holds
((a mod n)+(b mod n)) mod n = (a + (b mod n)) mod n &
((a mod n)+(b mod n)) mod n = ((a mod n) + b) mod n;

for a,b be Integer, n be Nat st n>0 holds
(a*b) mod n = (a*(b mod n)) mod n &
(a*b) mod n = ((a mod n)*b) mod n;

for a,b,i be Nat st 1 <= i & 0 < b holds
(a mod (b |^ i)) div (b |^ (i -'1)) = (a div (b |^ (i -'1))) mod b;

for i,n be Nat st i in Seg n holds i+1 in Seg (n+1);

for k be Nat holds Radix(k) > 0;

for x be Tuple of 1,k-SD holds SDDec(x) = DigA(x,1);

for x be Integer holds

for n be Nat
for x be Tuple of (n+1),k-SD, xn be Tuple of n,k-SD st
(for i be Nat st i in Seg n holds x.i = xn.i) holds
Sum DigitSD(x) = Sum(DigitSD(xn)^<*SubDigit(x,n+1,k)*>);

for n be Nat
for x be Tuple of (n+1),k-SD, xn be Tuple of n,k-SD st
(for i be Nat st i in Seg n holds x.i = xn.i) holds
SDDec(xn) + (Radix(k) |^ n)*DigA(x,n+1) = SDDec(x);

for n be Nat st n >= 1 holds
for x,y be Tuple of n,k-SD st k >= 2 holds
SDDec(x '+' y) + SD_Add_Carry(DigA(x,n) + DigA(y,n))
*(Radix(k) |^ n) = SDDec(x) + SDDec(y);

begin :: Definitions on the relation between a FinSequence of k-SD and
:: a FinSequence of NAT and some properties about them

definition let i,k,n be Nat, x be Tuple of n,NAT;
func SubDigit2(x,i,k) -> Element of NAT equals

end;

definition let n,k be Nat, x be Tuple of n,NAT;
func DigitSD2(x,k) -> Tuple of n,NAT means

for i be Nat st i in Seg n holds it/.i = SubDigit2(x,i,k);
end;

definition let n,k be Nat, x be Tuple of n,NAT;
func SDDec2(x,k) -> Nat equals

Sum DigitSD2(x,k);
end;

definition let i,k,x be Nat;
func DigitDC2(x,i,k) -> Nat equals

end;

definition let k,n,x be Nat;
func DecSD2(x,n,k) -> Tuple of n,NAT means

for i be Nat st i in Seg n holds it.i = DigitDC2(x,i,k);
end;

for n,k be Nat, x be Tuple of n,NAT, y be Tuple of n,k-SD
st x = y holds DigitSD2(x,k) = DigitSD(y);

for n,k be Nat, x be Tuple of n,NAT, y be Tuple of n,k-SD
st x = y holds SDDec2(x,k) = SDDec(y);

for x,n,k be Nat holds DecSD2(x,n,k) = DecSD(x,n,k);

for n be Nat st n >= 1 holds
for m,k be Nat st m is_represented_by n,k holds
m = SDDec2(DecSD2(m,n,k),k);

begin :: Algorithm of calculation of (a*b) mod c based on
:: radix-2^k SD numbers and its correctness

definition let q be Integer, f,j,k,n be Nat, c be Tuple of n,k-SD;
func Table1(q,c,f,j) -> Integer equals

(q*DigA(c,j)) mod f;
end;

definition let q be Integer, k,f,n be Nat, c be Tuple of n,k-SD;
assume n >= 1;
func Mul_mod(q,c,f,k) -> Tuple of n,INT means

it.1 = Table1(q,c,f,n) &
for i be Nat st 1 <= i & i <= n - 1 holds
ex I1,I2 be Integer st I1 = it.i & I2 = it.(i+1) &
I2 = (Radix(k)*I1+Table1(q,c,f,n -'i)) mod f;
end;

for n be Nat st n >= 1 holds
for q be Integer, ic,f,k be Nat
st ic is_represented_by n,k & f > 0 holds
for c be Tuple of n,k-SD st c = DecSD(ic,n,k) holds
Mul_mod(q,c,f,k).n = (q * ic) mod f;

begin :: Algorithm of calculation of (a^b) mod c based on
:: radix-2^k SD numbers and its correctness

definition let n,f,j,m be Nat, e be Tuple of n,NAT;
func Table2(m,e,f,j) -> Nat equals

(m |^ (e/.j)) mod f;
end;

definition let k,f,m,n be Nat, e be Tuple of n,NAT;
assume n >= 1;
func Pow_mod(m,e,f,k) -> Tuple of n,NAT means

it.1 = Table2(m,e,f,n) &
for i be Nat st 1 <= i & i <= n - 1 holds
ex i1,i2 be Nat st i1 = it.i & i2 = it.(i+1) &
i2 = (((i1 |^ Radix(k)) mod f) * Table2(m,e,f,n-'i)) mod f;
end;