for n being non zero Nat
for lk being Nat
for Key1, Key2 being Matrix of lk,6,NAT
for r being 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 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