:: High-speed algorithms for RSA cryptograms :: by Yasushi Fuwa and Yoshinori Fujisawa :: :: Received February 1, 2000 :: Copyright (c) 2000-2012 Association of Mizar Users begin theorem :: RADIX_2:1 for a being Nat holds a mod 1 = 0 proofend; theorem Th2: :: RADIX_2:2 for a, b being Integer for n being Nat st n > 0 holds ((a mod n) + (b mod n)) mod n = (a + (b mod n)) mod n proofend; theorem Th3: :: RADIX_2:3 for a, b being Integer for n being Nat st n > 0 holds (a * b) mod n = (a * (b mod n)) mod n proofend; theorem Th4: :: RADIX_2:4 for a, b, i being Nat st 1 <= i & 0 < b holds (a mod (b |^ i)) div (b |^ (i -' 1)) = (a div (b |^ (i -' 1))) mod b proofend; theorem Th5: :: RADIX_2:5 for i, n being Nat st i in Seg n holds i + 1 in Seg (n + 1) proofend; begin theorem Th6: :: RADIX_2:6 for k being Nat holds Radix k > 0 proofend; theorem Th7: :: RADIX_2:7 for k being Nat for x being Tuple of 1,k -SD holds SDDec x = DigA (x,1) proofend; theorem Th8: :: RADIX_2:8 for k being Nat for x being Integer holds (SD_Add_Data (x,k)) + ((SD_Add_Carry x) * (Radix k)) = x proofend; theorem Th9: :: RADIX_2:9 for k, n being Nat for x being Tuple of n + 1,k -SD for xn being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds x . i = xn . i ) holds Sum (DigitSD x) = Sum ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>) proofend; theorem Th10: :: RADIX_2:10 for k, n being Nat for x being Tuple of n + 1,k -SD for xn being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds x . i = xn . i ) holds (SDDec xn) + (((Radix k) |^ n) * (DigA (x,(n + 1)))) = SDDec x proofend; theorem :: RADIX_2:11 for k, n being Nat st n >= 1 holds for x, y being 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) proofend; begin :: a FinSequence of NAT and some properties about them definition let i, k, n be Nat; let 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); coherence ((Radix k) |^ (i -' 1)) * (x . i) is Element of NAT ; end; :: deftheorem defines SubDigit2 RADIX_2:def_1_:_ for i, k, n being Nat for x being Tuple of n, NAT holds SubDigit2 (x,i,k) = ((Radix k) |^ (i -' 1)) * (x . i); definition let n, k be Nat; let x be Tuple of n, NAT ; func DigitSD2 (x,k) -> Tuple of n, NAT means :Def2: :: RADIX_2:def 2 for i being Nat st i in Seg n holds it /. i = SubDigit2 (x,i,k); existence ex b1 being Tuple of n, NAT st for i being Nat st i in Seg n holds b1 /. i = SubDigit2 (x,i,k) proofend; uniqueness for b1, b2 being Tuple of n, NAT st ( for i being Nat st i in Seg n holds b1 /. i = SubDigit2 (x,i,k) ) & ( for i being Nat st i in Seg n holds b2 /. i = SubDigit2 (x,i,k) ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines DigitSD2 RADIX_2:def_2_:_ for n, k being Nat for x, b4 being Tuple of n, NAT holds ( b4 = DigitSD2 (x,k) iff for i being Nat st i in Seg n holds b4 /. i = SubDigit2 (x,i,k) ); definition let n, k be Nat; let x be Tuple of n, NAT ; func SDDec2 (x,k) -> Element of NAT equals :: RADIX_2:def 3 Sum (DigitSD2 (x,k)); coherence Sum (DigitSD2 (x,k)) is Element of NAT ; end; :: deftheorem defines SDDec2 RADIX_2:def_3_:_ for n, k being Nat for x being Tuple of n, NAT holds SDDec2 (x,k) = Sum (DigitSD2 (x,k)); 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)); coherence (x mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) is Element of NAT ; end; :: deftheorem defines DigitDC2 RADIX_2:def_4_:_ for i, k, x being Nat holds DigitDC2 (x,i,k) = (x mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)); definition let k, n, x be Nat; func DecSD2 (x,n,k) -> Tuple of n, NAT means :Def5: :: RADIX_2:def 5 for i being Nat st i in Seg n holds it . i = DigitDC2 (x,i,k); existence ex b1 being Tuple of n, NAT st for i being Nat st i in Seg n holds b1 . i = DigitDC2 (x,i,k) proofend; uniqueness for b1, b2 being Tuple of n, NAT st ( for i being Nat st i in Seg n holds b1 . i = DigitDC2 (x,i,k) ) & ( for i being Nat st i in Seg n holds b2 . i = DigitDC2 (x,i,k) ) holds b1 = b2 proofend; end; :: deftheorem Def5 defines DecSD2 RADIX_2:def_5_:_ for k, n, x being Nat for b4 being Tuple of n, NAT holds ( b4 = DecSD2 (x,n,k) iff for i being Nat st i in Seg n holds b4 . i = DigitDC2 (x,i,k) ); theorem Th12: :: RADIX_2:12 for n, k being Nat for x being Tuple of n, NAT for y being Tuple of n,k -SD st x = y holds DigitSD2 (x,k) = DigitSD y proofend; theorem Th13: :: RADIX_2:13 for n, k being Nat for x being Tuple of n, NAT for y being Tuple of n,k -SD st x = y holds SDDec2 (x,k) = SDDec y proofend; theorem Th14: :: RADIX_2:14 for x, n, k being Nat holds DecSD2 (x,n,k) = DecSD (x,n,k) proofend; theorem Th15: :: RADIX_2:15 for n being Nat st n >= 1 holds for m, k being Nat st m is_represented_by n,k holds m = SDDec2 ((DecSD2 (m,n,k)),k) proofend; begin :: radix-2^k SD numbers and its correctness definition let q be Integer; let f, j, k, n be Nat; let 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; correctness coherence (q * (DigA (c,j))) mod f is Integer; ; end; :: deftheorem defines Table1 RADIX_2:def_6_:_ for q being Integer for f, j, k, n being Nat for c being Tuple of n,k -SD holds Table1 (q,c,f,j) = (q * (DigA (c,j))) mod f; definition let q be Integer; let k, f, n be Nat; let c be Tuple of n,k -SD ; assume A1: n >= 1 ; func Mul_mod (q,c,f,k) -> Tuple of n, INT means :Def7: :: RADIX_2:def 7 ( it . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds ex I1, I2 being Integer st ( I1 = it . i & I2 = it . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) ); existence ex b1 being Tuple of n, INT st ( b1 . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds ex I1, I2 being Integer st ( I1 = b1 . i & I2 = b1 . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) ) proofend; uniqueness for b1, b2 being Tuple of n, INT st b1 . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds ex I1, I2 being Integer st ( I1 = b1 . i & I2 = b1 . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) & b2 . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds ex I1, I2 being Integer st ( I1 = b2 . i & I2 = b2 . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) holds b1 = b2 proofend; end; :: deftheorem Def7 defines Mul_mod RADIX_2:def_7_:_ for q being Integer for k, f, n being Nat for c being Tuple of n,k -SD st n >= 1 holds for b6 being Tuple of n, INT holds ( b6 = Mul_mod (q,c,f,k) iff ( b6 . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds ex I1, I2 being Integer st ( I1 = b6 . i & I2 = b6 . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) ) ); theorem :: RADIX_2:16 for n being Nat st n >= 1 holds for q being Integer for ic, f, k being Nat st ic is_represented_by n,k & f > 0 holds for c being Tuple of n,k -SD st c = DecSD (ic,n,k) holds (Mul_mod (q,c,f,k)) . n = (q * ic) mod f proofend; begin :: radix-2^k SD numbers and its correctness definition let n, f, j, m be Nat; let 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; correctness coherence (m |^ (e /. j)) mod f is Element of NAT ; ; end; :: deftheorem defines Table2 RADIX_2:def_8_:_ for n, f, j, m being Nat for e being Tuple of n, NAT holds Table2 (m,e,f,j) = (m |^ (e /. j)) mod f; definition let k, f, m, n be Nat; let e be Tuple of n, NAT ; assume A1: n >= 1 ; func Pow_mod (m,e,f,k) -> Tuple of n, NAT means :Def9: :: RADIX_2:def 9 ( it . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds ex i1, i2 being Nat st ( i1 = it . i & i2 = it . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) ); existence ex b1 being Tuple of n, NAT st ( b1 . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds ex i1, i2 being Nat st ( i1 = b1 . i & i2 = b1 . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) ) proofend; uniqueness for b1, b2 being Tuple of n, NAT st b1 . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds ex i1, i2 being Nat st ( i1 = b1 . i & i2 = b1 . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) & b2 . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds ex i1, i2 being Nat st ( i1 = b2 . i & i2 = b2 . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) holds b1 = b2 proofend; end; :: deftheorem Def9 defines Pow_mod RADIX_2:def_9_:_ for k, f, m, n being Nat for e being Tuple of n, NAT st n >= 1 holds for b6 being Tuple of n, NAT holds ( b6 = Pow_mod (m,e,f,k) iff ( b6 . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds ex i1, i2 being Nat st ( i1 = b6 . i & i2 = b6 . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) ) ); theorem :: RADIX_2:17 for n being Nat st n >= 1 holds for m, k, f, ie being Nat st ie is_represented_by n,k & f > 0 holds for e being Tuple of n, NAT st e = DecSD2 (ie,n,k) holds (Pow_mod (m,e,f,k)) . n = (m |^ ie) mod f proofend;