:: Formalization of the Advanced Encryption Standard -- Part {I}
:: by Kenichi Arai and Hiroyuki Okazaki
::
:: Received October 7, 2013
:: 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 (n -tuples_on D));
let x be Element of X;
:: original: .
redefine func F . x -> Element of m -tuples_on (n -tuples_on D);
coherence
F . x is Element of m -tuples_on (n -tuples_on D)

proof end;

end;

definition

let m be Nat;
let X, Y, D be non empty set ;
let F be Function of [:X,Y:],(m -tuples_on D);
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 (n -tuples_on D) 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 (8 -tuples_on D)

proof end;

theorem :: AESCIP_1:13

for D being non empty set
for x being Element of 4 -tuples_on (4 -tuples_on D)
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 (128 -tuples_on BOOLEAN),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) 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 b₁ being Function of (128 -tuples_on BOOLEAN),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) 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
((b₁ . input) . i) . j = mid (input,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7))

proof end;

uniqueness
for b₁, b₂ being Function of (128 -tuples_on BOOLEAN),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) 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
((b₁ . 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
((b₂ . input) . i) . j = mid (input,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefStatearray defines AES-Statearray AESCIP_1:def 1 :
for b₁ being Function of (128 -tuples_on BOOLEAN),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) holds
( b₁ = 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
((b₁ . 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

AES-Statearray is one-to-one

proof end;

theorem LMStat3: :: AESCIP_1:19

AES-Statearray is onto

proof end;

registration

cluster AES-Statearray -> bijective ;

correctness
coherence
AES-Statearray is bijective ;
by LMStat1, LMStat3;

end;

theorem LMINV1: :: AESCIP_1:20

for cipher being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds AES-Statearray . ((AES-Statearray ") . cipher) = cipher

proof end;

definition

let SBT be Permutation of (8 -tuples_on BOOLEAN);

func SubBytes SBT -> Function of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) means :DefSubBytes: :: AESCIP_1:def 2
for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
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 b₁ being Function of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) st
for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
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 & ((b₁ . input) . i) . j = SBT . inputij )

proof end;

uniqueness
for b₁, b₂ being Function of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) st ( for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
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 & ((b₁ . input) . i) . j = SBT . inputij ) ) & ( for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
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 & ((b₂ . input) . i) . j = SBT . inputij ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefSubBytes defines SubBytes AESCIP_1:def 2 :
for SBT being Permutation of (8 -tuples_on BOOLEAN)
for b₂ being Function of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) holds
( b₂ = SubBytes SBT iff for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
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 & ((b₂ . input) . i) . j = SBT . inputij ) );

definition

let SBT be Permutation of (8 -tuples_on BOOLEAN);

func InvSubBytes SBT -> Function of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) means :DefInvSubBytes: :: AESCIP_1:def 3
for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
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 b₁ being Function of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) st
for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
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 & ((b₁ . input) . i) . j = (SBT ") . inputij )

proof end;

uniqueness
for b₁, b₂ being Function of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) st ( for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
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 & ((b₁ . input) . i) . j = (SBT ") . inputij ) ) & ( for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
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 & ((b₂ . input) . i) . j = (SBT ") . inputij ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefInvSubBytes defines InvSubBytes AESCIP_1:def 3 :
for SBT being Permutation of (8 -tuples_on BOOLEAN)
for b₂ being Function of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) holds
( b₂ = InvSubBytes SBT iff for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
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 & ((b₂ . input) . i) . j = (SBT ") . inputij ) );

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

proof end;

INV08A: for SBT being Permutation of (8 -tuples_on BOOLEAN)
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 (8 -tuples_on BOOLEAN)
for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds (InvSubBytes SBT) . ((SubBytes SBT) . input) = input

proof end;

theorem INV08: :: AESCIP_1:22

for SBT being Permutation of (8 -tuples_on BOOLEAN)
for output being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds (SubBytes SBT) . ((InvSubBytes SBT) . output) = output

proof end;

theorem :: AESCIP_1:23

for SBT being Permutation of (8 -tuples_on BOOLEAN) 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 (8 -tuples_on BOOLEAN))),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) means :DefShiftRows: :: AESCIP_1:def 4
for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for i being Nat st i in Seg 4 holds
ex xi being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( xi = input . i & (it . input) . i = Op-Shift (xi,(5 - i)) );

existence
ex b₁ being Function of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) st
for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for i being Nat st i in Seg 4 holds
ex xi being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( xi = input . i & (b₁ . input) . i = Op-Shift (xi,(5 - i)) )

proof end;

uniqueness
for b₁, b₂ being Function of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) st ( for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for i being Nat st i in Seg 4 holds
ex xi being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( xi = input . i & (b₁ . input) . i = Op-Shift (xi,(5 - i)) ) ) & ( for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for i being Nat st i in Seg 4 holds
ex xi being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( xi = input . i & (b₂ . input) . i = Op-Shift (xi,(5 - i)) ) ) holds
b₁ = b₂

proof end;

end;

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

definition

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

existence
ex b₁ being Function of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) st
for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for i being Nat st i in Seg 4 holds
ex xi being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( xi = input . i & (b₁ . input) . i = Op-Shift (xi,(i - 1)) )

proof end;

uniqueness
for b₁, b₂ being Function of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) st ( for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for i being Nat st i in Seg 4 holds
ex xi being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( xi = input . i & (b₁ . input) . i = Op-Shift (xi,(i - 1)) ) ) & ( for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for i being Nat st i in Seg 4 holds
ex xi being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( xi = input . i & (b₂ . input) . i = Op-Shift (xi,(i - 1)) ) ) holds
b₁ = b₂

proof end;

end;

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

theorem INV04: :: AESCIP_1:24

for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds InvShiftRows . (ShiftRows . input) = input

proof end;

theorem INV05: :: AESCIP_1:25

for output being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds ShiftRows . (InvShiftRows . output) = output

proof end;

theorem :: AESCIP_1:26

( ShiftRows is one-to-one & ShiftRows is onto & InvShiftRows is one-to-one & InvShiftRows is onto & InvShiftRows = ShiftRows " & ShiftRows = InvShiftRows " ) by INV00, INV04, INV05;

definition

func AddRoundKey -> Function of [:(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))):],(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) means :DefAddRoundKey: :: AESCIP_1:def 6
for text, key being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
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 b₁ being Function of [:(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))):],(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) st
for text, key being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
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 & ((b₁ . (text,key)) . i) . j = Op-XOR (textij,keyij) )

proof end;

uniqueness
for b₁, b₂ being Function of [:(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))):],(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) st ( for text, key being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
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 & ((b₁ . (text,key)) . i) . j = Op-XOR (textij,keyij) ) ) & ( for text, key being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
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 & ((b₂ . (text,key)) . i) . j = Op-XOR (textij,keyij) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefAddRoundKey defines AddRoundKey AESCIP_1:def 6 :
for b₁ being Function of [:(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))):],(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) holds
( b₁ = AddRoundKey iff for text, key being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
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 & ((b₁ . (text,key)) . i) . j = Op-XOR (textij,keyij) ) );

definition

let SBT be Permutation of (8 -tuples_on BOOLEAN);
let x be Element of 4 -tuples_on (8 -tuples_on BOOLEAN);

func SubWord (SBT,x) -> Element of 4 -tuples_on (8 -tuples_on BOOLEAN) means :: AESCIP_1:def 7
for i being Element of Seg 4 holds it . i = SBT . (x . i);

existence
ex b₁ being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
for i being Element of Seg 4 holds b₁ . i = SBT . (x . i)

proof end;

uniqueness
for b₁, b₂ being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st ( for i being Element of Seg 4 holds b₁ . i = SBT . (x . i) ) & ( for i being Element of Seg 4 holds b₂ . i = SBT . (x . i) ) holds
b₁ = b₂

proof end;

end;

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

definition

let x be Element of 4 -tuples_on (8 -tuples_on BOOLEAN);

func RotWord x -> Element of 4 -tuples_on (8 -tuples_on BOOLEAN) equals :: AESCIP_1:def 8
Op-LeftShift x;

correctness
coherence
Op-LeftShift x is Element of 4 -tuples_on (8 -tuples_on BOOLEAN);
by DESCIP_1:6;

end;

:: deftheorem defines RotWord AESCIP_1:def 8 :
for x being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) 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 (n -tuples_on BOOLEAN);

func Op-WXOR (s,t) -> Element of m -tuples_on (n -tuples_on BOOLEAN) means :: AESCIP_1:def 9
for i being Element of Seg m holds it . i = Op-XOR ((s . i),(t . i));

existence
ex b₁ being Element of m -tuples_on (n -tuples_on BOOLEAN) st
for i being Element of Seg m holds b₁ . i = Op-XOR ((s . i),(t . i))

proof end;

uniqueness
for b₁, b₂ being Element of m -tuples_on (n -tuples_on BOOLEAN) st ( for i being Element of Seg m holds b₁ . i = Op-XOR ((s . i),(t . i)) ) & ( for i being Element of Seg m holds b₂ . i = Op-XOR ((s . i),(t . i)) ) holds
b₁ = b₂

proof end;

end;

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

definition

func Rcon -> Element of 10 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) 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 b₁ being Element of 10 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( b₁ . 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*>)*> & b₁ . 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*>)*> & b₁ . 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*>)*> & b₁ . 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*>)*> & b₁ . 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*>)*> & b₁ . 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*>)*> & b₁ . 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*>)*> & b₁ . 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*>)*> & b₁ . 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*>)*> & b₁ . 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 b₁, b₂ being Element of 10 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st b₁ . 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*>)*> & b₁ . 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*>)*> & b₁ . 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*>)*> & b₁ . 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*>)*> & b₁ . 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*>)*> & b₁ . 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*>)*> & b₁ . 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*>)*> & b₁ . 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*>)*> & b₁ . 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*>)*> & b₁ . 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*>)*> & b₂ . 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*>)*> & b₂ . 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*>)*> & b₂ . 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*>)*> & b₂ . 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*>)*> & b₂ . 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*>)*> & b₂ . 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*>)*> & b₂ . 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*>)*> & b₂ . 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*>)*> & b₂ . 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*>)*> & b₂ . 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
b₁ = b₂

proof end;

end;

:: deftheorem defines Rcon AESCIP_1:def 10 :
for b₁ being Element of 10 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds
( b₁ = Rcon iff ( b₁ . 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*>)*> & b₁ . 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*>)*> & b₁ . 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*>)*> & b₁ . 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*>)*> & b₁ . 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*>)*> & b₁ . 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*>)*> & b₁ . 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*>)*> & b₁ . 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*>)*> & b₁ . 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*>)*> & b₁ . 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 (8 -tuples_on BOOLEAN);
let m, i be Nat;
let w be Element of 4 -tuples_on (8 -tuples_on BOOLEAN);
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 (8 -tuples_on BOOLEAN) means :: AESCIP_1:def 11
ex T3 being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( T3 = Rcon . (i / m) & it = Op-WXOR ((SubWord (SBT,(RotWord w))),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 b₁, T3 being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( T3 = Rcon . (i / m) & b₁ = Op-WXOR ((SubWord (SBT,(RotWord w))),T3) ) ) & ( m = 8 & i mod 8 = 4 implies ex b₁ being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st b₁ = SubWord (SBT,w) ) & ( not i mod m = 0 & ( not m = 8 or not i mod 8 = 4 ) implies ex b₁ being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st b₁ = w ) )

proof end;

uniqueness
for b₁, b₂ being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) holds
( ( i mod m = 0 & ex T3 being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( T3 = Rcon . (i / m) & b₁ = Op-WXOR ((SubWord (SBT,(RotWord w))),T3) ) & ex T3 being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( T3 = Rcon . (i / m) & b₂ = Op-WXOR ((SubWord (SBT,(RotWord w))),T3) ) implies b₁ = b₂ ) & ( m = 8 & i mod 8 = 4 & b₁ = SubWord (SBT,w) & b₂ = SubWord (SBT,w) implies b₁ = b₂ ) & ( not i mod m = 0 & ( not m = 8 or not i mod 8 = 4 ) & b₁ = w & b₂ = w implies b₁ = b₂ ) ) ;
consistency
for b₁ being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st i mod m = 0 & m = 8 & i mod 8 = 4 holds
( ex T3 being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( T3 = Rcon . (i / m) & b₁ = Op-WXOR ((SubWord (SBT,(RotWord w))),T3) ) iff b₁ = SubWord (SBT,w) ) ;

end;

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

definition

let SBT be Permutation of (8 -tuples_on BOOLEAN);
let m be Nat;
assume AS: ( m = 4 or m = 6 or m = 8 ) ;

func KeyExpansionX (SBT,m) -> Function of (m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),((4 * (7 + m)) -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) means :: AESCIP_1:def 12
for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) 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 (8 -tuples_on BOOLEAN) 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 b₁ being Function of (m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),((4 * (7 + m)) -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) st
for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds
( ( for i being Element of NAT st i < m holds
(b₁ . 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 (8 -tuples_on BOOLEAN) st
( P = (b₁ . Key) . ((i - m) + 1) & Q = (b₁ . Key) . i & (b₁ . Key) . (i + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,i,Q))) ) ) )

proof end;

uniqueness
for b₁, b₂ being Function of (m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),((4 * (7 + m)) -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) st ( for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds
( ( for i being Element of NAT st i < m holds
(b₁ . 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 (8 -tuples_on BOOLEAN) st
( P = (b₁ . Key) . ((i - m) + 1) & Q = (b₁ . Key) . i & (b₁ . Key) . (i + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,i,Q))) ) ) ) ) & ( for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds
( ( for i being Element of NAT st i < m holds
(b₂ . 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 (8 -tuples_on BOOLEAN) st
( P = (b₂ . Key) . ((i - m) + 1) & Q = (b₂ . Key) . i & (b₂ . Key) . (i + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,i,Q))) ) ) ) ) holds
b₁ = b₂

proof end;

end;

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

definition

let SBT be Permutation of (8 -tuples_on BOOLEAN);
let m be Nat;

func KeyExpansion (SBT,m) -> Function of (m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),((7 + m) -tuples_on (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))) means :: AESCIP_1:def 13
for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ex w being Element of (4 * (7 + m)) -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) 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 b₁ being Function of (m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),((7 + m) -tuples_on (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))) st
for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ex w being Element of (4 * (7 + m)) -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( w = (KeyExpansionX (SBT,m)) . Key & ( for i being Nat st i < 7 + m holds
(b₁ . Key) . (i + 1) = <*(w . ((4 * i) + 1)),(w . ((4 * i) + 2)),(w . ((4 * i) + 3)),(w . ((4 * i) + 4))*> ) )

proof end;

uniqueness
for b₁, b₂ being Function of (m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),((7 + m) -tuples_on (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))) st ( for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ex w being Element of (4 * (7 + m)) -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( w = (KeyExpansionX (SBT,m)) . Key & ( for i being Nat st i < 7 + m holds
(b₁ . 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 (4 -tuples_on (8 -tuples_on BOOLEAN)) ex w being Element of (4 * (7 + m)) -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( w = (KeyExpansionX (SBT,m)) . Key & ( for i being Nat st i < 7 + m holds
(b₂ . Key) . (i + 1) = <*(w . ((4 * i) + 1)),(w . ((4 * i) + 2)),(w . ((4 * i) + 3)),(w . ((4 * i) + 4))*> ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines KeyExpansion AESCIP_1:def 13 :
for SBT being Permutation of (8 -tuples_on BOOLEAN)
for m being Nat
for b₃ being Function of (m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),((7 + m) -tuples_on (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))) holds
( b₃ = KeyExpansion (SBT,m) iff for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ex w being Element of (4 * (7 + m)) -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( w = (KeyExpansionX (SBT,m)) . Key & ( for i being Nat st i < 7 + m holds
(b₃ . 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 (8 -tuples_on BOOLEAN);
let MCFunc be Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)));
let m be Nat;
let text be Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN));
let Key be Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN));

func AES-ENC (SBT,MCFunc,text,Key) -> Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) means :defENC: :: AESCIP_1:def 14
ex seq being FinSequence of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( len seq = (7 + m) - 1 & ex Keyi1 being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) 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 (4 -tuples_on (8 -tuples_on BOOLEAN)) 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 (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( KeyNr = ((KeyExpansion (SBT,m)) . Key) . (7 + m) & it = AddRoundKey . (((ShiftRows * (SubBytes SBT)) . (seq . ((7 + m) - 1))),KeyNr) ) );

existence
ex b₁ being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ex seq being FinSequence of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( len seq = (7 + m) - 1 & ex Keyi1 being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) 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 (4 -tuples_on (8 -tuples_on BOOLEAN)) 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 (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( KeyNr = ((KeyExpansion (SBT,m)) . Key) . (7 + m) & b₁ = AddRoundKey . (((ShiftRows * (SubBytes SBT)) . (seq . ((7 + m) - 1))),KeyNr) ) )

proof end;

uniqueness
for b₁, b₂ being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st ex seq being FinSequence of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( len seq = (7 + m) - 1 & ex Keyi1 being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) 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 (4 -tuples_on (8 -tuples_on BOOLEAN)) 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 (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( KeyNr = ((KeyExpansion (SBT,m)) . Key) . (7 + m) & b₁ = AddRoundKey . (((ShiftRows * (SubBytes SBT)) . (seq . ((7 + m) - 1))),KeyNr) ) ) & ex seq being FinSequence of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( len seq = (7 + m) - 1 & ex Keyi1 being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) 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 (4 -tuples_on (8 -tuples_on BOOLEAN)) 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 (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( KeyNr = ((KeyExpansion (SBT,m)) . Key) . (7 + m) & b₂ = AddRoundKey . (((ShiftRows * (SubBytes SBT)) . (seq . ((7 + m) - 1))),KeyNr) ) ) holds
b₁ = b₂

proof end;

end;

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

definition

let SBT be Permutation of (8 -tuples_on BOOLEAN);
let MCFunc be Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)));
let m be Nat;
let text be Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN));
let Key be Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN));

func AES-DEC (SBT,MCFunc,text,Key) -> Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) means :defDEC: :: AESCIP_1:def 15
ex seq being FinSequence of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( len seq = (7 + m) - 1 & ex Keyi1 being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) 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 (4 -tuples_on (8 -tuples_on BOOLEAN)) 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 (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( KeyNr = (Rev ((KeyExpansion (SBT,m)) . Key)) . (7 + m) & it = AddRoundKey . ((seq . ((7 + m) - 1)),KeyNr) ) );

existence
ex b₁ being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ex seq being FinSequence of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( len seq = (7 + m) - 1 & ex Keyi1 being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) 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 (4 -tuples_on (8 -tuples_on BOOLEAN)) 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 (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( KeyNr = (Rev ((KeyExpansion (SBT,m)) . Key)) . (7 + m) & b₁ = AddRoundKey . ((seq . ((7 + m) - 1)),KeyNr) ) )

proof end;

uniqueness
for b₁, b₂ being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st ex seq being FinSequence of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( len seq = (7 + m) - 1 & ex Keyi1 being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) 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 (4 -tuples_on (8 -tuples_on BOOLEAN)) 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 (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( KeyNr = (Rev ((KeyExpansion (SBT,m)) . Key)) . (7 + m) & b₁ = AddRoundKey . ((seq . ((7 + m) - 1)),KeyNr) ) ) & ex seq being FinSequence of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( len seq = (7 + m) - 1 & ex Keyi1 being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) 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 (4 -tuples_on (8 -tuples_on BOOLEAN)) 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 (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( KeyNr = (Rev ((KeyExpansion (SBT,m)) . Key)) . (7 + m) & b₂ = AddRoundKey . ((seq . ((7 + m) - 1)),KeyNr) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defDEC defines AES-DEC AESCIP_1:def 15 :
for SBT being Permutation of (8 -tuples_on BOOLEAN)
for MCFunc being Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))
for m being Nat
for text being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for b₆ being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds
( b₆ = AES-DEC (SBT,MCFunc,text,Key) iff ex seq being FinSequence of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( len seq = (7 + m) - 1 & ex Keyi1 being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) 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 (4 -tuples_on (8 -tuples_on BOOLEAN)) 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 (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( KeyNr = (Rev ((KeyExpansion (SBT,m)) . Key)) . (7 + m) & b₆ = AddRoundKey . ((seq . ((7 + m) - 1)),KeyNr) ) ) );

theorem INV01: :: AESCIP_1:27

for MCFunc being Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))
for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds (MCFunc ") . (MCFunc . input) = input

proof end;

theorem :: AESCIP_1:28

for MCFunc being Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))
for output being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds MCFunc . ((MCFunc ") . output) = output

proof end;

theorem LAST01: :: AESCIP_1:29

for SBT being Permutation of (8 -tuples_on BOOLEAN)
for m being Nat
for text being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds ((InvSubBytes SBT) * InvShiftRows) . ((ShiftRows * (SubBytes SBT)) . text) = text

proof end;

theorem LAST02: :: AESCIP_1:30

for SBT being Permutation of (8 -tuples_on BOOLEAN)
for MCFunc being Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))
for m being Nat
for text being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds (((InvSubBytes SBT) * InvShiftRows) * (MCFunc ")) . (((MCFunc * ShiftRows) * (SubBytes SBT)) . text) = text

proof end;

theorem LAST03: :: AESCIP_1:31

for SBT being Permutation of (8 -tuples_on BOOLEAN)
for m being Nat
for text being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for dkeyi, ekeyi being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st ( m = 4 or m = 6 or m = 8 ) & dkeyi = (Rev ((KeyExpansion (SBT,m)) . Key)) . 1 & ekeyi = ((KeyExpansion (SBT,m)) . Key) . (7 + m) holds
AddRoundKey . ((AddRoundKey . (text,ekeyi)),dkeyi) = text

proof end;

LAST04: for SBT being Permutation of (8 -tuples_on BOOLEAN)
for m being Nat
for text, otext being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for Keyi1, KeyNr being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) 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 (8 -tuples_on BOOLEAN)
for m being Nat
for text being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for dkeyi, ekeyi being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st ( m = 4 or m = 6 or m = 8 ) & dkeyi = ((KeyExpansion (SBT,m)) . key) . 1 & ekeyi = (Rev ((KeyExpansion (SBT,m)) . key)) . (7 + m) holds
AddRoundKey . ((AddRoundKey . (text,ekeyi)),dkeyi) = text

proof end;

theorem :: AESCIP_1:33

for SBT being Permutation of (8 -tuples_on BOOLEAN)
for m being Nat
for text, otext being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for Keyi1, KeyNr being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) 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 (8 -tuples_on BOOLEAN)
for m, i being Nat
for text being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for eKeyi, dKeyi being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) 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
AddRoundKey . ((AddRoundKey . (text,eKeyi)),dKeyi) = text

proof end;

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

proof end;

theorem LASTXX: :: AESCIP_1:35

for SBT being Permutation of (8 -tuples_on BOOLEAN)
for MCFunc being Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))
for m being Nat
for text being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) 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 (8 -tuples_on D)

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 (8 -tuples_on D)

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 (8 -tuples_on D)

proof end;

definition

let r be Element of 128 -tuples_on BOOLEAN;

func AES-KeyInitState128 r -> Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) 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 b₁ being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( b₁ . 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))*> & b₁ . 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))*> & b₁ . 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))*> & b₁ . 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 b₁, b₂ being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st b₁ . 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))*> & b₁ . 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))*> & b₁ . 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))*> & b₁ . 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))*> & b₂ . 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))*> & b₂ . 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))*> & b₂ . 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))*> & b₂ . 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
b₁ = b₂

proof end;

end;

:: deftheorem defines AES-KeyInitState128 AESCIP_1:def 16 :
for r being Element of 128 -tuples_on BOOLEAN
for b₂ being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds
( b₂ = AES-KeyInitState128 r iff ( b₂ . 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))*> & b₂ . 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))*> & b₂ . 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))*> & b₂ . 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 (4 -tuples_on (8 -tuples_on BOOLEAN)) 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 b₁ being Element of 6 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( b₁ . 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))*> & b₁ . 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))*> & b₁ . 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))*> & b₁ . 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))*> & b₁ . 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))*> & b₁ . 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 b₁, b₂ being Element of 6 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st b₁ . 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))*> & b₁ . 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))*> & b₁ . 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))*> & b₁ . 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))*> & b₁ . 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))*> & b₁ . 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))*> & b₂ . 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))*> & b₂ . 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))*> & b₂ . 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))*> & b₂ . 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))*> & b₂ . 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))*> & b₂ . 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
b₁ = b₂

proof end;

end;

:: deftheorem defines AES-KeyInitState192 AESCIP_1:def 17 :
for r being Element of 192 -tuples_on BOOLEAN
for b₂ being Element of 6 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds
( b₂ = AES-KeyInitState192 r iff ( b₂ . 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))*> & b₂ . 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))*> & b₂ . 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))*> & b₂ . 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))*> & b₂ . 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))*> & b₂ . 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 (4 -tuples_on (8 -tuples_on BOOLEAN)) 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 b₁ being Element of 8 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( b₁ . 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))*> & b₁ . 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))*> & b₁ . 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))*> & b₁ . 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))*> & b₁ . 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))*> & b₁ . 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))*> & b₁ . 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))*> & b₁ . 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 b₁, b₂ being Element of 8 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st b₁ . 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))*> & b₁ . 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))*> & b₁ . 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))*> & b₁ . 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))*> & b₁ . 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))*> & b₁ . 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))*> & b₁ . 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))*> & b₁ . 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))*> & b₂ . 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))*> & b₂ . 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))*> & b₂ . 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))*> & b₂ . 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))*> & b₂ . 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))*> & b₂ . 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))*> & b₂ . 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))*> & b₂ . 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
b₁ = b₂

proof end;

end;

:: deftheorem defines AES-KeyInitState256 AESCIP_1:def 18 :
for r being Element of 256 -tuples_on BOOLEAN
for b₂ being Element of 8 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds
( b₂ = AES-KeyInitState256 r iff ( b₂ . 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))*> & b₂ . 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))*> & b₂ . 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))*> & b₂ . 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))*> & b₂ . 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))*> & b₂ . 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))*> & b₂ . 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))*> & b₂ . 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 (8 -tuples_on BOOLEAN);
let MixColumns be Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)));
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-Statearray ") . (AES-ENC (SBT,MixColumns,(AES-Statearray . message),(AES-KeyInitState128 Key)));

correctness
coherence
(AES-Statearray ") . (AES-ENC (SBT,MixColumns,(AES-Statearray . message),(AES-KeyInitState128 Key))) is Element of 128 -tuples_on BOOLEAN;

proof end;

end;

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

definition

let SBT be Permutation of (8 -tuples_on BOOLEAN);
let MixColumns be Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)));
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-Statearray ") . (AES-DEC (SBT,MixColumns,(AES-Statearray . cipher),(AES-KeyInitState128 Key)));

correctness
coherence
(AES-Statearray ") . (AES-DEC (SBT,MixColumns,(AES-Statearray . cipher),(AES-KeyInitState128 Key))) is Element of 128 -tuples_on BOOLEAN;

proof end;

end;

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

theorem :: AESCIP_1:37

for SBT being Permutation of (8 -tuples_on BOOLEAN)
for MixColumns being Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))
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 (8 -tuples_on BOOLEAN);
let MixColumns be Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)));
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-Statearray ") . (AES-ENC (SBT,MixColumns,(AES-Statearray . message),(AES-KeyInitState192 Key)));

correctness
coherence
(AES-Statearray ") . (AES-ENC (SBT,MixColumns,(AES-Statearray . message),(AES-KeyInitState192 Key))) is Element of 128 -tuples_on BOOLEAN;

proof end;

end;

:: deftheorem defines AES192-ENC AESCIP_1:def 21 :
for SBT being Permutation of (8 -tuples_on BOOLEAN)
for MixColumns being Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))
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-Statearray ") . (AES-ENC (SBT,MixColumns,(AES-Statearray . message),(AES-KeyInitState192 Key)));

definition

let SBT be Permutation of (8 -tuples_on BOOLEAN);
let MixColumns be Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)));
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-Statearray ") . (AES-DEC (SBT,MixColumns,(AES-Statearray . cipher),(AES-KeyInitState192 Key)));

correctness
coherence
(AES-Statearray ") . (AES-DEC (SBT,MixColumns,(AES-Statearray . cipher),(AES-KeyInitState192 Key))) is Element of 128 -tuples_on BOOLEAN;

proof end;

end;

:: deftheorem defines AES192-DEC AESCIP_1:def 22 :
for SBT being Permutation of (8 -tuples_on BOOLEAN)
for MixColumns being Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))
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-Statearray ") . (AES-DEC (SBT,MixColumns,(AES-Statearray . cipher),(AES-KeyInitState192 Key)));

theorem :: AESCIP_1:38

for SBT being Permutation of (8 -tuples_on BOOLEAN)
for MixColumns being Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))
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 (8 -tuples_on BOOLEAN);
let MixColumns be Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)));
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-Statearray ") . (AES-ENC (SBT,MixColumns,(AES-Statearray . message),(AES-KeyInitState256 Key)));

correctness
coherence
(AES-Statearray ") . (AES-ENC (SBT,MixColumns,(AES-Statearray . message),(AES-KeyInitState256 Key))) is Element of 128 -tuples_on BOOLEAN;

proof end;

end;

:: deftheorem defines AES256-ENC AESCIP_1:def 23 :
for SBT being Permutation of (8 -tuples_on BOOLEAN)
for MixColumns being Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))
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-Statearray ") . (AES-ENC (SBT,MixColumns,(AES-Statearray . message),(AES-KeyInitState256 Key)));

definition

let SBT be Permutation of (8 -tuples_on BOOLEAN);
let MixColumns be Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)));
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-Statearray ") . (AES-DEC (SBT,MixColumns,(AES-Statearray . cipher),(AES-KeyInitState256 Key)));

correctness
coherence
(AES-Statearray ") . (AES-DEC (SBT,MixColumns,(AES-Statearray . cipher),(AES-KeyInitState256 Key))) is Element of 128 -tuples_on BOOLEAN;

proof end;

end;

:: deftheorem defines AES256-DEC AESCIP_1:def 24 :
for SBT being Permutation of (8 -tuples_on BOOLEAN)
for MixColumns being Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))
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-Statearray ") . (AES-DEC (SBT,MixColumns,(AES-Statearray . cipher),(AES-KeyInitState256 Key)));

theorem :: AESCIP_1:39

for SBT being Permutation of (8 -tuples_on BOOLEAN)
for MixColumns being Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))
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;