:: Formalization of the Advanced Encryption Standard -- Part {I}
:: by Kenichi Arai and Hiroyuki Okazaki
::
:: Copyright (c) 2013-2021 Association of Mizar Users

theorem XLMOD02: :: AESCIP_1:1
for k, m being Nat st m <> 0 & (k + 1) mod m <> 0 holds
(k + 1) mod m = (k mod m) + 1
proof end;

theorem XLMOD01: :: AESCIP_1:2
for k, m being Nat st m <> 0 & (k + 1) mod m <> 0 holds
(k + 1) div m = k div m
proof end;

theorem XLMOD02X: :: AESCIP_1:3
for k, m being Nat st m <> 0 & (k + 1) mod m = 0 holds
m - 1 = k mod m
proof end;

theorem XLMOD01X: :: AESCIP_1:4
for k, m being Nat st m <> 0 & (k + 1) mod m = 0 holds
(k + 1) div m = (k div m) + 1
proof end;

theorem XLMOD03: :: AESCIP_1:5
for k, m being Nat holds (k - m) mod m = k mod m
proof end;

theorem XLMOD04: :: AESCIP_1:6
for k, m being Nat st m <> 0 holds
(k - m) div m = (k div m) - 1
proof end;

definition
let m, n be Nat;
let X, D be non empty set ;
let F be Function of X,(m -tuples_on ());
let x be Element of X;
:: original: .
redefine func F . x -> Element of m -tuples_on ();
coherence
F . x is Element of m -tuples_on ()
proof end;
end;

definition
let m be Nat;
let X, Y, D be non empty set ;
let F be Function of [:X,Y:],();
let x be Element of X;
let y be Element of Y;
:: original: .
redefine func F . (x,y) -> Element of m -tuples_on D;
coherence
F . (x,y) is Element of m -tuples_on D
proof end;
end;

theorem LM01: :: AESCIP_1:7
for m, n being Nat
for D being non empty set
for F1, F2 being Element of m -tuples_on () st ( for i, j being Nat st i in Seg m & j in Seg n holds
(F1 . i) . j = (F2 . i) . j ) holds
F1 = F2
proof end;

theorem LMGSEQ4: :: AESCIP_1:8
for D being non empty set
for x1, x2, x3, x4 being Element of D holds <*x1,x2,x3,x4*> is Element of 4 -tuples_on D
proof end;

theorem LMGSEQ5: :: AESCIP_1:9
for D being non empty set
for x1, x2, x3, x4, x5 being Element of D holds <*x1,x2,x3,x4,x5*> is Element of 5 -tuples_on D
proof end;

theorem :: AESCIP_1:10
for D being non empty set
for x1, x2, x3, x4, x5, x6, x7, x8 being Element of D holds <*x1,x2,x3,x4*> ^ <*x5,x6,x7,x8*> is Element of 8 -tuples_on D
proof end;

theorem LMGSEQ10: :: AESCIP_1:11
for D being non empty set
for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10 being Element of D holds <*x1,x2,x3,x4,x5*> ^ <*x6,x7,x8,x9,x10*> is Element of 10 -tuples_on D
proof end;

theorem LMGSEQ16: :: AESCIP_1:12
for D being non empty set
for x1, x2, x3, x4, x5, x6, x7, x8 being Element of 4 -tuples_on D holds <*(x1 ^ x5),(x2 ^ x6),(x3 ^ x7),(x4 ^ x8)*> is Element of 4 -tuples_on ()
proof end;

theorem :: AESCIP_1:13
for D being non empty set
for x being Element of 4 -tuples_on ()
for k being Element of NAT st k in Seg 4 holds
ex x1, x2, x3, x4 being Element of D st
( x1 = (x . k) . 1 & x2 = (x . k) . 2 & x3 = (x . k) . 3 & x4 = (x . k) . 4 )
proof end;

theorem INV00: :: AESCIP_1:14
for X, Y being non empty set
for f being Function of X,Y
for g being Function of Y,X st ( for x being Element of X holds g . (f . x) = x ) & ( for y being Element of Y holds f . (g . y) = y ) holds
( f is one-to-one & f is onto & g is one-to-one & g is onto & g = f " & f = g " )
proof end;

definition
func AES-Statearray -> Function of (),(4 -tuples_on ()) means :DefStatearray: :: AESCIP_1:def 1
for input being Element of 128 -tuples_on BOOLEAN
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
((it . input) . i) . j = mid (input,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7));
existence
ex b1 being Function of (),(4 -tuples_on ()) st
for input being Element of 128 -tuples_on BOOLEAN
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
((b1 . input) . i) . j = mid (input,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7))
proof end;
uniqueness
for b1, b2 being Function of (),(4 -tuples_on ()) st ( for input being Element of 128 -tuples_on BOOLEAN
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
((b1 . input) . i) . j = mid (input,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7)) ) & ( for input being Element of 128 -tuples_on BOOLEAN
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
((b2 . input) . i) . j = mid (input,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7)) ) holds
b1 = b2
proof end;
end;

:: deftheorem DefStatearray defines AES-Statearray AESCIP_1:def 1 :
for b1 being Function of (),(4 -tuples_on ()) holds
( b1 = AES-Statearray iff for input being Element of 128 -tuples_on BOOLEAN
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
((b1 . input) . i) . j = mid (input,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7)) );

theorem LMStat0: :: AESCIP_1:15
for k being Nat st 1 <= k & k <= 128 holds
ex i, j being Nat st
( i in Seg 4 & j in Seg 4 & (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k & k <= ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7 )
proof end;

theorem LMStat2A: :: AESCIP_1:16
for i, j, i0, j0 being Nat st i in Seg 4 & j in Seg 4 & i0 in Seg 4 & j0 in Seg 4 & ( not i = i0 or not j = j0 ) holds
{ k where k is Nat : ( (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k & k <= (8 + ((i -' 1) * 8)) + ((j -' 1) * 32) ) } /\ { k where k is Nat : ( (1 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) <= k & k <= (8 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) ) } = {}
proof end;

theorem LMStat2: :: AESCIP_1:17
for k, i, j, i0, j0 being Nat st 1 <= k & k <= 128 & i in Seg 4 & j in Seg 4 & i0 in Seg 4 & j0 in Seg 4 & (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k & k <= ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7 & (1 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) <= k & k <= ((1 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32)) + 7 holds
( i = i0 & j = j0 )
proof end;

theorem LMStat1: :: AESCIP_1:18
proof end;

theorem LMStat3: :: AESCIP_1:19
proof end;

registration
correctness by ;
end;

theorem LMINV1: :: AESCIP_1:20
for cipher being Element of 4 -tuples_on () holds AES-Statearray . ( . cipher) = cipher
proof end;

definition
let SBT be Permutation of ();
func SubBytes SBT -> Function of (4 -tuples_on ()),(4 -tuples_on ()) means :DefSubBytes: :: AESCIP_1:def 2
for input being Element of 4 -tuples_on ()
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
ex inputij being Element of 8 -tuples_on BOOLEAN st
( inputij = (input . i) . j & ((it . input) . i) . j = SBT . inputij );
existence
ex b1 being Function of (4 -tuples_on ()),(4 -tuples_on ()) st
for input being Element of 4 -tuples_on ()
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
ex inputij being Element of 8 -tuples_on BOOLEAN st
( inputij = (input . i) . j & ((b1 . input) . i) . j = SBT . inputij )
proof end;
uniqueness
for b1, b2 being Function of (4 -tuples_on ()),(4 -tuples_on ()) st ( for input being Element of 4 -tuples_on ()
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
ex inputij being Element of 8 -tuples_on BOOLEAN st
( inputij = (input . i) . j & ((b1 . input) . i) . j = SBT . inputij ) ) & ( for input being Element of 4 -tuples_on ()
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
ex inputij being Element of 8 -tuples_on BOOLEAN st
( inputij = (input . i) . j & ((b2 . input) . i) . j = SBT . inputij ) ) holds
b1 = b2
proof end;
end;

:: deftheorem DefSubBytes defines SubBytes AESCIP_1:def 2 :
for SBT being Permutation of ()
for b2 being Function of (4 -tuples_on ()),(4 -tuples_on ()) holds
( b2 = SubBytes SBT iff for input being Element of 4 -tuples_on ()
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
ex inputij being Element of 8 -tuples_on BOOLEAN st
( inputij = (input . i) . j & ((b2 . input) . i) . j = SBT . inputij ) );

definition
let SBT be Permutation of ();
func InvSubBytes SBT -> Function of (4 -tuples_on ()),(4 -tuples_on ()) means :DefInvSubBytes: :: AESCIP_1:def 3
for input being Element of 4 -tuples_on ()
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
ex inputij being Element of 8 -tuples_on BOOLEAN st
( inputij = (input . i) . j & ((it . input) . i) . j = (SBT ") . inputij );
existence
ex b1 being Function of (4 -tuples_on ()),(4 -tuples_on ()) st
for input being Element of 4 -tuples_on ()
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
ex inputij being Element of 8 -tuples_on BOOLEAN st
( inputij = (input . i) . j & ((b1 . input) . i) . j = (SBT ") . inputij )
proof end;
uniqueness
for b1, b2 being Function of (4 -tuples_on ()),(4 -tuples_on ()) st ( for input being Element of 4 -tuples_on ()
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
ex inputij being Element of 8 -tuples_on BOOLEAN st
( inputij = (input . i) . j & ((b1 . input) . i) . j = (SBT ") . inputij ) ) & ( for input being Element of 4 -tuples_on ()
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
ex inputij being Element of 8 -tuples_on BOOLEAN st
( inputij = (input . i) . j & ((b2 . input) . i) . j = (SBT ") . inputij ) ) holds
b1 = b2
proof end;
end;

:: deftheorem DefInvSubBytes defines InvSubBytes AESCIP_1:def 3 :
for SBT being Permutation of ()
for b2 being Function of (4 -tuples_on ()),(4 -tuples_on ()) holds
( b2 = InvSubBytes SBT iff for input being Element of 4 -tuples_on ()
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
ex inputij being Element of 8 -tuples_on BOOLEAN st
( inputij = (input . i) . j & ((b2 . input) . i) . j = (SBT ") . inputij ) );

INV07A: for SBT being Permutation of ()
for input being Element of 8 -tuples_on BOOLEAN holds (SBT ") . (SBT . input) = input

proof end;

INV08A: for SBT being Permutation of ()
for input being Element of 8 -tuples_on BOOLEAN holds SBT . ((SBT ") . input) = input

proof end;

theorem INV07: :: AESCIP_1:21
for SBT being Permutation of ()
for input being Element of 4 -tuples_on () holds (InvSubBytes SBT) . ((SubBytes SBT) . input) = input
proof end;

theorem INV08: :: AESCIP_1:22
for SBT being Permutation of ()
for output being Element of 4 -tuples_on () holds (SubBytes SBT) . ((InvSubBytes SBT) . output) = output
proof end;

theorem :: AESCIP_1:23
for SBT being Permutation of () holds
( SubBytes SBT is one-to-one & SubBytes SBT is onto & InvSubBytes SBT is one-to-one & InvSubBytes SBT is onto & InvSubBytes SBT = (SubBytes SBT) " & SubBytes SBT = (InvSubBytes SBT) " )
proof end;

definition
func ShiftRows -> Function of (4 -tuples_on ()),(4 -tuples_on ()) means :DefShiftRows: :: AESCIP_1:def 4
for input being Element of 4 -tuples_on ()
for i being Nat st i in Seg 4 holds
ex xi being Element of 4 -tuples_on () st
( xi = input . i & (it . input) . i = Op-Shift (xi,(5 - i)) );
existence
ex b1 being Function of (4 -tuples_on ()),(4 -tuples_on ()) st
for input being Element of 4 -tuples_on ()
for i being Nat st i in Seg 4 holds
ex xi being Element of 4 -tuples_on () st
( xi = input . i & (b1 . input) . i = Op-Shift (xi,(5 - i)) )
proof end;
uniqueness
for b1, b2 being Function of (4 -tuples_on ()),(4 -tuples_on ()) st ( for input being Element of 4 -tuples_on ()
for i being Nat st i in Seg 4 holds
ex xi being Element of 4 -tuples_on () st
( xi = input . i & (b1 . input) . i = Op-Shift (xi,(5 - i)) ) ) & ( for input being Element of 4 -tuples_on ()
for i being Nat st i in Seg 4 holds
ex xi being Element of 4 -tuples_on () st
( xi = input . i & (b2 . input) . i = Op-Shift (xi,(5 - i)) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem DefShiftRows defines ShiftRows AESCIP_1:def 4 :
for b1 being Function of (4 -tuples_on ()),(4 -tuples_on ()) holds
( b1 = ShiftRows iff for input being Element of 4 -tuples_on ()
for i being Nat st i in Seg 4 holds
ex xi being Element of 4 -tuples_on () st
( xi = input . i & (b1 . input) . i = Op-Shift (xi,(5 - i)) ) );

definition
func InvShiftRows -> Function of (4 -tuples_on ()),(4 -tuples_on ()) means :DefInvShiftRows: :: AESCIP_1:def 5
for input being Element of 4 -tuples_on ()
for i being Nat st i in Seg 4 holds
ex xi being Element of 4 -tuples_on () st
( xi = input . i & (it . input) . i = Op-Shift (xi,(i - 1)) );
existence
ex b1 being Function of (4 -tuples_on ()),(4 -tuples_on ()) st
for input being Element of 4 -tuples_on ()
for i being Nat st i in Seg 4 holds
ex xi being Element of 4 -tuples_on () st
( xi = input . i & (b1 . input) . i = Op-Shift (xi,(i - 1)) )
proof end;
uniqueness
for b1, b2 being Function of (4 -tuples_on ()),(4 -tuples_on ()) st ( for input being Element of 4 -tuples_on ()
for i being Nat st i in Seg 4 holds
ex xi being Element of 4 -tuples_on () st
( xi = input . i & (b1 . input) . i = Op-Shift (xi,(i - 1)) ) ) & ( for input being Element of 4 -tuples_on ()
for i being Nat st i in Seg 4 holds
ex xi being Element of 4 -tuples_on () st
( xi = input . i & (b2 . input) . i = Op-Shift (xi,(i - 1)) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem DefInvShiftRows defines InvShiftRows AESCIP_1:def 5 :
for b1 being Function of (4 -tuples_on ()),(4 -tuples_on ()) holds
( b1 = InvShiftRows iff for input being Element of 4 -tuples_on ()
for i being Nat st i in Seg 4 holds
ex xi being Element of 4 -tuples_on () st
( xi = input . i & (b1 . input) . i = Op-Shift (xi,(i - 1)) ) );

theorem INV04: :: AESCIP_1:24
for input being Element of 4 -tuples_on () holds InvShiftRows . (ShiftRows . input) = input
proof end;

theorem INV05: :: AESCIP_1:25
for output being Element of 4 -tuples_on () holds ShiftRows . (InvShiftRows . output) = output
proof end;

theorem :: AESCIP_1:26

definition
func AddRoundKey -> Function of [:(4 -tuples_on ()),(4 -tuples_on ()):],(4 -tuples_on ()) means :DefAddRoundKey: :: AESCIP_1:def 6
for text, key being Element of 4 -tuples_on ()
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
ex textij, keyij being Element of 8 -tuples_on BOOLEAN st
( textij = (text . i) . j & keyij = (key . i) . j & ((it . (text,key)) . i) . j = Op-XOR (textij,keyij) );
existence
ex b1 being Function of [:(4 -tuples_on ()),(4 -tuples_on ()):],(4 -tuples_on ()) st
for text, key being Element of 4 -tuples_on ()
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
ex textij, keyij being Element of 8 -tuples_on BOOLEAN st
( textij = (text . i) . j & keyij = (key . i) . j & ((b1 . (text,key)) . i) . j = Op-XOR (textij,keyij) )
proof end;
uniqueness
for b1, b2 being Function of [:(4 -tuples_on ()),(4 -tuples_on ()):],(4 -tuples_on ()) st ( for text, key being Element of 4 -tuples_on ()
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
ex textij, keyij being Element of 8 -tuples_on BOOLEAN st
( textij = (text . i) . j & keyij = (key . i) . j & ((b1 . (text,key)) . i) . j = Op-XOR (textij,keyij) ) ) & ( for text, key being Element of 4 -tuples_on ()
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
ex textij, keyij being Element of 8 -tuples_on BOOLEAN st
( textij = (text . i) . j & keyij = (key . i) . j & ((b2 . (text,key)) . i) . j = Op-XOR (textij,keyij) ) ) holds
b1 = b2
proof end;
end;

for b1 being Function of [:(4 -tuples_on ()),(4 -tuples_on ()):],(4 -tuples_on ()) holds
( b1 = AddRoundKey iff for text, key being Element of 4 -tuples_on ()
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
ex textij, keyij being Element of 8 -tuples_on BOOLEAN st
( textij = (text . i) . j & keyij = (key . i) . j & ((b1 . (text,key)) . i) . j = Op-XOR (textij,keyij) ) );

definition
let SBT be Permutation of ();
let x be Element of 4 -tuples_on ();
func SubWord (SBT,x) -> Element of 4 -tuples_on () means :: AESCIP_1:def 7
for i being Element of Seg 4 holds it . i = SBT . (x . i);
existence
ex b1 being Element of 4 -tuples_on () st
for i being Element of Seg 4 holds b1 . i = SBT . (x . i)
proof end;
uniqueness
for b1, b2 being Element of 4 -tuples_on () st ( for i being Element of Seg 4 holds b1 . i = SBT . (x . i) ) & ( for i being Element of Seg 4 holds b2 . i = SBT . (x . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines SubWord AESCIP_1:def 7 :
for SBT being Permutation of ()
for x, b3 being Element of 4 -tuples_on () holds
( b3 = SubWord (SBT,x) iff for i being Element of Seg 4 holds b3 . i = SBT . (x . i) );

definition
let x be Element of 4 -tuples_on ();
func RotWord x -> Element of 4 -tuples_on () equals :: AESCIP_1:def 8
Op-LeftShift x;
correctness
coherence
Op-LeftShift x is Element of 4 -tuples_on ()
;
by DESCIP_1:6;
end;

:: deftheorem defines RotWord AESCIP_1:def 8 :
for x being Element of 4 -tuples_on () holds RotWord x = Op-LeftShift x;

definition
let n, m be non zero Element of NAT ;
let s, t be Element of m -tuples_on ();
func Op-WXOR (s,t) -> Element of m -tuples_on () means :: AESCIP_1:def 9
for i being Element of Seg m holds it . i = Op-XOR ((s . i),(t . i));
existence
ex b1 being Element of m -tuples_on () st
for i being Element of Seg m holds b1 . i = Op-XOR ((s . i),(t . i))
proof end;
uniqueness
for b1, b2 being Element of m -tuples_on () st ( for i being Element of Seg m holds b1 . i = Op-XOR ((s . i),(t . i)) ) & ( for i being Element of Seg m holds b2 . i = Op-XOR ((s . i),(t . i)) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines Op-WXOR AESCIP_1:def 9 :
for n, m being non zero Element of NAT
for s, t, b5 being Element of m -tuples_on () holds
( b5 = Op-WXOR (s,t) iff for i being Element of Seg m holds b5 . i = Op-XOR ((s . i),(t . i)) );

definition
func Rcon -> Element of 10 -tuples_on () means :: AESCIP_1:def 10
( it . 1 = <*(<*0,0,0,0*> ^ <*0,0,0,1*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & it . 2 = <*(<*0,0,0,0*> ^ <*0,0,1,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & it . 3 = <*(<*0,0,0,0*> ^ <*0,1,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & it . 4 = <*(<*0,0,0,0*> ^ <*1,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & it . 5 = <*(<*0,0,0,1*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & it . 6 = <*(<*0,0,1,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & it . 7 = <*(<*0,1,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & it . 8 = <*(<*1,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & it . 9 = <*(<*0,0,0,1*> ^ <*1,0,1,1*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & it . 10 = <*(<*0,0,1,1*> ^ <*0,1,1,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> );
existence
ex b1 being Element of 10 -tuples_on () st
( b1 . 1 = <*(<*0,0,0,0*> ^ <*0,0,0,1*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b1 . 2 = <*(<*0,0,0,0*> ^ <*0,0,1,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b1 . 3 = <*(<*0,0,0,0*> ^ <*0,1,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b1 . 4 = <*(<*0,0,0,0*> ^ <*1,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b1 . 5 = <*(<*0,0,0,1*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b1 . 6 = <*(<*0,0,1,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b1 . 7 = <*(<*0,1,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b1 . 8 = <*(<*1,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b1 . 9 = <*(<*0,0,0,1*> ^ <*1,0,1,1*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b1 . 10 = <*(<*0,0,1,1*> ^ <*0,1,1,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> )
proof end;
uniqueness
for b1, b2 being Element of 10 -tuples_on () st b1 . 1 = <*(<*0,0,0,0*> ^ <*0,0,0,1*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b1 . 2 = <*(<*0,0,0,0*> ^ <*0,0,1,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b1 . 3 = <*(<*0,0,0,0*> ^ <*0,1,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b1 . 4 = <*(<*0,0,0,0*> ^ <*1,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b1 . 5 = <*(<*0,0,0,1*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b1 . 6 = <*(<*0,0,1,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b1 . 7 = <*(<*0,1,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b1 . 8 = <*(<*1,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b1 . 9 = <*(<*0,0,0,1*> ^ <*1,0,1,1*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b1 . 10 = <*(<*0,0,1,1*> ^ <*0,1,1,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b2 . 1 = <*(<*0,0,0,0*> ^ <*0,0,0,1*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b2 . 2 = <*(<*0,0,0,0*> ^ <*0,0,1,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b2 . 3 = <*(<*0,0,0,0*> ^ <*0,1,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b2 . 4 = <*(<*0,0,0,0*> ^ <*1,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b2 . 5 = <*(<*0,0,0,1*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b2 . 6 = <*(<*0,0,1,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b2 . 7 = <*(<*0,1,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b2 . 8 = <*(<*1,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b2 . 9 = <*(<*0,0,0,1*> ^ <*1,0,1,1*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b2 . 10 = <*(<*0,0,1,1*> ^ <*0,1,1,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> holds
b1 = b2
proof end;
end;

:: deftheorem defines Rcon AESCIP_1:def 10 :
for b1 being Element of 10 -tuples_on () holds
( b1 = Rcon iff ( b1 . 1 = <*(<*0,0,0,0*> ^ <*0,0,0,1*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b1 . 2 = <*(<*0,0,0,0*> ^ <*0,0,1,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b1 . 3 = <*(<*0,0,0,0*> ^ <*0,1,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b1 . 4 = <*(<*0,0,0,0*> ^ <*1,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b1 . 5 = <*(<*0,0,0,1*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b1 . 6 = <*(<*0,0,1,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b1 . 7 = <*(<*0,1,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b1 . 8 = <*(<*1,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b1 . 9 = <*(<*0,0,0,1*> ^ <*1,0,1,1*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b1 . 10 = <*(<*0,0,1,1*> ^ <*0,1,1,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> ) );

definition
let SBT be Permutation of ();
let m, i be Nat;
let w be Element of 4 -tuples_on ();
assume AS: ( ( m = 4 or m = 6 or m = 8 ) & i < 4 * (7 + m) & m <= i ) ;
func KeyExTemp (SBT,m,i,w) -> Element of 4 -tuples_on () means :: AESCIP_1:def 11
ex T3 being Element of 4 -tuples_on () st
( T3 = Rcon . (i / m) & it = Op-WXOR ((SubWord (SBT,())),T3) ) if i mod m = 0
it = SubWord (SBT,w) if ( m = 8 & i mod 8 = 4 )
otherwise it = w;
existence
( ( i mod m = 0 implies ex b1, T3 being Element of 4 -tuples_on () st
( T3 = Rcon . (i / m) & b1 = Op-WXOR ((SubWord (SBT,())),T3) ) ) & ( m = 8 & i mod 8 = 4 implies ex b1 being Element of 4 -tuples_on () st b1 = SubWord (SBT,w) ) & ( not i mod m = 0 & ( not m = 8 or not i mod 8 = 4 ) implies ex b1 being Element of 4 -tuples_on () st b1 = w ) )
proof end;
uniqueness
for b1, b2 being Element of 4 -tuples_on () holds
( ( i mod m = 0 & ex T3 being Element of 4 -tuples_on () st
( T3 = Rcon . (i / m) & b1 = Op-WXOR ((SubWord (SBT,())),T3) ) & ex T3 being Element of 4 -tuples_on () st
( T3 = Rcon . (i / m) & b2 = Op-WXOR ((SubWord (SBT,())),T3) ) implies b1 = b2 ) & ( m = 8 & i mod 8 = 4 & b1 = SubWord (SBT,w) & b2 = SubWord (SBT,w) implies b1 = b2 ) & ( not i mod m = 0 & ( not m = 8 or not i mod 8 = 4 ) & b1 = w & b2 = w implies b1 = b2 ) )
;
consistency
for b1 being Element of 4 -tuples_on () st i mod m = 0 & m = 8 & i mod 8 = 4 holds
( ex T3 being Element of 4 -tuples_on () st
( T3 = Rcon . (i / m) & b1 = Op-WXOR ((SubWord (SBT,())),T3) ) iff b1 = SubWord (SBT,w) )
;
end;

:: deftheorem defines KeyExTemp AESCIP_1:def 11 :
for SBT being Permutation of ()
for m, i being Nat
for w being Element of 4 -tuples_on () st ( m = 4 or m = 6 or m = 8 ) & i < 4 * (7 + m) & m <= i holds
for b5 being Element of 4 -tuples_on () holds
( ( i mod m = 0 implies ( b5 = KeyExTemp (SBT,m,i,w) iff ex T3 being Element of 4 -tuples_on () st
( T3 = Rcon . (i / m) & b5 = Op-WXOR ((SubWord (SBT,())),T3) ) ) ) & ( m = 8 & i mod 8 = 4 implies ( b5 = KeyExTemp (SBT,m,i,w) iff b5 = SubWord (SBT,w) ) ) & ( not i mod m = 0 & ( not m = 8 or not i mod 8 = 4 ) implies ( b5 = KeyExTemp (SBT,m,i,w) iff b5 = w ) ) );

definition
let SBT be Permutation of ();
let m be Nat;
assume AS: ( m = 4 or m = 6 or m = 8 ) ;
func KeyExpansionX (SBT,m) -> Function of (m -tuples_on ()),((4 * (7 + m)) -tuples_on ()) means :: AESCIP_1:def 12
for Key being Element of m -tuples_on () holds
( ( for i being Element of NAT st i < m holds
(it . Key) . (i + 1) = Key . (i + 1) ) & ( for i being Element of NAT st m <= i & i < 4 * (7 + m) holds
ex P, Q being Element of 4 -tuples_on () st
( P = (it . Key) . ((i - m) + 1) & Q = (it . Key) . i & (it . Key) . (i + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,i,Q))) ) ) );
existence
ex b1 being Function of (m -tuples_on ()),((4 * (7 + m)) -tuples_on ()) st
for Key being Element of m -tuples_on () holds
( ( for i being Element of NAT st i < m holds
(b1 . Key) . (i + 1) = Key . (i + 1) ) & ( for i being Element of NAT st m <= i & i < 4 * (7 + m) holds
ex P, Q being Element of 4 -tuples_on () st
( P = (b1 . Key) . ((i - m) + 1) & Q = (b1 . Key) . i & (b1 . Key) . (i + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,i,Q))) ) ) )
proof end;
uniqueness
for b1, b2 being Function of (m -tuples_on ()),((4 * (7 + m)) -tuples_on ()) st ( for Key being Element of m -tuples_on () holds
( ( for i being Element of NAT st i < m holds
(b1 . Key) . (i + 1) = Key . (i + 1) ) & ( for i being Element of NAT st m <= i & i < 4 * (7 + m) holds
ex P, Q being Element of 4 -tuples_on () st
( P = (b1 . Key) . ((i - m) + 1) & Q = (b1 . Key) . i & (b1 . Key) . (i + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,i,Q))) ) ) ) ) & ( for Key being Element of m -tuples_on () holds
( ( for i being Element of NAT st i < m holds
(b2 . Key) . (i + 1) = Key . (i + 1) ) & ( for i being Element of NAT st m <= i & i < 4 * (7 + m) holds
ex P, Q being Element of 4 -tuples_on () st
( P = (b2 . Key) . ((i - m) + 1) & Q = (b2 . Key) . i & (b2 . Key) . (i + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,i,Q))) ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines KeyExpansionX AESCIP_1:def 12 :
for SBT being Permutation of ()
for m being Nat st ( m = 4 or m = 6 or m = 8 ) holds
for b3 being Function of (m -tuples_on ()),((4 * (7 + m)) -tuples_on ()) holds
( b3 = KeyExpansionX (SBT,m) iff for Key being Element of m -tuples_on () holds
( ( for i being Element of NAT st i < m holds
(b3 . Key) . (i + 1) = Key . (i + 1) ) & ( for i being Element of NAT st m <= i & i < 4 * (7 + m) holds
ex P, Q being Element of 4 -tuples_on () st
( P = (b3 . Key) . ((i - m) + 1) & Q = (b3 . Key) . i & (b3 . Key) . (i + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,i,Q))) ) ) ) );

definition
let SBT be Permutation of ();
let m be Nat;
func KeyExpansion (SBT,m) -> Function of (m -tuples_on ()),((7 + m) -tuples_on (4 -tuples_on ())) means :: AESCIP_1:def 13
for Key being Element of m -tuples_on () ex w being Element of (4 * (7 + m)) -tuples_on () st
( w = (KeyExpansionX (SBT,m)) . Key & ( for i being Nat st i < 7 + m holds
(it . Key) . (i + 1) = <*(w . ((4 * i) + 1)),(w . ((4 * i) + 2)),(w . ((4 * i) + 3)),(w . ((4 * i) + 4))*> ) );
existence
ex b1 being Function of (m -tuples_on ()),((7 + m) -tuples_on (4 -tuples_on ())) st
for Key being Element of m -tuples_on () ex w being Element of (4 * (7 + m)) -tuples_on () st
( w = (KeyExpansionX (SBT,m)) . Key & ( for i being Nat st i < 7 + m holds
(b1 . Key) . (i + 1) = <*(w . ((4 * i) + 1)),(w . ((4 * i) + 2)),(w . ((4 * i) + 3)),(w . ((4 * i) + 4))*> ) )
proof end;
uniqueness
for b1, b2 being Function of (m -tuples_on ()),((7 + m) -tuples_on (4 -tuples_on ())) st ( for Key being Element of m -tuples_on () ex w being Element of (4 * (7 + m)) -tuples_on () st
( w = (KeyExpansionX (SBT,m)) . Key & ( for i being Nat st i < 7 + m holds
(b1 . Key) . (i + 1) = <*(w . ((4 * i) + 1)),(w . ((4 * i) + 2)),(w . ((4 * i) + 3)),(w . ((4 * i) + 4))*> ) ) ) & ( for Key being Element of m -tuples_on () ex w being Element of (4 * (7 + m)) -tuples_on () st
( w = (KeyExpansionX (SBT,m)) . Key & ( for i being Nat st i < 7 + m holds
(b2 . Key) . (i + 1) = <*(w . ((4 * i) + 1)),(w . ((4 * i) + 2)),(w . ((4 * i) + 3)),(w . ((4 * i) + 4))*> ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines KeyExpansion AESCIP_1:def 13 :
for SBT being Permutation of ()
for m being Nat
for b3 being Function of (m -tuples_on ()),((7 + m) -tuples_on (4 -tuples_on ())) holds
( b3 = KeyExpansion (SBT,m) iff for Key being Element of m -tuples_on () ex w being Element of (4 * (7 + m)) -tuples_on () st
( w = (KeyExpansionX (SBT,m)) . Key & ( for i being Nat st i < 7 + m holds
(b3 . Key) . (i + 1) = <*(w . ((4 * i) + 1)),(w . ((4 * i) + 2)),(w . ((4 * i) + 3)),(w . ((4 * i) + 4))*> ) ) );

definition
let SBT be Permutation of ();
let MCFunc be Permutation of (4 -tuples_on ());
let m be Nat;
let text be Element of 4 -tuples_on ();
let Key be Element of m -tuples_on ();
func AES-ENC (SBT,MCFunc,text,Key) -> Element of 4 -tuples_on () means :defENC: :: AESCIP_1:def 14
ex seq being FinSequence of 4 -tuples_on () st
( len seq = (7 + m) - 1 & ex Keyi1 being Element of 4 -tuples_on () st
( Keyi1 = ((KeyExpansion (SBT,m)) . Key) . 1 & seq . 1 = AddRoundKey . (text,Keyi1) ) & ( for i being Nat st 1 <= i & i < (7 + m) - 1 holds
ex Keyi being Element of 4 -tuples_on () st
( Keyi = ((KeyExpansion (SBT,m)) . Key) . (i + 1) & seq . (i + 1) = AddRoundKey . ((((MCFunc * ShiftRows) * (SubBytes SBT)) . (seq . i)),Keyi) ) ) & ex KeyNr being Element of 4 -tuples_on () st
( KeyNr = ((KeyExpansion (SBT,m)) . Key) . (7 + m) & it = AddRoundKey . (((ShiftRows * (SubBytes SBT)) . (seq . ((7 + m) - 1))),KeyNr) ) );
existence
ex b1 being Element of 4 -tuples_on () ex seq being FinSequence of 4 -tuples_on () st
( len seq = (7 + m) - 1 & ex Keyi1 being Element of 4 -tuples_on () st
( Keyi1 = ((KeyExpansion (SBT,m)) . Key) . 1 & seq . 1 = AddRoundKey . (text,Keyi1) ) & ( for i being Nat st 1 <= i & i < (7 + m) - 1 holds
ex Keyi being Element of 4 -tuples_on () st
( Keyi = ((KeyExpansion (SBT,m)) . Key) . (i + 1) & seq . (i + 1) = AddRoundKey . ((((MCFunc * ShiftRows) * (SubBytes SBT)) . (seq . i)),Keyi) ) ) & ex KeyNr being Element of 4 -tuples_on () st
( KeyNr = ((KeyExpansion (SBT,m)) . Key) . (7 + m) & b1 = AddRoundKey . (((ShiftRows * (SubBytes SBT)) . (seq . ((7 + m) - 1))),KeyNr) ) )
proof end;
uniqueness
for b1, b2 being Element of 4 -tuples_on () st ex seq being FinSequence of 4 -tuples_on () st
( len seq = (7 + m) - 1 & ex Keyi1 being Element of 4 -tuples_on () st
( Keyi1 = ((KeyExpansion (SBT,m)) . Key) . 1 & seq . 1 = AddRoundKey . (text,Keyi1) ) & ( for i being Nat st 1 <= i & i < (7 + m) - 1 holds
ex Keyi being Element of 4 -tuples_on () st
( Keyi = ((KeyExpansion (SBT,m)) . Key) . (i + 1) & seq . (i + 1) = AddRoundKey . ((((MCFunc * ShiftRows) * (SubBytes SBT)) . (seq . i)),Keyi) ) ) & ex KeyNr being Element of 4 -tuples_on () st
( KeyNr = ((KeyExpansion (SBT,m)) . Key) . (7 + m) & b1 = AddRoundKey . (((ShiftRows * (SubBytes SBT)) . (seq . ((7 + m) - 1))),KeyNr) ) ) & ex seq being FinSequence of 4 -tuples_on () st
( len seq = (7 + m) - 1 & ex Keyi1 being Element of 4 -tuples_on () st
( Keyi1 = ((KeyExpansion (SBT,m)) . Key) . 1 & seq . 1 = AddRoundKey . (text,Keyi1) ) & ( for i being Nat st 1 <= i & i < (7 + m) - 1 holds
ex Keyi being Element of 4 -tuples_on () st
( Keyi = ((KeyExpansion (SBT,m)) . Key) . (i + 1) & seq . (i + 1) = AddRoundKey . ((((MCFunc * ShiftRows) * (SubBytes SBT)) . (seq . i)),Keyi) ) ) & ex KeyNr being Element of 4 -tuples_on () st
( KeyNr = ((KeyExpansion (SBT,m)) . Key) . (7 + m) & b2 = AddRoundKey . (((ShiftRows * (SubBytes SBT)) . (seq . ((7 + m) - 1))),KeyNr) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defENC defines AES-ENC AESCIP_1:def 14 :
for SBT being Permutation of ()
for MCFunc being Permutation of (4 -tuples_on ())
for m being Nat
for text being Element of 4 -tuples_on ()
for Key being Element of m -tuples_on ()
for b6 being Element of 4 -tuples_on () holds
( b6 = AES-ENC (SBT,MCFunc,text,Key) iff ex seq being FinSequence of 4 -tuples_on () st
( len seq = (7 + m) - 1 & ex Keyi1 being Element of 4 -tuples_on () st
( Keyi1 = ((KeyExpansion (SBT,m)) . Key) . 1 & seq . 1 = AddRoundKey . (text,Keyi1) ) & ( for i being Nat st 1 <= i & i < (7 + m) - 1 holds
ex Keyi being Element of 4 -tuples_on () st
( Keyi = ((KeyExpansion (SBT,m)) . Key) . (i + 1) & seq . (i + 1) = AddRoundKey . ((((MCFunc * ShiftRows) * (SubBytes SBT)) . (seq . i)),Keyi) ) ) & ex KeyNr being Element of 4 -tuples_on () st
( KeyNr = ((KeyExpansion (SBT,m)) . Key) . (7 + m) & b6 = AddRoundKey . (((ShiftRows * (SubBytes SBT)) . (seq . ((7 + m) - 1))),KeyNr) ) ) );

definition
let SBT be Permutation of ();
let MCFunc be Permutation of (4 -tuples_on ());
let m be Nat;
let text be Element of 4 -tuples_on ();
let Key be Element of m -tuples_on ();
func AES-DEC (SBT,MCFunc,text,Key) -> Element of 4 -tuples_on () means :defDEC: :: AESCIP_1:def 15
ex seq being FinSequence of 4 -tuples_on () st
( len seq = (7 + m) - 1 & ex Keyi1 being Element of 4 -tuples_on () st
( Keyi1 = (Rev ((KeyExpansion (SBT,m)) . Key)) . 1 & seq . 1 = ((InvSubBytes SBT) * InvShiftRows) . (AddRoundKey . (text,Keyi1)) ) & ( for i being Nat st 1 <= i & i < (7 + m) - 1 holds
ex Keyi being Element of 4 -tuples_on () st
( Keyi = (Rev ((KeyExpansion (SBT,m)) . Key)) . (i + 1) & seq . (i + 1) = (((InvSubBytes SBT) * InvShiftRows) * (MCFunc ")) . (AddRoundKey . ((seq . i),Keyi)) ) ) & ex KeyNr being Element of 4 -tuples_on () st
( KeyNr = (Rev ((KeyExpansion (SBT,m)) . Key)) . (7 + m) & it = AddRoundKey . ((seq . ((7 + m) - 1)),KeyNr) ) );
existence
ex b1 being Element of 4 -tuples_on () ex seq being FinSequence of 4 -tuples_on () st
( len seq = (7 + m) - 1 & ex Keyi1 being Element of 4 -tuples_on () st
( Keyi1 = (Rev ((KeyExpansion (SBT,m)) . Key)) . 1 & seq . 1 = ((InvSubBytes SBT) * InvShiftRows) . (AddRoundKey . (text,Keyi1)) ) & ( for i being Nat st 1 <= i & i < (7 + m) - 1 holds
ex Keyi being Element of 4 -tuples_on () st
( Keyi = (Rev ((KeyExpansion (SBT,m)) . Key)) . (i + 1) & seq . (i + 1) = (((InvSubBytes SBT) * InvShiftRows) * (MCFunc ")) . (AddRoundKey . ((seq . i),Keyi)) ) ) & ex KeyNr being Element of 4 -tuples_on () st
( KeyNr = (Rev ((KeyExpansion (SBT,m)) . Key)) . (7 + m) & b1 = AddRoundKey . ((seq . ((7 + m) - 1)),KeyNr) ) )
proof end;
uniqueness
for b1, b2 being Element of 4 -tuples_on () st ex seq being FinSequence of 4 -tuples_on () st
( len seq = (7 + m) - 1 & ex Keyi1 being Element of 4 -tuples_on () st
( Keyi1 = (Rev ((KeyExpansion (SBT,m)) . Key)) . 1 & seq . 1 = ((InvSubBytes SBT) * InvShiftRows) . (AddRoundKey . (text,Keyi1)) ) & ( for i being Nat st 1 <= i & i < (7 + m) - 1 holds
ex Keyi being Element of 4 -tuples_on () st
( Keyi = (Rev ((KeyExpansion (SBT,m)) . Key)) . (i + 1) & seq . (i + 1) = (((InvSubBytes SBT) * InvShiftRows) * (MCFunc ")) . (AddRoundKey . ((seq . i),Keyi)) ) ) & ex KeyNr being Element of 4 -tuples_on () st
( KeyNr = (Rev ((KeyExpansion (SBT,m)) . Key)) . (7 + m) & b1 = AddRoundKey . ((seq . ((7 + m) - 1)),KeyNr) ) ) & ex seq being FinSequence of 4 -tuples_on () st
( len seq = (7 + m) - 1 & ex Keyi1 being Element of 4 -tuples_on () st
( Keyi1 = (Rev ((KeyExpansion (SBT,m)) . Key)) . 1 & seq . 1 = ((InvSubBytes SBT) * InvShiftRows) . (AddRoundKey . (text,Keyi1)) ) & ( for i being Nat st 1 <= i & i < (7 + m) - 1 holds
ex Keyi being Element of 4 -tuples_on () st
( Keyi = (Rev ((KeyExpansion (SBT,m)) . Key)) . (i + 1) & seq . (i + 1) = (((InvSubBytes SBT) * InvShiftRows) * (MCFunc ")) . (AddRoundKey . ((seq . i),Keyi)) ) ) & ex KeyNr being Element of 4 -tuples_on () st
( KeyNr = (Rev ((KeyExpansion (SBT,m)) . Key)) . (7 + m) & b2 = AddRoundKey . ((seq . ((7 + m) - 1)),KeyNr) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defDEC defines AES-DEC AESCIP_1:def 15 :
for SBT being Permutation of ()
for MCFunc being Permutation of (4 -tuples_on ())
for m being Nat
for text being Element of 4 -tuples_on ()
for Key being Element of m -tuples_on ()
for b6 being Element of 4 -tuples_on () holds
( b6 = AES-DEC (SBT,MCFunc,text,Key) iff ex seq being FinSequence of 4 -tuples_on () st
( len seq = (7 + m) - 1 & ex Keyi1 being Element of 4 -tuples_on () st
( Keyi1 = (Rev ((KeyExpansion (SBT,m)) . Key)) . 1 & seq . 1 = ((InvSubBytes SBT) * InvShiftRows) . (AddRoundKey . (text,Keyi1)) ) & ( for i being Nat st 1 <= i & i < (7 + m) - 1 holds
ex Keyi being Element of 4 -tuples_on () st
( Keyi = (Rev ((KeyExpansion (SBT,m)) . Key)) . (i + 1) & seq . (i + 1) = (((InvSubBytes SBT) * InvShiftRows) * (MCFunc ")) . (AddRoundKey . ((seq . i),Keyi)) ) ) & ex KeyNr being Element of 4 -tuples_on () st
( KeyNr = (Rev ((KeyExpansion (SBT,m)) . Key)) . (7 + m) & b6 = AddRoundKey . ((seq . ((7 + m) - 1)),KeyNr) ) ) );

theorem INV01: :: AESCIP_1:27
for MCFunc being Permutation of (4 -tuples_on ())
for input being Element of 4 -tuples_on () holds (MCFunc ") . (MCFunc . input) = input
proof end;

theorem :: AESCIP_1:28
for MCFunc being Permutation of (4 -tuples_on ())
for output being Element of 4 -tuples_on () holds MCFunc . ((MCFunc ") . output) = output
proof end;

theorem LAST01: :: AESCIP_1:29
for SBT being Permutation of ()
for m being Nat
for text being Element of 4 -tuples_on () holds ((InvSubBytes SBT) * InvShiftRows) . ((ShiftRows * (SubBytes SBT)) . text) = text
proof end;

theorem LAST02: :: AESCIP_1:30
for SBT being Permutation of ()
for MCFunc being Permutation of (4 -tuples_on ())
for m being Nat
for text being Element of 4 -tuples_on () holds (((InvSubBytes SBT) * InvShiftRows) * (MCFunc ")) . (((MCFunc * ShiftRows) * (SubBytes SBT)) . text) = text
proof end;

theorem LAST03: :: AESCIP_1:31
for SBT being Permutation of ()
for m being Nat
for text being Element of 4 -tuples_on ()
for Key being Element of m -tuples_on ()
for dkeyi, ekeyi being Element of 4 -tuples_on () st ( m = 4 or m = 6 or m = 8 ) & dkeyi = (Rev ((KeyExpansion (SBT,m)) . Key)) . 1 & ekeyi = ((KeyExpansion (SBT,m)) . Key) . (7 + m) holds
proof end;

LAST04: for SBT being Permutation of ()
for m being Nat
for text, otext being Element of 4 -tuples_on ()
for Key being Element of m -tuples_on ()
for Keyi1, KeyNr being Element of 4 -tuples_on () st ( m = 4 or m = 6 or m = 8 ) & Keyi1 = (Rev ((KeyExpansion (SBT,m)) . Key)) . 1 & KeyNr = ((KeyExpansion (SBT,m)) . Key) . (7 + m) & otext = AddRoundKey . (((ShiftRows * (SubBytes SBT)) . text),KeyNr) holds
((InvSubBytes SBT) * InvShiftRows) . (AddRoundKey . (otext,Keyi1)) = text

proof end;

theorem LAST05: :: AESCIP_1:32
for SBT being Permutation of ()
for m being Nat
for text being Element of 4 -tuples_on ()
for key being Element of m -tuples_on ()
for dkeyi, ekeyi being Element of 4 -tuples_on () st ( m = 4 or m = 6 or m = 8 ) & dkeyi = ((KeyExpansion (SBT,m)) . key) . 1 & ekeyi = (Rev ((KeyExpansion (SBT,m)) . key)) . (7 + m) holds
proof end;

theorem :: AESCIP_1:33
for SBT being Permutation of ()
for m being Nat
for text, otext being Element of 4 -tuples_on ()
for Key being Element of m -tuples_on ()
for Keyi1, KeyNr being Element of 4 -tuples_on () st ( m = 4 or m = 6 or m = 8 ) & Keyi1 = ((KeyExpansion (SBT,m)) . Key) . 1 & KeyNr = (Rev ((KeyExpansion (SBT,m)) . Key)) . (7 + m) & otext = AddRoundKey . (((ShiftRows * (SubBytes SBT)) . text),KeyNr) holds
((InvSubBytes SBT) * InvShiftRows) . (AddRoundKey . (otext,Keyi1)) = text
proof end;

theorem LAST08: :: AESCIP_1:34
for SBT being Permutation of ()
for m, i being Nat
for text being Element of 4 -tuples_on ()
for Key being Element of m -tuples_on ()
for eKeyi, dKeyi being Element of 4 -tuples_on () st ( m = 4 or m = 6 or m = 8 ) & i <= (7 + m) - 1 & eKeyi = ((KeyExpansion (SBT,m)) . Key) . ((7 + m) - i) & dKeyi = (Rev ((KeyExpansion (SBT,m)) . Key)) . (i + 1) holds
proof end;

LAST07: for SBT being Permutation of ()
for m being Nat
for text being Element of 4 -tuples_on ()
for Key being Element of m -tuples_on ()
for eKeyi, dKeyi being Element of 4 -tuples_on () st ( m = 4 or m = 6 or m = 8 ) & eKeyi = ((KeyExpansion (SBT,m)) . Key) . 1 & dKeyi = (Rev ((KeyExpansion (SBT,m)) . Key)) . (7 + m) holds

proof end;

theorem LASTXX: :: AESCIP_1:35
for SBT being Permutation of ()
for MCFunc being Permutation of (4 -tuples_on ())
for m being Nat
for text being Element of 4 -tuples_on ()
for Key being Element of m -tuples_on () st ( m = 4 or m = 6 or m = 8 ) holds
AES-DEC (SBT,MCFunc,(AES-ENC (SBT,MCFunc,text,Key)),Key) = text
proof end;

theorem LR8D1: :: AESCIP_1:36
for D being non empty set
for n, m being non zero Element of NAT
for r being Element of n -tuples_on D st m <= n & 8 <= n - m holds
Op-Left ((Op-Right (r,m)),8) is Element of 8 -tuples_on D
proof end;

Lm1: for D being non empty set
for n being non zero Element of NAT
for r being Element of n -tuples_on D st 8 <= n & 8 <= n - 8 & 16 <= n & 8 <= n - 16 & 24 <= n & 8 <= n - 24 holds
<*(Op-Left (r,8)),(Op-Left ((Op-Right (r,8)),8)),(Op-Left ((Op-Right (r,16)),8)),(Op-Left ((Op-Right (r,24)),8))*> is Element of 4 -tuples_on ()

proof end;

Lm2: for D being non empty set
for n, m, l, p, q being non zero Element of NAT
for r being Element of n -tuples_on D st m <= n & 8 <= n - m & l = m + 8 & l <= n & 8 <= n - l & p = m + 16 & p <= n & 8 <= n - p & q = m + 24 & q <= n & 8 <= n - q holds
<*(Op-Left ((Op-Right (r,m)),8)),(Op-Left ((Op-Right (r,l)),8)),(Op-Left ((Op-Right (r,p)),8)),(Op-Left ((Op-Right (r,q)),8))*> is Element of 4 -tuples_on ()

proof end;

Lm3: for D being non empty set
for n, m, l, p, q being non zero Element of NAT
for r being Element of n -tuples_on D st m <= n & 8 <= n - m & l = m + 8 & l <= n & 8 <= n - l & p = m + 16 & p <= n & 8 <= n - p & q = m + 24 & q <= n & 8 = n - q holds
<*(Op-Left ((Op-Right (r,m)),8)),(Op-Left ((Op-Right (r,l)),8)),(Op-Left ((Op-Right (r,p)),8)),(Op-Right (r,q))*> is Element of 4 -tuples_on ()

proof end;

definition
let r be Element of 128 -tuples_on BOOLEAN;
func AES-KeyInitState128 r -> Element of 4 -tuples_on () means :: AESCIP_1:def 16
( it . 1 = <*(Op-Left (r,8)),(Op-Left ((Op-Right (r,8)),8)),(Op-Left ((Op-Right (r,16)),8)),(Op-Left ((Op-Right (r,24)),8))*> & it . 2 = <*(Op-Left ((Op-Right (r,32)),8)),(Op-Left ((Op-Right (r,40)),8)),(Op-Left ((Op-Right (r,48)),8)),(Op-Left ((Op-Right (r,56)),8))*> & it . 3 = <*(Op-Left ((Op-Right (r,64)),8)),(Op-Left ((Op-Right (r,72)),8)),(Op-Left ((Op-Right (r,80)),8)),(Op-Left ((Op-Right (r,88)),8))*> & it . 4 = <*(Op-Left ((Op-Right (r,96)),8)),(Op-Left ((Op-Right (r,104)),8)),(Op-Left ((Op-Right (r,112)),8)),(Op-Right (r,120))*> );
existence
ex b1 being Element of 4 -tuples_on () st
( b1 . 1 = <*(Op-Left (r,8)),(Op-Left ((Op-Right (r,8)),8)),(Op-Left ((Op-Right (r,16)),8)),(Op-Left ((Op-Right (r,24)),8))*> & b1 . 2 = <*(Op-Left ((Op-Right (r,32)),8)),(Op-Left ((Op-Right (r,40)),8)),(Op-Left ((Op-Right (r,48)),8)),(Op-Left ((Op-Right (r,56)),8))*> & b1 . 3 = <*(Op-Left ((Op-Right (r,64)),8)),(Op-Left ((Op-Right (r,72)),8)),(Op-Left ((Op-Right (r,80)),8)),(Op-Left ((Op-Right (r,88)),8))*> & b1 . 4 = <*(Op-Left ((Op-Right (r,96)),8)),(Op-Left ((Op-Right (r,104)),8)),(Op-Left ((Op-Right (r,112)),8)),(Op-Right (r,120))*> )
proof end;
uniqueness
for b1, b2 being Element of 4 -tuples_on () st b1 . 1 = <*(Op-Left (r,8)),(Op-Left ((Op-Right (r,8)),8)),(Op-Left ((Op-Right (r,16)),8)),(Op-Left ((Op-Right (r,24)),8))*> & b1 . 2 = <*(Op-Left ((Op-Right (r,32)),8)),(Op-Left ((Op-Right (r,40)),8)),(Op-Left ((Op-Right (r,48)),8)),(Op-Left ((Op-Right (r,56)),8))*> & b1 . 3 = <*(Op-Left ((Op-Right (r,64)),8)),(Op-Left ((Op-Right (r,72)),8)),(Op-Left ((Op-Right (r,80)),8)),(Op-Left ((Op-Right (r,88)),8))*> & b1 . 4 = <*(Op-Left ((Op-Right (r,96)),8)),(Op-Left ((Op-Right (r,104)),8)),(Op-Left ((Op-Right (r,112)),8)),(Op-Right (r,120))*> & b2 . 1 = <*(Op-Left (r,8)),(Op-Left ((Op-Right (r,8)),8)),(Op-Left ((Op-Right (r,16)),8)),(Op-Left ((Op-Right (r,24)),8))*> & b2 . 2 = <*(Op-Left ((Op-Right (r,32)),8)),(Op-Left ((Op-Right (r,40)),8)),(Op-Left ((Op-Right (r,48)),8)),(Op-Left ((Op-Right (r,56)),8))*> & b2 . 3 = <*(Op-Left ((Op-Right (r,64)),8)),(Op-Left ((Op-Right (r,72)),8)),(Op-Left ((Op-Right (r,80)),8)),(Op-Left ((Op-Right (r,88)),8))*> & b2 . 4 = <*(Op-Left ((Op-Right (r,96)),8)),(Op-Left ((Op-Right (r,104)),8)),(Op-Left ((Op-Right (r,112)),8)),(Op-Right (r,120))*> holds
b1 = b2
proof end;
end;

:: deftheorem defines AES-KeyInitState128 AESCIP_1:def 16 :
for r being Element of 128 -tuples_on BOOLEAN
for b2 being Element of 4 -tuples_on () holds
( b2 = AES-KeyInitState128 r iff ( b2 . 1 = <*(Op-Left (r,8)),(Op-Left ((Op-Right (r,8)),8)),(Op-Left ((Op-Right (r,16)),8)),(Op-Left ((Op-Right (r,24)),8))*> & b2 . 2 = <*(Op-Left ((Op-Right (r,32)),8)),(Op-Left ((Op-Right (r,40)),8)),(Op-Left ((Op-Right (r,48)),8)),(Op-Left ((Op-Right (r,56)),8))*> & b2 . 3 = <*(Op-Left ((Op-Right (r,64)),8)),(Op-Left ((Op-Right (r,72)),8)),(Op-Left ((Op-Right (r,80)),8)),(Op-Left ((Op-Right (r,88)),8))*> & b2 . 4 = <*(Op-Left ((Op-Right (r,96)),8)),(Op-Left ((Op-Right (r,104)),8)),(Op-Left ((Op-Right (r,112)),8)),(Op-Right (r,120))*> ) );

definition
let r be Element of 192 -tuples_on BOOLEAN;
func AES-KeyInitState192 r -> Element of 6 -tuples_on () means :: AESCIP_1:def 17
( it . 1 = <*(Op-Left (r,8)),(Op-Left ((Op-Right (r,8)),8)),(Op-Left ((Op-Right (r,16)),8)),(Op-Left ((Op-Right (r,24)),8))*> & it . 2 = <*(Op-Left ((Op-Right (r,32)),8)),(Op-Left ((Op-Right (r,40)),8)),(Op-Left ((Op-Right (r,48)),8)),(Op-Left ((Op-Right (r,56)),8))*> & it . 3 = <*(Op-Left ((Op-Right (r,64)),8)),(Op-Left ((Op-Right (r,72)),8)),(Op-Left ((Op-Right (r,80)),8)),(Op-Left ((Op-Right (r,88)),8))*> & it . 4 = <*(Op-Left ((Op-Right (r,96)),8)),(Op-Left ((Op-Right (r,104)),8)),(Op-Left ((Op-Right (r,112)),8)),(Op-Left ((Op-Right (r,120)),8))*> & it . 5 = <*(Op-Left ((Op-Right (r,128)),8)),(Op-Left ((Op-Right (r,136)),8)),(Op-Left ((Op-Right (r,144)),8)),(Op-Left ((Op-Right (r,152)),8))*> & it . 6 = <*(Op-Left ((Op-Right (r,160)),8)),(Op-Left ((Op-Right (r,168)),8)),(Op-Left ((Op-Right (r,176)),8)),(Op-Right (r,184))*> );
existence
ex b1 being Element of 6 -tuples_on () st
( b1 . 1 = <*(Op-Left (r,8)),(Op-Left ((Op-Right (r,8)),8)),(Op-Left ((Op-Right (r,16)),8)),(Op-Left ((Op-Right (r,24)),8))*> & b1 . 2 = <*(Op-Left ((Op-Right (r,32)),8)),(Op-Left ((Op-Right (r,40)),8)),(Op-Left ((Op-Right (r,48)),8)),(Op-Left ((Op-Right (r,56)),8))*> & b1 . 3 = <*(Op-Left ((Op-Right (r,64)),8)),(Op-Left ((Op-Right (r,72)),8)),(Op-Left ((Op-Right (r,80)),8)),(Op-Left ((Op-Right (r,88)),8))*> & b1 . 4 = <*(Op-Left ((Op-Right (r,96)),8)),(Op-Left ((Op-Right (r,104)),8)),(Op-Left ((Op-Right (r,112)),8)),(Op-Left ((Op-Right (r,120)),8))*> & b1 . 5 = <*(Op-Left ((Op-Right (r,128)),8)),(Op-Left ((Op-Right (r,136)),8)),(Op-Left ((Op-Right (r,144)),8)),(Op-Left ((Op-Right (r,152)),8))*> & b1 . 6 = <*(Op-Left ((Op-Right (r,160)),8)),(Op-Left ((Op-Right (r,168)),8)),(Op-Left ((Op-Right (r,176)),8)),(Op-Right (r,184))*> )
proof end;
uniqueness
for b1, b2 being Element of 6 -tuples_on () st b1 . 1 = <*(Op-Left (r,8)),(Op-Left ((Op-Right (r,8)),8)),(Op-Left ((Op-Right (r,16)),8)),(Op-Left ((Op-Right (r,24)),8))*> & b1 . 2 = <*(Op-Left ((Op-Right (r,32)),8)),(Op-Left ((Op-Right (r,40)),8)),(Op-Left ((Op-Right (r,48)),8)),(Op-Left ((Op-Right (r,56)),8))*> & b1 . 3 = <*(Op-Left ((Op-Right (r,64)),8)),(Op-Left ((Op-Right (r,72)),8)),(Op-Left ((Op-Right (r,80)),8)),(Op-Left ((Op-Right (r,88)),8))*> & b1 . 4 = <*(Op-Left ((Op-Right (r,96)),8)),(Op-Left ((Op-Right (r,104)),8)),(Op-Left ((Op-Right (r,112)),8)),(Op-Left ((Op-Right (r,120)),8))*> & b1 . 5 = <*(Op-Left ((Op-Right (r,128)),8)),(Op-Left ((Op-Right (r,136)),8)),(Op-Left ((Op-Right (r,144)),8)),(Op-Left ((Op-Right (r,152)),8))*> & b1 . 6 = <*(Op-Left ((Op-Right (r,160)),8)),(Op-Left ((Op-Right (r,168)),8)),(Op-Left ((Op-Right (r,176)),8)),(Op-Right (r,184))*> & b2 . 1 = <*(Op-Left (r,8)),(Op-Left ((Op-Right (r,8)),8)),(Op-Left ((Op-Right (r,16)),8)),(Op-Left ((Op-Right (r,24)),8))*> & b2 . 2 = <*(Op-Left ((Op-Right (r,32)),8)),(Op-Left ((Op-Right (r,40)),8)),(Op-Left ((Op-Right (r,48)),8)),(Op-Left ((Op-Right (r,56)),8))*> & b2 . 3 = <*(Op-Left ((Op-Right (r,64)),8)),(Op-Left ((Op-Right (r,72)),8)),(Op-Left ((Op-Right (r,80)),8)),(Op-Left ((Op-Right (r,88)),8))*> & b2 . 4 = <*(Op-Left ((Op-Right (r,96)),8)),(Op-Left ((Op-Right (r,104)),8)),(Op-Left ((Op-Right (r,112)),8)),(Op-Left ((Op-Right (r,120)),8))*> & b2 . 5 = <*(Op-Left ((Op-Right (r,128)),8)),(Op-Left ((Op-Right (r,136)),8)),(Op-Left ((Op-Right (r,144)),8)),(Op-Left ((Op-Right (r,152)),8))*> & b2 . 6 = <*(Op-Left ((Op-Right (r,160)),8)),(Op-Left ((Op-Right (r,168)),8)),(Op-Left ((Op-Right (r,176)),8)),(Op-Right (r,184))*> holds
b1 = b2
proof end;
end;

:: deftheorem defines AES-KeyInitState192 AESCIP_1:def 17 :
for r being Element of 192 -tuples_on BOOLEAN
for b2 being Element of 6 -tuples_on () holds
( b2 = AES-KeyInitState192 r iff ( b2 . 1 = <*(Op-Left (r,8)),(Op-Left ((Op-Right (r,8)),8)),(Op-Left ((Op-Right (r,16)),8)),(Op-Left ((Op-Right (r,24)),8))*> & b2 . 2 = <*(Op-Left ((Op-Right (r,32)),8)),(Op-Left ((Op-Right (r,40)),8)),(Op-Left ((Op-Right (r,48)),8)),(Op-Left ((Op-Right (r,56)),8))*> & b2 . 3 = <*(Op-Left ((Op-Right (r,64)),8)),(Op-Left ((Op-Right (r,72)),8)),(Op-Left ((Op-Right (r,80)),8)),(Op-Left ((Op-Right (r,88)),8))*> & b2 . 4 = <*(Op-Left ((Op-Right (r,96)),8)),(Op-Left ((Op-Right (r,104)),8)),(Op-Left ((Op-Right (r,112)),8)),(Op-Left ((Op-Right (r,120)),8))*> & b2 . 5 = <*(Op-Left ((Op-Right (r,128)),8)),(Op-Left ((Op-Right (r,136)),8)),(Op-Left ((Op-Right (r,144)),8)),(Op-Left ((Op-Right (r,152)),8))*> & b2 . 6 = <*(Op-Left ((Op-Right (r,160)),8)),(Op-Left ((Op-Right (r,168)),8)),(Op-Left ((Op-Right (r,176)),8)),(Op-Right (r,184))*> ) );

definition
let r be Element of 256 -tuples_on BOOLEAN;
func AES-KeyInitState256 r -> Element of 8 -tuples_on () means :: AESCIP_1:def 18
( it . 1 = <*(Op-Left (r,8)),(Op-Left ((Op-Right (r,8)),8)),(Op-Left ((Op-Right (r,16)),8)),(Op-Left ((Op-Right (r,24)),8))*> & it . 2 = <*(Op-Left ((Op-Right (r,32)),8)),(Op-Left ((Op-Right (r,40)),8)),(Op-Left ((Op-Right (r,48)),8)),(Op-Left ((Op-Right (r,56)),8))*> & it . 3 = <*(Op-Left ((Op-Right (r,64)),8)),(Op-Left ((Op-Right (r,72)),8)),(Op-Left ((Op-Right (r,80)),8)),(Op-Left ((Op-Right (r,88)),8))*> & it . 4 = <*(Op-Left ((Op-Right (r,96)),8)),(Op-Left ((Op-Right (r,104)),8)),(Op-Left ((Op-Right (r,112)),8)),(Op-Left ((Op-Right (r,120)),8))*> & it . 5 = <*(Op-Left ((Op-Right (r,128)),8)),(Op-Left ((Op-Right (r,136)),8)),(Op-Left ((Op-Right (r,144)),8)),(Op-Left ((Op-Right (r,152)),8))*> & it . 6 = <*(Op-Left ((Op-Right (r,160)),8)),(Op-Left ((Op-Right (r,168)),8)),(Op-Left ((Op-Right (r,176)),8)),(Op-Left ((Op-Right (r,184)),8))*> & it . 7 = <*(Op-Left ((Op-Right (r,192)),8)),(Op-Left ((Op-Right (r,200)),8)),(Op-Left ((Op-Right (r,208)),8)),(Op-Left ((Op-Right (r,216)),8))*> & it . 8 = <*(Op-Left ((Op-Right (r,224)),8)),(Op-Left ((Op-Right (r,232)),8)),(Op-Left ((Op-Right (r,240)),8)),(Op-Right (r,248))*> );
existence
ex b1 being Element of 8 -tuples_on () st
( b1 . 1 = <*(Op-Left (r,8)),(Op-Left ((Op-Right (r,8)),8)),(Op-Left ((Op-Right (r,16)),8)),(Op-Left ((Op-Right (r,24)),8))*> & b1 . 2 = <*(Op-Left ((Op-Right (r,32)),8)),(Op-Left ((Op-Right (r,40)),8)),(Op-Left ((Op-Right (r,48)),8)),(Op-Left ((Op-Right (r,56)),8))*> & b1 . 3 = <*(Op-Left ((Op-Right (r,64)),8)),(Op-Left ((Op-Right (r,72)),8)),(Op-Left ((Op-Right (r,80)),8)),(Op-Left ((Op-Right (r,88)),8))*> & b1 . 4 = <*(Op-Left ((Op-Right (r,96)),8)),(Op-Left ((Op-Right (r,104)),8)),(Op-Left ((Op-Right (r,112)),8)),(Op-Left ((Op-Right (r,120)),8))*> & b1 . 5 = <*(Op-Left ((Op-Right (r,128)),8)),(Op-Left ((Op-Right (r,136)),8)),(Op-Left ((Op-Right (r,144)),8)),(Op-Left ((Op-Right (r,152)),8))*> & b1 . 6 = <*(Op-Left ((Op-Right (r,160)),8)),(Op-Left ((Op-Right (r,168)),8)),(Op-Left ((Op-Right (r,176)),8)),(Op-Left ((Op-Right (r,184)),8))*> & b1 . 7 = <*(Op-Left ((Op-Right (r,192)),8)),(Op-Left ((Op-Right (r,200)),8)),(Op-Left ((Op-Right (r,208)),8)),(Op-Left ((Op-Right (r,216)),8))*> & b1 . 8 = <*(Op-Left ((Op-Right (r,224)),8)),(Op-Left ((Op-Right (r,232)),8)),(Op-Left ((Op-Right (r,240)),8)),(Op-Right (r,248))*> )
proof end;
uniqueness
for b1, b2 being Element of 8 -tuples_on () st b1 . 1 = <*(Op-Left (r,8)),(Op-Left ((Op-Right (r,8)),8)),(Op-Left ((Op-Right (r,16)),8)),(Op-Left ((Op-Right (r,24)),8))*> & b1 . 2 = <*(Op-Left ((Op-Right (r,32)),8)),(Op-Left ((Op-Right (r,40)),8)),(Op-Left ((Op-Right (r,48)),8)),(Op-Left ((Op-Right (r,56)),8))*> & b1 . 3 = <*(Op-Left ((Op-Right (r,64)),8)),(Op-Left ((Op-Right (r,72)),8)),(Op-Left ((Op-Right (r,80)),8)),(Op-Left ((Op-Right (r,88)),8))*> & b1 . 4 = <*(Op-Left ((Op-Right (r,96)),8)),(Op-Left ((Op-Right (r,104)),8)),(Op-Left ((Op-Right (r,112)),8)),(Op-Left ((Op-Right (r,120)),8))*> & b1 . 5 = <*(Op-Left ((Op-Right (r,128)),8)),(Op-Left ((Op-Right (r,136)),8)),(Op-Left ((Op-Right (r,144)),8)),(Op-Left ((Op-Right (r,152)),8))*> & b1 . 6 = <*(Op-Left ((Op-Right (r,160)),8)),(Op-Left ((Op-Right (r,168)),8)),(Op-Left ((Op-Right (r,176)),8)),(Op-Left ((Op-Right (r,184)),8))*> & b1 . 7 = <*(Op-Left ((Op-Right (r,192)),8)),(Op-Left ((Op-Right (r,200)),8)),(Op-Left ((Op-Right (r,208)),8)),(Op-Left ((Op-Right (r,216)),8))*> & b1 . 8 = <*(Op-Left ((Op-Right (r,224)),8)),(Op-Left ((Op-Right (r,232)),8)),(Op-Left ((Op-Right (r,240)),8)),(Op-Right (r,248))*> & b2 . 1 = <*(Op-Left (r,8)),(Op-Left ((Op-Right (r,8)),8)),(Op-Left ((Op-Right (r,16)),8)),(Op-Left ((Op-Right (r,24)),8))*> & b2 . 2 = <*(Op-Left ((Op-Right (r,32)),8)),(Op-Left ((Op-Right (r,40)),8)),(Op-Left ((Op-Right (r,48)),8)),(Op-Left ((Op-Right (r,56)),8))*> & b2 . 3 = <*(Op-Left ((Op-Right (r,64)),8)),(Op-Left ((Op-Right (r,72)),8)),(Op-Left ((Op-Right (r,80)),8)),(Op-Left ((Op-Right (r,88)),8))*> & b2 . 4 = <*(Op-Left ((Op-Right (r,96)),8)),(Op-Left ((Op-Right (r,104)),8)),(Op-Left ((Op-Right (r,112)),8)),(Op-Left ((Op-Right (r,120)),8))*> & b2 . 5 = <*(Op-Left ((Op-Right (r,128)),8)),(Op-Left ((Op-Right (r,136)),8)),(Op-Left ((Op-Right (r,144)),8)),(Op-Left ((Op-Right (r,152)),8))*> & b2 . 6 = <*(Op-Left ((Op-Right (r,160)),8)),(Op-Left ((Op-Right (r,168)),8)),(Op-Left ((Op-Right (r,176)),8)),(Op-Left ((Op-Right (r,184)),8))*> & b2 . 7 = <*(Op-Left ((Op-Right (r,192)),8)),(Op-Left ((Op-Right (r,200)),8)),(Op-Left ((Op-Right (r,208)),8)),(Op-Left ((Op-Right (r,216)),8))*> & b2 . 8 = <*(Op-Left ((Op-Right (r,224)),8)),(Op-Left ((Op-Right (r,232)),8)),(Op-Left ((Op-Right (r,240)),8)),(Op-Right (r,248))*> holds
b1 = b2
proof end;
end;

:: deftheorem defines AES-KeyInitState256 AESCIP_1:def 18 :
for r being Element of 256 -tuples_on BOOLEAN
for b2 being Element of 8 -tuples_on () holds
( b2 = AES-KeyInitState256 r iff ( b2 . 1 = <*(Op-Left (r,8)),(Op-Left ((Op-Right (r,8)),8)),(Op-Left ((Op-Right (r,16)),8)),(Op-Left ((Op-Right (r,24)),8))*> & b2 . 2 = <*(Op-Left ((Op-Right (r,32)),8)),(Op-Left ((Op-Right (r,40)),8)),(Op-Left ((Op-Right (r,48)),8)),(Op-Left ((Op-Right (r,56)),8))*> & b2 . 3 = <*(Op-Left ((Op-Right (r,64)),8)),(Op-Left ((Op-Right (r,72)),8)),(Op-Left ((Op-Right (r,80)),8)),(Op-Left ((Op-Right (r,88)),8))*> & b2 . 4 = <*(Op-Left ((Op-Right (r,96)),8)),(Op-Left ((Op-Right (r,104)),8)),(Op-Left ((Op-Right (r,112)),8)),(Op-Left ((Op-Right (r,120)),8))*> & b2 . 5 = <*(Op-Left ((Op-Right (r,128)),8)),(Op-Left ((Op-Right (r,136)),8)),(Op-Left ((Op-Right (r,144)),8)),(Op-Left ((Op-Right (r,152)),8))*> & b2 . 6 = <*(Op-Left ((Op-Right (r,160)),8)),(Op-Left ((Op-Right (r,168)),8)),(Op-Left ((Op-Right (r,176)),8)),(Op-Left ((Op-Right (r,184)),8))*> & b2 . 7 = <*(Op-Left ((Op-Right (r,192)),8)),(Op-Left ((Op-Right (r,200)),8)),(Op-Left ((Op-Right (r,208)),8)),(Op-Left ((Op-Right (r,216)),8))*> & b2 . 8 = <*(Op-Left ((Op-Right (r,224)),8)),(Op-Left ((Op-Right (r,232)),8)),(Op-Left ((Op-Right (r,240)),8)),(Op-Right (r,248))*> ) );

definition
let SBT be Permutation of ();
let MixColumns be Permutation of (4 -tuples_on ());
let message, Key be Element of 128 -tuples_on BOOLEAN;
func AES128-ENC (SBT,MixColumns,message,Key) -> Element of 128 -tuples_on BOOLEAN equals :: AESCIP_1:def 19
. (AES-ENC (SBT,MixColumns,(AES-Statearray . message),()));
correctness
coherence
. (AES-ENC (SBT,MixColumns,(AES-Statearray . message),())) is Element of 128 -tuples_on BOOLEAN
;
proof end;
end;

:: deftheorem defines AES128-ENC AESCIP_1:def 19 :
for SBT being Permutation of ()
for MixColumns being Permutation of (4 -tuples_on ())
for message, Key being Element of 128 -tuples_on BOOLEAN holds AES128-ENC (SBT,MixColumns,message,Key) = . (AES-ENC (SBT,MixColumns,(AES-Statearray . message),()));

definition
let SBT be Permutation of ();
let MixColumns be Permutation of (4 -tuples_on ());
let cipher, Key be Element of 128 -tuples_on BOOLEAN;
func AES128-DEC (SBT,MixColumns,cipher,Key) -> Element of 128 -tuples_on BOOLEAN equals :: AESCIP_1:def 20
. (AES-DEC (SBT,MixColumns,(AES-Statearray . cipher),()));
correctness
coherence
. (AES-DEC (SBT,MixColumns,(AES-Statearray . cipher),())) is Element of 128 -tuples_on BOOLEAN
;
proof end;
end;

:: deftheorem defines AES128-DEC AESCIP_1:def 20 :
for SBT being Permutation of ()
for MixColumns being Permutation of (4 -tuples_on ())
for cipher, Key being Element of 128 -tuples_on BOOLEAN holds AES128-DEC (SBT,MixColumns,cipher,Key) = . (AES-DEC (SBT,MixColumns,(AES-Statearray . cipher),()));

theorem :: AESCIP_1:37
for SBT being Permutation of ()
for MixColumns being Permutation of (4 -tuples_on ())
for message, Key being Element of 128 -tuples_on BOOLEAN holds AES128-DEC (SBT,MixColumns,(AES128-ENC (SBT,MixColumns,message,Key)),Key) = message
proof end;

definition
let SBT be Permutation of ();
let MixColumns be Permutation of (4 -tuples_on ());
let message be Element of 128 -tuples_on BOOLEAN;
let Key be Element of 192 -tuples_on BOOLEAN;
func AES192-ENC (SBT,MixColumns,message,Key) -> Element of 128 -tuples_on BOOLEAN equals :: AESCIP_1:def 21
. (AES-ENC (SBT,MixColumns,(AES-Statearray . message),()));
correctness
coherence
. (AES-ENC (SBT,MixColumns,(AES-Statearray . message),())) is Element of 128 -tuples_on BOOLEAN
;
proof end;
end;

:: deftheorem defines AES192-ENC AESCIP_1:def 21 :
for SBT being Permutation of ()
for MixColumns being Permutation of (4 -tuples_on ())
for message being Element of 128 -tuples_on BOOLEAN
for Key being Element of 192 -tuples_on BOOLEAN holds AES192-ENC (SBT,MixColumns,message,Key) = . (AES-ENC (SBT,MixColumns,(AES-Statearray . message),()));

definition
let SBT be Permutation of ();
let MixColumns be Permutation of (4 -tuples_on ());
let cipher be Element of 128 -tuples_on BOOLEAN;
let Key be Element of 192 -tuples_on BOOLEAN;
func AES192-DEC (SBT,MixColumns,cipher,Key) -> Element of 128 -tuples_on BOOLEAN equals :: AESCIP_1:def 22
. (AES-DEC (SBT,MixColumns,(AES-Statearray . cipher),()));
correctness
coherence
. (AES-DEC (SBT,MixColumns,(AES-Statearray . cipher),())) is Element of 128 -tuples_on BOOLEAN
;
proof end;
end;

:: deftheorem defines AES192-DEC AESCIP_1:def 22 :
for SBT being Permutation of ()
for MixColumns being Permutation of (4 -tuples_on ())
for cipher being Element of 128 -tuples_on BOOLEAN
for Key being Element of 192 -tuples_on BOOLEAN holds AES192-DEC (SBT,MixColumns,cipher,Key) = . (AES-DEC (SBT,MixColumns,(AES-Statearray . cipher),()));

theorem :: AESCIP_1:38
for SBT being Permutation of ()
for MixColumns being Permutation of (4 -tuples_on ())
for message being Element of 128 -tuples_on BOOLEAN
for Key being Element of 192 -tuples_on BOOLEAN holds AES192-DEC (SBT,MixColumns,(AES192-ENC (SBT,MixColumns,message,Key)),Key) = message
proof end;

definition
let SBT be Permutation of ();
let MixColumns be Permutation of (4 -tuples_on ());
let message be Element of 128 -tuples_on BOOLEAN;
let Key be Element of 256 -tuples_on BOOLEAN;
func AES256-ENC (SBT,MixColumns,message,Key) -> Element of 128 -tuples_on BOOLEAN equals :: AESCIP_1:def 23
. (AES-ENC (SBT,MixColumns,(AES-Statearray . message),()));
correctness
coherence
. (AES-ENC (SBT,MixColumns,(AES-Statearray . message),())) is Element of 128 -tuples_on BOOLEAN
;
proof end;
end;

:: deftheorem defines AES256-ENC AESCIP_1:def 23 :
for SBT being Permutation of ()
for MixColumns being Permutation of (4 -tuples_on ())
for message being Element of 128 -tuples_on BOOLEAN
for Key being Element of 256 -tuples_on BOOLEAN holds AES256-ENC (SBT,MixColumns,message,Key) = . (AES-ENC (SBT,MixColumns,(AES-Statearray . message),()));

definition
let SBT be Permutation of ();
let MixColumns be Permutation of (4 -tuples_on ());
let cipher be Element of 128 -tuples_on BOOLEAN;
let Key be Element of 256 -tuples_on BOOLEAN;
func AES256-DEC (SBT,MixColumns,cipher,Key) -> Element of 128 -tuples_on BOOLEAN equals :: AESCIP_1:def 24
. (AES-DEC (SBT,MixColumns,(AES-Statearray . cipher),()));
correctness
coherence
. (AES-DEC (SBT,MixColumns,(AES-Statearray . cipher),())) is Element of 128 -tuples_on BOOLEAN
;
proof end;
end;

:: deftheorem defines AES256-DEC AESCIP_1:def 24 :
for SBT being Permutation of ()
for MixColumns being Permutation of (4 -tuples_on ())
for cipher being Element of 128 -tuples_on BOOLEAN
for Key being Element of 256 -tuples_on BOOLEAN holds AES256-DEC (SBT,MixColumns,cipher,Key) = . (AES-DEC (SBT,MixColumns,(AES-Statearray . cipher),()));

theorem :: AESCIP_1:39
for SBT being Permutation of ()
for MixColumns being Permutation of (4 -tuples_on ())
for message being Element of 128 -tuples_on BOOLEAN
for Key being Element of 256 -tuples_on BOOLEAN holds AES256-DEC (SBT,MixColumns,(AES256-ENC (SBT,MixColumns,message,Key)),Key) = message
proof end;