:: 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) ) ) );