Spot the Difference

Task description

U svijetu gdje se sve mijenja, miješa i xora, probaj pronaći tajni ključ. Flag je u formatu CTF2026[md5sum(ključ)]. (In a world where everything changes, mixes and XORs, try to find the secret key. The flag is CTF2026[md5sum(key)].)

A four-round substitution-permutation network cipher, encrypting 4-byte blocks, with a chosen-plaintext oracle available over the network.

The cipher

for j in range(4):
    temp = temp XOR keys[j]
    temp = sbox(temp)     # byte-wise substitution
    temp = pbox(temp)     # bit-level permutation

Four rounds, a 16-byte key split into four 4-byte round keys with no key schedule at all (each round key is just used as-is), an 8-bit substitution box and a 32-bit permutation applied across the whole 4-byte block each round.

The anomaly the title points at

A Difference Distribution Table (DDT) for an S-box records, for every pair of input and output differences, how often that pair occurs across all possible inputs. A well-designed S-box keeps every entry small, typically no more than 10 to 14 out of 256, so that no single input difference reliably predicts a specific output difference. Computing the DDT for this cipher’s S-box turns up one glaring exception:

DDT[0x5E][0x5B] = 122 / 256 ≈ 47.7%

An input difference of 0x5E produces the output difference 0x5B nearly half the time, instead of the roughly 4% a sound S-box would show at its worst. That’s the “difference” the challenge’s own title and description are pointing at: the S-box behaves almost linearly for that one specific input difference, a serious weakness, though not one this particular solve needed to exploit directly in the classical differential-cryptanalysis sense.

Solving for the key directly with Z3

Rather than building a classical differential attack around that one weak difference, modeling the entire cipher as a set of bit-level logical constraints and handing it to the Z3 SMT solver recovers the key outright, given enough known plaintext-ciphertext pairs. With a 128-bit key and only a 32-bit block, around a dozen pairs uniquely determine it.

The practical difficulty is getting Z3 to actually finish in reasonable time; fully random plaintexts make for a much harder constraint problem than structured ones do. Splitting the chosen plaintexts into three groups helped considerably:

• five pairs varying only the first two bytes, with the last two fixed at zero (constrains two key bytes cleanly),
• five pairs varying only the last two bytes, with the first two fixed at zero (constrains the other two),
• three fully random pairs, to add cross-byte constraints the first two groups don’t cover on their own.

solver = Solver()
K = [BitVec(f'k{i}', 8) for i in range(16)]

def mk_sbox(solver, x):
    y = BitVec(f's{next_id()}', 8)
    for v in range(256):
        solver.add(Implies(x == v, y == sbox_list[v]))
    return y

def mk_encrypt(solver, pt, key):
    st = [BitVecVal(pt[i], 8) for i in range(4)]
    for j in range(4):
        kj = key[j*4:(j+1)*4]
        st = [st[i] ^ kj[i] for i in range(4)]
        st = [mk_sbox(solver, st[i]) for i in range(4)]
        st = mk_pbox(st)   # bit-level permutation, built the same way
    return st

for pt, ct in pairs:
    enc = mk_encrypt(solver, list(pt), K)
    for i in range(4):
        solver.add(enc[i] == ct[i])

solver.check()
key = bytes([solver.model().eval(K[i]).as_long() for i in range(16)])

Result

Key (hex): 6733a13868503910262a0743f2423a31
MD5(key):  1d299dcd62b19b71a45971d2bf9a1518

Verified against 10 fresh plaintext-ciphertext pairs from the server, all matching. The flag:

CTF2026[1d299dcd62b19b71a45971d2bf9a1518]

Why the plaintext structure mattered

An SMT solver’s performance on a problem like this depends heavily on how its constraints are shaped, not just on how many there are. Fully random plaintexts give the solver no early structure to exploit while searching; deliberately constraining some bytes to zero across several plaintexts lets it pin down individual key bytes with far less backtracking, even though the underlying cipher and the number of unknowns are exactly the same either way.