begin
Lm1:
for i, j being Element of NAT st i <> 0 & i < j & j is prime holds
i,j are_relative_prime
Lm2:
for j, i, k being Element of NAT st j is prime & i < j & k < j & i <> 0 holds
ex a being Element of NAT st (a * i) mod j = k
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
begin
:: deftheorem defines ZERO IDEA_1:def 1 :
for n being Element of NAT holds ZERO n = n |-> FALSE;
:: deftheorem Def2 defines 'xor' IDEA_1:def 2 :
for n being Element of NAT
for x, y, b4 being Tuple of n, BOOLEAN holds
( b4 = x 'xor' y iff for i being Element of NAT st i in Seg n holds
b4 /. i = (x /. i) 'xor' (y /. i) );
theorem
canceled;
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
:: deftheorem Def3 defines is_expressible_by IDEA_1:def 3 :
for n, i being Element of NAT holds
( i is_expressible_by n iff i < 2 to_power n );
theorem
:: deftheorem defines ADD_MOD IDEA_1:def 4 :
for n being Element of NAT
for i, j being Nat holds ADD_MOD (i,j,n) = (i + j) mod (2 to_power n);
:: deftheorem Def5 defines NEG_N IDEA_1:def 5 :
for n, i being Element of NAT st i is_expressible_by n holds
NEG_N (i,n) = (2 to_power n) - i;
:: deftheorem defines NEG_MOD IDEA_1:def 6 :
for n, i being Element of NAT holds NEG_MOD (i,n) = (NEG_N (i,n)) mod (2 to_power n);
theorem Th12:
theorem
theorem Th14:
theorem Th15:
for
i,
j,
n,
k being
Element of
NAT holds
ADD_MOD (
(ADD_MOD (i,j,n)),
k,
n)
= ADD_MOD (
i,
(ADD_MOD (j,k,n)),
n)
theorem Th16:
theorem
:: deftheorem Def7 defines ChangeVal_1 IDEA_1:def 7 :
for n, i being Nat holds
( ( i = 0 implies ChangeVal_1 (i,n) = 2 to_power n ) & ( not i = 0 implies ChangeVal_1 (i,n) = i ) );
theorem Th18:
theorem Th19:
:: deftheorem Def8 defines ChangeVal_2 IDEA_1:def 8 :
for n, i being Element of NAT holds
( ( i = 2 to_power n implies ChangeVal_2 (i,n) = 0 ) & ( not i = 2 to_power n implies ChangeVal_2 (i,n) = i ) );
theorem
theorem Th21:
:: deftheorem defines MUL_MOD IDEA_1:def 9 :
for n being Element of NAT
for i, j being Nat holds MUL_MOD (i,j,n) = ChangeVal_2 ((((ChangeVal_1 (i,n)) * (ChangeVal_1 (j,n))) mod ((2 to_power n) + 1)),n);
definition
let n be non
empty Element of
NAT ;
let i be
Element of
NAT ;
assume that A1:
i is_expressible_by n
and A2:
(2 to_power n) + 1 is
prime
;
func INV_MOD (
i,
n)
-> Element of
NAT means :
Def10:
(
MUL_MOD (
i,
it,
n)
= 1 &
it is_expressible_by n );
existence
ex b1 being Element of NAT st
( MUL_MOD (i,b1,n) = 1 & b1 is_expressible_by n )
uniqueness
for b1, b2 being Element of NAT st MUL_MOD (i,b1,n) = 1 & b1 is_expressible_by n & MUL_MOD (i,b2,n) = 1 & b2 is_expressible_by n holds
b1 = b2
end;
:: deftheorem Def10 defines INV_MOD IDEA_1:def 10 :
for n being non empty Element of NAT
for i being Element of NAT st i is_expressible_by n & (2 to_power n) + 1 is prime holds
for b3 being Element of NAT holds
( b3 = INV_MOD (i,n) iff ( MUL_MOD (i,b3,n) = 1 & b3 is_expressible_by n ) );
theorem
theorem Th23:
theorem Th24:
for
n,
i,
j,
k being
Element of
NAT st
(2 to_power n) + 1 is
prime &
i is_expressible_by n &
j is_expressible_by n &
k is_expressible_by n holds
MUL_MOD (
(MUL_MOD (i,j,n)),
k,
n)
= MUL_MOD (
i,
(MUL_MOD (j,k,n)),
n)
theorem Th25:
theorem
begin
definition
let n be
Element of
NAT ;
let m,
k be
FinSequence of
NAT ;
func IDEAoperationA (
m,
k,
n)
-> FinSequence of
NAT means :
Def11:
(
len it = len m & ( for
i being
Element of
NAT st
i in dom m holds
( (
i = 1 implies
it . i = MUL_MOD (
(m . 1),
(k . 1),
n) ) & (
i = 2 implies
it . i = ADD_MOD (
(m . 2),
(k . 2),
n) ) & (
i = 3 implies
it . i = ADD_MOD (
(m . 3),
(k . 3),
n) ) & (
i = 4 implies
it . i = MUL_MOD (
(m . 4),
(k . 4),
n) ) & (
i <> 1 &
i <> 2 &
i <> 3 &
i <> 4 implies
it . i = m . i ) ) ) );
existence
ex b1 being FinSequence of NAT st
( len b1 = len m & ( for i being Element of NAT st i in dom m holds
( ( i = 1 implies b1 . i = MUL_MOD ((m . 1),(k . 1),n) ) & ( i = 2 implies b1 . i = ADD_MOD ((m . 2),(k . 2),n) ) & ( i = 3 implies b1 . i = ADD_MOD ((m . 3),(k . 3),n) ) & ( i = 4 implies b1 . i = MUL_MOD ((m . 4),(k . 4),n) ) & ( i <> 1 & i <> 2 & i <> 3 & i <> 4 implies b1 . i = m . i ) ) ) )
uniqueness
for b1, b2 being FinSequence of NAT st len b1 = len m & ( for i being Element of NAT st i in dom m holds
( ( i = 1 implies b1 . i = MUL_MOD ((m . 1),(k . 1),n) ) & ( i = 2 implies b1 . i = ADD_MOD ((m . 2),(k . 2),n) ) & ( i = 3 implies b1 . i = ADD_MOD ((m . 3),(k . 3),n) ) & ( i = 4 implies b1 . i = MUL_MOD ((m . 4),(k . 4),n) ) & ( i <> 1 & i <> 2 & i <> 3 & i <> 4 implies b1 . i = m . i ) ) ) & len b2 = len m & ( for i being Element of NAT st i in dom m holds
( ( i = 1 implies b2 . i = MUL_MOD ((m . 1),(k . 1),n) ) & ( i = 2 implies b2 . i = ADD_MOD ((m . 2),(k . 2),n) ) & ( i = 3 implies b2 . i = ADD_MOD ((m . 3),(k . 3),n) ) & ( i = 4 implies b2 . i = MUL_MOD ((m . 4),(k . 4),n) ) & ( i <> 1 & i <> 2 & i <> 3 & i <> 4 implies b2 . i = m . i ) ) ) holds
b1 = b2
end;
:: deftheorem Def11 defines IDEAoperationA IDEA_1:def 11 :
for n being Element of NAT
for m, k, b4 being FinSequence of NAT holds
( b4 = IDEAoperationA (m,k,n) iff ( len b4 = len m & ( for i being Element of NAT st i in dom m holds
( ( i = 1 implies b4 . i = MUL_MOD ((m . 1),(k . 1),n) ) & ( i = 2 implies b4 . i = ADD_MOD ((m . 2),(k . 2),n) ) & ( i = 3 implies b4 . i = ADD_MOD ((m . 3),(k . 3),n) ) & ( i = 4 implies b4 . i = MUL_MOD ((m . 4),(k . 4),n) ) & ( i <> 1 & i <> 2 & i <> 3 & i <> 4 implies b4 . i = m . i ) ) ) ) );
definition
let n be non
empty Element of
NAT ;
let m,
k be
FinSequence of
NAT ;
func IDEAoperationB (
m,
k,
n)
-> FinSequence of
NAT means :
Def12:
(
len it = len m & ( for
i being
Element of
NAT st
i in dom m holds
( (
i = 1 implies
it . i = Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)))) ) & (
i = 2 implies
it . i = Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)),n)))) ) & (
i = 3 implies
it . i = Absval ((n -BinarySequence (m . 3)) 'xor' (n -BinarySequence (MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)))) ) & (
i = 4 implies
it . i = Absval ((n -BinarySequence (m . 4)) 'xor' (n -BinarySequence (ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)),n)))) ) & (
i <> 1 &
i <> 2 &
i <> 3 &
i <> 4 implies
it . i = m . i ) ) ) );
existence
ex b1 being FinSequence of NAT st
( len b1 = len m & ( for i being Element of NAT st i in dom m holds
( ( i = 1 implies b1 . i = Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)))) ) & ( i = 2 implies b1 . i = Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)),n)))) ) & ( i = 3 implies b1 . i = Absval ((n -BinarySequence (m . 3)) 'xor' (n -BinarySequence (MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)))) ) & ( i = 4 implies b1 . i = Absval ((n -BinarySequence (m . 4)) 'xor' (n -BinarySequence (ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)),n)))) ) & ( i <> 1 & i <> 2 & i <> 3 & i <> 4 implies b1 . i = m . i ) ) ) )
uniqueness
for b1, b2 being FinSequence of NAT st len b1 = len m & ( for i being Element of NAT st i in dom m holds
( ( i = 1 implies b1 . i = Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)))) ) & ( i = 2 implies b1 . i = Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)),n)))) ) & ( i = 3 implies b1 . i = Absval ((n -BinarySequence (m . 3)) 'xor' (n -BinarySequence (MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)))) ) & ( i = 4 implies b1 . i = Absval ((n -BinarySequence (m . 4)) 'xor' (n -BinarySequence (ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)),n)))) ) & ( i <> 1 & i <> 2 & i <> 3 & i <> 4 implies b1 . i = m . i ) ) ) & len b2 = len m & ( for i being Element of NAT st i in dom m holds
( ( i = 1 implies b2 . i = Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)))) ) & ( i = 2 implies b2 . i = Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)),n)))) ) & ( i = 3 implies b2 . i = Absval ((n -BinarySequence (m . 3)) 'xor' (n -BinarySequence (MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)))) ) & ( i = 4 implies b2 . i = Absval ((n -BinarySequence (m . 4)) 'xor' (n -BinarySequence (ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)),n)))) ) & ( i <> 1 & i <> 2 & i <> 3 & i <> 4 implies b2 . i = m . i ) ) ) holds
b1 = b2
end;
:: deftheorem Def12 defines IDEAoperationB IDEA_1:def 12 :
for n being non empty Element of NAT
for m, k, b4 being FinSequence of NAT holds
( b4 = IDEAoperationB (m,k,n) iff ( len b4 = len m & ( for i being Element of NAT st i in dom m holds
( ( i = 1 implies b4 . i = Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)))) ) & ( i = 2 implies b4 . i = Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)),n)))) ) & ( i = 3 implies b4 . i = Absval ((n -BinarySequence (m . 3)) 'xor' (n -BinarySequence (MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)))) ) & ( i = 4 implies b4 . i = Absval ((n -BinarySequence (m . 4)) 'xor' (n -BinarySequence (ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)),n)))) ) & ( i <> 1 & i <> 2 & i <> 3 & i <> 4 implies b4 . i = m . i ) ) ) ) );
definition
let m be
FinSequence of
NAT ;
func IDEAoperationC m -> FinSequence of
NAT means :
Def13:
(
len it = len m & ( for
i being
Element of
NAT st
i in dom m holds
it . i = IFEQ (
i,2,
(m . 3),
(IFEQ (i,3,(m . 2),(m . i)))) ) );
existence
ex b1 being FinSequence of NAT st
( len b1 = len m & ( for i being Element of NAT st i in dom m holds
b1 . i = IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) ) )
uniqueness
for b1, b2 being FinSequence of NAT st len b1 = len m & ( for i being Element of NAT st i in dom m holds
b1 . i = IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) ) & len b2 = len m & ( for i being Element of NAT st i in dom m holds
b2 . i = IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) ) holds
b1 = b2
end;
:: deftheorem Def13 defines IDEAoperationC IDEA_1:def 13 :
for m, b2 being FinSequence of NAT holds
( b2 = IDEAoperationC m iff ( len b2 = len m & ( for i being Element of NAT st i in dom m holds
b2 . i = IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) ) ) );
theorem Th27:
theorem Th28:
Lm3:
for m being FinSequence of NAT
for i being Element of NAT st i = 2 & i in dom m holds
(IDEAoperationC m) . i = m . 3
Lm4:
for m being FinSequence of NAT
for i being Element of NAT st i = 3 & i in dom m holds
(IDEAoperationC m) . i = m . 2
Lm5:
for m being FinSequence of NAT
for i being Element of NAT st i <> 2 & i <> 3 & i in dom m holds
(IDEAoperationC m) . i = m . i
theorem
theorem Th30:
for
n being non
empty Element of
NAT for
m,
k1,
k2 being
FinSequence of
NAT st
(2 to_power n) + 1 is
prime &
len m >= 4 &
m . 1
is_expressible_by n &
m . 2
is_expressible_by n &
m . 3
is_expressible_by n &
m . 4
is_expressible_by n &
k1 . 1
is_expressible_by n &
k1 . 2
is_expressible_by n &
k1 . 3
is_expressible_by n &
k1 . 4
is_expressible_by n &
k2 . 1
= INV_MOD (
(k1 . 1),
n) &
k2 . 2
= NEG_MOD (
(k1 . 2),
n) &
k2 . 3
= NEG_MOD (
(k1 . 3),
n) &
k2 . 4
= INV_MOD (
(k1 . 4),
n) holds
IDEAoperationA (
(IDEAoperationA (m,k1,n)),
k2,
n)
= m
theorem Th31:
for
n being non
empty Element of
NAT for
m,
k1,
k2 being
FinSequence of
NAT st
(2 to_power n) + 1 is
prime &
len m >= 4 &
m . 1
is_expressible_by n &
m . 2
is_expressible_by n &
m . 3
is_expressible_by n &
m . 4
is_expressible_by n &
k1 . 1
is_expressible_by n &
k1 . 2
is_expressible_by n &
k1 . 3
is_expressible_by n &
k1 . 4
is_expressible_by n &
k2 . 1
= INV_MOD (
(k1 . 1),
n) &
k2 . 2
= NEG_MOD (
(k1 . 3),
n) &
k2 . 3
= NEG_MOD (
(k1 . 2),
n) &
k2 . 4
= INV_MOD (
(k1 . 4),
n) holds
IDEAoperationA (
(IDEAoperationC (IDEAoperationA ((IDEAoperationC m),k1,n))),
k2,
n)
= m
theorem Th32:
theorem
begin
:: deftheorem defines MESSAGES IDEA_1:def 14 :
MESSAGES = NAT * ;
definition
let n be non
empty Element of
NAT ;
let k be
FinSequence of
NAT ;
func IDEA_P (
k,
n)
-> Function of
MESSAGES,
MESSAGES means :
Def15:
for
m being
FinSequence of
NAT holds
it . m = IDEAoperationA (
(IDEAoperationC (IDEAoperationB (m,k,n))),
k,
n);
existence
ex b1 being Function of MESSAGES,MESSAGES st
for m being FinSequence of NAT holds b1 . m = IDEAoperationA ((IDEAoperationC (IDEAoperationB (m,k,n))),k,n)
uniqueness
for b1, b2 being Function of MESSAGES,MESSAGES st ( for m being FinSequence of NAT holds b1 . m = IDEAoperationA ((IDEAoperationC (IDEAoperationB (m,k,n))),k,n) ) & ( for m being FinSequence of NAT holds b2 . m = IDEAoperationA ((IDEAoperationC (IDEAoperationB (m,k,n))),k,n) ) holds
b1 = b2
end;
:: deftheorem Def15 defines IDEA_P IDEA_1:def 15 :
for n being non empty Element of NAT
for k being FinSequence of NAT
for b3 being Function of MESSAGES,MESSAGES holds
( b3 = IDEA_P (k,n) iff for m being FinSequence of NAT holds b3 . m = IDEAoperationA ((IDEAoperationC (IDEAoperationB (m,k,n))),k,n) );
definition
let n be non
empty Element of
NAT ;
let k be
FinSequence of
NAT ;
func IDEA_Q (
k,
n)
-> Function of
MESSAGES,
MESSAGES means :
Def16:
for
m being
FinSequence of
NAT holds
it . m = IDEAoperationB (
(IDEAoperationA ((IDEAoperationC m),k,n)),
k,
n);
existence
ex b1 being Function of MESSAGES,MESSAGES st
for m being FinSequence of NAT holds b1 . m = IDEAoperationB ((IDEAoperationA ((IDEAoperationC m),k,n)),k,n)
uniqueness
for b1, b2 being Function of MESSAGES,MESSAGES st ( for m being FinSequence of NAT holds b1 . m = IDEAoperationB ((IDEAoperationA ((IDEAoperationC m),k,n)),k,n) ) & ( for m being FinSequence of NAT holds b2 . m = IDEAoperationB ((IDEAoperationA ((IDEAoperationC m),k,n)),k,n) ) holds
b1 = b2
end;
:: deftheorem Def16 defines IDEA_Q IDEA_1:def 16 :
for n being non empty Element of NAT
for k being FinSequence of NAT
for b3 being Function of MESSAGES,MESSAGES holds
( b3 = IDEA_Q (k,n) iff for m being FinSequence of NAT holds b3 . m = IDEAoperationB ((IDEAoperationA ((IDEAoperationC m),k,n)),k,n) );
definition
let r,
lk be
Element of
NAT ;
let n be non
empty Element of
NAT ;
let Key be
Matrix of
lk,6,
NAT ;
func IDEA_P_F (
Key,
n,
r)
-> FinSequence means :
Def17:
(
len it = r & ( for
i being
Element of
NAT st
i in dom it holds
it . i = IDEA_P (
(Line (Key,i)),
n) ) );
existence
ex b1 being FinSequence st
( len b1 = r & ( for i being Element of NAT st i in dom b1 holds
b1 . i = IDEA_P ((Line (Key,i)),n) ) )
uniqueness
for b1, b2 being FinSequence st len b1 = r & ( for i being Element of NAT st i in dom b1 holds
b1 . i = IDEA_P ((Line (Key,i)),n) ) & len b2 = r & ( for i being Element of NAT st i in dom b2 holds
b2 . i = IDEA_P ((Line (Key,i)),n) ) holds
b1 = b2
end;
:: deftheorem Def17 defines IDEA_P_F IDEA_1:def 17 :
for r, lk being Element of NAT
for n being non empty Element of NAT
for Key being Matrix of lk,6, NAT
for b5 being FinSequence holds
( b5 = IDEA_P_F (Key,n,r) iff ( len b5 = r & ( for i being Element of NAT st i in dom b5 holds
b5 . i = IDEA_P ((Line (Key,i)),n) ) ) );
definition
let r,
lk be
Element of
NAT ;
let n be non
empty Element of
NAT ;
let Key be
Matrix of
lk,6,
NAT ;
func IDEA_Q_F (
Key,
n,
r)
-> FinSequence means :
Def18:
(
len it = r & ( for
i being
Element of
NAT st
i in dom it holds
it . i = IDEA_Q (
(Line (Key,((r -' i) + 1))),
n) ) );
existence
ex b1 being FinSequence st
( len b1 = r & ( for i being Element of NAT st i in dom b1 holds
b1 . i = IDEA_Q ((Line (Key,((r -' i) + 1))),n) ) )
uniqueness
for b1, b2 being FinSequence st len b1 = r & ( for i being Element of NAT st i in dom b1 holds
b1 . i = IDEA_Q ((Line (Key,((r -' i) + 1))),n) ) & len b2 = r & ( for i being Element of NAT st i in dom b2 holds
b2 . i = IDEA_Q ((Line (Key,((r -' i) + 1))),n) ) holds
b1 = b2
end;
:: deftheorem Def18 defines IDEA_Q_F IDEA_1:def 18 :
for r, lk being Element of NAT
for n being non empty Element of NAT
for Key being Matrix of lk,6, NAT
for b5 being FinSequence holds
( b5 = IDEA_Q_F (Key,n,r) iff ( len b5 = r & ( for i being Element of NAT st i in dom b5 holds
b5 . i = IDEA_Q ((Line (Key,((r -' i) + 1))),n) ) ) );
definition
let k be
FinSequence of
NAT ;
let n be
Element of
NAT ;
func IDEA_PS (
k,
n)
-> Function of
MESSAGES,
MESSAGES means :
Def19:
for
m being
FinSequence of
NAT holds
it . m = IDEAoperationA (
m,
k,
n);
existence
ex b1 being Function of MESSAGES,MESSAGES st
for m being FinSequence of NAT holds b1 . m = IDEAoperationA (m,k,n)
uniqueness
for b1, b2 being Function of MESSAGES,MESSAGES st ( for m being FinSequence of NAT holds b1 . m = IDEAoperationA (m,k,n) ) & ( for m being FinSequence of NAT holds b2 . m = IDEAoperationA (m,k,n) ) holds
b1 = b2
end;
:: deftheorem Def19 defines IDEA_PS IDEA_1:def 19 :
for k being FinSequence of NAT
for n being Element of NAT
for b3 being Function of MESSAGES,MESSAGES holds
( b3 = IDEA_PS (k,n) iff for m being FinSequence of NAT holds b3 . m = IDEAoperationA (m,k,n) );
definition
let k be
FinSequence of
NAT ;
let n be
Element of
NAT ;
func IDEA_QS (
k,
n)
-> Function of
MESSAGES,
MESSAGES means :
Def20:
for
m being
FinSequence of
NAT holds
it . m = IDEAoperationA (
m,
k,
n);
existence
ex b1 being Function of MESSAGES,MESSAGES st
for m being FinSequence of NAT holds b1 . m = IDEAoperationA (m,k,n)
uniqueness
for b1, b2 being Function of MESSAGES,MESSAGES st ( for m being FinSequence of NAT holds b1 . m = IDEAoperationA (m,k,n) ) & ( for m being FinSequence of NAT holds b2 . m = IDEAoperationA (m,k,n) ) holds
b1 = b2
end;
:: deftheorem Def20 defines IDEA_QS IDEA_1:def 20 :
for k being FinSequence of NAT
for n being Element of NAT
for b3 being Function of MESSAGES,MESSAGES holds
( b3 = IDEA_QS (k,n) iff for m being FinSequence of NAT holds b3 . m = IDEAoperationA (m,k,n) );
definition
let n be non
empty Element of
NAT ;
let k be
FinSequence of
NAT ;
func IDEA_PE (
k,
n)
-> Function of
MESSAGES,
MESSAGES means :
Def21:
for
m being
FinSequence of
NAT holds
it . m = IDEAoperationA (
(IDEAoperationB (m,k,n)),
k,
n);
existence
ex b1 being Function of MESSAGES,MESSAGES st
for m being FinSequence of NAT holds b1 . m = IDEAoperationA ((IDEAoperationB (m,k,n)),k,n)
uniqueness
for b1, b2 being Function of MESSAGES,MESSAGES st ( for m being FinSequence of NAT holds b1 . m = IDEAoperationA ((IDEAoperationB (m,k,n)),k,n) ) & ( for m being FinSequence of NAT holds b2 . m = IDEAoperationA ((IDEAoperationB (m,k,n)),k,n) ) holds
b1 = b2
end;
:: deftheorem Def21 defines IDEA_PE IDEA_1:def 21 :
for n being non empty Element of NAT
for k being FinSequence of NAT
for b3 being Function of MESSAGES,MESSAGES holds
( b3 = IDEA_PE (k,n) iff for m being FinSequence of NAT holds b3 . m = IDEAoperationA ((IDEAoperationB (m,k,n)),k,n) );
definition
let n be non
empty Element of
NAT ;
let k be
FinSequence of
NAT ;
func IDEA_QE (
k,
n)
-> Function of
MESSAGES,
MESSAGES means :
Def22:
for
m being
FinSequence of
NAT holds
it . m = IDEAoperationB (
(IDEAoperationA (m,k,n)),
k,
n);
existence
ex b1 being Function of MESSAGES,MESSAGES st
for m being FinSequence of NAT holds b1 . m = IDEAoperationB ((IDEAoperationA (m,k,n)),k,n)
uniqueness
for b1, b2 being Function of MESSAGES,MESSAGES st ( for m being FinSequence of NAT holds b1 . m = IDEAoperationB ((IDEAoperationA (m,k,n)),k,n) ) & ( for m being FinSequence of NAT holds b2 . m = IDEAoperationB ((IDEAoperationA (m,k,n)),k,n) ) holds
b1 = b2
end;
:: deftheorem Def22 defines IDEA_QE IDEA_1:def 22 :
for n being non empty Element of NAT
for k being FinSequence of NAT
for b3 being Function of MESSAGES,MESSAGES holds
( b3 = IDEA_QE (k,n) iff for m being FinSequence of NAT holds b3 . m = IDEAoperationB ((IDEAoperationA (m,k,n)),k,n) );
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem
theorem
canceled;
theorem Th47:
begin
theorem Th48:
for
n being non
empty Element of
NAT for
lk being
Element of
NAT for
Key1,
Key2 being
Matrix of
lk,6,
NAT for
r being
Element of
NAT for
m being
FinSequence of
NAT st
lk >= r &
(2 to_power n) + 1 is
prime &
len m >= 4 &
m . 1
is_expressible_by n &
m . 2
is_expressible_by n &
m . 3
is_expressible_by n &
m . 4
is_expressible_by n & ( for
i being
Element of
NAT st
i <= r holds
(
Key1 * (
i,1)
is_expressible_by n &
Key1 * (
i,2)
is_expressible_by n &
Key1 * (
i,3)
is_expressible_by n &
Key1 * (
i,4)
is_expressible_by n &
Key1 * (
i,5)
is_expressible_by n &
Key1 * (
i,6)
is_expressible_by n &
Key2 * (
i,1)
is_expressible_by n &
Key2 * (
i,2)
is_expressible_by n &
Key2 * (
i,3)
is_expressible_by n &
Key2 * (
i,4)
is_expressible_by n &
Key2 * (
i,5)
is_expressible_by n &
Key2 * (
i,6)
is_expressible_by n &
Key2 * (
i,1)
= INV_MOD (
(Key1 * (i,1)),
n) &
Key2 * (
i,2)
= NEG_MOD (
(Key1 * (i,3)),
n) &
Key2 * (
i,3)
= NEG_MOD (
(Key1 * (i,2)),
n) &
Key2 * (
i,4)
= INV_MOD (
(Key1 * (i,4)),
n) &
Key1 * (
i,5)
= Key2 * (
i,5) &
Key1 * (
i,6)
= Key2 * (
i,6) ) ) holds
(compose (((IDEA_P_F (Key1,n,r)) ^ (IDEA_Q_F (Key2,n,r))),MESSAGES)) . m = m
theorem
for
n being non
empty Element of
NAT for
lk being
Element of
NAT for
Key1,
Key2 being
Matrix of
lk,6,
NAT for
r being
Element of
NAT for
ks1,
ks2,
ke1,
ke2,
m being
FinSequence of
NAT st
lk >= r &
(2 to_power n) + 1 is
prime &
len m >= 4 &
m . 1
is_expressible_by n &
m . 2
is_expressible_by n &
m . 3
is_expressible_by n &
m . 4
is_expressible_by n & ( for
i being
Element of
NAT st
i <= r holds
(
Key1 * (
i,1)
is_expressible_by n &
Key1 * (
i,2)
is_expressible_by n &
Key1 * (
i,3)
is_expressible_by n &
Key1 * (
i,4)
is_expressible_by n &
Key1 * (
i,5)
is_expressible_by n &
Key1 * (
i,6)
is_expressible_by n &
Key2 * (
i,1)
is_expressible_by n &
Key2 * (
i,2)
is_expressible_by n &
Key2 * (
i,3)
is_expressible_by n &
Key2 * (
i,4)
is_expressible_by n &
Key2 * (
i,5)
is_expressible_by n &
Key2 * (
i,6)
is_expressible_by n &
Key2 * (
i,1)
= INV_MOD (
(Key1 * (i,1)),
n) &
Key2 * (
i,2)
= NEG_MOD (
(Key1 * (i,3)),
n) &
Key2 * (
i,3)
= NEG_MOD (
(Key1 * (i,2)),
n) &
Key2 * (
i,4)
= INV_MOD (
(Key1 * (i,4)),
n) &
Key1 * (
i,5)
= Key2 * (
i,5) &
Key1 * (
i,6)
= Key2 * (
i,6) ) ) &
ks1 . 1
is_expressible_by n &
ks1 . 2
is_expressible_by n &
ks1 . 3
is_expressible_by n &
ks1 . 4
is_expressible_by n &
ks2 . 1
= INV_MOD (
(ks1 . 1),
n) &
ks2 . 2
= NEG_MOD (
(ks1 . 2),
n) &
ks2 . 3
= NEG_MOD (
(ks1 . 3),
n) &
ks2 . 4
= INV_MOD (
(ks1 . 4),
n) &
ke1 . 1
is_expressible_by n &
ke1 . 2
is_expressible_by n &
ke1 . 3
is_expressible_by n &
ke1 . 4
is_expressible_by n &
ke2 . 1
= INV_MOD (
(ke1 . 1),
n) &
ke2 . 2
= NEG_MOD (
(ke1 . 2),
n) &
ke2 . 3
= NEG_MOD (
(ke1 . 3),
n) &
ke2 . 4
= INV_MOD (
(ke1 . 4),
n) &
ke2 . 5
= ke1 . 5 &
ke2 . 6
= ke1 . 6 holds
((IDEA_QS (ks2,n)) * ((compose ((IDEA_Q_F (Key2,n,r)),MESSAGES)) * ((IDEA_QE (ke2,n)) * ((IDEA_PE (ke1,n)) * ((compose ((IDEA_P_F (Key1,n,r)),MESSAGES)) * (IDEA_PS (ks1,n))))))) . m = m