Writeup for CTF fez.py with symbolic executiong (claripy). This is a RE question includes a python source code(fez.py,modified for python3) and a log file(fez.log). The fez_sym.py is my solution with claripy.

fez.log

50543fc0bca1bb4f21300f0074990f846a8009febded0b2198324c1b31d2e2563c908dcabbc461f194e70527e03a807e9a478f9a56f7
66bbd551d9847c1a10755987b43f8b214ee9c6ec2949eef01321b0bc42cffce6bdbd604924e5cbd99b7c56cf461561186921087fa1e9
44fc6f82bdd0dff9aca3e0e82cbb9d6683516524c245494b89c272a83d2b88452ec0bfa0a73ffb42e304fe3748896111b9bdf4171903

fez.py

import os
def xor(a,b):
    assert len(a)==len(b)
    c=bytearray()
    for i in range(len(a)):
        #c+=chr(ord(a[i])^ord(b[i]))
        c.append((a[i])^(b[i]))
    return c
def round(M,K):
    L=M[0:27]
    R=M[27:54]
    new_l=R
    new_r=xor(xor(R,L),K)
    return new_l+new_r
def fez(m,K):
    for i in K:
        m=round(m,i)
    return m

K=[]
for i in range(7):
    K.append(os.urandom(27))
m=open("flag","rb").read()

assert len(m)<54
m+=os.urandom(54-len(m))

test=os.urandom(54)

print (test.hex())
print (fez(test,K).hex())
print (fez(m,K).hex())

fez_sym.py

import os
import claripy
s = claripy.Solver()

def xor(a,b):
    # assert len(a)==len(b)
    # c=bytearray()
    # for i in range(len(a)):
    #     #c+=chr(ord(a[i])^ord(b[i]))
    #     c.append((a[i])^(b[i]))
    # return c
    return a^b
def round(M,K):
    #L=M[0:27]
    #R=M[27:54]
    
    L=M.get_bytes(0,27)
    R=M.get_bytes(27,27)
    new_l=R
    new_r=xor(xor(R,L),K)
    print(new_l)
    print(new_r)

    return claripy.Concat(new_l,new_r)
def fez(m,K):
    for i in K:
        m=round(m,i)
        print("round:",i)
        print(m)    
    return m

K=[]
for i in range(7):
    #K.append(os.urandom(27))
    K.append(claripy.BVS("K%d"%i,27*8))
#m=open("flag","rb").read()
#assert len(m)<54
#m+=os.urandom(54-len(m))

m = claripy.BVS("m", 54*8)

test=bytes(bytearray.fromhex("50543fc0bca1bb4f21300f0074990f846a8009febded0b2198324c1b31d2e2563c908dcabbc461f194e70527e03a807e9a478f9a56f7")) 
#bytearray need to be converted to bytes, or (test_s == test) will be 'False' instead of a BV.
test_s = claripy.BVS("test_s",54*8)
test_s_con = (test_s == test)
s.add(test_s_con == True)

fez_test_k = bytes(bytearray.fromhex("66bbd551d9847c1a10755987b43f8b214ee9c6ec2949eef01321b0bc42cffce6bdbd604924e5cbd99b7c56cf461561186921087fa1e9"))
fez_m_k = bytes(bytearray.fromhex("44fc6f82bdd0dff9aca3e0e82cbb9d6683516524c245494b89c272a83d2b88452ec0bfa0a73ffb42e304fe3748896111b9bdf4171903"))

fez_test_k_sym = fez(test_s,K)
fez_m_k_sym = fez(m,K)

print("--------------")
print("fez_test_k_sym:",fez_test_k_sym)
print("fez_m_k_sym   :",fez_m_k_sym)


fez_e_sym = (fez_test_k_sym == fez_test_k)
fez_m_sym = (fez_m_k_sym == fez_m_k)


s.add(fez_e_sym == True)
s.add(fez_m_sym == True)
print(m)

print("==================================")
print("s.satisfiable:",s.satisfiable())
m_r = s.eval(m, 1)[0].to_bytes(54,'big')
print(m_r)
# print (test.hex())
# print (fez(test,K).hex())
# print (fez(m,K).hex())