-
-
Save 00xc/4fc261156bd919c0179abf38e4eae637 to your computer and use it in GitHub Desktop.
DownUnderCTF 2021 - Flag Checker solve script
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
from z3 import * | |
def ch_transform(c): | |
return ((c >> 7) * 0x1b ^ c * 2) & 0xff | |
def reverse_shuffle(inp): | |
mappings = {0: 29, 1: 34, 2: 13, 3: 18, 4: 15, 5: 20, 6: 35, 7: 28, 8: 19, 9: 12, 10: 21, 11: 14, 12: 3, 13: 8, 14: 25, 15: 30, 16: 1, 17: 6, 18: 9, 19: 2, 20: 31, 21: 24, 22: 7, 23: 0, 24: 5, 25: 10, 26: 17, 27: 22, 28: 27, 29: 32, 30: 11, 31: 4, 32: 23, 33: 16, 34: 33, 35: 26} | |
mappings = {v:k for k,v in mappings.items()} | |
out = [None] * len(inp) | |
for orig, new in mappings.items(): | |
out[new] = inp[orig] | |
return out | |
def reverse_num_combine(inp, nums): | |
# The known output values | |
n_out = [inp[nums[i]] for i in range(6)] | |
# The unknown input values that produce the output | |
n = [BitVec(f"n{i}", 32) for i in range(6)] | |
s = Solver() | |
s.add(inp[nums[0]] == ch_transform(n[4]) ^ ch_transform(n[0]) ^ n[0] ^ n[2] ^ ch_transform(n[2])) | |
s.add(inp[nums[1]] == ch_transform(n[5]) ^ ch_transform(n[1]) ^ n[1] ^ n[3] ^ ch_transform(n[3])) | |
s.add(inp[nums[2]] == ch_transform(n[0]) ^ n[4]) | |
s.add(inp[nums[3]] == ch_transform(n[1]) ^ n[5]) | |
s.add(inp[nums[4]] == ch_transform(n[2]) ^ ch_transform(n[0]) ^ n[0]) | |
s.add(inp[nums[5]] == ch_transform(n[3]) ^ ch_transform(n[1]) ^ n[1]) | |
if s.check() == sat: | |
m = s.model() | |
final_nums = [int(str(m[e])) for e in n] | |
for i in range(6): | |
inp[nums[i]] = final_nums[i] | |
return inp | |
def reverse_combine(inp): | |
nums = [ | |
[0,1,2,6,12,18], | |
[3,4,5,11,17,23], | |
[7,8,9,13,14,15], | |
[10,16,22,28,29,35], | |
[19,20,24,25,26,30], | |
[21,27,31,32,33,34] | |
] | |
for n in nums[::-1]: | |
inp = reverse_num_combine(inp, n) | |
return inp | |
if __name__ == '__main__': | |
target = bytes.fromhex("0f4f733c41c6a4afb441d665c899aab36c99613c4edd704615663c1b7f16a66f2313126e") | |
for _ in range(16): | |
target = reverse_shuffle(target) | |
target = reverse_combine(target) | |
print("".join(map(chr, target))) | |
# DUCTF{rev3rs1bl3___and___1nv3rtibl3} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment