:: Algebraic group on Fixed-length bit integer and its adaptation
:: to {IDEA} Cryptography
:: by Yasushi Fuwa and Yoshinori Fujisawa
::
:: Received September 7, 1998
:: Copyright (c) 1998-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, FINSEQ_2, MARGREL1, CARD_1, ARYTM_3, INT_2,
NAT_1, RELAT_1, XXREAL_0, INT_1, ARYTM_1, GRCAT_1, XBOOLEAN, FINSEQ_1,
PARTFUN1, FUNCT_1, POWER, BINARI_3, FUNCOP_1, XBOOLE_0, BINARITH,
MATRIX_1, INCSP_1, ORDINAL4, FUNCT_7, FUNCT_2, TARSKI, TREES_1, IDEA_1,
XCMPLX_0;
notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
INT_1, INT_2, NAT_1, NAT_D, MARGREL1, RELAT_1, FUNCT_1, FUNCOP_1,
MATRIX_0, PARTFUN1, FUNCT_2, FUNCT_7, SERIES_1, FINSEQ_1, FINSEQ_2,
RECDEF_1, BINARITH, BINARI_3, XXREAL_0;
constructors NAT_D, SERIES_1, BINARITH, FUNCT_7, MATRIX_1, BINARI_3, RECDEF_1,
RELSET_1, XTUPLE_0;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, XXREAL_0,
XREAL_0, NAT_1, INT_1, FINSEQ_1, MARGREL1, FUNCT_7, VALUED_0, CARD_1,
FINSEQ_2, RELSET_1, FINSEQ_3;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions FUNCOP_1;
equalities FINSEQ_2, XBOOLEAN;
expansions FUNCOP_1;
theorems NAT_1, NAT_2, NEWTON, INT_1, INT_2, FINSEQ_1, FINSEQ_2, FUNCT_1,
FUNCT_2, FUNCT_7, FUNCOP_1, POWER, EULER_1, EULER_2, BINARITH, BINARI_3,
RELSET_1, RELAT_1, XBOOLE_1, XREAL_1, XXREAL_0, XBOOLEAN, NAT_D,
PARTFUN1, ORDINAL1, XREAL_0, CARD_1, MATRIX_0, TARSKI;
schemes FINSEQ_1, FINSEQ_2, NAT_1, FUNCT_2;
begin ::Some selected theorems on integers
reserve i,j,k,n for Nat;
reserve x,y,z for Tuple of n, BOOLEAN;
Lm1: i<>0 & i < j & j is prime implies i,j are_coprime
proof
assume that
A1: i<>0 and
A2: i < j and
A3: j is prime;
now
set IJ = i gcd j;
A4: IJ <> j
proof
assume IJ = j;
then j divides i by NAT_D:def 5;
then consider n being Nat such that
A5: i = j*n by NAT_D:def 3;
n <> 0 by A1,A5;
then j*n >= j*1 by NAT_1:14,XREAL_1:64;
hence contradiction by A2,A5;
end;
IJ divides j by NAT_D:def 5;
then IJ = 1 or IJ = j by A3,INT_2:def 4;
hence thesis by A4,INT_2:def 3;
end;
hence thesis;
end;
Lm2: j is prime & i<j & k<j & i<>0 implies ex a being Nat st (a*i)
mod j = k
proof
assume that
A1: j is prime and
A2: i<j and
A3: k<j and
A4: i<>0;
consider a,b being Integer such that
A5: a*i + b*j = k by A1,A2,A4,Lm1,EULER_1:10;
A6: j>0 by A1,INT_2:def 4;
now
per cases;
suppose
A7: a >= 0;
now
per cases;
suppose
b >= 0;
then reconsider a,b as Element of NAT by A7,INT_1:3;
take a;
(a*i + b*j) mod j = (a*i + ((b*j) mod j)) mod j by NAT_D:23
.= (a*i + 0) mod j
.= (a*i) mod j;
hence thesis by A3,A5,NAT_D:24;
end;
suppose
A8: b < 0;
reconsider a as Element of NAT by A7,INT_1:3;
consider b9 being Integer such that
A9: b9=0-b;
take a;
reconsider b9 as Element of NAT by A8,A9,INT_1:3;
a*i + b*j + b9*j = a*i by A9;
then (a*i) mod j = k mod j by A5,NAT_D:21
.= k by A3,NAT_D:24;
hence thesis;
end;
end;
hence thesis;
end;
suppose
A10: a < 0;
consider a1 being Integer such that
A11: a1 = 0 - a;
reconsider a1 as Element of NAT by A10,A11,INT_1:3;
consider a2 being Nat such that
A12: a2=(a1 div j) + 1;
consider a9 being Integer such that
A13: a9=a + a2 * j;
A14: a9 = -a1 + (a1 div j)*j + j by A11,A12,A13;
consider t being Nat such that
A15: a1 = j * (a1 div j) + t and
A16: t < j by A6,NAT_D:def 1;
-t + t < -t + j by A16,XREAL_1:6;
then reconsider a9 as Element of NAT by A14,A15,INT_1:3;
now
per cases;
suppose
b >= 0;
then reconsider b as Element of NAT by INT_1:3;
take a9;
A17: (k + a2*j*i) mod j = (k + a2*i*j) mod j .= k mod j by NAT_D:21
.= k by A3,NAT_D:24;
a*i + b*j + a2*j*i = a9*i + b*j by A13;
hence (a9*i) mod j = k by A5,A17,NAT_D:21;
end;
suppose
A18: b < 0;
take a9;
consider b9 being Integer such that
A19: b9=0-b;
reconsider b9 as Element of NAT by A18,A19,INT_1:3;
k + a2*j*i + b9*j = k + (a2*i+ b9)*j;
hence (a9*i) mod j = k mod j by A5,A13,A19,NAT_D:21
.= k by A3,NAT_D:24;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th1:
for i,j,k holds j is prime & i<j & k<j & i<>0 implies ex a being
Nat st (a*i) mod j = k & a < j
proof
let i,j,k be Nat;
assume that
A1: j is prime and
A2: i<j and
A3: k<j & i<>0;
consider a being Nat such that
A4: (a*i) mod j = k by A1,A2,A3,Lm2;
consider a9 being Nat such that
A5: a9 = a mod j;
take a9;
thus thesis by A2,A4,A5,EULER_2:8,NAT_D:1;
end;
theorem Th2:
for n,k1,k2 being Nat holds n <> 0 & k1 mod n = k2 mod
n & k1 <= k2 implies ex t being Nat st k2 - k1 = n*t
proof
let n,k1,k2 be Nat;
assume that
A1: n <> 0 and
A2: k1 mod n = k2 mod n and
A3: k1 <= k2;
consider t being Integer such that
A4: t = (k2 div n) - (k1 div n);
(k2 div n) >= (k1 div n) by A3,NAT_2:24;
then (k2 div n) - (k1 div n) >= (k1 div n) - (k1 div n) by XREAL_1:9;
then reconsider t as Element of NAT by A4,INT_1:3;
take t;
k1 = n * (k1 div n) + (k1 mod n) & k2 = n * (k2 div n) + (k2 mod n) by A1,
NAT_D:2;
hence thesis by A2,A4;
end;
theorem Th3:
for a, b being Nat holds a - b <= a
proof
let a, b be Nat;
a - b <= a - 0 by XREAL_1:13;
hence thesis;
end;
theorem Th4:
for b1,b2,c being Nat holds b2 <= c implies b2 - b1 <= c
proof
let b1,b2,c be Nat;
assume b2 <= c;
then
A1: b2 - b1 <= c - b1 by XREAL_1:9;
c - b1 <= c by Th3;
hence thesis by A1,XXREAL_0:2;
end;
theorem Th5:
for a,b,c being Nat holds 0<a & 0<b & a<c & b<c & c is
prime implies (a * b) mod c <> 0
proof
let a,b,c be Nat;
assume that
A1: 0<a & 0<b and
A2: a<c and
A3: b<c and
A4: c is prime;
assume (a * b) mod c = 0;
then (a * b) = c * ((a * b) div c) + 0 by A2,NAT_D:2;
then c divides (a * b) by NAT_D:def 3;
then c divides a or c divides b by A4,NEWTON:80;
hence contradiction by A1,A2,A3,NAT_D:7;
end;
begin :: Algebraic group on Fixed-length bit Integer
:: In this section,we construct an algebraic group on
:: Fixed-length bit Integer.
:: IDEA's Basic operators are 'xor', ADD_MOD and MUL_MOD.
:: 'xor' is 16-bitwise XOR. ADD_MOD is addition mod 2^{16}.
:: MUL_MOD is multiplication mod 2^(16)+1. And, we define
:: two functions NEG_MOD and INV_MOD that give inverse
:: element of ADD_MOD and MUL_MOD respectively.
definition
let n;
func ZERO( n ) -> Tuple of n, BOOLEAN equals
n |-> FALSE;
correctness;
end;
definition
let n;
let x, y be Tuple of n, BOOLEAN;
func x 'xor' y -> Tuple of n, BOOLEAN means
:Def2:
for i st i in Seg n holds it/.i = (x/.i) 'xor' (y/.i);
existence
proof
deffunc F(Nat)=(x/.$1) 'xor' (y/.$1);
consider z being FinSequence of BOOLEAN such that
A1: len z = n and
A2: for j be Nat st j in dom z holds z.j = F(j) from FINSEQ_2:sch 1;
A3: dom z = Seg n by A1,FINSEQ_1:def 3;
z is Element of n-tuples_on BOOLEAN by A1,FINSEQ_2:92;
then reconsider z as Tuple of n, BOOLEAN;
take z;
let i;
assume
A4: i in Seg n;
then i in dom z by A1,FINSEQ_1:def 3;
hence z/.i = z.i by PARTFUN1:def 6
.= (x/.i) 'xor' (y/.i) by A2,A3,A4;
end;
uniqueness
proof
let z1, z2 be Tuple of n, BOOLEAN such that
A5: for i st i in Seg n holds z1/.i = (x/.i) 'xor' (y/.i) and
A6: for i st i in Seg n holds z2/.i = (x/.i) 'xor' (y/.i);
A7: len z1 = n by CARD_1:def 7;
then
A8: dom z1 = Seg n by FINSEQ_1:def 3;
A9: len z2 = n by CARD_1:def 7;
now
let j be Nat;
assume
A10: j in dom z1;
then
A11: j in dom z2 by A9,A8,FINSEQ_1:def 3;
thus z1.j = z1/.j by A10,PARTFUN1:def 6
.= (x/.j) 'xor' (y/.j) by A5,A8,A10
.= z2/.j by A6,A8,A10
.= z2.j by A11,PARTFUN1:def 6;
end;
hence thesis by A7,A9,FINSEQ_2:9;
end;
end;
theorem Th6:
for n,x holds x 'xor' x = ZERO(n)
proof
let n;
let x be Tuple of n, BOOLEAN;
A1: len (x 'xor' x) = n by CARD_1:def 7;
then
A2: dom (x 'xor' x) = Seg n by FINSEQ_1:def 3;
A3: now
let j be Nat;
assume
A4: j in dom (x 'xor' x);
A5: ZERO(n).j = FALSE;
thus (x 'xor' x).j = (x 'xor' x)/.j by A4,PARTFUN1:def 6
.= (x/.j) 'xor' (x/.j) by A2,A4,Def2
.= ZERO(n).j by A5,XBOOLEAN:138;
end;
len (ZERO(n)) = n by CARD_1:def 7;
hence thesis by A1,A3,FINSEQ_2:9;
end;
theorem Th7:
for n,x,y holds x 'xor' y = y 'xor' x
proof
let n;
let x,y be Tuple of n, BOOLEAN;
A1: len (x 'xor' y) = n by CARD_1:def 7;
then
A2: dom (x 'xor' y) = Seg n by FINSEQ_1:def 3;
A3: len (y 'xor' x) = n by CARD_1:def 7;
now
let j be Nat;
assume
A4: j in dom (x 'xor' y);
then
A5: j in dom (y 'xor' x) by A3,A2,FINSEQ_1:def 3;
thus (x 'xor' y).j = (x 'xor' y)/.j by A4,PARTFUN1:def 6
.= (y/.j) 'xor' (x/.j) by A2,A4,Def2
.= (y 'xor' x)/.j by A2,A4,Def2
.= (y 'xor' x).j by A5,PARTFUN1:def 6;
end;
hence thesis by A1,A3,FINSEQ_2:9;
end;
definition
let n;
let x, y be Tuple of n, BOOLEAN;
redefine func x 'xor' y; :: redefines 'xor' (IDEA_1, definition)
commutativity by Th7;
end;
theorem Th8:
for n,x holds ZERO(n) 'xor' x = x
proof
let n;
let x be Tuple of n, BOOLEAN;
A1: len ((ZERO(n)) 'xor' x) = n by CARD_1:def 7;
then
A2: dom ((ZERO(n)) 'xor' x) = Seg n by FINSEQ_1:def 3;
A3: len x = n by CARD_1:def 7;
now
let j be Nat;
assume
A4: j in dom ((ZERO(n)) 'xor' x);
then
A5: j in dom x by A3,A2,FINSEQ_1:def 3;
j in dom (ZERO(n)) by A2,A4,FUNCOP_1:13;
then
A6: (ZERO(n))/.j = (n |-> FALSE).j by PARTFUN1:def 6
.= FALSE;
thus ((ZERO(n)) 'xor' x).j = ((ZERO(n)) 'xor' x)/.j by A4,PARTFUN1:def 6
.= FALSE 'xor' (x/.j) by A2,A4,A6,Def2
.= x/.j by BINARITH:8
.= x.j by A5,PARTFUN1:def 6;
end;
hence thesis by A1,A3,FINSEQ_2:9;
end;
theorem Th9:
for n,x,y,z holds (x 'xor' y) 'xor' z = x 'xor' (y 'xor' z)
proof
let n;
let x,y,z be Tuple of n, BOOLEAN;
A1: len ((x 'xor' y) 'xor' z) = n by CARD_1:def 7;
then
A2: dom ((x 'xor' y) 'xor' z) = Seg n by FINSEQ_1:def 3;
A3: len (x 'xor' (y 'xor' z)) = n by CARD_1:def 7;
now
let j be Nat;
assume
A4: j in dom ((x 'xor' y) 'xor' z);
then
A5: j in dom (x 'xor' (y 'xor' z)) by A3,A2,FINSEQ_1:def 3;
thus ((x 'xor' y) 'xor' z).j = ((x 'xor' y) 'xor' z)/.j by A4,
PARTFUN1:def 6
.= ((x 'xor' y)/.j) 'xor' (z/.j) by A2,A4,Def2
.= ((x/.j) 'xor' (y/.j)) 'xor' (z/.j) by A2,A4,Def2
.= (x/.j) 'xor' ((y/.j) 'xor' (z/.j)) by XBOOLEAN:73
.= (x/.j) 'xor' ((y 'xor' z)/.j) by A2,A4,Def2
.= ((x 'xor' (y 'xor' z)))/.j by A2,A4,Def2
.= (x 'xor' (y 'xor' z)).j by A5,PARTFUN1:def 6;
end;
hence thesis by A1,A3,FINSEQ_2:9;
end;
definition
let n;
let i be Nat;
pred i is_expressible_by n means
i < 2 to_power(n);
end;
theorem
for n holds n-BinarySequence 0 = ZERO(n)
proof
let n;
A1: len (n-BinarySequence 0) = n by CARD_1:def 7;
then
A2: dom (n-BinarySequence 0) = Seg n by FINSEQ_1:def 3;
A3: len (ZERO(n)) = n by CARD_1:def 7;
then
A4: dom ZERO(n) = Seg n by FINSEQ_1:def 3;
A5: dom (n-BinarySequence 0) = Seg n by A1,FINSEQ_1:def 3;
now
let j be Nat;
A6: (0 div 2 to_power(j-'1)) mod 2 = 0 mod 2
.= 0 by NAT_D:26;
assume
A7: j in dom (n-BinarySequence 0);
then j in dom (ZERO(n)) by A2,FUNCOP_1:13;
then
A8: (ZERO(n))/.j = (n |-> FALSE).j by PARTFUN1:def 6
.= FALSE;
thus (n-BinarySequence 0).j = (n-BinarySequence 0)/.j by A7,PARTFUN1:def 6
.= IFEQ((0 div 2 to_power(j-'1)) mod 2,0,FALSE,TRUE) by A2,A7,
BINARI_3:def 1
.= (ZERO(n))/.j by A6,A8,FUNCOP_1:def 8
.= ZERO(n).j by A5,A4,A7,PARTFUN1:def 6;
end;
hence thesis by A1,A3,FINSEQ_2:9;
end;
definition
let n;
let i, j be Nat;
func ADD_MOD(i,j,n) -> Nat equals
(i + j) mod 2 to_power(n);
coherence;
end;
definition
let n;
let i be Nat;
assume
A1: i is_expressible_by n;
func NEG_N(i,n) -> Nat equals
:Def5:
2 to_power(n) - i;
coherence
proof
i < 2 to_power(n) by A1;
then 2 to_power(n) - i > i - i by XREAL_1:9;
then 2 to_power(n) - i is Element of NAT by INT_1:3;
hence thesis;
end;
end;
definition
let n;
let i be Nat;
func NEG_MOD(i,n) -> Nat equals
NEG_N(i,n) mod 2 to_power(n);
coherence;
end;
theorem Th11:
i is_expressible_by n implies ADD_MOD(i, NEG_MOD(i,n), n) = 0
proof
assume i is_expressible_by n;
then i + NEG_N(i,n) = i + (2 to_power(n) - i) by Def5
.= 0 + 2 to_power(n);
hence ADD_MOD(i, NEG_MOD(i,n), n) = 2 to_power(n) mod 2 to_power(n) by
NAT_D:23
.= 0 by NAT_D:25;
end;
theorem
ADD_MOD(i,j,n) = ADD_MOD(j,i,n);
theorem Th13:
i is_expressible_by n implies ADD_MOD(0,i,n) = i
by NAT_D:24;
theorem Th14:
ADD_MOD(ADD_MOD(i,j,n),k,n) = ADD_MOD(i,ADD_MOD(j,k,n),n)
proof
thus ADD_MOD(ADD_MOD(i,j,n),k,n) = (i+j+k) mod 2 to_power(n) by NAT_D:23
.= (i+(j+k)) mod 2 to_power(n)
.= ADD_MOD(i,ADD_MOD(j,k,n),n) by NAT_D:22;
end;
theorem Th15:
ADD_MOD(i,j,n) is_expressible_by n
by NAT_D:1,POWER:34;
theorem
NEG_MOD(i,n) is_expressible_by n
by NAT_D:1,POWER:34;
definition
let n, i be Nat;
func ChangeVal_1(i,n) -> Nat equals
:Def7:
2 to_power(n) if i = 0
otherwise i;
coherence;
correctness;
end;
theorem Th17:
i is_expressible_by n implies ChangeVal_1(i,n) <= 2 to_power(n)
& ChangeVal_1(i,n) > 0
proof
assume
A1: i is_expressible_by n;
A2: 2 to_power(n) > 0 by POWER:34;
per cases;
suppose
i=0;
hence thesis by A2,Def7;
end;
suppose
A3: i<>0;
then ChangeVal_1(i,n) = i by Def7;
hence thesis by A1,A3;
end;
end;
theorem Th18:
for n,a1,a2 be Nat holds a1 is_expressible_by n & a2
is_expressible_by n & ChangeVal_1(a1,n) = ChangeVal_1(a2,n) implies a1 = a2
proof
let n,a1,a2 be Nat;
assume that
A1: a1 is_expressible_by n and
A2: a2 is_expressible_by n and
A3: ChangeVal_1(a1,n) = ChangeVal_1(a2,n);
A4: a1 <> 2 to_power(n) by A1;
A5: a2 <> 2 to_power(n) by A2;
per cases;
suppose
A6: ChangeVal_1(a1,n) = 2 to_power(n);
hence a2 = 0 by A3,A5,Def7
.= a1 by A4,A6,Def7;
end;
suppose
A7: ChangeVal_1(a1,n) <> 2 to_power(n);
hence a2 = ChangeVal_1(a1,n) by A3,Def7
.= a1 by A7,Def7;
end;
end;
definition
let n,i be Nat;
func ChangeVal_2(i,n) -> Nat equals
:Def8:
0 if i = 2 to_power(n)
otherwise i;
correctness;
end;
theorem
i is_expressible_by n implies ChangeVal_2(i,n) is_expressible_by n
by Def8;
theorem Th20:
for n,a1,a2 be Nat holds a1 <> 0 & a2 <> 0 &
ChangeVal_2(a1,n) = ChangeVal_2(a2,n) implies a1 = a2
proof
let n,a1,a2 be Nat;
assume that
A1: a1 <> 0 & a2 <> 0 and
A2: ChangeVal_2(a1,n) = ChangeVal_2(a2,n);
per cases;
suppose
A3: ChangeVal_2(a1,n) = 0;
then a2 = 2 to_power(n) or a2 = 0 by A2,Def8;
hence thesis by A1,A3,Def8;
end;
suppose
A4: ChangeVal_2(a1,n) <> 0;
then
A5: a1 <> 2 to_power(n) by Def8;
a2 <> 2 to_power(n) by A2,A4,Def8;
hence a2 = ChangeVal_2(a1,n) by A2,Def8
.= a1 by A5,Def8;
end;
end;
definition
let n;
let i,j be Nat;
func MUL_MOD(i,j,n) -> Nat equals
ChangeVal_2((ChangeVal_1(i,n)*
ChangeVal_1(j,n)) mod (2 to_power(n)+1),n);
coherence;
end;
definition
let n be non zero Nat;
let i be Nat;
assume that
A1: i is_expressible_by n and
A2: (2 to_power(n) + 1) is prime;
func INV_MOD(i,n) -> Nat means
:Def10:
MUL_MOD(i,it,n) = 1 & it is_expressible_by n;
existence
proof
A3: 2 to_power(n) > 0 by POWER:34;
then
A4: 2 to_power(n) + 1 > 0 + 1 by XREAL_1:6;
then 2 to_power(n) + 1 - 1 >= 1 + 1 - 1 by NAT_1:13;
then 2 to_power(n) + 1 - 1 - 1 >= 1 + 1 - 1 - 1 by XREAL_1:9;
then reconsider n3=2 to_power(n) + 1 - 1 - 1 as Element of NAT
by INT_1:3;
reconsider nn=2 to_power(n) + 1 as Nat;
reconsider n2=2 to_power(n) + 1 - 1 as Nat;
A5: 2 to_power(n) <> 1 by POWER:35;
n2 * n2 = nn*n3 + 1;
then
A6: (n2*n2) mod nn = 1 mod nn by NAT_D:21
.= 1 by A4,NAT_D:24;
per cases;
suppose
A7: i=0;
consider j such that
A8: j = 0;
take j;
A9: j is_expressible_by n by A3,A8;
MUL_MOD(i,j,n) = ChangeVal_2((2 to_power(n)*ChangeVal_1(0,n)) mod
nn,n) by A7,A8,Def7
.= ChangeVal_2((n2*n2) mod nn,n) by Def7
.= 1 by A5,A6,Def8;
hence thesis by A9;
end;
suppose
A10: i<>0;
i < 2 to_power(n) by A1;
then i < 2 to_power(n)+1 by NAT_1:13;
then consider a being Nat such that
A11: (a*i) mod (2 to_power(n)+1) = 1 and
A12: a < (2 to_power(n)+1) by A2,A4,A10,Th1;
take k=ChangeVal_2(a,n);
A13: a <> 0 by A11,NAT_D:24;
now
per cases;
suppose
A14: a <> 2 to_power(n);
then
A15: k = a by Def8;
then k <= 2 to_power(n) by A12,NAT_1:13;
then k < 2 to_power(n) by A14,A15,XXREAL_0:1;
then
A16: k is_expressible_by n;
MUL_MOD(i,k,n) = ChangeVal_2((i* ChangeVal_1(k,n)) mod (2
to_power(n)+1),n) by A10,Def7
.= ChangeVal_2((i*a)mod (2 to_power(n)+1),n) by A13,A15,Def7
.= 1 by A5,A11,Def8;
hence thesis by A16;
end;
suppose
A17: a = 2 to_power(n);
then
A18: k = 0 by Def8;
then
A19: k is_expressible_by n by A3;
MUL_MOD(i,k,n) = ChangeVal_2((i* ChangeVal_1(k,n)) mod (2
to_power(n)+1),n) by A10,Def7
.= ChangeVal_2((i*a)mod (2 to_power(n)+1),n) by A17,A18,Def7
.= 1 by A5,A11,Def8;
hence thesis by A19;
end;
end;
hence thesis;
end;
end;
uniqueness
proof
let a1, a2 be Nat such that
A20: MUL_MOD(i,a1,n) = 1 and
A21: a1 is_expressible_by n and
A22: MUL_MOD(i,a2,n) = 1 and
A23: a2 is_expressible_by n;
consider b2 being Nat such that
A24: b2 = ChangeVal_1(a2,n);
b2 <= 2 to_power(n) by A23,A24,Th17;
then
A25: b2 < 2 to_power(n)+1 by NAT_1:13;
consider b1 being Nat such that
A26: b1 = ChangeVal_1(a1,n);
b1 <= 2 to_power(n) by A21,A26,Th17;
then
A27: b1 < 2 to_power(n)+1 by NAT_1:13;
consider k being Nat such that
A28: k = ChangeVal_1(i,n);
A29: k <= 2 to_power(n) by A1,A28,Th17;
then
A30: k < 2 to_power(n)+1 by NAT_1:13;
A31: k > 0 by A1,A28,Th17;
b2 > 0 by A23,A24,Th17;
then
A32: (k * b2) mod (2 to_power(n)+1) <> 0 by A2,A31,A30,A25,Th5;
b1 > 0 by A21,A26,Th17;
then (k * b1) mod (2 to_power(n)+1) <> 0 by A2,A31,A30,A27,Th5;
then
A33: (k * b1) mod (2 to_power(n)+1) = (k * b2) mod (2 to_power(n)+1) by A20,A22
,A28,A26,A24,A32,Th20;
now
per cases;
suppose
A34: b1 <= b2;
consider b being Integer such that
A35: b = b2 - b1;
b1 - b1 <= b2 - b1 by A34,XREAL_1:9;
then reconsider b as Element of NAT by A35,INT_1:3;
ex t being Nat st k*b2 - k*b1 = (2 to_power(n)+ 1)*t by A33
,A34,Th2,NAT_1:4;
then (2 to_power(n)+1) divides k*b by A35,NAT_D:def 3;
then
A36: (2 to_power(n)+1) divides k or (2 to_power(n)+1) divides b by A2,
NEWTON:80;
b <= 2 to_power(n) by A23,A24,A35,Th4,Th17;
then
A37: not (2 to_power(n)+1) <= b by NAT_1:13;
not (2 to_power(n)+1) <= k by A29,NAT_1:13;
then not 0 < b by A31,A36,A37,NAT_D:7;
then b2 - b1 + b1 = 0 + b1 by A35;
hence b1 = b2;
end;
suppose
A38: b2 <= b1;
consider b being Integer such that
A39: b = b1 - b2;
b2 - b2 <= b1 - b2 by A38,XREAL_1:9;
then reconsider b as Element of NAT by A39,INT_1:3;
ex t being Nat st k*b1 - k*b2 = (2 to_power(n)+ 1)*t by A33
,A38,Th2,NAT_1:4;
then (2 to_power(n)+1) divides k*b by A39,NAT_D:def 3;
then
A40: (2 to_power(n)+1) divides k or (2 to_power(n)+1) divides b by A2,
NEWTON:80;
b <= 2 to_power(n) by A21,A26,A39,Th4,Th17;
then
A41: not (2 to_power(n)+1) <= b by NAT_1:13;
not (2 to_power(n)+1) <= k by A29,NAT_1:13;
then not 0 < b by A31,A40,A41,NAT_D:7;
then b1 - b2 + b2 = 0 + b2 by A39;
hence b2 = b1;
end;
end;
hence thesis by A21,A23,A26,A24,Th18;
end;
end;
theorem
MUL_MOD(i,j,n) = MUL_MOD(j,i,n);
theorem Th22:
i is_expressible_by n implies MUL_MOD(1,i,n) = i
proof
A1: ChangeVal_1(1,n) = 1 by Def7;
assume i is_expressible_by n;
then
A2: i < 2 to_power n;
per cases;
suppose
A3: i = 0;
then ChangeVal_1(i,n) = 2 to_power(n) by Def7;
then (ChangeVal_1(i,n)) mod ((2 to_power n)+1) = 2 to_power(n) by NAT_D:24
,XREAL_1:29;
hence thesis by A1,A3,Def8;
end;
suppose
A4: i <> 0;
2 to_power n < (2 to_power n)+1 by XREAL_1:29;
then
A5: i < (2 to_power n)+1 by A2,XXREAL_0:2;
(ChangeVal_1(i,n)) mod ((2 to_power n)+1) = i mod ((2 to_power n)+1)
by A4,Def7;
then (ChangeVal_1(i,n)) mod ((2 to_power n)+1) = i by A5,NAT_D:24;
hence thesis by A2,A1,Def8;
end;
end;
theorem Th23:
(2 to_power(n)+1) is prime & i is_expressible_by n & j
is_expressible_by n & k is_expressible_by n implies MUL_MOD(MUL_MOD(i,j,n),k,n)
= MUL_MOD(i,MUL_MOD(j,k,n),n)
proof
assume that
A1: (2 to_power(n)+1) is prime and
A2: i is_expressible_by n and
A3: j is_expressible_by n and
A4: k is_expressible_by n;
set J = ChangeVal_1(j,n);
A5: J > 0 by A3,Th17;
set I = ChangeVal_1(i,n);
I <= 2 to_power(n) by A2,Th17;
then
A6: I < 2 to_power(n)+1 by NAT_1:13;
J <= 2 to_power(n) by A3,Th17;
then
A7: J < 2 to_power(n)+1 by NAT_1:13;
set K = ChangeVal_1(k,n);
A8: K > 0 by A4,Th17;
K <= 2 to_power(n) by A4,Th17;
then
A9: K < 2 to_power(n)+1 by NAT_1:13;
A10: I > 0 by A2,Th17;
now
set CV = (I*J) mod (2 to_power(n)+1);
(I*J) mod (2 to_power(n)+1) < (2 to_power(n)+1) by NAT_D:1;
then
A11: (I*J) mod (2 to_power(n)+1) <= 2 to_power(n) by NAT_1:13;
A12: CV <> 0 by A1,A6,A10,A7,A5,Th5;
now
per cases by A11,XXREAL_0:1;
suppose
A13: CV = 2 to_power(n);
then
A14: MUL_MOD(MUL_MOD(i,j,n),k,n) = ChangeVal_2((ChangeVal_1(0,n )*K)
mod (2 to_power(n)+1),n) by Def8
.= ChangeVal_2((CV*K) mod (2 to_power(n)+1),n) by A13,Def7
.= ChangeVal_2(((I*J)*K) mod (2 to_power(n)+1),n) by EULER_2:8;
set CV2 = (J*K) mod (2 to_power(n)+1);
CV2 < (2 to_power(n)+1) by NAT_D:1;
then
A15: CV2 <= 2 to_power(n) by NAT_1:13;
A16: CV2 <> 0 by A1,A7,A5,A9,A8,Th5;
now
per cases by A15,XXREAL_0:1;
suppose
A17: CV2 = 2 to_power(n);
then
MUL_MOD(i,MUL_MOD(j,k,n),n) = ChangeVal_2((I*ChangeVal_1(0,n)
) mod (2 to_power(n)+1),n) by Def8
.= ChangeVal_2((I*CV2) mod (2 to_power(n)+1),n) by A17,Def7
.= ChangeVal_2((I*(J*K)) mod (2 to_power(n)+1),n) by EULER_2:8
.= ChangeVal_2((I*J*K) mod (2 to_power(n)+1),n);
hence thesis by A14;
end;
suppose
CV2 < 2 to_power(n);
then MUL_MOD(j,k,n) = CV2 by Def8;
then MUL_MOD(i,MUL_MOD(j,k,n),n) = ChangeVal_2((I*CV2) mod (2
to_power(n)+1),n) by A16,Def7
.= ChangeVal_2((I*(J*K)) mod (2 to_power(n)+1),n) by EULER_2:8
.= ChangeVal_2((I*J*K) mod (2 to_power(n)+1),n);
hence thesis by A14;
end;
end;
hence thesis;
end;
suppose
CV < 2 to_power(n);
then
A18: MUL_MOD(MUL_MOD(i,j,n),k,n) = ChangeVal_2((ChangeVal_1(CV, n)*K)
mod (2 to_power(n)+1),n) by Def8
.= ChangeVal_2((CV*K) mod (2 to_power(n)+1),n) by A12,Def7
.= ChangeVal_2(((I*J)*K) mod (2 to_power(n)+1),n) by EULER_2:8;
set CV2 = (J*K) mod (2 to_power(n)+1);
CV2 < (2 to_power(n)+1) by NAT_D:1;
then
A19: CV2 <= 2 to_power(n) by NAT_1:13;
A20: CV2 <> 0 by A1,A7,A5,A9,A8,Th5;
now
per cases by A19,XXREAL_0:1;
suppose
A21: CV2 = 2 to_power(n);
then
MUL_MOD(i,MUL_MOD(j,k,n),n) = ChangeVal_2((I*ChangeVal_1(0,n)
) mod (2 to_power(n)+1),n) by Def8
.= ChangeVal_2((I*CV2) mod (2 to_power(n)+1),n) by A21,Def7
.= ChangeVal_2((I*(J*K)) mod (2 to_power(n)+1),n) by EULER_2:8
.= ChangeVal_2((I*J*K) mod (2 to_power(n)+1),n);
hence thesis by A18;
end;
suppose
CV2 < 2 to_power(n);
then MUL_MOD(j,k,n) = CV2 by Def8;
then MUL_MOD(i,MUL_MOD(j,k,n),n) = ChangeVal_2((I*CV2) mod (2
to_power(n)+1),n) by A20,Def7
.= ChangeVal_2((I*(J*K)) mod (2 to_power(n)+1),n) by EULER_2:8
.= ChangeVal_2((I*J*K) mod (2 to_power(n)+1),n);
hence thesis by A18;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis;
end;
theorem Th24:
MUL_MOD(i,j,n) is_expressible_by n
proof
set CV = (ChangeVal_1(i,n)*ChangeVal_1(j,n)) mod (2 to_power(n)+1);
(ChangeVal_1(i,n)*ChangeVal_1(j,n)) mod (2 to_power(n)+1) < (2 to_power(
n)+1) by NAT_D:1;
then
A1: (ChangeVal_1(i,n)*ChangeVal_1(j,n)) mod (2 to_power(n)+1) <= 2 to_power(
n) by NAT_1:13;
A2: 0 < 2 to_power(n) by POWER:34;
now
per cases by A1,XXREAL_0:1;
suppose
CV = 2 to_power(n);
then ChangeVal_2(CV,n) = 0 by Def8;
hence thesis by A2;
end;
suppose
A3: CV < 2 to_power(n);
then ChangeVal_2(CV,n) = CV by Def8;
hence thesis by A3;
end;
end;
hence thesis;
end;
theorem
ChangeVal_2(i,n) = 1 implies i = 1
proof
assume
A1: ChangeVal_2(i,n) = 1;
assume
A2: i <> 1;
now
per cases;
suppose
i = 2 to_power(n);
hence contradiction by A1,Def8;
end;
suppose
i <> 2 to_power(n);
hence contradiction by A1,A2,Def8;
end;
end;
hence thesis;
end;
begin :: Operations of IDEA Cryptograms
:: We define three IDEA's operations IDEAoperationA, IDEAoperationB
:: and IDEAoperationC using the basic operators. IDEA Cryptogram
:: encrypts 64-bit plain text to 64-bit ciphertext. These texts
:: are divided into 4 16-bits text blocks. Here, we use m as the
:: text block sequence. And, IDEA's operations use key sequence
:: explains k in this section. n is bit-length of text blocks.
:: Definiton of IDEA Operation A
definition
let n;
let m,k be FinSequence of NAT;
func IDEAoperationA(m, k, n) -> FinSequence of NAT means
:Def11:
len(it) =
len(m) & for i being 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
proof
defpred P[set,set] means ($1=1 implies $2 = MUL_MOD(m.1, k.1, n)) & ($1=2
implies $2 = ADD_MOD(m.2, k.2, n)) & ($1=3 implies $2 = ADD_MOD(m.3, k.3, n)) &
($1=4 implies $2 = MUL_MOD(m.4, k.4, n)) & ($1<>1 & $1 <> 2 & $1<>3 & $1<>4
implies $2 = m.$1);
A1: for j be Nat st j in Seg len m
ex x being Element of NAT st P[j,x]
proof
let j be Nat;
assume j in Seg len m;
then reconsider j as Element of NAT;
per cases;
suppose
A2: j = 1;
reconsider M=MUL_MOD(m.1, k.1, n) as Element of NAT
by ORDINAL1:def 12;
take M;
thus thesis by A2;
end;
suppose
A3: j = 2;
take ADD_MOD(m.2, k.2, n);
thus thesis by A3;
end;
suppose
A4: j = 3;
take ADD_MOD(m.3, k.3, n);
thus thesis by A4;
end;
suppose
A5: j = 4;
reconsider M=MUL_MOD(m.4, k.4, n) as Element of NAT
by ORDINAL1:def 12;
take M;
thus thesis by A5;
end;
suppose
A6: j<>1 & j<>2 & j<>3 & j<>4;
take m.j;
thus thesis by A6;
end;
end;
consider z being FinSequence of NAT such that
A7: dom z = Seg len m & for i be Nat st i in Seg len m holds P[i,z.i]
from FINSEQ_1:sch 5(A1);
take z;
dom m = Seg len m by FINSEQ_1:def 3;
hence thesis by A7,FINSEQ_1:def 3;
end;
uniqueness
proof
let z1,z2 be FinSequence of NAT such that
A8: len(z1) = len(m) and
A9: for i being Nat st i in dom m holds (i=1 implies z1.i
= MUL_MOD(m.1, k.1, n)) & (i=2 implies z1.i = ADD_MOD(m.2, k.2, n)) & (i=3
implies z1.i = ADD_MOD(m.3, k.3, n)) & (i=4 implies z1.i = MUL_MOD(m.4, k.4, n)
) & (i<>1 & i <> 2 & i<>3 & i<>4 implies z1.i = m.i) and
A10: len(z2) = len(m) and
A11: for i st i in dom m holds (i=1 implies z2.i = MUL_MOD(m.1, k.1, n
)) & (i=2 implies z2.i = ADD_MOD(m.2, k.2, n)) & (i=3 implies z2.i = ADD_MOD(m.
3, k.3, n)) & (i=4 implies z2.i = MUL_MOD(m.4, k.4, n)) & (i<>1 & i <> 2 & i<>3
& i<>4 implies z2.i = m.i);
A12: dom m = Seg len z2 by A10,FINSEQ_1:def 3
.= dom z2 by FINSEQ_1:def 3;
A13: now
let j be Nat;
assume
A14: j in dom m;
now
per cases;
suppose
A15: j = 1;
hence z1.j = MUL_MOD(m.1, k.1, n) by A9,A14
.= z2.j by A11,A14,A15;
end;
suppose
A16: j = 2;
hence z1.j = ADD_MOD(m.2, k.2, n) by A9,A14
.= z2.j by A11,A14,A16;
end;
suppose
A17: j = 3;
hence z1.j = ADD_MOD(m.3, k.3, n) by A9,A14
.= z2.j by A11,A14,A17;
end;
suppose
A18: j = 4;
hence z1.j = MUL_MOD(m.4, k.4, n) by A9,A14
.= z2.j by A11,A14,A18;
end;
suppose
A19: j<>1 & j<>2 & j<>3 & j<>4;
hence z1.j = m.j by A9,A14
.= z2.j by A11,A14,A19;
end;
end;
hence z1.j = z2.j;
end;
dom m = Seg len z1 by A8,FINSEQ_1:def 3
.= dom z1 by FINSEQ_1:def 3;
hence thesis by A12,A13,FINSEQ_1:13;
end;
end;
:: Definiton of IDEA Operation B
reserve m,k,k1,k2 for FinSequence of NAT;
definition
let n be non zero 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 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
proof
defpred P[set,set] means ($1=1 implies $2 = 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))))& ($1=2 implies $2 = 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))))& ($1=3
implies $2 = 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))))& (
$1=4 implies $2 = 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))))& ($1<>1 & $1 <> 2 & $1<>3 & $1<>4 implies $2 = m.$1);
A1: for j be Nat st j in Seg len m ex x being Element of NAT st P[j,x]
proof
let j be Nat;
assume j in Seg len m;
reconsider j as Nat;
per cases;
suppose
A2: j = 1;
take 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)));
thus thesis by A2;
end;
suppose
A3: j = 2;
take 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)));
thus thesis by A3;
end;
suppose
A4: j = 3;
take 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)));
thus thesis by A4;
end;
suppose
A5: j = 4;
take 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)));
thus thesis by A5;
end;
suppose
A6: j<>1 & j<>2 & j<>3 & j<>4;
take m.j;
thus thesis by A6;
end;
end;
consider z being FinSequence of NAT such that
A7: dom z = Seg len m & for i be Nat st i in Seg len m holds P[i,z.i]
from FINSEQ_1:sch 5(A1);
take z;
Seg len m = dom m by FINSEQ_1:def 3;
hence thesis by A7,FINSEQ_1:def 3;
end;
uniqueness
proof
let z1,z2 be FinSequence of NAT such that
A8: len(z1) = len(m) and
A9: for i st i in dom m holds (i=1 implies z1.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
z1.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 z1.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 z1.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
z1.i = m.i) and
A10: len(z2) = len(m) and
A11: for i st i in dom m holds (i=1 implies z2.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
z2.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 z2.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 z2.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
z2.i = m.i);
A12: dom m = Seg len(z2) by A10,FINSEQ_1:def 3
.= dom z2 by FINSEQ_1:def 3;
A13: now
let j be Nat;
assume
A14: j in dom m;
now
per cases;
suppose
A15: j = 1;
hence z1.j = 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))) by A9,A14
.= z2.j by A11,A14,A15;
end;
suppose
A16: j = 2;
hence z1.j = 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))) by A9,A14
.= z2.j by A11,A14,A16;
end;
suppose
A17: j = 3;
hence z1.j = 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))) by A9,A14
.= z2.j by A11,A14,A17;
end;
suppose
A18: j = 4;
hence z1.j = 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))) by A9,A14
.= z2.j by A11,A14,A18;
end;
suppose
A19: j<>1 & j<>2 & j<>3 & j<>4;
hence z1.j = m.j by A9,A14
.= z2.j by A11,A14,A19;
end;
end;
hence z1.j = z2.j;
end;
dom m = Seg len(z1) by A8,FINSEQ_1:def 3
.= dom z1 by FINSEQ_1:def 3;
hence thesis by A12,A13,FINSEQ_1:13;
end;
end;
:: Definiton of IDEA Operation C
definition
let m be FinSequence of NAT;
func IDEAoperationC(m) -> FinSequence of NAT means
:Def13:
len(it) = len(m)
& for i being Nat st i in dom m holds it.i = IFEQ(i,2,m.3,IFEQ(i,3,m
.2,m.i));
existence
proof
defpred P[set,set] means ($1=2 implies $2 = m.3) & ($1=3 implies $2 = m.2)
& ($1<>2 & $1<>3 implies $2 = m.$1);
A1: for k be Nat st k in Seg len m
ex x being Element of NAT st P[k,x]
proof
let k be Nat;
assume k in Seg len m;
reconsider k as Nat;
per cases;
suppose
A2: k = 2;
take m.3;
thus thesis by A2;
end;
suppose
A3: k = 3;
take m.2;
thus thesis by A3;
end;
suppose
A4: k<>2 & k<>3;
take m.k;
thus thesis by A4;
end;
end;
consider z being FinSequence of NAT such that
A5: dom z = Seg len m and
A6: for i be Nat st i in Seg len m holds P[i,z.i] from FINSEQ_1:sch 5(
A1);
A7: for i st i in Seg len m holds IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) = z.i
proof
let i be Nat;
assume
A8: i in Seg len m;
A9: i = 3 implies IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) = m.2
proof
assume
A10: i = 3;
then IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) = IFEQ(i,3,m.2,m.i) by
FUNCOP_1:def 8
.= m.2 by A10,FUNCOP_1:def 8;
hence thesis;
end;
A11: i = 2 implies IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) = m.3 by FUNCOP_1:def 8;
i<>2 & i<>3 implies IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) = m.i
proof
assume that
A12: i <> 2 and
A13: i <> 3;
IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) = IFEQ(i,3,m.2,m.i) by A12,
FUNCOP_1:def 8
.= m.i by A13,FUNCOP_1:def 8;
hence thesis;
end;
then i<>2 & i<>3 implies IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) = z.i by A6,A8;
hence thesis by A6,A8,A11,A9;
end;
take z;
Seg len m = dom m by FINSEQ_1:def 3;
hence thesis by A5,A7,FINSEQ_1:def 3;
end;
uniqueness
proof
let z1,z2 be FinSequence of NAT such that
A14: len(z1) = len(m) and
A15: for i st i in dom m holds z1.i = IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) and
A16: len(z2) = len(m) and
A17: for i st i in dom m holds z2.i = IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i));
A18: dom m = Seg len(z2) by A16,FINSEQ_1:def 3
.= dom z2 by FINSEQ_1:def 3;
A19: now
let j be Nat;
assume
A20: j in dom m;
now
per cases;
suppose
j = 2;
then
A21: IFEQ(j,2,m.3,IFEQ(j,3,m.2,m.j)) = m.3 by FUNCOP_1:def 8;
then z2.j = m.3 by A17,A20;
hence z1.j = z2.j by A15,A20,A21;
end;
suppose
A22: j = 3;
A23: j = 3 implies IFEQ(j,2,m.3,IFEQ(j,3,m.2,m.j)) = m.2
proof
assume
A24: j = 3;
then IFEQ(j,2,m.3,IFEQ(j,3,m.2,m.j)) = IFEQ(j,3,m.2,m.j) by
FUNCOP_1:def 8
.= m.2 by A24,FUNCOP_1:def 8;
hence thesis;
end;
then z2.j = m.2 by A17,A20,A22;
hence z1.j = z2.j by A15,A20,A22,A23;
end;
suppose
A25: j<>2 & j<>3;
A26: j<>2 & j<>3 implies IFEQ(j,2,m.3,IFEQ(j,3,m.2,m.j)) = m.j
proof
assume that
A27: j <> 2 and
A28: j <> 3;
IFEQ(j,2,m.3,IFEQ(j,3,m.2,m.j)) = IFEQ(j,3,m.2,m.j) by A27,
FUNCOP_1:def 8
.= m.j by A28,FUNCOP_1:def 8;
hence thesis;
end;
then z2.j = m.j by A17,A20,A25;
hence z1.j = z2.j by A15,A20,A25,A26;
end;
end;
hence z1.j = z2.j;
end;
dom m = Seg len(z1) by A14,FINSEQ_1:def 3
.= dom z1 by FINSEQ_1:def 3;
hence thesis by A18,A19,FINSEQ_1:13;
end;
end;
theorem Th26:
len m >= 4 implies IDEAoperationA(m,k,n).1 is_expressible_by n &
IDEAoperationA(m,k,n).2 is_expressible_by n & IDEAoperationA(m,k,n).3
is_expressible_by n & IDEAoperationA(m,k,n).4 is_expressible_by n
proof
assume
A1: len m >= 4;
then 1 <= len m by XXREAL_0:2;
then 1 in Seg len m by FINSEQ_1:1;
then 1 in dom m by FINSEQ_1:def 3;
then
A2: IDEAoperationA(m,k,n).1 = MUL_MOD(m.1, k.1, n) by Def11;
3 <= len m by A1,XXREAL_0:2;
then 3 in Seg len m by FINSEQ_1:1;
then 3 in dom m by FINSEQ_1:def 3;
then
A3: IDEAoperationA(m,k,n).3 = ADD_MOD(m.3, k.3, n) by Def11;
2 <= len m by A1,XXREAL_0:2;
then 2 in Seg len m by FINSEQ_1:1;
then 2 in dom m by FINSEQ_1:def 3;
then
A4: IDEAoperationA(m,k,n).2 = ADD_MOD(m.2, k.2, n) by Def11;
4 in Seg len m by A1,FINSEQ_1:1;
then 4 in dom m by FINSEQ_1:def 3;
then IDEAoperationA(m,k,n).4 = MUL_MOD(m.4, k.4, n) by Def11;
hence thesis by A2,A4,A3,Th15,Th24;
end;
theorem Th27:
for n being non zero Nat holds len m >= 4 implies
IDEAoperationB(m,k,n).1 is_expressible_by n & IDEAoperationB(m,k,n).2
is_expressible_by n & IDEAoperationB(m,k,n).3 is_expressible_by n &
IDEAoperationB(m,k,n).4 is_expressible_by n
proof
let n be non zero Nat;
assume
A1: len m >= 4;
then 1 <= len m by XXREAL_0:2;
then 1 in Seg len m by FINSEQ_1:1;
then 1 in dom m by FINSEQ_1:def 3;
then IDEAoperationB(m,k,n).1 = 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))) by Def12;
then
A2: IDEAoperationB(m,k,n).1 < 2 to_power n by BINARI_3:1;
3 <= len m by A1,XXREAL_0:2;
then 3 in Seg len m by FINSEQ_1:1;
then 3 in dom m by FINSEQ_1:def 3;
then IDEAoperationB(m,k,n).3 = 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))) by Def12;
then
A3: IDEAoperationB(m,k,n).3 < 2 to_power n by BINARI_3:1;
2 <= len m by A1,XXREAL_0:2;
then 2 in Seg len m by FINSEQ_1:1;
then 2 in dom m by FINSEQ_1:def 3;
then IDEAoperationB(m,k,n).2 = 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))) by Def12;
then
A4: IDEAoperationB(m,k,n).2 < 2 to_power n by BINARI_3:1;
4 in Seg len m by A1,FINSEQ_1:1;
then 4 in dom m by FINSEQ_1:def 3;
then IDEAoperationB(m,k,n).4 = 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))) by Def12;
then IDEAoperationB(m,k,n).4 < 2 to_power n by BINARI_3:1;
hence thesis by A2,A4,A3;
end;
Lm3: for i st i = 2 & i in dom m holds IDEAoperationC(m).i = m.3
proof
let i be Nat;
assume that
A1: i = 2 and
A2: i in dom m;
IDEAoperationC(m).i = IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) by A2,Def13
.= m.3 by A1,FUNCOP_1:def 8;
hence thesis;
end;
Lm4: for i st i = 3 & i in dom m holds IDEAoperationC(m).i = m.2
proof
let i be Nat;
assume that
A1: i = 3 and
A2: i in dom m;
IDEAoperationC(m).i = IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) by A2,Def13
.= IFEQ(i,3,m.2,m.i) by A1,FUNCOP_1:def 8
.= m.2 by A1,FUNCOP_1:def 8;
hence thesis;
end;
Lm5: for i st i <> 2 & i <> 3 & i in dom m holds IDEAoperationC(m).i = m.i
proof
let i be Nat;
assume that
A1: i <> 2 and
A2: i <> 3 and
A3: i in dom m;
IDEAoperationC(m).i = IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) by A3,Def13
.= IFEQ(i,3,m.2,m.i) by A1,FUNCOP_1:def 8
.= m.i by A2,FUNCOP_1:def 8;
hence thesis;
end;
theorem
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 implies IDEAoperationC(m).1
is_expressible_by n & IDEAoperationC(m).2 is_expressible_by n & IDEAoperationC(
m).3 is_expressible_by n & IDEAoperationC(m).4 is_expressible_by n
proof
assume that
A1: len m >= 4 and
A2: m.1 is_expressible_by n & m.2 is_expressible_by n & m.3
is_expressible_by n & m.4 is_expressible_by n;
1 <= len m by A1,XXREAL_0:2;
then 1 in Seg len m by FINSEQ_1:1;
then
A3: 1 in dom m by FINSEQ_1:def 3;
3 <= len m by A1,XXREAL_0:2;
then 3 in Seg len m by FINSEQ_1:1;
then
A4: 3 in dom m by FINSEQ_1:def 3;
2 <= len m by A1,XXREAL_0:2;
then 2 in Seg len m by FINSEQ_1:1;
then
A5: 2 in dom m by FINSEQ_1:def 3;
4 in Seg len m by A1,FINSEQ_1:1;
then 4 in dom m by FINSEQ_1:def 3;
hence thesis by A2,A3,A5,A4,Lm3,Lm4,Lm5;
end;
theorem Th29:
for n being non zero Nat,m,k1,k2 holds 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) implies IDEAoperationA( IDEAoperationA(m,k1,n), k2, n) = m
proof
let n be non zero Nat;
let m,k1,k2 be FinSequence of NAT;
assume that
A1: 2 to_power(n)+1 is prime and
A2: len m >= 4 and
A3: m.1 is_expressible_by n and
A4: m.2 is_expressible_by n and
A5: m.3 is_expressible_by n and
A6: m.4 is_expressible_by n and
A7: k1.1 is_expressible_by n and
A8: k1.2 is_expressible_by n and
A9: k1.3 is_expressible_by n and
A10: k1.4 is_expressible_by n and
A11: k2.1=INV_MOD(k1.1,n) and
A12: k2.2=NEG_MOD(k1.2,n) and
A13: k2.3=NEG_MOD(k1.3,n) and
A14: k2.4=INV_MOD(k1.4,n);
A15: k2.4 is_expressible_by n by A1,A10,A14,Def10;
2 <= len m by A2,XXREAL_0:2;
then 2 in Seg len m by FINSEQ_1:1;
then
A16: 2 in dom m by FINSEQ_1:def 3;
Seg len m = dom m by FINSEQ_1:def 3;
then
A17: 4 in dom m by A2,FINSEQ_1:1;
1 <= len m by A2,XXREAL_0:2;
then 1 in Seg len m by FINSEQ_1:1;
then
A18: 1 in dom m by FINSEQ_1:def 3;
3 <= len m by A2,XXREAL_0:2;
then 3 in Seg len m by FINSEQ_1:1;
then
A19: 3 in dom m by FINSEQ_1:def 3;
consider I1 being FinSequence of NAT such that
A20: I1 = IDEAoperationA(m,k1,n);
consider I2 being FinSequence of NAT such that
A21: I2 = IDEAoperationA(I1,k2,n);
A22: k2.1 is_expressible_by n by A1,A7,A11,Def10;
A23: now
let j be Nat;
assume
A24: j in Seg len m;
then j in Seg len I1 by A20,Def11;
then
A25: j in dom I1 by FINSEQ_1:def 3;
A26: j in dom m by A24,FINSEQ_1:def 3;
now
per cases;
suppose
A27: j = 1;
hence I2.j = MUL_MOD(I1.1, k2.1, n) by A21,A25,Def11
.= MUL_MOD(MUL_MOD(m.1, k1.1, n),k2.1,n) by A20,A18,Def11
.= MUL_MOD(m.1, MUL_MOD(k1.1,k2.1,n), n) by A1,A3,A7,A22,Th23
.= MUL_MOD(1, m.1, n) by A1,A7,A11,Def10
.= m.j by A3,A27,Th22;
end;
suppose
A28: j = 2;
hence I2.j = ADD_MOD(I1.2, k2.2, n) by A21,A25,Def11
.= ADD_MOD(ADD_MOD(m.2, k1.2, n), k2.2, n) by A20,A16,Def11
.= ADD_MOD(m.2, ADD_MOD(k1.2, k2.2, n), n) by Th14
.= ADD_MOD(0, m.2, n) by A8,A12,Th11
.= m.j by A4,A28,Th13;
end;
suppose
A29: j = 3;
hence I2.j = ADD_MOD(I1.3, k2.3, n) by A21,A25,Def11
.= ADD_MOD(ADD_MOD(m.3, k1.3, n), k2.3, n) by A20,A19,Def11
.= ADD_MOD(m.3, ADD_MOD(k1.3, k2.3, n), n) by Th14
.= ADD_MOD(0, m.3, n) by A9,A13,Th11
.= m.j by A5,A29,Th13;
end;
suppose
A30: j = 4;
hence I2.j = MUL_MOD(I1.4, k2.4, n) by A21,A25,Def11
.= MUL_MOD(MUL_MOD(m.4, k1.4, n),k2.4,n) by A20,A17,Def11
.= MUL_MOD(m.4, MUL_MOD(k1.4,k2.4,n), n) by A1,A6,A10,A15,Th23
.= MUL_MOD(1, m.4, n) by A1,A10,A14,Def10
.= m.j by A6,A30,Th22;
end;
suppose
A31: j<>1 & j<>2 & j<>3 & j<>4;
hence I2.j = I1.j by A21,A25,Def11
.= m.j by A20,A26,A31,Def11;
end;
end;
hence I2.j = m.j;
end;
A32: Seg len m = dom m by FINSEQ_1:def 3;
Seg len m = Seg len(I1) by A20,Def11
.= Seg len(I2) by A21,Def11
.= dom I2 by FINSEQ_1:def 3;
hence thesis by A20,A21,A32,A23,FINSEQ_1:13;
end;
theorem Th30:
for n being non zero Nat,m,k1,k2 holds 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) implies IDEAoperationA(IDEAoperationC(IDEAoperationA(
IDEAoperationC(m),k1,n)),k2,n) = m
proof
let n be non zero Nat;
let m,k1,k2 be FinSequence of NAT;
assume that
A1: 2 to_power(n)+1 is prime and
A2: len m >= 4 and
A3: m.1 is_expressible_by n and
A4: m.2 is_expressible_by n and
A5: m.3 is_expressible_by n and
A6: m.4 is_expressible_by n and
A7: k1.1 is_expressible_by n and
A8: k1.2 is_expressible_by n and
A9: k1.3 is_expressible_by n and
A10: k1.4 is_expressible_by n and
A11: k2.1=INV_MOD(k1.1,n) and
A12: k2.2=NEG_MOD(k1.3,n) and
A13: k2.3=NEG_MOD(k1.2,n) and
A14: k2.4=INV_MOD(k1.4,n);
A15: k2.1 is_expressible_by n by A1,A7,A11,Def10;
1 <= len m by A2,XXREAL_0:2;
then
A16: 1 in Seg len m by FINSEQ_1:1;
then
A17: 1 in dom m by FINSEQ_1:def 3;
A18: 4 in Seg len m by A2,FINSEQ_1:1;
then
A19: 4 in dom m by FINSEQ_1:def 3;
3 <= len m by A2,XXREAL_0:2;
then
A20: 3 in Seg len m by FINSEQ_1:1;
then
A21: 3 in dom m by FINSEQ_1:def 3;
A22: k2.4 is_expressible_by n by A1,A10,A14,Def10;
consider I1 being FinSequence of NAT such that
A23: I1 = IDEAoperationC(m);
4 in Seg len(I1) by A23,A18,Def13;
then
A24: 4 in dom(I1) by FINSEQ_1:def 3;
1 in Seg len(I1) by A23,A16,Def13;
then
A25: 1 in dom(I1) by FINSEQ_1:def 3;
2 <= len m by A2,XXREAL_0:2;
then
A26: 2 in Seg len m by FINSEQ_1:1;
then
A27: 2 in dom m by FINSEQ_1:def 3;
3 in Seg len(I1) by A23,A20,Def13;
then
A28: 3 in dom(I1) by FINSEQ_1:def 3;
2 in Seg len(I1) by A23,A26,Def13;
then
A29: 2 in dom(I1) by FINSEQ_1:def 3;
consider I2 being FinSequence of NAT such that
A30: I2 = IDEAoperationA(I1,k1,n);
A31: len(I2) = len(I1) by A30,Def11;
then 2 in Seg len(I2) by A23,A26,Def13;
then
A32: 2 in dom(I2) by FINSEQ_1:def 3;
4 in Seg len(I2) by A23,A31,A18,Def13;
then
A33: 4 in dom(I2) by FINSEQ_1:def 3;
1 in Seg len(I2) by A23,A31,A16,Def13;
then
A34: 1 in dom(I2) by FINSEQ_1:def 3;
3 in Seg len(I2) by A23,A31,A20,Def13;
then
A35: 3 in dom(I2) by FINSEQ_1:def 3;
consider I3 being FinSequence of NAT such that
A36: I3 = IDEAoperationC(I2);
A37: len(I3) = len(I2) by A36,Def13;
then 2 in Seg len(I3) by A23,A31,A26,Def13;
then
A38: 2 in dom(I3) by FINSEQ_1:def 3;
4 in Seg len(I3) by A23,A31,A37,A18,Def13;
then
A39: 4 in dom(I3) by FINSEQ_1:def 3;
3 in Seg len(I3) by A23,A31,A37,A20,Def13;
then
A40: 3 in dom(I3) by FINSEQ_1:def 3;
consider I4 being FinSequence of NAT such that
A41: I4 = IDEAoperationA(I3,k2,n);
1 in Seg len(I3) by A23,A31,A37,A16,Def13;
then
A42: 1 in dom(I3) by FINSEQ_1:def 3;
A43: now
let j be Nat;
assume
A44: j in Seg len m;
then
A45: j in dom m by FINSEQ_1:def 3;
A46: j in Seg len I1 by A23,A44,Def13;
then
A47: j in Seg len I2 by A30,Def11;
then
A48: j in dom I2 by FINSEQ_1:def 3;
j in Seg len I3 by A36,A47,Def13;
then
A49: j in dom I3 by FINSEQ_1:def 3;
A50: j in dom I1 by A46,FINSEQ_1:def 3;
now
per cases;
suppose
A51: j = 1;
hence I4.j = MUL_MOD(I3.1, k2.1, n) by A41,A42,Def11
.= MUL_MOD(I2.1, k2.1, n) by A36,A34,Lm5
.= MUL_MOD(MUL_MOD(I1.1, k1.1, n), k2.1, n) by A30,A25,Def11
.= MUL_MOD(MUL_MOD(m.1, k1.1, n), k2.1, n) by A23,A17,Lm5
.= MUL_MOD(m.1, MUL_MOD(k1.1, k2.1, n), n) by A1,A3,A7,A15,Th23
.= MUL_MOD(1, m.1, n) by A1,A7,A11,Def10
.= m.j by A3,A51,Th22;
end;
suppose
A52: j = 2;
hence I4.j = ADD_MOD(I3.2, k2.2, n) by A41,A38,Def11
.= ADD_MOD(I2.3, k2.2, n) by A36,A32,Lm3
.= ADD_MOD(ADD_MOD(I1.3, k1.3, n), k2.2, n) by A30,A28,Def11
.= ADD_MOD(ADD_MOD(m.2, k1.3, n), k2.2, n) by A23,A21,Lm4
.= ADD_MOD(m.2, ADD_MOD(k1.3, k2.2, n), n) by Th14
.= ADD_MOD(0, m.2, n) by A9,A12,Th11
.= m.j by A4,A52,Th13;
end;
suppose
A53: j = 3;
hence I4.j = ADD_MOD(I3.3, k2.3, n) by A41,A40,Def11
.= ADD_MOD(I2.2, k2.3, n) by A36,A35,Lm4
.= ADD_MOD(ADD_MOD(I1.2, k1.2, n), k2.3, n) by A30,A29,Def11
.= ADD_MOD(ADD_MOD(m.3, k1.2, n), k2.3, n) by A23,A27,Lm3
.= ADD_MOD(m.3, ADD_MOD(k1.2, k2.3, n), n) by Th14
.= ADD_MOD(0, m.3, n) by A8,A13,Th11
.= m.j by A5,A53,Th13;
end;
suppose
A54: j = 4;
hence I4.j = MUL_MOD(I3.4, k2.4, n) by A41,A39,Def11
.= MUL_MOD(I2.4, k2.4, n) by A36,A33,Lm5
.= MUL_MOD(MUL_MOD(I1.4, k1.4, n), k2.4, n) by A30,A24,Def11
.= MUL_MOD(MUL_MOD(m.4, k1.4, n), k2.4, n) by A23,A19,Lm5
.= MUL_MOD(m.4, MUL_MOD(k1.4, k2.4, n), n) by A1,A6,A10,A22,Th23
.= MUL_MOD(1, m.4, n) by A1,A10,A14,Def10
.= m.j by A6,A54,Th22;
end;
suppose
A55: j<>1 & j<>2 & j<>3 & j<>4;
hence I4.j = I3.j by A41,A49,Def11
.= I2.j by A36,A48,A55,Lm5
.= I1.j by A30,A50,A55,Def11
.= m.j by A23,A45,A55,Lm5;
end;
end;
hence I4.j = m.j;
end;
A56: Seg len m = dom m by FINSEQ_1:def 3;
Seg len m = Seg len(I1) by A23,Def13
.= Seg len(I2) by A30,Def11
.= Seg len(I3) by A36,Def13
.= Seg len(I4) by A41,Def11
.= dom I4 by FINSEQ_1:def 3;
hence thesis by A23,A30,A36,A41,A56,A43,FINSEQ_1:13;
end;
theorem Th31:
for n being non zero Nat,m,k1,k2 holds 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 & k2.5=k1.5 & k2.6=k1.6 implies IDEAoperationB(
IDEAoperationB(m,k1,n), k2, n) = m
proof
let n be non zero Nat;
let m,k1,k2 be FinSequence of NAT;
assume that
A1: len m >= 4 and
A2: m.1 is_expressible_by n and
A3: m.2 is_expressible_by n and
A4: m.3 is_expressible_by n and
A5: m.4 is_expressible_by n and
A6: k2.5= k1.5 and
A7: k2.6= k1.6;
consider t10 being Nat such that
A8: t10 = MUL_MOD( Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence
m.3)),k1.5,n);
consider t11 being Nat such that
A9: t11 = MUL_MOD(ADD_MOD(t10, Absval((n-BinarySequence m.2) 'xor' (n
-BinarySequence m.4)),n),k1.6,n);
consider I1 being FinSequence of NAT such that
A10: I1 = IDEAoperationB(m,k1,n);
1 <= len m by A1,XXREAL_0:2;
then 1 in Seg len m by FINSEQ_1:1;
then 1 in dom m by FINSEQ_1:def 3;
then
A11: I1.1 = Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence t11)) by A8
,A9,A10,Def12;
consider t20 being Nat such that
A12: t20 = MUL_MOD( Absval((n-BinarySequence I1.1) 'xor' (n
-BinarySequence I1.3)),k2.5,n);
3 <= len m by A1,XXREAL_0:2;
then 3 in Seg len m by FINSEQ_1:1;
then 3 in dom m by FINSEQ_1:def 3;
then
A13: I1.3 = Absval((n-BinarySequence m.3) 'xor' (n-BinarySequence t11)) by A8
,A9,A10,Def12;
then
A14: t20 = MUL_MOD( Absval(((n-BinarySequence m.1) 'xor' (n-BinarySequence
t11)) 'xor' (n-BinarySequence Absval((n-BinarySequence m.3) 'xor' (n
-BinarySequence t11)))),k2.5,n) by A12,A11,BINARI_3:36
.= MUL_MOD( Absval(((n-BinarySequence m.1) 'xor' (n-BinarySequence t11))
'xor' ((n-BinarySequence m.3) 'xor' (n-BinarySequence t11))),k2.5,n) by
BINARI_3:36
.= MUL_MOD( Absval((n-BinarySequence m.1) 'xor' ((n-BinarySequence t11)
'xor' ((n-BinarySequence t11) 'xor' (n-BinarySequence m.3)))),k2.5,n) by Th9
.= MUL_MOD( Absval((n-BinarySequence m.1) 'xor' (((n-BinarySequence t11)
'xor' (n-BinarySequence t11)) 'xor' (n-BinarySequence m.3))),k2.5,n) by Th9
.= MUL_MOD( Absval((n-BinarySequence m.1) 'xor' (ZERO(n) 'xor' (n
-BinarySequence m.3))),k2.5,n) by Th6
.= t10 by A6,A8,Th8;
consider t21 being Nat such that
A15: t21 = MUL_MOD(ADD_MOD(t20, Absval((n-BinarySequence I1.2) 'xor' (n
-BinarySequence I1.4)),n),k2.6,n);
consider t12 being Nat such that
A16: t12 = ADD_MOD(t10, t11, n);
2 <= len m by A1,XXREAL_0:2;
then 2 in Seg len m by FINSEQ_1:1;
then 2 in dom m by FINSEQ_1:def 3;
then
A17: I1.2 = Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence t12)) by A8
,A9,A16,A10,Def12;
consider I2 being FinSequence of NAT such that
A18: I2 = IDEAoperationB(I1,k2,n);
4 in Seg len m by A1,FINSEQ_1:1;
then 4 in dom m by FINSEQ_1:def 3;
then
A19: I1.4 = Absval((n-BinarySequence m.4) 'xor' (n-BinarySequence t12)) by A8
,A9,A16,A10,Def12;
then
A20: t21 = MUL_MOD(ADD_MOD(t10, Absval(((n-BinarySequence m.2) 'xor' (n
-BinarySequence t12) ) 'xor' (n-BinarySequence Absval( (n-BinarySequence m.4)
'xor' (n-BinarySequence t12) ) ) ),n),k2.6,n) by A15,A17,A14,BINARI_3:36
.= MUL_MOD(ADD_MOD(t10, Absval(((n-BinarySequence m.2) 'xor' (n
-BinarySequence t12) ) 'xor' ((n-BinarySequence m.4) 'xor' (n-BinarySequence
t12) ) ),n),k2.6,n) by BINARI_3:36
.= MUL_MOD(ADD_MOD(t10, Absval( (n-BinarySequence m.2) 'xor' ((n
-BinarySequence t12) 'xor' ((n-BinarySequence t12) 'xor' (n-BinarySequence m.4)
) ) ),n),k2.6,n) by Th9
.= MUL_MOD(ADD_MOD(t10, Absval( (n-BinarySequence m.2) 'xor' ((n
-BinarySequence t12) 'xor' (n-BinarySequence t12) 'xor' (n-BinarySequence m.4)
) ),n),k2.6,n) by Th9
.= MUL_MOD(ADD_MOD(t10, Absval( (n-BinarySequence m.2) 'xor' (ZERO(n)
'xor' (n-BinarySequence m.4) ) ),n),k2.6,n) by Th6
.= t11 by A7,A9,Th8;
A21: now
let j be Nat;
assume
A22: j in Seg len m;
then j in Seg len I1 by A10,Def12;
then
A23: j in dom I1 by FINSEQ_1:def 3;
A24: j in dom m by A22,FINSEQ_1:def 3;
now
per cases;
suppose
A25: j = 1;
A26: m.1 < 2 to_power n by A2;
thus I2.j = Absval((n-BinarySequence I1.1) 'xor' (n-BinarySequence t11
)) by A12,A15,A18,A20,A23,A25,Def12
.= Absval(((n-BinarySequence m.1) 'xor' (n-BinarySequence t11))
'xor' (n-BinarySequence t11)) by A11,BINARI_3:36
.= Absval((n-BinarySequence m.1) 'xor' ((n-BinarySequence t11)
'xor' (n-BinarySequence t11))) by Th9
.= Absval(ZERO(n) 'xor' (n-BinarySequence m.1)) by Th6
.= Absval(n-BinarySequence m.1) by Th8
.= m.j by A25,A26,BINARI_3:35;
end;
suppose
A27: j = 2;
A28: m.2 < 2 to_power n by A3;
thus I2.j = Absval((n-BinarySequence I1.2) 'xor' (n-BinarySequence t12
)) by A16,A12,A15,A18,A14,A20,A23,A27,Def12
.= Absval(((n-BinarySequence m.2) 'xor' (n-BinarySequence t12))
'xor' (n-BinarySequence t12)) by A17,BINARI_3:36
.= Absval((n-BinarySequence m.2) 'xor' ((n-BinarySequence t12)
'xor' (n-BinarySequence t12)))by Th9
.= Absval(ZERO(n) 'xor' (n-BinarySequence m.2)) by Th6
.= Absval(n-BinarySequence m.2) by Th8
.= m.j by A27,A28,BINARI_3:35;
end;
suppose
A29: j = 3;
A30: m.3 < 2 to_power n by A4;
thus I2.j = Absval((n-BinarySequence I1.3) 'xor' (n-BinarySequence t11
)) by A12,A15,A18,A20,A23,A29,Def12
.= Absval(((n-BinarySequence m.3) 'xor' (n-BinarySequence t11))
'xor' (n-BinarySequence t11)) by A13,BINARI_3:36
.= Absval((n-BinarySequence m.3) 'xor' ((n-BinarySequence t11)
'xor' (n-BinarySequence t11))) by Th9
.= Absval(ZERO(n) 'xor' (n-BinarySequence m.3)) by Th6
.= Absval(n-BinarySequence m.3) by Th8
.= m.j by A29,A30,BINARI_3:35;
end;
suppose
A31: j = 4;
A32: m.4 < 2 to_power n by A5;
thus I2.j = Absval((n-BinarySequence I1.4) 'xor' (n-BinarySequence t12
)) by A16,A12,A15,A18,A14,A20,A23,A31,Def12
.= Absval(((n-BinarySequence m.4) 'xor' (n-BinarySequence t12))
'xor' (n-BinarySequence t12)) by A19,BINARI_3:36
.= Absval((n-BinarySequence m.4) 'xor' ((n-BinarySequence t12)
'xor' (n-BinarySequence t12))) by Th9
.= Absval(ZERO(n) 'xor' (n-BinarySequence m.4)) by Th6
.= Absval(n-BinarySequence m.4) by Th8
.= m.j by A31,A32,BINARI_3:35;
end;
suppose
A33: j<>1 & j<>2 & j<>3 & j<>4;
hence I2.j = I1.j by A18,A23,Def12
.= m.j by A10,A24,A33,Def12;
end;
end;
hence I2.j = m.j;
end;
A34: Seg len m = dom m by FINSEQ_1:def 3;
Seg len m = Seg len(I1) by A10,Def12
.= Seg len(I2) by A18,Def12
.= dom I2 by FINSEQ_1:def 3;
hence thesis by A10,A18,A34,A21,FINSEQ_1:13;
end;
theorem
for m holds len m >= 4 implies IDEAoperationC( IDEAoperationC(m) ) = m
proof
let m be FinSequence of NAT;
consider I1 being FinSequence of NAT such that
A1: I1 = IDEAoperationC(m);
assume
A2: len m >= 4;
then 2 <= len m by XXREAL_0:2;
then 2 in Seg len m by FINSEQ_1:1;
then 2 in dom m by FINSEQ_1:def 3;
then
A3: I1.2 = m.3 by A1,Lm3;
consider I2 being FinSequence of NAT such that
A4: I2 = IDEAoperationC(I1);
3 <= len m by A2,XXREAL_0:2;
then 3 in Seg len m by FINSEQ_1:1;
then 3 in dom m by FINSEQ_1:def 3;
then
A5: I1.3 = m.2 by A1,Lm4;
A6: now
let j be Nat;
assume
A7: j in Seg len m;
then j in Seg len I1 by A1,Def13;
then
A8: j in dom I1 by FINSEQ_1:def 3;
A9: j in dom m by A7,FINSEQ_1:def 3;
now
per cases;
suppose
j = 2;
hence I2.j = m.j by A4,A5,A8,Lm3;
end;
suppose
j = 3;
hence I2.j = m.j by A4,A3,A8,Lm4;
end;
suppose
A10: j<>2 & j<>3;
hence I2.j = I1.j by A4,A8,Lm5
.= m.j by A1,A9,A10,Lm5;
end;
end;
hence I2.j = m.j;
end;
A11: Seg len m = dom m by FINSEQ_1:def 3;
Seg len m = Seg len(I1) by A1,Def13
.= Seg len(I2) by A4,Def13
.= dom I2 by FINSEQ_1:def 3;
hence thesis by A1,A4,A11,A6,FINSEQ_1:13;
end;
begin :: Sequences of IDEA Cryptogram's operations
:: For making a model of IDEA, we define sequences of IDEA's
:: operations IDEA_P, IDEA_PS, IDEA_PE, IDEA_Q, IDEA_QS and
:: IDEA_QE. And, we define MESSAGES as plain and cipher text.
definition
func MESSAGES -> set equals
NAT*;
coherence;
end;
registration
cluster MESSAGES -> non empty;
coherence;
end;
registration
cluster MESSAGES -> functional;
coherence;
end;
registration
cluster -> FinSequence-like for Element of MESSAGES;
coherence;
end;
definition
let n be non zero Nat,k;
func IDEA_P(k,n) -> Function of MESSAGES, MESSAGES means
:Def15:
for m holds it.m = IDEAoperationA(IDEAoperationC(IDEAoperationB(m,k,n)),k,n);
existence
proof
defpred P[set,set] means ex F be FinSequence of NAT st $1 = F & $2 =
IDEAoperationA(IDEAoperationC( IDEAoperationB(F,k,n)),k,n);
A1: for e being Element of MESSAGES ex u being Element of MESSAGES st P[e, u]
proof
let e be Element of MESSAGES;
reconsider F = e as FinSequence of NAT by FINSEQ_1:def 11;
reconsider u = IDEAoperationA(IDEAoperationC( IDEAoperationB(F,k,n)),k,n
) as Element of MESSAGES by FINSEQ_1:def 11;
take u;
thus thesis;
end;
consider m1 being Function of MESSAGES,MESSAGES such that
A2: for e being Element of MESSAGES holds P[e,m1.e] from FUNCT_2:sch 3
(A1);
take m1;
let m be FinSequence of NAT;
m is Element of MESSAGES by FINSEQ_1:def 11;
then ex F being FinSequence of NAT st m = F & m1.m = IDEAoperationA(
IDEAoperationC( IDEAoperationB(F,k,n)),k,n) by A2;
hence thesis;
end;
uniqueness
proof
let m1,m2 be Function of MESSAGES, MESSAGES such that
A3: for m being FinSequence of NAT holds m1.m = IDEAoperationA(
IDEAoperationC( IDEAoperationB(m,k,n)),k,n) and
A4: for m being FinSequence of NAT holds m2.m = IDEAoperationA(
IDEAoperationC( IDEAoperationB(m,k,n)),k,n);
A5: now
let j be object;
reconsider jj = j as set by TARSKI:1;
assume j in MESSAGES;
then reconsider jj as FinSequence of NAT by FINSEQ_1:def 11;
thus m1.j = IDEAoperationA(IDEAoperationC( IDEAoperationB(jj,k,n)),k,n)
by A3
.= m2.j by A4;
end;
dom m1 = MESSAGES & dom m2 = MESSAGES by FUNCT_2:def 1;
hence thesis by A5,FUNCT_1:2;
end;
end;
definition
let n be non zero Nat,k;
func IDEA_Q(k,n) -> Function of MESSAGES, MESSAGES means
:Def16:
for m holds it.m = IDEAoperationB(IDEAoperationA(IDEAoperationC(m),k,n),k,n);
existence
proof
defpred P[set,set] means ex F be FinSequence of NAT st $1 = F & $2 =
IDEAoperationB(IDEAoperationA( IDEAoperationC(F),k,n),k,n);
A1: for e being Element of MESSAGES ex u being Element of MESSAGES st P[e, u]
proof
let e be Element of MESSAGES;
reconsider F = e as FinSequence of NAT by FINSEQ_1:def 11;
reconsider u = IDEAoperationB(IDEAoperationA( IDEAoperationC(F),k,n),k,n
) as Element of MESSAGES by FINSEQ_1:def 11;
take u;
thus thesis;
end;
consider m1 being Function of MESSAGES,MESSAGES such that
A2: for e being Element of MESSAGES holds P[e,m1.e] from FUNCT_2:sch 3
(A1);
take m1;
let m be FinSequence of NAT;
m is Element of MESSAGES by FINSEQ_1:def 11;
then ex F being FinSequence of NAT st m = F & m1.m = IDEAoperationB(
IDEAoperationA( IDEAoperationC(F),k,n),k,n) by A2;
hence thesis;
end;
uniqueness
proof
let m1,m2 be Function of MESSAGES, MESSAGES such that
A3: for m being FinSequence of NAT holds m1.m = IDEAoperationB(
IDEAoperationA( IDEAoperationC(m),k,n),k,n) and
A4: for m being FinSequence of NAT holds m2.m = IDEAoperationB(
IDEAoperationA( IDEAoperationC(m),k,n),k,n);
A5: now
let j be object;
reconsider jj = j as set by TARSKI:1;
assume j in MESSAGES;
then reconsider jj as FinSequence of NAT by FINSEQ_1:def 11;
thus m1.j = IDEAoperationB(IDEAoperationA( IDEAoperationC(jj),k,n),k,n)
by A3
.= m2.j by A4;
end;
dom m1 = MESSAGES & dom m2 = MESSAGES by FUNCT_2:def 1;
hence thesis by A5,FUNCT_1:2;
end;
end;
definition
let r,lk be Nat,n be non zero Nat, Key be Matrix of
lk,6,NAT;
func IDEA_P_F(Key,n,r) -> FinSequence means
:Def17:
len it = r & for i st i in dom it holds it.i = IDEA_P(Line(Key,i),n);
existence
proof
deffunc F(Nat)=IDEA_P(Line(Key,$1),n);
consider z being FinSequence such that
A1: len z = r & for k being Nat st k in dom z holds z.k= F(k) from
FINSEQ_1:sch 2;
take z;
thus thesis by A1;
end;
uniqueness
proof
let z1,z2 be FinSequence such that
A2: len z1 = r and
A3: for i being Nat st i in dom z1 holds z1.i = IDEA_P(Line
( Key,i),n) and
A4: len z2 = r and
A5: for i being Nat st i in dom z2 holds z2.i = IDEA_P(Line
( Key,i),n);
A6: now
let j be Nat;
assume
A7: j in Seg r;
then
A8: j in dom z2 by A4,FINSEQ_1:def 3;
j in dom z1 by A2,A7,FINSEQ_1:def 3;
then z1.j = IDEA_P(Line(Key,j),n) by A3
.= z2.j by A5,A8;
hence z1.j = z2.j;
end;
Seg r = dom z1 & Seg r = dom z2 by A2,A4,FINSEQ_1:def 3;
hence thesis by A6,FINSEQ_1:13;
end;
end;
registration
let r,lk be Nat,n be non zero Nat, Key be Matrix of
lk,6,NAT;
cluster IDEA_P_F(Key,n,r) -> Function-yielding;
coherence
proof
for x being object st x in dom IDEA_P_F(Key,n,r)
holds IDEA_P_F(Key,n,r).x is Function
proof
let x be object;
assume
A1: x in dom IDEA_P_F(Key,n,r);
then consider xx being Nat such that
A2: xx = x;
IDEA_P_F(Key,n,r).xx = IDEA_P(Line(Key,xx),n) by A1,A2,Def17;
hence thesis by A2;
end;
hence thesis;
end;
end;
definition
let r,lk be Nat,n be non zero Nat, Key be Matrix of
lk,6,NAT;
func IDEA_Q_F(Key,n,r) -> FinSequence means
:Def18:
len it = r & for i st i in dom it holds it.i = IDEA_Q(Line(Key,r-'i+1),n);
existence
proof
deffunc F(Nat)=IDEA_Q(Line(Key,r-'$1+1),n);
consider z being FinSequence such that
A1: len z = r & for k being Nat st k in dom z holds z.k= F(k) from
FINSEQ_1:sch 2;
take z;
thus thesis by A1;
end;
uniqueness
proof
let z1,z2 be FinSequence such that
A2: len z1 = r and
A3: for i being Nat st i in dom z1 holds z1.i = IDEA_Q(Line
( Key,r-'i+1),n) and
A4: len z2 = r and
A5: for i being Nat st i in dom z2 holds z2.i = IDEA_Q(Line
( Key,r-'i+1),n);
A6: now
let j be Nat;
assume
A7: j in Seg r;
then
A8: j in dom z2 by A4,FINSEQ_1:def 3;
j in dom z1 by A2,A7,FINSEQ_1:def 3;
then z1.j = IDEA_Q(Line(Key,r-'j+1),n) by A3
.= z2.j by A5,A8;
hence z1.j = z2.j;
end;
Seg r = dom z1 & Seg r = dom z2 by A2,A4,FINSEQ_1:def 3;
hence thesis by A6,FINSEQ_1:13;
end;
end;
registration
let r,lk be Nat,n be non zero Nat, Key be Matrix of
lk,6,NAT;
cluster IDEA_Q_F(Key,n,r) -> Function-yielding;
coherence
proof
let x be object;
assume
A1: x in dom IDEA_Q_F(Key,n,r);
then consider xx being Nat such that
A2: xx = x;
IDEA_Q_F(Key,n,r).xx = IDEA_Q(Line(Key,r-'xx+1),n) by A1,A2,Def18;
hence thesis by A2;
end;
end;
definition
let k,n;
func IDEA_PS(k,n) -> Function of MESSAGES, MESSAGES means
:Def19:
for m holds it.m = IDEAoperationA(m,k,n);
existence
proof
defpred P[set,set] means ex F be FinSequence of NAT st $1 = F & $2 =
IDEAoperationA(F,k,n);
A1: for e being Element of MESSAGES ex u being Element of MESSAGES st P[e, u]
proof
let e be Element of MESSAGES;
reconsider F = e as FinSequence of NAT by FINSEQ_1:def 11;
reconsider u = IDEAoperationA(F,k,n) as Element of MESSAGES by
FINSEQ_1:def 11;
take u;
thus thesis;
end;
consider m1 being Function of MESSAGES,MESSAGES such that
A2: for e being Element of MESSAGES holds P[e,m1.e] from FUNCT_2:sch 3
(A1);
take m1;
let m be FinSequence of NAT;
m is Element of MESSAGES by FINSEQ_1:def 11;
then ex F being FinSequence of NAT st m = F & m1.m = IDEAoperationA(F,k,n)
by A2;
hence thesis;
end;
uniqueness
proof
let m1,m2 be Function of MESSAGES, MESSAGES such that
A3: for m being FinSequence of NAT holds m1.m = IDEAoperationA(m,k,n) and
A4: for m being FinSequence of NAT holds m2.m = IDEAoperationA(m,k,n);
A5: now
let j be object;
reconsider jj = j as set by TARSKI:1;
assume j in MESSAGES;
then reconsider jj as FinSequence of NAT by FINSEQ_1:def 11;
thus m1.j = IDEAoperationA(jj,k,n) by A3
.= m2.j by A4;
end;
dom m1 = MESSAGES & dom m2 = MESSAGES by FUNCT_2:def 1;
hence thesis by A5,FUNCT_1:2;
end;
end;
definition
let k,n;
func IDEA_QS(k,n) -> Function of MESSAGES, MESSAGES means
:Def20:
for m holds it.m = IDEAoperationA(m,k,n);
existence
proof
defpred P[set,set] means ex F be FinSequence of NAT st $1 = F & $2 =
IDEAoperationA(F,k,n);
A1: for e being Element of MESSAGES ex u being Element of MESSAGES st P[e, u]
proof
let e be Element of MESSAGES;
reconsider F = e as FinSequence of NAT by FINSEQ_1:def 11;
reconsider u = IDEAoperationA(F,k,n) as Element of MESSAGES by
FINSEQ_1:def 11;
take u;
thus thesis;
end;
consider m1 being Function of MESSAGES,MESSAGES such that
A2: for e being Element of MESSAGES holds P[e,m1.e] from FUNCT_2:sch 3
(A1);
take m1;
let m be FinSequence of NAT;
m is Element of MESSAGES by FINSEQ_1:def 11;
then ex F being FinSequence of NAT st m = F & m1.m = IDEAoperationA(F,k,n)
by A2;
hence thesis;
end;
uniqueness
proof
let m1,m2 be Function of MESSAGES, MESSAGES such that
A3: for m being FinSequence of NAT holds m1.m = IDEAoperationA(m,k,n) and
A4: for m being FinSequence of NAT holds m2.m = IDEAoperationA(m,k,n);
A5: now
let j be object;
reconsider jj = j as set by TARSKI:1;
assume j in MESSAGES;
then reconsider jj as FinSequence of NAT by FINSEQ_1:def 11;
thus m1.j = IDEAoperationA(jj,k,n) by A3
.= m2.j by A4;
end;
dom m1 = MESSAGES & dom m2 = MESSAGES by FUNCT_2:def 1;
hence thesis by A5,FUNCT_1:2;
end;
end;
definition
let n be non zero Nat,k;
func IDEA_PE(k,n) -> Function of MESSAGES, MESSAGES means
:Def21:
for m holds it.m = IDEAoperationA(IDEAoperationB(m,k,n),k,n);
existence
proof
defpred P[set,set] means ex F be FinSequence of NAT st $1 = F & $2 =
IDEAoperationA(IDEAoperationB(F,k,n),k,n);
A1: for e being Element of MESSAGES ex u being Element of MESSAGES st P[e, u]
proof
let e be Element of MESSAGES;
reconsider F = e as FinSequence of NAT by FINSEQ_1:def 11;
reconsider u = IDEAoperationA( IDEAoperationB(F,k,n),k,n) as Element of
MESSAGES by FINSEQ_1:def 11;
take u;
thus thesis;
end;
consider m1 being Function of MESSAGES,MESSAGES such that
A2: for e being Element of MESSAGES holds P[e,m1.e] from FUNCT_2:sch 3
(A1);
take m1;
let m be FinSequence of NAT;
m is Element of MESSAGES by FINSEQ_1:def 11;
then ex F being FinSequence of NAT st m = F & m1.m = IDEAoperationA(
IDEAoperationB(F,k,n),k,n) by A2;
hence thesis;
end;
uniqueness
proof
let m1,m2 be Function of MESSAGES, MESSAGES such that
A3: for m being FinSequence of NAT holds m1.m = IDEAoperationA(
IDEAoperationB(m,k,n),k,n) and
A4: for m being FinSequence of NAT holds m2.m = IDEAoperationA(
IDEAoperationB(m,k,n),k,n);
A5: now
let j be object;
reconsider jj = j as set by TARSKI:1;
assume j in MESSAGES;
then reconsider jj as FinSequence of NAT by FINSEQ_1:def 11;
thus m1.j = IDEAoperationA( IDEAoperationB(jj,k,n),k,n) by A3
.= m2.j by A4;
end;
dom m1 = MESSAGES & dom m2 = MESSAGES by FUNCT_2:def 1;
hence thesis by A5,FUNCT_1:2;
end;
end;
definition
let n be non zero Nat,k;
func IDEA_QE(k,n) -> Function of MESSAGES, MESSAGES means
:Def22:
for m holds it.m = IDEAoperationB(IDEAoperationA(m,k,n),k,n);
existence
proof
defpred P[set,set] means ex F be FinSequence of NAT st $1 = F & $2 =
IDEAoperationB(IDEAoperationA(F,k,n),k,n);
A1: for e being Element of MESSAGES ex u being Element of MESSAGES st P[e, u]
proof
let e be Element of MESSAGES;
reconsider F = e as FinSequence of NAT by FINSEQ_1:def 11;
reconsider u = IDEAoperationB( IDEAoperationA(F,k,n),k,n) as Element of
MESSAGES by FINSEQ_1:def 11;
take u;
thus thesis;
end;
consider m1 being Function of MESSAGES,MESSAGES such that
A2: for e being Element of MESSAGES holds P[e,m1.e] from FUNCT_2:sch 3
(A1);
take m1;
let m be FinSequence of NAT;
m is Element of MESSAGES by FINSEQ_1:def 11;
then ex F being FinSequence of NAT st m = F & m1.m = IDEAoperationB(
IDEAoperationA(F,k,n),k,n) by A2;
hence thesis;
end;
uniqueness
proof
let m1,m2 be Function of MESSAGES, MESSAGES such that
A3: for m being FinSequence of NAT holds m1.m = IDEAoperationB(
IDEAoperationA(m,k,n),k,n) and
A4: for m being FinSequence of NAT holds m2.m = IDEAoperationB(
IDEAoperationA(m,k,n),k,n);
A5: now
let j be object;
reconsider jj = j as set by TARSKI:1;
assume j in MESSAGES;
then reconsider jj as FinSequence of NAT by FINSEQ_1:def 11;
thus m1.j = IDEAoperationB( IDEAoperationA(jj,k,n),k,n) by A3
.= m2.j by A4;
end;
dom m1 = MESSAGES & dom m2 = MESSAGES by FUNCT_2:def 1;
hence thesis by A5,FUNCT_1:2;
end;
end;
theorem Th33:
for n being non zero Nat,m,k1,k2 holds 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) & k2.5 = k1.5 & k2.6 = k1.6 implies (IDEA_Q(k2,n)*IDEA_P(
k1,n)).m = m
proof
let n be non zero Nat;
let m,k1,k2;
assume that
A1: 2 to_power(n)+1 is prime and
A2: len m >= 4 and
A3: 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
A4: 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) and
A5: k2.5 = k1.5 & k2.6 = k1.6;
A6: IDEAoperationB(m,k1,n).2 is_expressible_by n & IDEAoperationB(m,k1,n).3
is_expressible_by n by A2,Th27;
A7: IDEAoperationB(m,k1,n).4 is_expressible_by n by A2,Th27;
A8: len IDEAoperationB(m,k1,n) >= 4 & IDEAoperationB(m,k1,n).1
is_expressible_by n by A2,Def12,Th27;
dom IDEA_P(k1,n) = MESSAGES by FUNCT_2:def 1;
then m in dom IDEA_P(k1,n) by FINSEQ_1:def 11;
then (IDEA_Q(k2,n)*IDEA_P(k1,n)).m = IDEA_Q(k2,n).(IDEA_P(k1,n).m) by
FUNCT_1:13
.= IDEA_Q(k2,n). IDEAoperationA(IDEAoperationC(IDEAoperationB(m,k1,n)),
k1,n) by Def15
.= IDEAoperationB(IDEAoperationA(IDEAoperationC( IDEAoperationA(
IDEAoperationC(IDEAoperationB(m,k1,n)),k1,n) ),k2,n),k2,n) by Def16
.= IDEAoperationB(IDEAoperationB(m,k1,n),k2,n) by A1,A4,A8,A6,A7,Th30
.= m by A2,A3,A5,Th31;
hence thesis;
end;
theorem Th34:
for n being non zero Nat,m,k1,k2 holds 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) implies (IDEA_QS(k2,n)*IDEA_PS(k1,n)).m = m
proof
let n be non zero Nat;
let m,k1,k2;
assume
A1: 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);
dom IDEA_PS(k1,n) = MESSAGES by FUNCT_2:def 1;
then m in dom IDEA_PS(k1,n) by FINSEQ_1:def 11;
then (IDEA_QS(k2,n)*IDEA_PS(k1,n)).m = IDEA_QS(k2,n).(IDEA_PS(k1,n).m) by
FUNCT_1:13
.= IDEA_QS(k2,n).IDEAoperationA(m,k1,n) by Def19
.= IDEAoperationA(IDEAoperationA(m,k1,n),k2,n) by Def20
.= m by A1,Th29;
hence thesis;
end;
theorem Th35:
for n being non zero Nat,m,k1,k2 holds 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) & k2.5 = k1.5 & k2.6 = k1.6 implies (IDEA_QE(k2,n)*IDEA_PE
(k1,n)).m = m
proof
let n be non zero Nat;
let m,k1,k2;
assume that
A1: 2 to_power(n)+1 is prime and
A2: len m >= 4 and
A3: 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
A4: 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) and
A5: k2.5 = k1.5 & k2.6 = k1.6;
A6: IDEAoperationB(m,k1,n).2 is_expressible_by n & IDEAoperationB(m,k1,n).3
is_expressible_by n by A2,Th27;
A7: IDEAoperationB(m,k1,n).4 is_expressible_by n by A2,Th27;
A8: len IDEAoperationB(m,k1,n) >= 4 & IDEAoperationB(m,k1,n).1
is_expressible_by n by A2,Def12,Th27;
dom IDEA_PE(k1,n) = MESSAGES by FUNCT_2:def 1;
then m in dom IDEA_PE(k1,n) by FINSEQ_1:def 11;
then (IDEA_QE(k2,n)*IDEA_PE(k1,n)).m = IDEA_QE(k2,n).(IDEA_PE(k1,n).m) by
FUNCT_1:13
.= IDEA_QE(k2,n). IDEAoperationA(IDEAoperationB(m,k1,n),k1,n) by Def21
.= IDEAoperationB(IDEAoperationA( IDEAoperationA(IDEAoperationB(m,k1,n),
k1,n),k2,n),k2,n) by Def22
.= IDEAoperationB(IDEAoperationB(m,k1,n),k2,n) by A1,A4,A8,A6,A7,Th29
.= m by A2,A3,A5,Th31;
hence thesis;
end;
theorem Th36:
for n being non zero Nat,lk being Nat,
Key being Matrix of lk,6,NAT, k being Nat holds IDEA_P_F(Key,n,(k+1)
) = IDEA_P_F(Key,n,k)^<* IDEA_P(Line(Key,(k+1)),n) *>
proof
let n be non zero Nat;
let lk be Nat;
let Key be Matrix of lk,6,NAT;
let k be Nat;
A1: for i being Nat st 1 <= i & i <= len IDEA_P_F(Key,n,(k+1)) holds
IDEA_P_F(Key,n,(k+1)).i = (IDEA_P_F(Key,n,k)^<* IDEA_P(Line(Key,(k+1)),n) *>).i
proof
dom <* IDEA_P(Line(Key,(k+1)),n) *> = Seg 1 by FINSEQ_1:def 8;
then
A2: 1 in dom <*IDEA_P(Line(Key,(k+1)),n)*> by FINSEQ_1:1;
let i be Nat;
assume that
A3: 1 <= i and
A4: i <= len IDEA_P_F(Key,n,(k+1));
i in Seg len IDEA_P_F(Key,n,(k+1)) by A3,A4,FINSEQ_1:1;
then
A5: i in dom IDEA_P_F(Key,n,(k+1)) by FINSEQ_1:def 3;
A6: i <= k+1 by A4,Def17;
now
per cases;
suppose
i <> k+1;
then i <= k by A6,NAT_1:8;
then i in Seg k by A3,FINSEQ_1:1;
then i in Seg len IDEA_P_F(Key,n,k) by Def17;
then
A7: i in dom IDEA_P_F(Key,n,k) by FINSEQ_1:def 3;
hence
(IDEA_P_F(Key,n,k)^<* IDEA_P(Line(Key,(k+1)),n) *>).i = IDEA_P_F(
Key,n,k).i by FINSEQ_1:def 7
.= IDEA_P(Line(Key,i),n) by A7,Def17
.= IDEA_P_F(Key,n,(k+1)).i by A5,Def17;
end;
suppose
A8: i = k+1;
hence
(IDEA_P_F(Key,n,k)^<* IDEA_P(Line(Key,(k+1)),n) *>).i =(IDEA_P_F(
Key,n,k)^<* IDEA_P(Line(Key,(k+1)),n) *>). (len IDEA_P_F(Key,n,k) + 1) by Def17
.= <* IDEA_P(Line(Key,(k+1)),n) *>.1 by A2,FINSEQ_1:def 7
.= IDEA_P(Line(Key,(k+1)),n)
.= IDEA_P_F(Key,n,(k+1)).i by A5,A8,Def17;
end;
end;
hence thesis;
end;
len (IDEA_P_F(Key,n,k)^<* IDEA_P(Line(Key,(k+1)),n) *>) = len IDEA_P_F(
Key,n,k) + len <* IDEA_P(Line(Key,(k+1)),n) *> by FINSEQ_1:22
.= k + len <* IDEA_P(Line(Key,(k+1)),n) *> by Def17
.= k + 1 by FINSEQ_1:39;
then
len IDEA_P_F(Key,n,(k+1)) = len (IDEA_P_F(Key,n,k)^<* IDEA_P(Line(Key,(k
+1)),n) *>) by Def17;
hence thesis by A1,FINSEQ_1:14;
end;
theorem Th37:
for n being non zero Nat,lk being Nat,
Key being Matrix of lk,6,NAT, k being Nat holds IDEA_Q_F(Key,n,(k+1)
) = <* IDEA_Q(Line(Key,k+1),n) *>^IDEA_Q_F(Key,n,k)
proof
let n be non zero Nat;
let lk be Nat;
let Key be Matrix of lk,6,NAT;
let k be Nat;
A1: for i being Nat st 1 <= i & i <= len IDEA_Q_F(Key,n,(k+1)) holds
IDEA_Q_F(Key,n,(k+1)).i = (<* IDEA_Q(Line(Key,k+1),n) *>^IDEA_Q_F(Key,n,k)).i
proof
dom <* IDEA_Q(Line(Key,(k+1)),n) *> = Seg 1 by FINSEQ_1:def 8;
then
A2: 1 in dom <*IDEA_Q(Line(Key,(k+1)),n)*> by FINSEQ_1:1;
let i be Nat;
assume that
A3: 1 <= i and
A4: i <= len IDEA_Q_F(Key,n,(k+1));
A5: i <= k+1 by A4,Def18;
1 <= len IDEA_Q_F(Key,n,(k+1)) by A3,A4,XXREAL_0:2;
then 1 in Seg len IDEA_Q_F(Key,n,(k+1)) by FINSEQ_1:1;
then
A6: 1 in dom IDEA_Q_F(Key,n,(k+1)) by FINSEQ_1:def 3;
i in Seg len IDEA_Q_F(Key,n,(k+1)) by A3,A4,FINSEQ_1:1;
then
A7: i in dom IDEA_Q_F(Key,n,(k+1)) by FINSEQ_1:def 3;
now
per cases;
suppose
A8: i <> 1;
consider ii be Integer such that
A9: ii = i - 1;
A10: ii + 1 = i by A9;
A11: (k+1) - i >= i - i by A5,XREAL_1:9;
1 - 1 <= i - 1 by A3,XREAL_1:9;
then reconsider ii as Element of NAT by A9,INT_1:3;
A12: i-1 <= k+1-1 by A5,XREAL_1:9;
then ii - ii <= k - ii by A9,XREAL_1:9;
then
A13: k -' ii = (k+1) + -i by A9,XREAL_0:def 2
.=(k+1) -' i by A11,XREAL_0:def 2;
1 < i by A3,A8,XXREAL_0:1;
then 1 + 1 <= i by NAT_1:13;
then 1 + 1 - 1 <= i - 1 by XREAL_1:9;
then ii in Seg k by A9,A12,FINSEQ_1:1;
then ii in Seg len IDEA_Q_F(Key,n,k) by Def18;
then
A14: ii in dom IDEA_Q_F(Key,n,k) by FINSEQ_1:def 3;
thus (<* IDEA_Q(Line(Key,k+1),n) *>^IDEA_Q_F(Key,n,k)).i =(<* IDEA_Q(
Line(Key,k+1),n) *>^IDEA_Q_F(Key,n,k)). (len <*IDEA_Q(Line(Key,(k+1)),n)*>+ii)
by A10,FINSEQ_1:40
.=IDEA_Q_F(Key,n,k).ii by A14,FINSEQ_1:def 7
.=IDEA_Q(Line(Key,(k+1)-'i+1),n) by A14,A13,Def18
.=IDEA_Q_F(Key,n,k+1).i by A7,Def18;
end;
suppose
A15: i = 1;
hence (<* IDEA_Q(Line(Key,k+1),n) *>^IDEA_Q_F(Key,n,k)).i = <* IDEA_Q(
Line(Key,k+1),n) *>.1 by A2,FINSEQ_1:def 7
.= IDEA_Q(Line(Key,k+1),n)
.= IDEA_Q(Line(Key,(k+1)-'1 + 1),n) by A3,A5,XREAL_1:235,XXREAL_0:2
.= IDEA_Q_F(Key,n,k+1).i by A6,A15,Def18;
end;
end;
hence thesis;
end;
len (<* IDEA_Q(Line(Key,k+1),n) *>^IDEA_Q_F(Key,n,k)) = len <* IDEA_Q(
Line(Key,k+1),n) *> + len IDEA_Q_F(Key,n,k) by FINSEQ_1:22
.= len <* IDEA_Q(Line(Key,k+1),n) *> + k by Def18
.= k + 1 by FINSEQ_1:39;
then
len IDEA_Q_F(Key,n,(k+1)) = len (<* IDEA_Q(Line(Key,k+1),n) *>^IDEA_Q_F(
Key,n,k)) by Def18;
hence thesis by A1,FINSEQ_1:14;
end;
theorem Th38:
for n being non zero Nat,lk being Nat,
Key being Matrix of lk,6,NAT, k being Nat holds IDEA_P_F(Key,n,k) is
FuncSeq-like FinSequence
proof
let n be non zero Nat;
let lk be Nat;
let Key be Matrix of lk,6,NAT;
let k be Nat;
set p = Seg(k+1) --> MESSAGES;
A1: dom p = Seg(k+1) by FUNCOP_1:13;
reconsider p as FinSequence;
A2: for i being Nat st i in dom IDEA_P_F(Key,n,k)
holds IDEA_P_F(Key,n,k).i in Funcs(p.i, p.(i+1))
proof
let i be Nat;
assume
A3: i in dom IDEA_P_F(Key,n,k);
then
A4: i in Seg len IDEA_P_F(Key,n,k) by FINSEQ_1:def 3;
then i in Seg k by Def17;
then
A5: i <= k by FINSEQ_1:1;
then
A6: i <= k+1 by NAT_1:12;
1 <= (i+1) & (i+1) <= k+1 by A5,NAT_1:12,XREAL_1:6;
then (i+1) in Seg (k+1) by FINSEQ_1:1;
then
A7: p.(i+1) = MESSAGES by FUNCOP_1:7;
1 <= i by A4,FINSEQ_1:1;
then i in Seg (k+1) by A6,FINSEQ_1:1;
then
A8: p.i = MESSAGES by FUNCOP_1:7;
IDEA_P_F(Key,n,k).i = IDEA_P(Line(Key,i),n) by A3,Def17;
hence thesis by A8,A7,FUNCT_2:9;
end;
len p = k+1 by A1,FINSEQ_1:def 3;
then len p = len IDEA_P_F(Key,n,k)+1 by Def17;
hence thesis by A2,FUNCT_7:def 8;
end;
theorem Th39:
for n being non zero Nat,lk being Nat,
Key being Matrix of lk,6,NAT, k being Nat holds IDEA_Q_F(Key,n,k) is
FuncSeq-like FinSequence
proof
let n be non zero Nat;
let lk be Nat;
let Key be Matrix of lk,6,NAT;
let k be Nat;
set p = Seg(k+1) --> MESSAGES;
A1: dom p = Seg(k+1) by FUNCOP_1:13;
reconsider p as FinSequence;
A2: for i being Nat st i in dom IDEA_Q_F(Key,n,k)
holds IDEA_Q_F(Key,n,k).i in Funcs(p.i, p.(i+1))
proof
let i be Nat;
assume
A3: i in dom IDEA_Q_F(Key,n,k);
then
A4: i in Seg len IDEA_Q_F(Key,n,k) by FINSEQ_1:def 3;
then i in Seg k by Def18;
then
A5: i <= k by FINSEQ_1:1;
then
A6: i <= k+1 by NAT_1:12;
1 <= (i+1) & (i+1) <= k+1 by A5,NAT_1:12,XREAL_1:6;
then (i+1) in Seg (k+1) by FINSEQ_1:1;
then
A7: p.(i+1) = MESSAGES by FUNCOP_1:7;
1 <= i by A4,FINSEQ_1:1;
then i in Seg (k+1) by A6,FINSEQ_1:1;
then
A8: p.i = MESSAGES by FUNCOP_1:7;
IDEA_Q_F(Key,n,k).i = IDEA_Q(Line(Key,k-'i+1),n) by A3,Def18;
hence thesis by A8,A7,FUNCT_2:9;
end;
len p = k+1 by A1,FINSEQ_1:def 3;
then len p = len IDEA_Q_F(Key,n,k)+1 by Def18;
hence thesis by A2,FUNCT_7:def 8;
end;
theorem Th40:
for n being non zero Nat,lk being Nat,
Key being Matrix of lk,6,NAT, k being Nat holds k <> 0 implies
IDEA_P_F(Key,n,k) is FuncSequence of MESSAGES,MESSAGES
proof
let n be non zero Nat;
let lk be Nat, Key be Matrix of lk,6,NAT, k be Nat;
A1: k = len IDEA_P_F(Key,n,k) by Def17;
assume
A2: k<>0;
then 0+1 < k+1 by XREAL_1:6;
then
A3: 1 <= k by NAT_1:13;
0+1 < k+1 by A2,XREAL_1:6;
then 1 <= k by NAT_1:13;
then 1 in Seg len IDEA_P_F(Key,n,k) by A1,FINSEQ_1:1;
then
A4: 1 in dom IDEA_P_F(Key,n,k) by FINSEQ_1:def 3;
len (IDEA_P_F(Key,n,k)) = k by Def17;
then not IDEA_P_F(Key,n,k)=<*>MESSAGES by A2;
then
A5: firstdom IDEA_P_F(Key,n,k) = proj1 (IDEA_P_F(Key,n,k).1) by FUNCT_7:def 6
.= proj1 (IDEA_P(Line(Key,1),n)) by A4,Def17
.= dom IDEA_P(Line(Key,1),n)
.= MESSAGES by FUNCT_2:def 1;
k = len IDEA_P_F(Key,n,k) by Def17;
then k in Seg len IDEA_P_F(Key,n,k) by A3,FINSEQ_1:1;
then
A6: k in dom IDEA_P_F(Key,n,k) by FINSEQ_1:def 3;
len (IDEA_P_F(Key,n,k)) <> 0 by A2,Def17;
then not IDEA_P_F(Key,n,k)=<*>MESSAGES;
then
lastrng IDEA_P_F(Key,n,k) = proj2 (IDEA_P_F(Key,n,k). len (IDEA_P_F(Key
,n,k))) by FUNCT_7:def 7
.= proj2 (IDEA_P_F(Key,n,k).k) by Def17
.= proj2 (IDEA_P(Line(Key,k),n)) by A6,Def17
.= rng IDEA_P(Line(Key,k),n);
then
A7: lastrng IDEA_P_F(Key,n,k) c= MESSAGES by RELAT_1:def 19;
IDEA_P_F(Key,n,k) is FuncSequence by Th38;
hence thesis by A7,A5,FUNCT_7:def 9;
end;
theorem Th41:
for n being non zero Nat,lk being Nat,
Key being Matrix of lk,6,NAT, k being Nat holds k <> 0 implies
IDEA_Q_F(Key,n,k) is FuncSequence of MESSAGES,MESSAGES
proof
let n be non zero Nat, lk be Nat, Key be Matrix of lk
,6,NAT, r be Nat;
assume
A1: r<>0;
then 0+1 < r+1 by XREAL_1:6;
then
A2: 1 <= r by NAT_1:13;
0+1 < r+1 by A1,XREAL_1:6;
then
A3: 1 <= r by NAT_1:13;
r = len IDEA_Q_F(Key,n,r) by Def18;
then 1 in Seg len IDEA_Q_F(Key,n,r) by A3,FINSEQ_1:1;
then
A4: 1 in dom IDEA_Q_F(Key,n,r) by FINSEQ_1:def 3;
len (IDEA_Q_F(Key,n,r)) <> 0 by A1,Def18;
then not IDEA_Q_F(Key,n,r)=<*>MESSAGES;
then
A5: firstdom IDEA_Q_F(Key,n,r) = proj1 (IDEA_Q_F(Key,n,r).1) by FUNCT_7:def 6
.= proj1 (IDEA_Q(Line(Key,r-'1+1),n)) by A4,Def18
.= dom IDEA_Q(Line(Key,r-'1+1),n)
.= MESSAGES by FUNCT_2:def 1;
r = len IDEA_Q_F(Key,n,r) by Def18;
then r in Seg len IDEA_Q_F(Key,n,r) by A2,FINSEQ_1:1;
then
A6: r in dom IDEA_Q_F(Key,n,r) by FINSEQ_1:def 3;
len (IDEA_Q_F(Key,n,r)) <> 0 by A1,Def18;
then not IDEA_Q_F(Key,n,r)=<*>MESSAGES;
then
lastrng IDEA_Q_F(Key,n,r) = proj2 (IDEA_Q_F(Key,n,r). len (IDEA_Q_F(Key
,n,r))) by FUNCT_7:def 7
.= proj2 (IDEA_Q_F(Key,n,r).r) by Def18
.= proj2 (IDEA_Q(Line(Key,r-'r+1),n)) by A6,Def18
.= rng IDEA_Q(Line(Key,r-'r+1),n);
then
A7: lastrng IDEA_Q_F(Key,n,r) c= MESSAGES by RELAT_1:def 19;
IDEA_Q_F(Key,n,r) is FuncSequence by Th39;
hence thesis by A7,A5,FUNCT_7:def 9;
end;
theorem Th42:
for n being non zero Nat,M being FinSequence of NAT,
m,k st M = IDEA_P(k,n).m & len m >= 4 holds 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
proof
let n be non zero Nat, M be FinSequence of NAT,m,k;
assume that
A1: M = IDEA_P(k,n).m and
A2: len m >= 4;
A3: len m = len IDEAoperationB(m,k,n) by Def12
.= len IDEAoperationC(IDEAoperationB(m,k,n)) by Def13;
M = IDEAoperationA(IDEAoperationC(IDEAoperationB(m,k,n)),k,n) by A1,Def15;
hence thesis by A2,A3,Def11,Th26;
end;
theorem Th43:
for n being non zero Nat,lk being Nat,
Key being Matrix of lk,6,NAT, r being Nat holds rng compose(IDEA_P_F
(Key,n,r),MESSAGES) c=MESSAGES & dom compose(IDEA_P_F(Key,n,r),MESSAGES) =
MESSAGES
proof
let n be non zero Nat, lk be Nat, Key be Matrix of lk
,6,NAT, r be Nat;
A1: rng compose(IDEA_P_F(Key,n,r),MESSAGES) c= MESSAGES
proof
per cases;
suppose
A2: r<>0;
then 0+1 < r+1 by XREAL_1:6;
then
A3: 1 <= r by NAT_1:13;
r = len IDEA_P_F(Key,n,r) by Def17;
then r in Seg len IDEA_P_F(Key,n,r) by A3,FINSEQ_1:1;
then
A4: r in dom IDEA_P_F(Key,n,r) by FINSEQ_1:def 3;
len (IDEA_P_F(Key,n,r)) <> 0 by A2,Def17;
then
A5: not IDEA_P_F(Key,n,r)=<*>MESSAGES;
then
lastrng IDEA_P_F(Key,n,r) = proj2 (IDEA_P_F(Key,n,r). len (IDEA_P_F
(Key,n,r))) by FUNCT_7:def 7
.= proj2 (IDEA_P_F(Key,n,r).r) by Def17
.= proj2 (IDEA_P(Line(Key,r),n)) by A4,Def17
.= rng IDEA_P(Line(Key,r),n);
then
A6: lastrng IDEA_P_F(Key,n,r) c= MESSAGES by RELAT_1:def 19;
rng compose(IDEA_P_F(Key,n,r),MESSAGES) c= lastrng IDEA_P_F(Key,n,r
) by A5,FUNCT_7:59;
hence thesis by A6,XBOOLE_1:1;
end;
suppose
r=0;
then len IDEA_P_F(Key,n,r) = 0 by Def17;
then IDEA_P_F(Key,n,r) = {};
then compose(IDEA_P_F(Key,n,r),MESSAGES) = id MESSAGES by FUNCT_7:39;
hence thesis;
end;
end;
A7: IDEA_P_F(Key,n,r) is FuncSequence by Th38;
dom compose(IDEA_P_F(Key,n,r),MESSAGES) = MESSAGES
proof
per cases;
suppose
r=0;
then len IDEA_P_F(Key,n,r) = 0 by Def17;
then IDEA_P_F(Key,n,r) = {};
then compose(IDEA_P_F(Key,n,r),MESSAGES) = id MESSAGES by FUNCT_7:39;
hence thesis;
end;
suppose
A8: r<>0;
then 0+1 < r+1 by XREAL_1:6;
then
A9: 1 <= r by NAT_1:13;
r = len IDEA_P_F(Key,n,r) by Def17;
then 1 in Seg len IDEA_P_F(Key,n,r) by A9,FINSEQ_1:1;
then
A10: 1 in dom IDEA_P_F(Key,n,r) by FINSEQ_1:def 3;
len (IDEA_P_F(Key,n,r)) <> 0 by A8,Def17;
then not IDEA_P_F(Key,n,r)=<*>MESSAGES;
then firstdom IDEA_P_F(Key,n,r) = proj1 (IDEA_P_F(Key,n,r).1) by
FUNCT_7:def 6
.= proj1 (IDEA_P(Line(Key,1),n)) by A10,Def17
.= dom IDEA_P(Line(Key,1),n)
.= MESSAGES by FUNCT_2:def 1;
hence thesis by A7,FUNCT_7:62;
end;
end;
hence thesis by A1;
end;
theorem
for n being non zero Nat,lk being Nat, Key
being Matrix of lk,6,NAT, r being Nat holds rng compose(IDEA_Q_F(Key
,n,r),MESSAGES) c=MESSAGES & dom compose(IDEA_Q_F(Key,n,r),MESSAGES) =MESSAGES
proof
let n be non zero Nat, lk be Nat, Key be Matrix of lk
,6,NAT, r be Nat;
A1: rng compose(IDEA_Q_F(Key,n,r),MESSAGES) c= MESSAGES
proof
per cases;
suppose
A2: r<>0;
then 0+1 < r+1 by XREAL_1:6;
then
A3: 1 <= r by NAT_1:13;
r = len IDEA_Q_F(Key,n,r) by Def18;
then r in Seg len IDEA_Q_F(Key,n,r) by A3,FINSEQ_1:1;
then
A4: r in dom IDEA_Q_F(Key,n,r) by FINSEQ_1:def 3;
len (IDEA_Q_F(Key,n,r)) <> 0 by A2,Def18;
then
A5: not IDEA_Q_F(Key,n,r)=<*>MESSAGES;
then
lastrng IDEA_Q_F(Key,n,r) = proj2 (IDEA_Q_F(Key,n,r). len (IDEA_Q_F
(Key,n,r))) by FUNCT_7:def 7
.= proj2 (IDEA_Q_F(Key,n,r).r) by Def18
.= proj2 (IDEA_Q(Line(Key,r-'r+1),n)) by A4,Def18
.= rng IDEA_Q(Line(Key,r-'r+1),n);
then
A6: lastrng IDEA_Q_F(Key,n,r) c= MESSAGES by RELAT_1:def 19;
rng compose(IDEA_Q_F(Key,n,r),MESSAGES) c= lastrng IDEA_Q_F(Key,n,r
) by A5,FUNCT_7:59;
hence thesis by A6,XBOOLE_1:1;
end;
suppose
r=0;
then len IDEA_Q_F(Key,n,r) = 0 by Def18;
then IDEA_Q_F(Key,n,r) = {};
then compose(IDEA_Q_F(Key,n,r),MESSAGES) = id MESSAGES by FUNCT_7:39;
hence thesis;
end;
end;
A7: IDEA_Q_F(Key,n,r) is FuncSequence by Th39;
dom compose(IDEA_Q_F(Key,n,r),MESSAGES) = MESSAGES
proof
per cases;
suppose
r=0;
then len IDEA_Q_F(Key,n,r) = 0 by Def18;
then IDEA_Q_F(Key,n,r) = {};
then compose(IDEA_Q_F(Key,n,r),MESSAGES) = id MESSAGES by FUNCT_7:39;
hence thesis;
end;
suppose
A8: r<>0;
then 0+1 < r+1 by XREAL_1:6;
then
A9: 1 <= r by NAT_1:13;
r = len IDEA_Q_F(Key,n,r) by Def18;
then 1 in Seg len IDEA_Q_F(Key,n,r) by A9,FINSEQ_1:1;
then
A10: 1 in dom IDEA_Q_F(Key,n,r) by FINSEQ_1:def 3;
len (IDEA_Q_F(Key,n,r)) <> 0 by A8,Def18;
then not IDEA_Q_F(Key,n,r)=<*>MESSAGES;
then firstdom IDEA_Q_F(Key,n,r) = proj1 (IDEA_Q_F(Key,n,r).1) by
FUNCT_7:def 6
.= proj1 (IDEA_Q(Line(Key,r-'1+1),n)) by A10,Def18
.= dom IDEA_Q(Line(Key,r-'1+1),n)
.= MESSAGES by FUNCT_2:def 1;
hence thesis by A7,FUNCT_7:62;
end;
end;
hence thesis by A1;
end;
theorem Th45:
for n being non zero Nat,lk being Nat,
Key being Matrix of lk,6,NAT, r being Nat,M being FinSequence of NAT
,m st M = compose(IDEA_P_F(Key,n,r),MESSAGES).m & 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 holds 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
proof
let n be non zero Nat, lk be Nat, Key be Matrix of lk
,6,NAT, r be Nat, M be FinSequence of NAT,m;
assume that
A1: M = compose(IDEA_P_F(Key,n,r),MESSAGES).m and
A2: len m >= 4 and
A3: m.1 is_expressible_by n & m.2 is_expressible_by n & m.3
is_expressible_by n & m.4 is_expressible_by n;
A4: m in MESSAGES by FINSEQ_1:def 11;
per cases;
suppose
r = 0;
then len IDEA_P_F(Key,n,r) = 0 by Def17;
then IDEA_P_F(Key,n,r) = {};
then M = (id MESSAGES).m by A1,FUNCT_7:39
.= m by A4,FUNCT_1:18;
hence thesis by A2,A3;
end;
suppose
A5: r <> 0;
consider r1 being Integer such that
A6: r1=r-1;
defpred P[Nat] means for M being FinSequence of NAT st M =
compose(IDEA_P_F(Key,n,$1),MESSAGES).m holds len M >= 4;
A7: m in MESSAGES by FINSEQ_1:def 11;
A8: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
A9: dom compose(IDEA_P_F(Key,n,k),MESSAGES) = MESSAGES by Th43;
A10: rng compose(IDEA_P_F(Key,n,k),MESSAGES) c= MESSAGES by Th43;
then
rng compose(IDEA_P_F(Key,n,k),MESSAGES) c= dom IDEA_P(Line(Key,(k+1
)),n) by FUNCT_2:def 1;
then
A11: dom (IDEA_P(Line(Key,(k+1)),n)* compose(IDEA_P_F(Key,n,k),MESSAGES)
)= MESSAGES by A9,RELAT_1:27;
compose(IDEA_P_F(Key,n,k),MESSAGES).m in rng(compose(IDEA_P_F(Key,n
,k),MESSAGES)) by A7,A9,FUNCT_1:def 3;
then reconsider
M1 = compose(IDEA_P_F(Key,n,k),MESSAGES).m as FinSequence of
NAT by A10,FINSEQ_1:def 11;
assume P[k];
then
A12: len M1 >= 4;
let M be FinSequence of NAT;
assume M = compose(IDEA_P_F(Key,n,k+1),MESSAGES).m;
then M = compose(IDEA_P_F(Key,n,k)^<* IDEA_P(Line(Key,(k+1)),n) *>,
MESSAGES).m by Th36;
then
M = (IDEA_P(Line(Key,(k+1)),n)* compose(IDEA_P_F(Key,n,k),MESSAGES)
).m by FUNCT_7:41;
then
M = IDEA_P(Line(Key,(k+1)),n). (compose(IDEA_P_F(Key,n,k),MESSAGES)
.m) by A7,A11,FUNCT_1:12;
hence thesis by A12,Th42;
end;
1 <= r by A5,NAT_1:14;
then 1 - 1 <= r - 1 by XREAL_1:9;
then reconsider r1 as Element of NAT by A6,INT_1:3;
dom compose(IDEA_P_F(Key,n,r1),MESSAGES) = MESSAGES by Th43;
then
A13: compose(IDEA_P_F(Key,n,r1),MESSAGES).m in rng(compose(IDEA_P_F(Key,n,
r1),MESSAGES)) by A4,FUNCT_1:def 3;
rng compose(IDEA_P_F(Key,n,r1),MESSAGES) c= MESSAGES by Th43;
then reconsider
M1 = compose(IDEA_P_F(Key,n,r1),MESSAGES).m as FinSequence of
NAT by A13,FINSEQ_1:def 11;
A14: P[0]
proof
let M be FinSequence of NAT;
len IDEA_P_F(Key,n,0) = 0 by Def17;
then
A15: IDEA_P_F(Key,n,0) = {};
assume M = compose(IDEA_P_F(Key,n,0),MESSAGES).m;
then M = (id MESSAGES).m by A15,FUNCT_7:39
.= m by A7,FUNCT_1:18;
hence thesis by A2;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A14,A8);
then
A16: len M1 >= 4;
IDEA_P_F(Key,n,(r1+1)) = IDEA_P_F(Key,n,r1)^<* IDEA_P(Line(Key,(r1+1)
),n) *> by Th36;
then
A17: compose(IDEA_P_F(Key,n,r),MESSAGES) = IDEA_P(Line(Key,r),n)*compose(
IDEA_P_F(Key,n,r1),MESSAGES) by A6,FUNCT_7:41;
then
m in dom(IDEA_P(Line(Key,r),n)* compose(IDEA_P_F(Key,n,r1),MESSAGES))
by A4,Th43;
then
M = IDEA_P(Line(Key,r),n).(compose(IDEA_P_F(Key,n,r1),MESSAGES).m) by A1
,A17,FUNCT_1:12;
hence thesis by A16,Th42;
end;
end;
begin :: Modeling of IDEA Cryptogram
:: IDEA encryption algorithm is as follows:
:: IDEA_PS -> IDEA_P -> IDEA_P -> ... -> IDEA_P -> IDEA_PE
:: IDEA decryption algorithm is as follows:
:: IDEA_QE -> IDEA_Q -> IDEA_Q -> ... -> IDEA_Q -> IDEA_QS
:: Theorem 49 ensures that the ciphertext that is encrypted by IDEA
:: encryption algorithm can be decrypted by IDEA decryption algorithm.
theorem Th46:
for n being non zero Nat,lk being Nat,
Key1,Key2 being Matrix of lk,6,NAT, r being Nat,m 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 holds i <= r 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)) holds compose(IDEA_P_F(
Key1,n,r)^IDEA_Q_F(Key2,n,r),MESSAGES).m = m
proof
let n be non zero Nat, lk be Nat;
let Key1,Key2 be Matrix of lk,6,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
holds i <= r 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)) holds compose(
IDEA_P_F(Key1,n,r)^IDEA_Q_F(Key2,n,r), MESSAGES).m = m
proof
defpred P[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
holds i <= $1 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)) 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 P[k] holds P[k + 1]
proof
let k be Nat;
assume
A3: P[k];
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 holds i <= k+1 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);
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 holds 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)
proof
let i be Nat;
assume i <= k;
then i <= k+1 by A35,XXREAL_0:2;
hence thesis by A11;
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 thesis;
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: P[0] by FUNCT_1:18;
thus for k being Nat holds P[k] from NAT_1:sch 2(A37, A2);
end;
hence thesis;
end;
theorem
for n being non zero Nat,lk being Nat, Key1,
Key2 being Matrix of lk,6,NAT, r being Nat,ks1,ks2,ke1,ke2 being
FinSequence of NAT,m 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 holds i <= r 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))& 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
proof
let n be non zero Nat, lk be Nat, Key1,Key2 be Matrix
of lk,6,NAT, r be Nat, ks1,ks2,ke1,ke2 be FinSequence of NAT,m;
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 holds i <= r 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) 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;
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;
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;
end;
suppose
A17: r <> 0;
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;
end;
end;