:: High-speed algorithms for RSA cryptograms
:: by Yasushi Fuwa and Yoshinori Fujisawa
::
:: Received February 1, 2000
:: Copyright (c) 2000-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, CARD_1, RELAT_1, ARYTM_3, XXREAL_0,
ARYTM_1, NEWTON, FINSEQ_1, RADIX_1, POWER, FINSEQ_2, PARTFUN1, FUNCT_1,
CARD_3, ORDINAL4, SUBSET_1, TARSKI, REAL_1, RADIX_2, FUNCT_7;
notations TARSKI, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, INT_1,
NAT_1, NAT_D, FUNCT_1, POWER, PARTFUN1, FINSEQ_1, FINSEQ_2, NEWTON,
RVSUM_1, GR_CY_1, WSIERP_1, RADIX_1, SUBSET_1, RECDEF_1;
constructors REAL_1, NAT_D, NEWTON, POWER, BINARITH, WSIERP_1, GR_CY_1,
RADIX_1, RECDEF_1, NUMBERS;
registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1,
MEMBERED, NEWTON, VALUED_0, FINSEQ_2, FINSEQ_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin :: Some Useful Theorems
reserve k for Nat;
theorem :: RADIX_2:1
for a be Nat holds a mod 1 = 0;
theorem :: RADIX_2:2
for a,b be Integer, n be Nat holds
((a mod n)+(b mod n)) mod n = (a + (b mod n)) mod n;
theorem :: RADIX_2:3
for a,b be Integer, n be Nat holds (a*b) mod n = (a*(b mod n)) mod n;
theorem :: RADIX_2:4
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;
theorem :: RADIX_2:5
for i,n be Nat st i in Seg n holds i+1 in Seg (n+1);
begin :: Properties of Addition operation using radix-2^k SD numbers
theorem :: RADIX_2:6
for k be Nat holds Radix(k) > 0;
theorem :: RADIX_2:7
for x be Tuple of 1,k-SD holds SDDec(x) = DigA(x,1);
theorem :: RADIX_2:8
for x be Integer holds SD_Add_Data(x,k) + SD_Add_Carry(x)*Radix(k ) = x;
theorem :: RADIX_2:9
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)*>);
theorem :: RADIX_2:10
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);
theorem :: RADIX_2:11
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
:: RADIX_2:def 1
(Radix(k) |^ (i -'1))*(x.i);
end;
definition
let n,k be Nat, x be Tuple of n,NAT;
func DigitSD2(x,k) -> Tuple of n,NAT means
:: RADIX_2:def 2
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) -> Element of NAT equals
:: RADIX_2:def 3
Sum DigitSD2(x,k);
end;
definition
let i,k,x be Nat;
func DigitDC2(x,i,k) -> Element of NAT equals
:: RADIX_2:def 4
(x mod (Radix(k) |^ i)) div (
Radix(k) |^ (i -'1));
end;
definition
let k,n,x be Nat;
func DecSD2(x,n,k) -> Tuple of n,NAT means
:: RADIX_2:def 5
for i be Nat st i in Seg n holds it.i = DigitDC2(x,i,k);
end;
theorem :: RADIX_2:12
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);
theorem :: RADIX_2:13
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);
theorem :: RADIX_2:14
for x,n,k be Nat holds DecSD2(x,n,k) = DecSD(x,n,k);
theorem :: RADIX_2:15
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
:: RADIX_2:def 6
(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
:: RADIX_2:def 7
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;
theorem :: RADIX_2:16
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) -> Element of NAT equals
:: RADIX_2:def 8
(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
:: RADIX_2:def 9
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;
theorem :: RADIX_2:17
for n be Nat st n >= 1 holds for m,k,f,ie be Nat st ie
is_represented_by n,k & f>0 holds for e be Tuple of n,NAT st e = DecSD2(ie,n,k)
holds Pow_mod(m,e,f,k).n = (m |^ ie) mod f;