picoCTF 2018 keygen-me-2 Reversing

keygen-me-2 - Points: 750 - (Solves: 105)

요약

z3 solver 로 풀었습니다.

Description

The software has been updated.
Can you find us a new product key for the program in /problems/keygen-me-2_4_3cb8c5fbaa87ce402753132dd68f9003

solve.py

from z3 import *

ord = lambda a1    : If(And(0x41 <= a1, a1 <= 0x5a), a1-0x37, a1-0x30)
mod = lambda a1, a2: If(a1 % a2 >= 0, a1 % a2, a1 % a2 + a2)

a1 = [BitVec('a1_%d' % i, 8) for i in range(16)]

s = Solver()

for i in range(16):
        s.add(Or(And(0x30 <= a1[i], a1[i] <= 0x39), And(0x41 <= a1[i], a1[i] <= 0x5a)))

# key_constraint_01(char *a1)
v1 = ord(a1[0])
v2 = ord(a1[1])
s.add(mod(v1 + v2, 36) == 14)
# key_constraint_02(char *a1)
v1 = ord(a1[2])
v2 = ord(a1[3])
s.add(mod(v1 + v2, 36) == 24)
# key_constraint_03(char *a1)
v1 = ord(a1[2])
v2 = ord(a1[0])
s.add(mod(v1 - v2, 36) == 6)
# key_constraint_04(char *a1)
v1 = ord(a1[1])
v2 = ord(a1[3]) + v1
v3 = ord(a1[5])
s.add(mod(v2 + v3, 36) == 4)
# key_constraint_05(char *a1)
v1 = ord(a1[2])
v2 = ord(a1[4]) + v1
v3 = ord(a1[6])
s.add(mod(v2 + v3, 36) == 13)
# key_constraint_06(char *a1)
v1 = ord(a1[3])
v2 = ord(a1[4]) + v1
v3 = ord(a1[5])
s.add(mod(v2 + v3, 36) == 22)
# key_constraint_07(char *a1)
v1 = ord(a1[6])
v2 = ord(a1[8]) + v1
v3 = ord(a1[10])
s.add(mod(v2 + v3, 36) == 31)
# key_constraint_08(char *a1)
v1 = ord(a1[1])
v2 = ord(a1[4]) + v1
v3 = ord(a1[7])
s.add(mod(v2 + v3, 36) == 7)
# key_constraint_09(char *a1)
v1 = ord(a1[9])
v2 = ord(a1[12]) + v1
v3 = ord(a1[15])
s.add(mod(v2 + v3, 36) == 20)
# key_constraint_10(char *a1)
v1 = ord(a1[13])
v2 = ord(a1[14]) + v1
v3 = ord(a1[15])
s.add(mod(v2 + v3, 36) == 12)
# key_constraint_11(char *a1)
v1 = ord(a1[8])
v2 = ord(a1[9]) + v1
v3 = ord(a1[10])
s.add(mod(v2 + v3, 36) == 27)
# key_constraint_12(char *a1)
v1 = ord(a1[7])
v2 = ord(a1[12]) + v1
v3 = ord(a1[13])
s.add(mod(v2 + v3, 36) == 23)

if s.check() == sat:
        m = s.model()
        flag = ''
        for i in range(16):
                flag += chr(m[a1[i]].as_long())
        print flag

flag

j3rrry@pico-2018-shell-2:/problems/keygen-me-2_4_3cb8c5fbaa87ce402753132dd68f9003$ ./activate LTRXBEB3O7W9XN9G
Product Activated Successfully: picoCTF{c0n5tr41nt_50lv1nG_15_W4y_f45t3r_2355915573}