let SBT be 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
let m be 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
let text be 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
let key be 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
let dkeyi, ekeyi be Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); ( ( m = 4 or m = 6 or m = 8 ) & dkeyi = (Rev ((KeyExpansion (SBT,m)) . key)) . 1 & ekeyi = ((KeyExpansion (SBT,m)) . key) . (7 + m) implies AddRoundKey . ((AddRoundKey . (text,ekeyi)),dkeyi) = text )
assume AS:
( ( m = 4 or m = 6 or m = 8 ) & dkeyi = (Rev ((KeyExpansion (SBT,m)) . key)) . 1 & ekeyi = ((KeyExpansion (SBT,m)) . key) . (7 + m) )
; AddRoundKey . ((AddRoundKey . (text,ekeyi)),dkeyi) = text
set p = (KeyExpansion (SBT,m)) . key;
(KeyExpansion (SBT,m)) . key in (7 + m) -tuples_on (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))
;
then B0:
ex s being Element of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) * st
( (KeyExpansion (SBT,m)) . key = s & len s = 7 + m )
;
1 + 0 < 7 + m
by XREAL_1:8;
then
1 in Seg (7 + m)
;
then B1:
1 in dom ((KeyExpansion (SBT,m)) . key)
by FINSEQ_1:def 3, B0;
A0: dkeyi =
((KeyExpansion (SBT,m)) . key) . (((len ((KeyExpansion (SBT,m)) . key)) - 1) + 1)
by AS, FINSEQ_5:58, B1
.=
ekeyi
by B0, AS
;
now for i, j being Nat st i in Seg 4 & j in Seg 4 holds
((AddRoundKey . ((AddRoundKey . (text,ekeyi)),dkeyi)) . i) . j = (text . i) . jlet i,
j be
Nat;
( i in Seg 4 & j in Seg 4 implies ((AddRoundKey . ((AddRoundKey . (text,ekeyi)),dkeyi)) . i) . j = (text . i) . j )assume A3:
(
i in Seg 4 &
j in Seg 4 )
;
((AddRoundKey . ((AddRoundKey . (text,ekeyi)),dkeyi)) . i) . j = (text . i) . jthen consider etextij,
ekeyij being
Element of 8
-tuples_on BOOLEAN such that A4:
(
etextij = (text . i) . j &
ekeyij = (ekeyi . i) . j &
((AddRoundKey . (text,ekeyi)) . i) . j = Op-XOR (
etextij,
ekeyij) )
by DefAddRoundKey;
consider dtextij,
dkeyij being
Element of 8
-tuples_on BOOLEAN such that A5:
(
dtextij = ((AddRoundKey . (text,ekeyi)) . i) . j &
dkeyij = (dkeyi . i) . j &
((AddRoundKey . ((AddRoundKey . (text,ekeyi)),dkeyi)) . i) . j = Op-XOR (
dtextij,
dkeyij) )
by DefAddRoundKey, A3;
thus
((AddRoundKey . ((AddRoundKey . (text,ekeyi)),dkeyi)) . i) . j = (text . i) . j
by A4, A5, A0, DESCIP_1:17;
verum end;
hence
AddRoundKey . ((AddRoundKey . (text,ekeyi)),dkeyi) = text
by LM01; verum