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