:: 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-2012 Association of Mizar Users


begin

Lm1:  for i, j being Element of NAT st i <> 0 &amp; i < j &amp; j is prime holds
i,j are_relative_prime
proofend;

Lm2:  for j, i, k being Element of NAT st j is prime &amp; i < j &amp; k < j &amp; i <> 0 holds
ex a being Element of NAT st (a * i) mod j = k
proofend;

theorem Th1: :: IDEA_1:1
for i, j, k being Element of NAT st j is prime &amp; i < j &amp; k < j &amp; i <> 0 holds
ex a being Element of NAT st
( (a * i) mod j = k &amp; a < j )
proofend;

theorem Th2: :: IDEA_1:2
for n, k1, k2 being Element of NAT st n <> 0 &amp; k1 mod n = k2 mod n &amp; k1 <= k2 holds
ex t being Element of NAT st k2 - k1 = n * t
proofend;

theorem Th3: :: IDEA_1:3
for a, b being Element of NAT holds a - b <= a
proofend;

theorem Th4: :: IDEA_1:4
for b1, b2, c being Element of NAT st b2 <= c holds
b2 - b1 <= c
proofend;

theorem Th5: :: IDEA_1:5
for a, b, c being Element of NAT st 0 < a &amp; 0 < b &amp; a < c &amp; b < c &amp; c is prime holds
(a * b) mod c <> 0
proofend;

begin

:: 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 be Element of NAT ;
func ZERO n ->  Tuple of n, BOOLEAN  equals :: IDEA_1:def 1
n |-> FALSE;
correctness
coherence
n |-> FALSE is Tuple of n, BOOLEAN ;
;
end;

:: deftheorem  defines ZERO IDEA_1:def_1_:_
 for n being Element of NAT holds ZERO n = n |-> FALSE;

definition
let n be Element of NAT ;
let x, y be Tuple of n, BOOLEAN ;
funcx 'xor' y ->  Tuple of n, BOOLEAN  means :Def2: :: IDEA_1:def 2
 for i being Element of NAT st i in Seg n holds
it /. i = (x /. i) 'xor' (y /. i);
existence
 ex b1 being Tuple of n, BOOLEAN st
for i being Element of NAT st i in Seg n holds
b1 /. i = (x /. i) 'xor' (y /. i)
proofend;
uniqueness
 for b1, b2 being Tuple of n, BOOLEAN st ( for i being Element of NAT st i in Seg n holds
b1 /. i = (x /. i) 'xor' (y /. i) ) &amp; ( for i being Element of NAT st i in Seg n holds
b2 /. i = (x /. i) 'xor' (y /. i) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines 'xor' IDEA_1:def_2_:_
 for n being Element of NAT
for x, y, b4 being Tuple of n, BOOLEAN holds
( b4 = x 'xor' y iff for i being Element of NAT st i in Seg n holds
b4 /. i = (x /. i) 'xor' (y /. i) );

theorem Th6: :: IDEA_1:6
for n being Element of NAT
for x being Tuple of n, BOOLEAN holds x 'xor' x = ZERO n
proofend;

theorem Th7: :: IDEA_1:7
for n being Element of NAT
for x, y being Tuple of n, BOOLEAN holds x 'xor' y = y 'xor' x
proofend;

definition
let n be Element of NAT ;
let x, y be Tuple of n, BOOLEAN ;
:: original:'xor'
redefine funcx 'xor' y ->  Tuple of n, BOOLEAN ;
commutativity
 for x, y being Tuple of n, BOOLEAN holds x 'xor' y = y 'xor' x by Th7;
end;

theorem Th8: :: IDEA_1:8
for n being Element of NAT
for x being Tuple of n, BOOLEAN holds (ZERO n) 'xor' x = x
proofend;

theorem Th9: :: IDEA_1:9
for n being Element of NAT
for x, y, z being Tuple of n, BOOLEAN holds (x 'xor' y) 'xor' z = x 'xor' (y 'xor' z)
proofend;

definition
let n, i be Element of NAT ;
predi is_expressible_by n means :Def3: :: IDEA_1:def 3
i < 2 to_power n;
end;

:: deftheorem Def3 defines is_expressible_by IDEA_1:def_3_:_
 for n, i being Element of NAT holds
( i is_expressible_by n iff i < 2 to_power n );

theorem :: IDEA_1:10
for n being Element of NAT holds n -BinarySequence 0 = ZERO n
proofend;

definition
let n be Element of NAT ;
let i, j be Nat;
func ADD_MOD (i,j,n) ->  Element of NAT  equals :: IDEA_1:def 4
(i + j) mod (2 to_power n);
coherence
 (i + j) mod (2 to_power n) is Element of NAT ;
end;

:: deftheorem  defines ADD_MOD IDEA_1:def_4_:_
 for n being Element of NAT
for i, j being Nat holds ADD_MOD (i,j,n) = (i + j) mod (2 to_power n);

definition
let n, i be Element of NAT ;
assume A1: i is_expressible_by n ;
func NEG_N (i,n) ->  Element of NAT  equals :Def5: :: IDEA_1:def 5
(2 to_power n) - i;
coherence
 (2 to_power n) - i is Element of NAT
proofend;
end;

:: deftheorem Def5 defines NEG_N IDEA_1:def_5_:_
 for n, i being Element of NAT st i is_expressible_by n holds
NEG_N (i,n) = (2 to_power n) - i;

definition
let n, i be Element of NAT ;
func NEG_MOD (i,n) ->  Element of NAT  equals :: IDEA_1:def 6
(NEG_N (i,n)) mod (2 to_power n);
coherence
 (NEG_N (i,n)) mod (2 to_power n) is Element of NAT ;
end;

:: deftheorem  defines NEG_MOD IDEA_1:def_6_:_
 for n, i being Element of NAT holds NEG_MOD (i,n) = (NEG_N (i,n)) mod (2 to_power n);

theorem Th11: :: IDEA_1:11
for i, n being Element of NAT st i is_expressible_by n holds
ADD_MOD (i,(NEG_MOD (i,n)),n) = 0
proofend;

theorem :: IDEA_1:12
for i, j, n being Element of NAT holds ADD_MOD (i,j,n) = ADD_MOD (j,i,n) ;

theorem Th13: :: IDEA_1:13
for i, n being Element of NAT st i is_expressible_by n holds
ADD_MOD (0,i,n) = i
proofend;

theorem Th14: :: IDEA_1:14
for i, j, n, k being Element of NAT holds ADD_MOD ((ADD_MOD (i,j,n)),k,n) = ADD_MOD (i,(ADD_MOD (j,k,n)),n)
proofend;

theorem Th15: :: IDEA_1:15
for i, j, n being Element of NAT holds ADD_MOD (i,j,n) is_expressible_by n
proofend;

theorem :: IDEA_1:16
for i, n being Element of NAT holds NEG_MOD (i,n) is_expressible_by n
proofend;

definition
let n, i be Nat;
func ChangeVal_1 (i,n) ->  Element of NAT  equals :Def7: :: IDEA_1:def 7
2 to_power n if i = 0
otherwise i;
coherence
 ( ( i = 0 implies 2 to_power n is Element of NAT ) &amp; ( not i = 0 implies i is Element of NAT ) ) by ORDINAL1:def_12;
correctness
consistency
for b1 being Element of NAT holds verum;
;
end;

:: deftheorem Def7 defines ChangeVal_1 IDEA_1:def_7_:_
 for n, i being Nat holds
( ( i = 0 implies ChangeVal_1 (i,n) = 2 to_power n ) &amp; ( not i = 0 implies ChangeVal_1 (i,n) = i ) );

theorem Th17: :: IDEA_1:17
for i, n being Element of NAT st i is_expressible_by n holds
( ChangeVal_1 (i,n) <= 2 to_power n &amp; ChangeVal_1 (i,n) > 0 )
proofend;

theorem Th18: :: IDEA_1:18
for n, a1, a2 being Element of NAT st a1 is_expressible_by n &amp; a2 is_expressible_by n &amp; ChangeVal_1 (a1,n) = ChangeVal_1 (a2,n) holds
a1 = a2
proofend;

definition
let n, i be Element of NAT ;
func ChangeVal_2 (i,n) ->  Element of NAT  equals :Def8: :: IDEA_1:def 8
 0  if i = 2 to_power n
otherwise i;
correctness
coherence
( ( i = 2 to_power n implies 0 is Element of NAT ) &amp; ( not i = 2 to_power n implies i is Element of NAT ) );
consistency
for b1 being Element of NAT holds verum;
;
end;

:: deftheorem Def8 defines ChangeVal_2 IDEA_1:def_8_:_
 for n, i being Element of NAT holds
( ( i = 2 to_power n implies ChangeVal_2 (i,n) = 0 ) &amp; ( not i = 2 to_power n implies ChangeVal_2 (i,n) = i ) );

theorem :: IDEA_1:19
for i, n being Element of NAT st i is_expressible_by n holds
ChangeVal_2 (i,n) is_expressible_by n
proofend;

theorem Th20: :: IDEA_1:20
for n, a1, a2 being Element of NAT st a1 <> 0 &amp; a2 <> 0 &amp; ChangeVal_2 (a1,n) = ChangeVal_2 (a2,n) holds
a1 = a2
proofend;

definition
let n be Element of NAT ;
let i, j be Nat;
func MUL_MOD (i,j,n) ->  Element of NAT  equals :: IDEA_1:def 9
 ChangeVal_2 ((((ChangeVal_1 (i,n)) * (ChangeVal_1 (j,n))) mod ((2 to_power n) + 1)),n);
coherence
 ChangeVal_2 ((((ChangeVal_1 (i,n)) * (ChangeVal_1 (j,n))) mod ((2 to_power n) + 1)),n) is Element of NAT ;
end;

:: deftheorem  defines MUL_MOD IDEA_1:def_9_:_
 for n being Element of NAT
for i, j being Nat holds MUL_MOD (i,j,n) = ChangeVal_2 ((((ChangeVal_1 (i,n)) * (ChangeVal_1 (j,n))) mod ((2 to_power n) + 1)),n);

definition
let n be non empty Element of NAT ;
let i be Element of NAT ;
assume that
A1: i is_expressible_by n and
A2: (2 to_power n) + 1 is prime ;
func INV_MOD (i,n) ->  Element of NAT  means :Def10: :: IDEA_1:def 10
( MUL_MOD (i,it,n) = 1 &amp; it is_expressible_by n );
existence
 ex b1 being Element of NAT st
( MUL_MOD (i,b1,n) = 1 &amp; b1 is_expressible_by n )
proofend;
uniqueness
 for b1, b2 being Element of NAT st MUL_MOD (i,b1,n) = 1 &amp; b1 is_expressible_by n &amp; MUL_MOD (i,b2,n) = 1 &amp; b2 is_expressible_by n holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines INV_MOD IDEA_1:def_10_:_
 for n being non empty Element of NAT
for i being Element of NAT st i is_expressible_by n &amp; (2 to_power n) + 1 is prime holds
for b3 being Element of NAT holds
( b3 = INV_MOD (i,n) iff ( MUL_MOD (i,b3,n) = 1 &amp; b3 is_expressible_by n ) );

theorem :: IDEA_1:21
for i, j, n being Element of NAT holds MUL_MOD (i,j,n) = MUL_MOD (j,i,n) ;

theorem Th22: :: IDEA_1:22
for i, n being Element of NAT st i is_expressible_by n holds
MUL_MOD (1,i,n) = i
proofend;

theorem Th23: :: IDEA_1:23
for n, i, j, k being Element of NAT st (2 to_power n) + 1 is prime &amp; i is_expressible_by n &amp; j is_expressible_by n &amp; k is_expressible_by n holds
MUL_MOD ((MUL_MOD (i,j,n)),k,n) = MUL_MOD (i,(MUL_MOD (j,k,n)),n)
proofend;

theorem Th24: :: IDEA_1:24
for i, j, n being Element of NAT holds MUL_MOD (i,j,n) is_expressible_by n
proofend;

theorem :: IDEA_1:25
for i, n being Element of NAT st ChangeVal_2 (i,n) = 1 holds
i = 1
proofend;

begin

:: 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 be Element of NAT ;
let m, k be FinSequence of NAT ;
func IDEAoperationA (m,k,n) ->  FinSequence of NAT  means :Def11: :: IDEA_1:def 11
( len it = len m &amp; ( for i being Element of NAT st i in dom m holds
( ( i = 1 implies it . i = MUL_MOD ((m . 1),(k . 1),n) ) &amp; ( i = 2 implies it . i = ADD_MOD ((m . 2),(k . 2),n) ) &amp; ( i = 3 implies it . i = ADD_MOD ((m . 3),(k . 3),n) ) &amp; ( i = 4 implies it . i = MUL_MOD ((m . 4),(k . 4),n) ) &amp; ( i <> 1 &amp; i <> 2 &amp; i <> 3 &amp; i <> 4 implies it . i = m . i ) ) ) );
existence
 ex b1 being FinSequence of NAT st
( len b1 = len m &amp; ( for i being Element of NAT st i in dom m holds
( ( i = 1 implies b1 . i = MUL_MOD ((m . 1),(k . 1),n) ) &amp; ( i = 2 implies b1 . i = ADD_MOD ((m . 2),(k . 2),n) ) &amp; ( i = 3 implies b1 . i = ADD_MOD ((m . 3),(k . 3),n) ) &amp; ( i = 4 implies b1 . i = MUL_MOD ((m . 4),(k . 4),n) ) &amp; ( i <> 1 &amp; i <> 2 &amp; i <> 3 &amp; i <> 4 implies b1 . i = m . i ) ) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of NAT st len b1 = len m &amp; ( for i being Element of NAT st i in dom m holds
( ( i = 1 implies b1 . i = MUL_MOD ((m . 1),(k . 1),n) ) &amp; ( i = 2 implies b1 . i = ADD_MOD ((m . 2),(k . 2),n) ) &amp; ( i = 3 implies b1 . i = ADD_MOD ((m . 3),(k . 3),n) ) &amp; ( i = 4 implies b1 . i = MUL_MOD ((m . 4),(k . 4),n) ) &amp; ( i <> 1 &amp; i <> 2 &amp; i <> 3 &amp; i <> 4 implies b1 . i = m . i ) ) ) &amp; len b2 = len m &amp; ( for i being Element of NAT st i in dom m holds
( ( i = 1 implies b2 . i = MUL_MOD ((m . 1),(k . 1),n) ) &amp; ( i = 2 implies b2 . i = ADD_MOD ((m . 2),(k . 2),n) ) &amp; ( i = 3 implies b2 . i = ADD_MOD ((m . 3),(k . 3),n) ) &amp; ( i = 4 implies b2 . i = MUL_MOD ((m . 4),(k . 4),n) ) &amp; ( i <> 1 &amp; i <> 2 &amp; i <> 3 &amp; i <> 4 implies b2 . i = m . i ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines IDEAoperationA IDEA_1:def_11_:_
 for n being Element of NAT
for m, k, b4 being FinSequence of NAT holds
( b4 = IDEAoperationA (m,k,n) iff ( len b4 = len m &amp; ( for i being Element of NAT st i in dom m holds
( ( i = 1 implies b4 . i = MUL_MOD ((m . 1),(k . 1),n) ) &amp; ( i = 2 implies b4 . i = ADD_MOD ((m . 2),(k . 2),n) ) &amp; ( i = 3 implies b4 . i = ADD_MOD ((m . 3),(k . 3),n) ) &amp; ( i = 4 implies b4 . i = MUL_MOD ((m . 4),(k . 4),n) ) &amp; ( i <> 1 &amp; i <> 2 &amp; i <> 3 &amp; i <> 4 implies b4 . i = m . i ) ) ) ) );

definition
let n be non empty Element of NAT ;
let m, k be FinSequence of NAT ;
func IDEAoperationB (m,k,n) ->  FinSequence of NAT  means :Def12: :: IDEA_1:def 12
( len it = len m &amp; ( for i being Element of NAT st i in dom m holds
( ( i = 1 implies it . i = Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)))) ) &amp; ( 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)))) ) &amp; ( 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)))) ) &amp; ( 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)))) ) &amp; ( i <> 1 &amp; i <> 2 &amp; i <> 3 &amp; i <> 4 implies it . i = m . i ) ) ) );
existence
 ex b1 being FinSequence of NAT st
( len b1 = len m &amp; ( for i being Element of NAT st i in dom m holds
( ( i = 1 implies b1 . i = Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)))) ) &amp; ( i = 2 implies b1 . i = Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)),n)))) ) &amp; ( i = 3 implies b1 . i = Absval ((n -BinarySequence (m . 3)) 'xor' (n -BinarySequence (MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)))) ) &amp; ( i = 4 implies b1 . i = Absval ((n -BinarySequence (m . 4)) 'xor' (n -BinarySequence (ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)),n)))) ) &amp; ( i <> 1 &amp; i <> 2 &amp; i <> 3 &amp; i <> 4 implies b1 . i = m . i ) ) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of NAT st len b1 = len m &amp; ( for i being Element of NAT st i in dom m holds
( ( i = 1 implies b1 . i = Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)))) ) &amp; ( i = 2 implies b1 . i = Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)),n)))) ) &amp; ( i = 3 implies b1 . i = Absval ((n -BinarySequence (m . 3)) 'xor' (n -BinarySequence (MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)))) ) &amp; ( i = 4 implies b1 . i = Absval ((n -BinarySequence (m . 4)) 'xor' (n -BinarySequence (ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)),n)))) ) &amp; ( i <> 1 &amp; i <> 2 &amp; i <> 3 &amp; i <> 4 implies b1 . i = m . i ) ) ) &amp; len b2 = len m &amp; ( for i being Element of NAT st i in dom m holds
( ( i = 1 implies b2 . i = Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)))) ) &amp; ( i = 2 implies b2 . i = Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)),n)))) ) &amp; ( i = 3 implies b2 . i = Absval ((n -BinarySequence (m . 3)) 'xor' (n -BinarySequence (MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)))) ) &amp; ( i = 4 implies b2 . i = Absval ((n -BinarySequence (m . 4)) 'xor' (n -BinarySequence (ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)),n)))) ) &amp; ( i <> 1 &amp; i <> 2 &amp; i <> 3 &amp; i <> 4 implies b2 . i = m . i ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def12 defines IDEAoperationB IDEA_1:def_12_:_
 for n being non empty Element of NAT
for m, k, b4 being FinSequence of NAT holds
( b4 = IDEAoperationB (m,k,n) iff ( len b4 = len m &amp; ( for i being Element of NAT st i in dom m holds
( ( i = 1 implies b4 . i = Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)))) ) &amp; ( i = 2 implies b4 . i = Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)),n)))) ) &amp; ( i = 3 implies b4 . i = Absval ((n -BinarySequence (m . 3)) 'xor' (n -BinarySequence (MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)))) ) &amp; ( i = 4 implies b4 . i = Absval ((n -BinarySequence (m . 4)) 'xor' (n -BinarySequence (ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)),n)))) ) &amp; ( i <> 1 &amp; i <> 2 &amp; i <> 3 &amp; i <> 4 implies b4 . i = m . i ) ) ) ) );

:: Definiton of IDEA Operation C
definition
let m be FinSequence of NAT ;
func IDEAoperationC m ->  FinSequence of NAT  means :Def13: :: IDEA_1:def 13
( len it = len m &amp; ( for i being Element of NAT st i in dom m holds
it . i = IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) ) );
existence
 ex b1 being FinSequence of NAT st
( len b1 = len m &amp; ( for i being Element of NAT st i in dom m holds
b1 . i = IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of NAT st len b1 = len m &amp; ( for i being Element of NAT st i in dom m holds
b1 . i = IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) ) &amp; len b2 = len m &amp; ( for i being Element of NAT st i in dom m holds
b2 . i = IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def13 defines IDEAoperationC IDEA_1:def_13_:_
 for m, b2 being FinSequence of NAT holds
( b2 = IDEAoperationC m iff ( len b2 = len m &amp; ( for i being Element of NAT st i in dom m holds
b2 . i = IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) ) ) );

theorem Th26: :: IDEA_1:26
for n being Element of NAT
for m, k being FinSequence of NAT st len m >= 4 holds
( (IDEAoperationA (m,k,n)) . 1 is_expressible_by n &amp; (IDEAoperationA (m,k,n)) . 2 is_expressible_by n &amp; (IDEAoperationA (m,k,n)) . 3 is_expressible_by n &amp; (IDEAoperationA (m,k,n)) . 4 is_expressible_by n )
proofend;

theorem Th27: :: IDEA_1:27
for m, k being FinSequence of NAT
for n being non empty Element of NAT st len m >= 4 holds
( (IDEAoperationB (m,k,n)) . 1 is_expressible_by n &amp; (IDEAoperationB (m,k,n)) . 2 is_expressible_by n &amp; (IDEAoperationB (m,k,n)) . 3 is_expressible_by n &amp; (IDEAoperationB (m,k,n)) . 4 is_expressible_by n )
proofend;

Lm3:  for m being FinSequence of NAT
for i being Element of NAT st i = 2 &amp; i in dom m holds
(IDEAoperationC m) . i = m . 3
proofend;

Lm4:  for m being FinSequence of NAT
for i being Element of NAT st i = 3 &amp; i in dom m holds
(IDEAoperationC m) . i = m . 2
proofend;

Lm5:  for m being FinSequence of NAT
for i being Element of NAT st i <> 2 &amp; i <> 3 &amp; i in dom m holds
(IDEAoperationC m) . i = m . i
proofend;

theorem :: IDEA_1:28
for n being Element of NAT
for m being FinSequence of NAT st len m >= 4 &amp; m . 1 is_expressible_by n &amp; m . 2 is_expressible_by n &amp; m . 3 is_expressible_by n &amp; m . 4 is_expressible_by n holds
( (IDEAoperationC m) . 1 is_expressible_by n &amp; (IDEAoperationC m) . 2 is_expressible_by n &amp; (IDEAoperationC m) . 3 is_expressible_by n &amp; (IDEAoperationC m) . 4 is_expressible_by n )
proofend;

theorem Th29: :: IDEA_1:29
for n being non empty Element of NAT
for m, k1, k2 being FinSequence of NAT st (2 to_power n) + 1 is prime &amp; len m >= 4 &amp; m . 1 is_expressible_by n &amp; m . 2 is_expressible_by n &amp; m . 3 is_expressible_by n &amp; m . 4 is_expressible_by n &amp; k1 . 1 is_expressible_by n &amp; k1 . 2 is_expressible_by n &amp; k1 . 3 is_expressible_by n &amp; k1 . 4 is_expressible_by n &amp; k2 . 1 = INV_MOD ((k1 . 1),n) &amp; k2 . 2 = NEG_MOD ((k1 . 2),n) &amp; k2 . 3 = NEG_MOD ((k1 . 3),n) &amp; k2 . 4 = INV_MOD ((k1 . 4),n) holds
IDEAoperationA ((IDEAoperationA (m,k1,n)),k2,n) = m
proofend;

theorem Th30: :: IDEA_1:30
for n being non empty Element of NAT
for m, k1, k2 being FinSequence of NAT st (2 to_power n) + 1 is prime &amp; len m >= 4 &amp; m . 1 is_expressible_by n &amp; m . 2 is_expressible_by n &amp; m . 3 is_expressible_by n &amp; m . 4 is_expressible_by n &amp; k1 . 1 is_expressible_by n &amp; k1 . 2 is_expressible_by n &amp; k1 . 3 is_expressible_by n &amp; k1 . 4 is_expressible_by n &amp; k2 . 1 = INV_MOD ((k1 . 1),n) &amp; k2 . 2 = NEG_MOD ((k1 . 3),n) &amp; k2 . 3 = NEG_MOD ((k1 . 2),n) &amp; k2 . 4 = INV_MOD ((k1 . 4),n) holds
IDEAoperationA ((IDEAoperationC (IDEAoperationA ((IDEAoperationC m),k1,n))),k2,n) = m
proofend;

theorem Th31: :: IDEA_1:31
for n being non empty Element of NAT
for m, k1, k2 being FinSequence of NAT st len m >= 4 &amp; m . 1 is_expressible_by n &amp; m . 2 is_expressible_by n &amp; m . 3 is_expressible_by n &amp; m . 4 is_expressible_by n &amp; k2 . 5 = k1 . 5 &amp; k2 . 6 = k1 . 6 holds
IDEAoperationB ((IDEAoperationB (m,k1,n)),k2,n) = m
proofend;

theorem :: IDEA_1:32
for m being FinSequence of NAT st len m >= 4 holds
IDEAoperationC (IDEAoperationC m) = m
proofend;

begin

:: 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 :: IDEA_1:def 14
NAT * ;
coherence
 NAT * is set ;
end;

:: deftheorem  defines MESSAGES IDEA_1:def_14_:_
 MESSAGES = NAT * ;

registration
cluster MESSAGES  ->  non empty ;
coherence
 not MESSAGES is empty ;
end;

registration
cluster MESSAGES  ->  functional ;
coherence
 MESSAGES is functional ;
end;

registration
cluster  ->  FinSequence-like for Element of MESSAGES ;
coherence
 for b1 being Element of MESSAGES holds b1 is FinSequence-like ;
end;

definition
let n be non empty Element of NAT ;
let k be FinSequence of NAT ;
func IDEA_P (k,n) ->  Function of MESSAGES,MESSAGES means :Def15: :: IDEA_1:def 15
 for m being FinSequence of NAT holds it . m = IDEAoperationA ((IDEAoperationC (IDEAoperationB (m,k,n))),k,n);
existence
 ex b1 being Function of MESSAGES,MESSAGES st
for m being FinSequence of NAT holds b1 . m = IDEAoperationA ((IDEAoperationC (IDEAoperationB (m,k,n))),k,n)
proofend;
uniqueness
 for b1, b2 being Function of MESSAGES,MESSAGES st ( for m being FinSequence of NAT holds b1 . m = IDEAoperationA ((IDEAoperationC (IDEAoperationB (m,k,n))),k,n) ) &amp; ( for m being FinSequence of NAT holds b2 . m = IDEAoperationA ((IDEAoperationC (IDEAoperationB (m,k,n))),k,n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def15 defines IDEA_P IDEA_1:def_15_:_
 for n being non empty Element of NAT
for k being FinSequence of NAT
for b3 being Function of MESSAGES,MESSAGES holds
( b3 = IDEA_P (k,n) iff for m being FinSequence of NAT holds b3 . m = IDEAoperationA ((IDEAoperationC (IDEAoperationB (m,k,n))),k,n) );

definition
let n be non empty Element of NAT ;
let k be FinSequence of NAT ;
func IDEA_Q (k,n) ->  Function of MESSAGES,MESSAGES means :Def16: :: IDEA_1:def 16
 for m being FinSequence of NAT holds it . m = IDEAoperationB ((IDEAoperationA ((IDEAoperationC m),k,n)),k,n);
existence
 ex b1 being Function of MESSAGES,MESSAGES st
for m being FinSequence of NAT holds b1 . m = IDEAoperationB ((IDEAoperationA ((IDEAoperationC m),k,n)),k,n)
proofend;
uniqueness
 for b1, b2 being Function of MESSAGES,MESSAGES st ( for m being FinSequence of NAT holds b1 . m = IDEAoperationB ((IDEAoperationA ((IDEAoperationC m),k,n)),k,n) ) &amp; ( for m being FinSequence of NAT holds b2 . m = IDEAoperationB ((IDEAoperationA ((IDEAoperationC m),k,n)),k,n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def16 defines IDEA_Q IDEA_1:def_16_:_
 for n being non empty Element of NAT
for k being FinSequence of NAT
for b3 being Function of MESSAGES,MESSAGES holds
( b3 = IDEA_Q (k,n) iff for m being FinSequence of NAT holds b3 . m = IDEAoperationB ((IDEAoperationA ((IDEAoperationC m),k,n)),k,n) );

definition
let r, lk be Element of NAT ;
let n be non empty Element of NAT ;
let Key be Matrix of lk,6, NAT ;
func IDEA_P_F (Key,n,r) ->  FinSequence means :Def17: :: IDEA_1:def 17
( len it = r &amp; ( for i being Element of NAT st i in dom it holds
it . i = IDEA_P ((Line (Key,i)),n) ) );
existence
 ex b1 being FinSequence st
( len b1 = r &amp; ( for i being Element of NAT st i in dom b1 holds
b1 . i = IDEA_P ((Line (Key,i)),n) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence st len b1 = r &amp; ( for i being Element of NAT st i in dom b1 holds
b1 . i = IDEA_P ((Line (Key,i)),n) ) &amp; len b2 = r &amp; ( for i being Element of NAT st i in dom b2 holds
b2 . i = IDEA_P ((Line (Key,i)),n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def17 defines IDEA_P_F IDEA_1:def_17_:_
 for r, lk being Element of NAT
for n being non empty Element of NAT
for Key being Matrix of lk,6, NAT
for b5 being FinSequence holds
( b5 = IDEA_P_F (Key,n,r) iff ( len b5 = r &amp; ( for i being Element of NAT st i in dom b5 holds
b5 . i = IDEA_P ((Line (Key,i)),n) ) ) );

registration
let r, lk be Element of NAT ;
let n be non empty Element of NAT ;
let Key be Matrix of lk,6, NAT ;
cluster IDEA_P_F (Key,n,r) ->  Function-yielding ;
coherence
 IDEA_P_F (Key,n,r) is Function-yielding
proofend;
end;

definition
let r, lk be Element of NAT ;
let n be non empty Element of NAT ;
let Key be Matrix of lk,6, NAT ;
func IDEA_Q_F (Key,n,r) ->  FinSequence means :Def18: :: IDEA_1:def 18
( len it = r &amp; ( for i being Element of NAT st i in dom it holds
it . i = IDEA_Q ((Line (Key,((r -' i) + 1))),n) ) );
existence
 ex b1 being FinSequence st
( len b1 = r &amp; ( for i being Element of NAT st i in dom b1 holds
b1 . i = IDEA_Q ((Line (Key,((r -' i) + 1))),n) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence st len b1 = r &amp; ( for i being Element of NAT st i in dom b1 holds
b1 . i = IDEA_Q ((Line (Key,((r -' i) + 1))),n) ) &amp; len b2 = r &amp; ( for i being Element of NAT st i in dom b2 holds
b2 . i = IDEA_Q ((Line (Key,((r -' i) + 1))),n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def18 defines IDEA_Q_F IDEA_1:def_18_:_
 for r, lk being Element of NAT
for n being non empty Element of NAT
for Key being Matrix of lk,6, NAT
for b5 being FinSequence holds
( b5 = IDEA_Q_F (Key,n,r) iff ( len b5 = r &amp; ( for i being Element of NAT st i in dom b5 holds
b5 . i = IDEA_Q ((Line (Key,((r -' i) + 1))),n) ) ) );

registration
let r, lk be Element of NAT ;
let n be non empty Element of NAT ;
let Key be Matrix of lk,6, NAT ;
cluster IDEA_Q_F (Key,n,r) ->  Function-yielding ;
coherence
 IDEA_Q_F (Key,n,r) is Function-yielding
proofend;
end;

definition
let k be FinSequence of NAT ;
let n be Element of NAT ;
func IDEA_PS (k,n) ->  Function of MESSAGES,MESSAGES means :Def19: :: IDEA_1:def 19
 for m being FinSequence of NAT holds it . m = IDEAoperationA (m,k,n);
existence
 ex b1 being Function of MESSAGES,MESSAGES st
for m being FinSequence of NAT holds b1 . m = IDEAoperationA (m,k,n)
proofend;
uniqueness
 for b1, b2 being Function of MESSAGES,MESSAGES st ( for m being FinSequence of NAT holds b1 . m = IDEAoperationA (m,k,n) ) &amp; ( for m being FinSequence of NAT holds b2 . m = IDEAoperationA (m,k,n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def19 defines IDEA_PS IDEA_1:def_19_:_
 for k being FinSequence of NAT
for n being Element of NAT
for b3 being Function of MESSAGES,MESSAGES holds
( b3 = IDEA_PS (k,n) iff for m being FinSequence of NAT holds b3 . m = IDEAoperationA (m,k,n) );

definition
let k be FinSequence of NAT ;
let n be Element of NAT ;
func IDEA_QS (k,n) ->  Function of MESSAGES,MESSAGES means :Def20: :: IDEA_1:def 20
 for m being FinSequence of NAT holds it . m = IDEAoperationA (m,k,n);
existence
 ex b1 being Function of MESSAGES,MESSAGES st
for m being FinSequence of NAT holds b1 . m = IDEAoperationA (m,k,n)
proofend;
uniqueness
 for b1, b2 being Function of MESSAGES,MESSAGES st ( for m being FinSequence of NAT holds b1 . m = IDEAoperationA (m,k,n) ) &amp; ( for m being FinSequence of NAT holds b2 . m = IDEAoperationA (m,k,n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def20 defines IDEA_QS IDEA_1:def_20_:_
 for k being FinSequence of NAT
for n being Element of NAT
for b3 being Function of MESSAGES,MESSAGES holds
( b3 = IDEA_QS (k,n) iff for m being FinSequence of NAT holds b3 . m = IDEAoperationA (m,k,n) );

definition
let n be non empty Element of NAT ;
let k be FinSequence of NAT ;
func IDEA_PE (k,n) ->  Function of MESSAGES,MESSAGES means :Def21: :: IDEA_1:def 21
 for m being FinSequence of NAT holds it . m = IDEAoperationA ((IDEAoperationB (m,k,n)),k,n);
existence
 ex b1 being Function of MESSAGES,MESSAGES st
for m being FinSequence of NAT holds b1 . m = IDEAoperationA ((IDEAoperationB (m,k,n)),k,n)
proofend;
uniqueness
 for b1, b2 being Function of MESSAGES,MESSAGES st ( for m being FinSequence of NAT holds b1 . m = IDEAoperationA ((IDEAoperationB (m,k,n)),k,n) ) &amp; ( for m being FinSequence of NAT holds b2 . m = IDEAoperationA ((IDEAoperationB (m,k,n)),k,n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def21 defines IDEA_PE IDEA_1:def_21_:_
 for n being non empty Element of NAT
for k being FinSequence of NAT
for b3 being Function of MESSAGES,MESSAGES holds
( b3 = IDEA_PE (k,n) iff for m being FinSequence of NAT holds b3 . m = IDEAoperationA ((IDEAoperationB (m,k,n)),k,n) );

definition
let n be non empty Element of NAT ;
let k be FinSequence of NAT ;
func IDEA_QE (k,n) ->  Function of MESSAGES,MESSAGES means :Def22: :: IDEA_1:def 22
 for m being FinSequence of NAT holds it . m = IDEAoperationB ((IDEAoperationA (m,k,n)),k,n);
existence
 ex b1 being Function of MESSAGES,MESSAGES st
for m being FinSequence of NAT holds b1 . m = IDEAoperationB ((IDEAoperationA (m,k,n)),k,n)
proofend;
uniqueness
 for b1, b2 being Function of MESSAGES,MESSAGES st ( for m being FinSequence of NAT holds b1 . m = IDEAoperationB ((IDEAoperationA (m,k,n)),k,n) ) &amp; ( for m being FinSequence of NAT holds b2 . m = IDEAoperationB ((IDEAoperationA (m,k,n)),k,n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def22 defines IDEA_QE IDEA_1:def_22_:_
 for n being non empty Element of NAT
for k being FinSequence of NAT
for b3 being Function of MESSAGES,MESSAGES holds
( b3 = IDEA_QE (k,n) iff for m being FinSequence of NAT holds b3 . m = IDEAoperationB ((IDEAoperationA (m,k,n)),k,n) );

theorem Th33: :: IDEA_1:33
for n being non empty Element of NAT
for m, k1, k2 being FinSequence of NAT st (2 to_power n) + 1 is prime &amp; len m >= 4 &amp; m . 1 is_expressible_by n &amp; m . 2 is_expressible_by n &amp; m . 3 is_expressible_by n &amp; m . 4 is_expressible_by n &amp; k1 . 1 is_expressible_by n &amp; k1 . 2 is_expressible_by n &amp; k1 . 3 is_expressible_by n &amp; k1 . 4 is_expressible_by n &amp; k2 . 1 = INV_MOD ((k1 . 1),n) &amp; k2 . 2 = NEG_MOD ((k1 . 3),n) &amp; k2 . 3 = NEG_MOD ((k1 . 2),n) &amp; k2 . 4 = INV_MOD ((k1 . 4),n) &amp; k2 . 5 = k1 . 5 &amp; k2 . 6 = k1 . 6 holds
((IDEA_Q (k2,n)) * (IDEA_P (k1,n))) . m = m
proofend;

theorem Th34: :: IDEA_1:34
for n being non empty Element of NAT
for m, k1, k2 being FinSequence of NAT st (2 to_power n) + 1 is prime &amp; len m >= 4 &amp; m . 1 is_expressible_by n &amp; m . 2 is_expressible_by n &amp; m . 3 is_expressible_by n &amp; m . 4 is_expressible_by n &amp; k1 . 1 is_expressible_by n &amp; k1 . 2 is_expressible_by n &amp; k1 . 3 is_expressible_by n &amp; k1 . 4 is_expressible_by n &amp; k2 . 1 = INV_MOD ((k1 . 1),n) &amp; k2 . 2 = NEG_MOD ((k1 . 2),n) &amp; k2 . 3 = NEG_MOD ((k1 . 3),n) &amp; k2 . 4 = INV_MOD ((k1 . 4),n) holds
((IDEA_QS (k2,n)) * (IDEA_PS (k1,n))) . m = m
proofend;

theorem Th35: :: IDEA_1:35
for n being non empty Element of NAT
for m, k1, k2 being FinSequence of NAT st (2 to_power n) + 1 is prime &amp; len m >= 4 &amp; m . 1 is_expressible_by n &amp; m . 2 is_expressible_by n &amp; m . 3 is_expressible_by n &amp; m . 4 is_expressible_by n &amp; k1 . 1 is_expressible_by n &amp; k1 . 2 is_expressible_by n &amp; k1 . 3 is_expressible_by n &amp; k1 . 4 is_expressible_by n &amp; k2 . 1 = INV_MOD ((k1 . 1),n) &amp; k2 . 2 = NEG_MOD ((k1 . 2),n) &amp; k2 . 3 = NEG_MOD ((k1 . 3),n) &amp; k2 . 4 = INV_MOD ((k1 . 4),n) &amp; k2 . 5 = k1 . 5 &amp; k2 . 6 = k1 . 6 holds
((IDEA_QE (k2,n)) * (IDEA_PE (k1,n))) . m = m
proofend;

theorem Th36: :: IDEA_1:36
for n being non empty Element of NAT
for lk being Element of NAT
for Key being Matrix of lk,6, NAT
for k being Element of NAT holds IDEA_P_F (Key,n,(k + 1)) = (IDEA_P_F (Key,n,k)) ^ <*(IDEA_P ((Line (Key,(k + 1))),n))*>
proofend;

theorem Th37: :: IDEA_1:37
for n being non empty Element of NAT
for lk being Element of NAT
for Key being Matrix of lk,6, NAT
for k being Element of NAT holds IDEA_Q_F (Key,n,(k + 1)) = <*(IDEA_Q ((Line (Key,(k + 1))),n))*> ^ (IDEA_Q_F (Key,n,k))
proofend;

theorem Th38: :: IDEA_1:38
for n being non empty Element of NAT
for lk being Element of NAT
for Key being Matrix of lk,6, NAT
for k being Element of NAT holds IDEA_P_F (Key,n,k) is FuncSeq-like FinSequence
proofend;

theorem Th39: :: IDEA_1:39
for n being non empty Element of NAT
for lk being Element of NAT
for Key being Matrix of lk,6, NAT
for k being Element of NAT holds IDEA_Q_F (Key,n,k) is FuncSeq-like FinSequence
proofend;

theorem Th40: :: IDEA_1:40
for n being non empty Element of NAT
for lk being Element of NAT
for Key being Matrix of lk,6, NAT
for k being Element of NAT st k <> 0 holds
IDEA_P_F (Key,n,k) is FuncSequence of MESSAGES , MESSAGES
proofend;

theorem Th41: :: IDEA_1:41
for n being non empty Element of NAT
for lk being Element of NAT
for Key being Matrix of lk,6, NAT
for k being Element of NAT st k <> 0 holds
IDEA_Q_F (Key,n,k) is FuncSequence of MESSAGES , MESSAGES
proofend;

theorem Th42: :: IDEA_1:42
for n being non empty Element of NAT
for M, m, k being FinSequence of NAT st M = (IDEA_P (k,n)) . m &amp; len m >= 4 holds
( len M >= 4 &amp; M . 1 is_expressible_by n &amp; M . 2 is_expressible_by n &amp; M . 3 is_expressible_by n &amp; M . 4 is_expressible_by n )
proofend;

theorem Th43: :: IDEA_1:43
for n being non empty Element of NAT
for lk being Element of NAT
for Key being Matrix of lk,6, NAT
for r being Element of NAT holds
( rng (compose ((IDEA_P_F (Key,n,r)),MESSAGES)) c= MESSAGES &amp; dom (compose ((IDEA_P_F (Key,n,r)),MESSAGES)) = MESSAGES )
proofend;

theorem :: IDEA_1:44
for n being non empty Element of NAT
for lk being Element of NAT
for Key being Matrix of lk,6, NAT
for r being Element of NAT holds
( rng (compose ((IDEA_Q_F (Key,n,r)),MESSAGES)) c= MESSAGES &amp; dom (compose ((IDEA_Q_F (Key,n,r)),MESSAGES)) = MESSAGES )
proofend;

theorem Th45: :: IDEA_1:45
for n being non empty Element of NAT
for lk being Element of NAT
for Key being Matrix of lk,6, NAT
for r being Element of NAT
for M, m being FinSequence of NAT st M = (compose ((IDEA_P_F (Key,n,r)),MESSAGES)) . m &amp; len m >= 4 &amp; m . 1 is_expressible_by n &amp; m . 2 is_expressible_by n &amp; m . 3 is_expressible_by n &amp; m . 4 is_expressible_by n holds
( len M >= 4 &amp; M . 1 is_expressible_by n &amp; M . 2 is_expressible_by n &amp; M . 3 is_expressible_by n &amp; M . 4 is_expressible_by n )
proofend;

begin

:: 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: :: IDEA_1:46
for n being non empty Element of NAT
for lk being Element of NAT
for Key1, Key2 being Matrix of lk,6, NAT
for r being Element of NAT
for m being FinSequence of NAT st lk >= r &amp; (2 to_power n) + 1 is prime &amp; len m >= 4 &amp; m . 1 is_expressible_by n &amp; m . 2 is_expressible_by n &amp; m . 3 is_expressible_by n &amp; m . 4 is_expressible_by n &amp; ( for i being Element of NAT st i <= r holds
( Key1 * (i,1) is_expressible_by n &amp; Key1 * (i,2) is_expressible_by n &amp; Key1 * (i,3) is_expressible_by n &amp; Key1 * (i,4) is_expressible_by n &amp; Key1 * (i,5) is_expressible_by n &amp; Key1 * (i,6) is_expressible_by n &amp; Key2 * (i,1) is_expressible_by n &amp; Key2 * (i,2) is_expressible_by n &amp; Key2 * (i,3) is_expressible_by n &amp; Key2 * (i,4) is_expressible_by n &amp; Key2 * (i,5) is_expressible_by n &amp; Key2 * (i,6) is_expressible_by n &amp; Key2 * (i,1) = INV_MOD ((Key1 * (i,1)),n) &amp; Key2 * (i,2) = NEG_MOD ((Key1 * (i,3)),n) &amp; Key2 * (i,3) = NEG_MOD ((Key1 * (i,2)),n) &amp; Key2 * (i,4) = INV_MOD ((Key1 * (i,4)),n) &amp; Key1 * (i,5) = Key2 * (i,5) &amp; Key1 * (i,6) = Key2 * (i,6) ) ) holds
(compose (((IDEA_P_F (Key1,n,r)) ^ (IDEA_Q_F (Key2,n,r))),MESSAGES)) . m = m
proofend;

theorem :: IDEA_1:47
for n being non empty Element of NAT
for lk being Element of NAT
for Key1, Key2 being Matrix of lk,6, NAT
for r being Element of NAT
for ks1, ks2, ke1, ke2, m being FinSequence of NAT st lk >= r &amp; (2 to_power n) + 1 is prime &amp; len m >= 4 &amp; m . 1 is_expressible_by n &amp; m . 2 is_expressible_by n &amp; m . 3 is_expressible_by n &amp; m . 4 is_expressible_by n &amp; ( for i being Element of NAT st i <= r holds
( Key1 * (i,1) is_expressible_by n &amp; Key1 * (i,2) is_expressible_by n &amp; Key1 * (i,3) is_expressible_by n &amp; Key1 * (i,4) is_expressible_by n &amp; Key1 * (i,5) is_expressible_by n &amp; Key1 * (i,6) is_expressible_by n &amp; Key2 * (i,1) is_expressible_by n &amp; Key2 * (i,2) is_expressible_by n &amp; Key2 * (i,3) is_expressible_by n &amp; Key2 * (i,4) is_expressible_by n &amp; Key2 * (i,5) is_expressible_by n &amp; Key2 * (i,6) is_expressible_by n &amp; Key2 * (i,1) = INV_MOD ((Key1 * (i,1)),n) &amp; Key2 * (i,2) = NEG_MOD ((Key1 * (i,3)),n) &amp; Key2 * (i,3) = NEG_MOD ((Key1 * (i,2)),n) &amp; Key2 * (i,4) = INV_MOD ((Key1 * (i,4)),n) &amp; Key1 * (i,5) = Key2 * (i,5) &amp; Key1 * (i,6) = Key2 * (i,6) ) ) &amp; ks1 . 1 is_expressible_by n &amp; ks1 . 2 is_expressible_by n &amp; ks1 . 3 is_expressible_by n &amp; ks1 . 4 is_expressible_by n &amp; ks2 . 1 = INV_MOD ((ks1 . 1),n) &amp; ks2 . 2 = NEG_MOD ((ks1 . 2),n) &amp; ks2 . 3 = NEG_MOD ((ks1 . 3),n) &amp; ks2 . 4 = INV_MOD ((ks1 . 4),n) &amp; ke1 . 1 is_expressible_by n &amp; ke1 . 2 is_expressible_by n &amp; ke1 . 3 is_expressible_by n &amp; ke1 . 4 is_expressible_by n &amp; ke2 . 1 = INV_MOD ((ke1 . 1),n) &amp; ke2 . 2 = NEG_MOD ((ke1 . 2),n) &amp; ke2 . 3 = NEG_MOD ((ke1 . 3),n) &amp; ke2 . 4 = INV_MOD ((ke1 . 4),n) &amp; ke2 . 5 = ke1 . 5 &amp; 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
proofend;