let n be non zero Nat; :: thesis:
let lk be Nat; :: thesis:
let Key1, Key2 be Matrix of lk,6,NAT; :: thesis:
let r be Nat; :: thesis:
let ks1, ks2, ke1, ke2 be FinSequence of NAT ; :: thesis:
let m be FinSequence of NAT ; :: thesis:
assume that
A1: lk >= r and
A2: (2 to_power n) + 1 is prime and
A3: len m >= 4 and
A4: ( 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
A5: 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) ) and
A6: ( 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) ) and
A7: ( 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 ) ; :: thesis:
A8: m in MESSAGES by FINSEQ_1:def 11;
then (IDEA_PS (ks1,n)) . m in MESSAGES by FUNCT_2:5;
then reconsider m1 = (IDEA_PS (ks1,n)) . m as FinSequence of NAT by FINSEQ_1:def 11;
A9: m1 in MESSAGES by FINSEQ_1:def 11;
A10: len m1 = len (IDEAoperationA (m,ks1,n)) by Def19
.= len m by Def11 ;
m1 . 4 = (IDEAoperationA (m,ks1,n)) . 4 by Def19;
then A11: m1 . 4 is_expressible_by n by A3, Th26;
m1 . 3 = (IDEAoperationA (m,ks1,n)) . 3 by Def19;
then A12: m1 . 3 is_expressible_by n by A3, Th26;
m1 . 2 = (IDEAoperationA (m,ks1,n)) . 2 by Def19;
then A13: m1 . 2 is_expressible_by n by A3, Th26;
m1 . 1 = (IDEAoperationA (m,ks1,n)) . 1 by Def19;
then A14: m1 . 1 is_expressible_by n by A3, Th26;

per cases ;

suppose A15: r = 0 ; :: thesis:

then len (IDEA_Q_F (Key2,n,r)) = 0 by Def18;
then A16: IDEA_Q_F (Key2,n,r) = {} ;
len (IDEA_P_F (Key1,n,r)) = 0 by A15, Def17;
then IDEA_P_F (Key1,n,r) = {} ;
hence ((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 = ((IDEA_QS (ks2,n)) * ((compose ({},MESSAGES)) * ((IDEA_QE (ke2,n)) * ((IDEA_PE (ke1,n)) * ((compose ({},MESSAGES)) * (IDEA_PS (ks1,n))))))) . m by A16
.= ((IDEA_QS (ks2,n)) * ((id MESSAGES) * ((IDEA_QE (ke2,n)) * ((IDEA_PE (ke1,n)) * ((compose ({},MESSAGES)) * (IDEA_PS (ks1,n))))))) . m by FUNCT_7:39
.= ((IDEA_QS (ks2,n)) * ((id MESSAGES) * ((IDEA_QE (ke2,n)) * ((IDEA_PE (ke1,n)) * ((id MESSAGES) * (IDEA_PS (ks1,n))))))) . m by FUNCT_7:39
.= ((IDEA_QS (ks2,n)) * ((IDEA_QE (ke2,n)) * ((IDEA_PE (ke1,n)) * ((id MESSAGES) * (IDEA_PS (ks1,n)))))) . m by FUNCT_2:17
.= ((IDEA_QS (ks2,n)) * ((IDEA_QE (ke2,n)) * ((IDEA_PE (ke1,n)) * (IDEA_PS (ks1,n))))) . m by FUNCT_2:17
.= (IDEA_QS (ks2,n)) . (((IDEA_QE (ke2,n)) * ((IDEA_PE (ke1,n)) * (IDEA_PS (ks1,n)))) . m) by A8, FUNCT_2:15
.= (IDEA_QS (ks2,n)) . ((IDEA_QE (ke2,n)) . (((IDEA_PE (ke1,n)) * (IDEA_PS (ks1,n))) . m)) by A8, FUNCT_2:15
.= (IDEA_QS (ks2,n)) . ((IDEA_QE (ke2,n)) . ((IDEA_PE (ke1,n)) . m1)) by A8, FUNCT_2:15
.= (IDEA_QS (ks2,n)) . (((IDEA_QE (ke2,n)) * (IDEA_PE (ke1,n))) . m1) by A9, FUNCT_2:15
.= (IDEA_QS (ks2,n)) . ((IDEA_PS (ks1,n)) . m) by A2, A3, A7, A10, A14, A13, A12, A11, Th35
.= ((IDEA_QS (ks2,n)) * (IDEA_PS (ks1,n))) . m by A8, FUNCT_2:15
.= m by A2, A3, A4, A6, Th34 ;
:: thesis:

end;

suppose A17: r <> 0 ; :: thesis:

then A18: IDEA_P_F (Key1,n,r) is FuncSequence of MESSAGES , MESSAGES by Th40;
then A19: firstdom (IDEA_P_F (Key1,n,r)) = MESSAGES by FUNCT_7:def 9;
then A20: dom (compose ((IDEA_P_F (Key1,n,r)),MESSAGES)) = MESSAGES by A18, FUNCT_7:62;
( IDEA_P_F (Key1,n,r) = {} implies rng (compose ((IDEA_P_F (Key1,n,r)),MESSAGES)) = {} ) by A19, FUNCT_7:def 6;
then A21: rng (compose ((IDEA_P_F (Key1,n,r)),MESSAGES)) c= lastrng (IDEA_P_F (Key1,n,r)) by FUNCT_7:59, XBOOLE_1:2;
lastrng (IDEA_P_F (Key1,n,r)) c= MESSAGES by A18, FUNCT_7:def 9;
then rng (compose ((IDEA_P_F (Key1,n,r)),MESSAGES)) c= MESSAGES by A21, XBOOLE_1:1;
then reconsider PF = compose ((IDEA_P_F (Key1,n,r)),MESSAGES) as Function of MESSAGES,MESSAGES by A20, FUNCT_2:def 1, RELSET_1:4;
A22: rng PF c= MESSAGES by RELAT_1:def 19;
PF . m1 in MESSAGES by A9, FUNCT_2:5;
then reconsider m2 = PF . m1 as FinSequence of NAT by FINSEQ_1:def 11;
A23: ( len m2 >= 4 & m2 . 1 is_expressible_by n ) by A3, A10, A14, A13, A12, A11, Th45;
A24: IDEA_Q_F (Key2,n,r) is FuncSequence of MESSAGES , MESSAGES by A17, Th41;
then A25: firstdom (IDEA_Q_F (Key2,n,r)) = MESSAGES by FUNCT_7:def 9;
then A26: dom (compose ((IDEA_Q_F (Key2,n,r)),MESSAGES)) = MESSAGES by A24, FUNCT_7:62;
( IDEA_Q_F (Key2,n,r) = {} implies rng (compose ((IDEA_Q_F (Key2,n,r)),MESSAGES)) = {} ) by A25, FUNCT_7:def 6;
then A27: rng (compose ((IDEA_Q_F (Key2,n,r)),MESSAGES)) c= lastrng (IDEA_Q_F (Key2,n,r)) by FUNCT_7:59, XBOOLE_1:2;
lastrng (IDEA_Q_F (Key2,n,r)) c= MESSAGES by A24, FUNCT_7:def 9;
then rng (compose ((IDEA_Q_F (Key2,n,r)),MESSAGES)) c= MESSAGES by A27, XBOOLE_1:1;
then reconsider QF = compose ((IDEA_Q_F (Key2,n,r)),MESSAGES) as Function of MESSAGES,MESSAGES by A26, FUNCT_2:def 1, RELSET_1:4;
A28: m2 in MESSAGES by FINSEQ_1:def 11;
A29: QF . (PF . m1) = (QF * PF) . m1 by A9, FUNCT_2:15
.= (compose (((IDEA_P_F (Key1,n,r)) ^ (IDEA_Q_F (Key2,n,r))),MESSAGES)) . m1 by A22, FUNCT_7:48
.= m1 by A1, A2, A3, A5, A10, A14, A13, A12, A11, Th46 ;
A30: m2 . 4 is_expressible_by n by A3, A10, A14, A13, A12, A11, Th45;
A31: ( m2 . 2 is_expressible_by n & m2 . 3 is_expressible_by n ) by A3, A10, A14, A13, A12, A11, Th45;
thus ((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 = (IDEA_QS (ks2,n)) . ((QF * ((IDEA_QE (ke2,n)) * ((IDEA_PE (ke1,n)) * (PF * (IDEA_PS (ks1,n)))))) . m) by A8, FUNCT_2:15
.= (IDEA_QS (ks2,n)) . (QF . (((IDEA_QE (ke2,n)) * ((IDEA_PE (ke1,n)) * (PF * (IDEA_PS (ks1,n))))) . m)) by A8, FUNCT_2:15
.= (IDEA_QS (ks2,n)) . (QF . ((IDEA_QE (ke2,n)) . (((IDEA_PE (ke1,n)) * (PF * (IDEA_PS (ks1,n)))) . m))) by A8, FUNCT_2:15
.= (IDEA_QS (ks2,n)) . (QF . ((IDEA_QE (ke2,n)) . ((IDEA_PE (ke1,n)) . ((PF * (IDEA_PS (ks1,n))) . m)))) by A8, FUNCT_2:15
.= (IDEA_QS (ks2,n)) . (QF . ((IDEA_QE (ke2,n)) . ((IDEA_PE (ke1,n)) . (PF . ((IDEA_PS (ks1,n)) . m))))) by A8, FUNCT_2:15
.= (IDEA_QS (ks2,n)) . (QF . (((IDEA_QE (ke2,n)) * (IDEA_PE (ke1,n))) . m2)) by A28, FUNCT_2:15
.= (IDEA_QS (ks2,n)) . m1 by A2, A7, A23, A31, A30, A29, Th35
.= ((IDEA_QS (ks2,n)) * (IDEA_PS (ks1,n))) . m by A8, FUNCT_2:15
.= m by A2, A3, A4, A6, Th34 ; :: thesis:

end;