let n be non zero Nat; for lk being Nat
for Key1, Key2 being Matrix of lk,6,NAT
for r being 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 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
let lk be Nat; for Key1, Key2 being Matrix of lk,6,NAT
for r being 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 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
let Key1, Key2 be Matrix of lk,6,NAT; for r being 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 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
for m being FinSequence of NAT
for r being 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 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
proof
let m be
FinSequence of
NAT ;
for r being 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 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
defpred S1[
Nat]
means (
lk >= $1 &
(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
Nat st
i <= $1 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) ) ) implies
(compose (((IDEA_P_F (Key1,n,$1)) ^ (IDEA_Q_F (Key2,n,$1))),MESSAGES)) . m = m );
A1:
len (IDEA_P_F (Key1,n,0)) = 0
by Def17;
A2:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A3:
S1[
k]
;
S1[k + 1]
consider k1 being
Nat such that A4:
k1 = k + 1
;
A5:
dom (compose ((IDEA_P_F (Key1,n,k)),MESSAGES)) = MESSAGES
by Th43;
A6:
rng (compose ((IDEA_P_F (Key1,n,k)),MESSAGES)) c= MESSAGES
by Th43;
A7:
m in MESSAGES
by FINSEQ_1:def 11;
then
(compose ((IDEA_P_F (Key1,n,k)),MESSAGES)) . m in rng (compose ((IDEA_P_F (Key1,n,k)),MESSAGES))
by A5, FUNCT_1:def 3;
then reconsider M =
(compose ((IDEA_P_F (Key1,n,k)),MESSAGES)) . m as
FinSequence of
NAT by A6, FINSEQ_1:def 11;
assume that A8:
lk >= k + 1
and A9:
(2 to_power n) + 1 is
prime
and A10:
(
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 )
and A11:
for
i being
Nat st
i <= k + 1 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) )
;
(compose (((IDEA_P_F (Key1,n,(k + 1))) ^ (IDEA_Q_F (Key2,n,(k + 1)))),MESSAGES)) . m = m
A12:
(
len M >= 4 &
M . 1
is_expressible_by n )
by A10, Th45;
A13:
width Key1 = 6
by A8, MATRIX_0:23;
then
1
in Seg (width Key1)
by FINSEQ_1:1;
then A14:
(Line (Key1,(k + 1))) . 1
= Key1 * (
k1,1)
by A4, MATRIX_0:def 7;
then A15:
(Line (Key1,(k + 1))) . 1
is_expressible_by n
by A11, A4;
A16:
width Key2 = 6
by A8, MATRIX_0:23;
then
5
in Seg (width Key2)
by FINSEQ_1:1;
then A17:
(Line (Key2,(k + 1))) . 5
= Key2 * (
k1,5)
by A4, MATRIX_0:def 7;
3
in Seg (width Key1)
by A13, FINSEQ_1:1;
then A18:
(Line (Key1,(k + 1))) . 3
= Key1 * (
k1,3)
by A4, MATRIX_0:def 7;
then A19:
(Line (Key1,(k + 1))) . 3
is_expressible_by n
by A11, A4;
2
in Seg (width Key1)
by A13, FINSEQ_1:1;
then A20:
(Line (Key1,(k + 1))) . 2
= Key1 * (
k1,2)
by A4, MATRIX_0:def 7;
then A21:
(Line (Key1,(k + 1))) . 2
is_expressible_by n
by A11, A4;
3
in Seg (width Key2)
by A16, FINSEQ_1:1;
then
(Line (Key2,(k + 1))) . 3
= Key2 * (
k1,3)
by A4, MATRIX_0:def 7;
then A22:
(Line (Key2,(k + 1))) . 3
= NEG_MOD (
((Line (Key1,(k + 1))) . 2),
n)
by A11, A4, A20;
2
in Seg (width Key2)
by A16, FINSEQ_1:1;
then
(Line (Key2,(k + 1))) . 2
= Key2 * (
k1,2)
by A4, MATRIX_0:def 7;
then A23:
(Line (Key2,(k + 1))) . 2
= NEG_MOD (
((Line (Key1,(k + 1))) . 3),
n)
by A11, A4, A18;
5
in Seg (width Key1)
by A13, FINSEQ_1:1;
then
(Line (Key1,(k + 1))) . 5
= Key1 * (
k1,5)
by A4, MATRIX_0:def 7;
then A24:
(Line (Key2,(k + 1))) . 5
= (Line (Key1,(k + 1))) . 5
by A11, A4, A17;
A25:
M . 4
is_expressible_by n
by A10, Th45;
A26:
(
M . 2
is_expressible_by n &
M . 3
is_expressible_by n )
by A10, Th45;
4
in Seg (width Key1)
by A13, FINSEQ_1:1;
then A27:
(Line (Key1,(k + 1))) . 4
= Key1 * (
k1,4)
by A4, MATRIX_0:def 7;
then A28:
(Line (Key1,(k + 1))) . 4
is_expressible_by n
by A11, A4;
4
in Seg (width Key2)
by A16, FINSEQ_1:1;
then
(Line (Key2,(k + 1))) . 4
= Key2 * (
k1,4)
by A4, MATRIX_0:def 7;
then A29:
(Line (Key2,(k + 1))) . 4
= INV_MOD (
((Line (Key1,(k + 1))) . 4),
n)
by A11, A4, A27;
6
in Seg (width Key2)
by A16, FINSEQ_1:1;
then A30:
(Line (Key2,(k + 1))) . 6
= Key2 * (
k1,6)
by A4, MATRIX_0:def 7;
6
in Seg (width Key1)
by A13, FINSEQ_1:1;
then
(Line (Key1,(k + 1))) . 6
= Key1 * (
k1,6)
by A4, MATRIX_0:def 7;
then A31:
(Line (Key2,(k + 1))) . 6
= (Line (Key1,(k + 1))) . 6
by A11, A4, A30;
dom ((IDEA_Q ((Line (Key2,(k + 1))),n)) * (IDEA_P ((Line (Key1,(k + 1))),n))) = MESSAGES
by FUNCT_2:def 1;
then A32:
dom (((IDEA_Q ((Line (Key2,(k + 1))),n)) * (IDEA_P ((Line (Key1,(k + 1))),n))) * (compose ((IDEA_P_F (Key1,n,k)),MESSAGES))) = MESSAGES
by A6, A5, RELAT_1:27;
rng (compose (((IDEA_P_F (Key1,n,k)) ^ (<*(IDEA_P ((Line (Key1,(k + 1))),n))*> ^ <*(IDEA_Q ((Line (Key2,(k + 1))),n))*>)),MESSAGES)) =
rng (compose ((((IDEA_P_F (Key1,n,k)) ^ <*(IDEA_P ((Line (Key1,(k + 1))),n))*>) ^ <*(IDEA_Q ((Line (Key2,(k + 1))),n))*>),MESSAGES))
by FINSEQ_1:32
.=
rng ((IDEA_Q ((Line (Key2,(k + 1))),n)) * (compose (((IDEA_P_F (Key1,n,k)) ^ <*(IDEA_P ((Line (Key1,(k + 1))),n))*>),MESSAGES)))
by FUNCT_7:41
;
then A33:
rng (compose (((IDEA_P_F (Key1,n,k)) ^ (<*(IDEA_P ((Line (Key1,(k + 1))),n))*> ^ <*(IDEA_Q ((Line (Key2,(k + 1))),n))*>)),MESSAGES)) c= MESSAGES
by RELAT_1:def 19;
1
in Seg (width Key2)
by A16, FINSEQ_1:1;
then
(Line (Key2,(k + 1))) . 1
= Key2 * (
k1,1)
by A4, MATRIX_0:def 7;
then A34:
(Line (Key2,(k + 1))) . 1
= INV_MOD (
((Line (Key1,(k + 1))) . 1),
n)
by A11, A4, A14;
A35:
k + 1
>= k
by NAT_1:11;
A36:
for
i being
Nat st
i <= k 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) )
proof
let i be
Nat;
( i <= k implies ( 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) ) )
assume
i <= k
;
( 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) )
then
i <= k + 1
by A35, XXREAL_0:2;
hence
(
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) )
by A11;
verum
end;
(compose (((IDEA_P_F (Key1,n,(k + 1))) ^ (IDEA_Q_F (Key2,n,(k + 1)))),MESSAGES)) . m =
(compose ((((IDEA_P_F (Key1,n,k)) ^ <*(IDEA_P ((Line (Key1,(k + 1))),n))*>) ^ (IDEA_Q_F (Key2,n,(k + 1)))),MESSAGES)) . m
by Th36
.=
(compose ((((IDEA_P_F (Key1,n,k)) ^ <*(IDEA_P ((Line (Key1,(k + 1))),n))*>) ^ (<*(IDEA_Q ((Line (Key2,(k + 1))),n))*> ^ (IDEA_Q_F (Key2,n,k)))),MESSAGES)) . m
by Th37
.=
(compose (((((IDEA_P_F (Key1,n,k)) ^ <*(IDEA_P ((Line (Key1,(k + 1))),n))*>) ^ <*(IDEA_Q ((Line (Key2,(k + 1))),n))*>) ^ (IDEA_Q_F (Key2,n,k))),MESSAGES)) . m
by FINSEQ_1:32
.=
(compose ((((IDEA_P_F (Key1,n,k)) ^ (<*(IDEA_P ((Line (Key1,(k + 1))),n))*> ^ <*(IDEA_Q ((Line (Key2,(k + 1))),n))*>)) ^ (IDEA_Q_F (Key2,n,k))),MESSAGES)) . m
by FINSEQ_1:32
.=
((compose ((IDEA_Q_F (Key2,n,k)),MESSAGES)) * (compose (((IDEA_P_F (Key1,n,k)) ^ (<*(IDEA_P ((Line (Key1,(k + 1))),n))*> ^ <*(IDEA_Q ((Line (Key2,(k + 1))),n))*>)),MESSAGES))) . m
by A33, FUNCT_7:48
.=
((compose ((IDEA_Q_F (Key2,n,k)),MESSAGES)) * ((compose ((<*(IDEA_P ((Line (Key1,(k + 1))),n))*> ^ <*(IDEA_Q ((Line (Key2,(k + 1))),n))*>),MESSAGES)) * (compose ((IDEA_P_F (Key1,n,k)),MESSAGES)))) . m
by A6, FUNCT_7:48
.=
((compose ((IDEA_Q_F (Key2,n,k)),MESSAGES)) * ((compose (<*(IDEA_P ((Line (Key1,(k + 1))),n)),(IDEA_Q ((Line (Key2,(k + 1))),n))*>,MESSAGES)) * (compose ((IDEA_P_F (Key1,n,k)),MESSAGES)))) . m
by FINSEQ_1:def 9
.=
((compose ((IDEA_Q_F (Key2,n,k)),MESSAGES)) * ((((IDEA_Q ((Line (Key2,(k + 1))),n)) * (IDEA_P ((Line (Key1,(k + 1))),n))) * (id MESSAGES)) * (compose ((IDEA_P_F (Key1,n,k)),MESSAGES)))) . m
by FUNCT_7:51
.=
((compose ((IDEA_Q_F (Key2,n,k)),MESSAGES)) * (((IDEA_Q ((Line (Key2,(k + 1))),n)) * (IDEA_P ((Line (Key1,(k + 1))),n))) * (compose ((IDEA_P_F (Key1,n,k)),MESSAGES)))) . m
by FUNCT_2:17
.=
(compose ((IDEA_Q_F (Key2,n,k)),MESSAGES)) . ((((IDEA_Q ((Line (Key2,(k + 1))),n)) * (IDEA_P ((Line (Key1,(k + 1))),n))) * (compose ((IDEA_P_F (Key1,n,k)),MESSAGES))) . m)
by A32, A7, FUNCT_1:13
.=
(compose ((IDEA_Q_F (Key2,n,k)),MESSAGES)) . (((IDEA_Q ((Line (Key2,(k + 1))),n)) * (IDEA_P ((Line (Key1,(k + 1))),n))) . ((compose ((IDEA_P_F (Key1,n,k)),MESSAGES)) . m))
by A5, A7, FUNCT_1:13
.=
(compose ((IDEA_Q_F (Key2,n,k)),MESSAGES)) . ((compose ((IDEA_P_F (Key1,n,k)),MESSAGES)) . m)
by A9, A12, A26, A25, A15, A21, A19, A28, A34, A23, A22, A29, A24, A31, Th33
.=
((compose ((IDEA_Q_F (Key2,n,k)),MESSAGES)) * (compose ((IDEA_P_F (Key1,n,k)),MESSAGES))) . m
by A5, A7, FUNCT_1:13
.=
m
by A3, A8, A9, A10, A35, A36, A6, FUNCT_7:48, XXREAL_0:2
;
hence
(compose (((IDEA_P_F (Key1,n,(k + 1))) ^ (IDEA_Q_F (Key2,n,(k + 1)))),MESSAGES)) . m = m
;
verum
end;
len (IDEA_Q_F (Key2,n,0)) = 0
by Def18;
then
IDEA_Q_F (
Key2,
n,
0)
= {}
;
then (IDEA_P_F (Key1,n,0)) ^ (IDEA_Q_F (Key2,n,0)) =
IDEA_P_F (
Key1,
n,
0)
by FINSEQ_1:34
.=
{}
by A1
;
then
(
m in MESSAGES &
compose (
((IDEA_P_F (Key1,n,0)) ^ (IDEA_Q_F (Key2,n,0))),
MESSAGES)
= id MESSAGES )
by FINSEQ_1:def 11, FUNCT_7:39;
then A37:
S1[
0 ]
by FUNCT_1:18;
thus
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A37, A2); verum
end;
hence
for r being 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 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
; verum