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