# PicoCTF 2018 - Keygen-me 2 (Reverse) The software has been updated. Can you find us a new product key for the program in /problems/keygen-me-2_3_5e45e804e9c1a9de2f8124266b173c35 A binary and the hint "z3"

## Main

Like the first Keygen-Me, we see through the main function that we need to provide a 16 bytes key matching [A-Z0-9].

Only if the function validate_key return True will the flag be displayed. ``````_BOOL4 __cdecl check_valid_char(char a1)
{
return a1 > 47 && a1 <= 57 || a1 > 64 && a1 <= 90;
}``````

## validate_key(char *s)

This function take our input and apply 12 constraints on it, we quickly see that each key_constraint must return true. So we have to determinate how each of theses function could return true ! ## key_constraint_XX

The pictures just below are showing how each constraints functions works, they are really similars but are checking different char of the key.  ## Making the equation

We will need z3 for solve this equation. Z3 is a Theorem Prover we can use through it python lib, we can found the project here and some documentations about.

I always wanted to learn about but never did it, until I really need it for this challenge, thank's to twitter community I could get some help quickly to understand the basics. Thanks again guys !

Oh I forgot, in each key_constraints function two functions are used : mod and ord. They are trivial function but I quickly implemented in Python in order to be sure to get the exact same behavior

``````def _ord(c):
if c > 47 and c <= 57:
return c - 48
else:
return c - 55

def _mod(a, b):
if a % b >= 0:
return a % b
else:
return a % b + b``````

The we need to declare a IntVector of 16 value, this Z3 object is kind of a list of integer constants of size 16 in our case.

Then we add the first kind of constraint : each byte must be >= 0 and <= 35 (because of the key value possibilities and mod / ord function).

And finaly we implement in Python each of these constraints like this :

``````from z3 import *

flag = IntVector("f", 16)
s = Solver()

for i in range(0, 16):

s.add(((flag + flag) % 36) == 14)
s.add(((flag + flag) % 36) == 24)
s.add(((flag - flag) % 36) == 6)
s.add(((flag + flag + flag) % 36) == 4)
s.add(((flag + flag + flag) % 36) == 13)
s.add(((flag + flag + flag) % 36) == 22)
s.add(((flag + flag + flag) % 36) == 31)
s.add(((flag + flag + flag) % 36) == 7)
s.add(((flag + flag + flag) % 36) == 20)
s.add(((flag + flag + flag) % 36) == 12)
s.add(((flag + flag + flag) % 36) == 27)
s.add(((flag + flag + flag) % 36) == 23)

# if there is a solution
if s.check() != unsat:

mod = s.model() # we display the model

for i in range(16): # and we print nicely the two possible values due to the ord function
x = mod[flag[i]].as_long()
print (chr(x + 55), chr(x + 48))``````

``````switch :: ~/CTF/pico2018/keygen-me-2 » python solv2.py
[f__4 = 32,
f__6 = 11,
f__15 = 7,
f__1 = 14,
f__7 = 33,
f__13 = 20,
f__0 = 0,
f__9 = 7,
f__8 = 23,
f__3 = 18,
f__2 = 6,
f__14 = 21,
f__11 = 0,
f__10 = 33,
f__5 = 8,
f__12 = 6]

('7', '0')
('E', '>')
('=', '6')
('I', 'B')
('W', 'P')
('?', '8')
('B', ';')
('X', 'Q')
('N', 'G')
('>', '7')
('X', 'Q')
('7', '0')
('=', '6')
('K', 'D')
('L', 'E')
('>', '7')``````

We can quickly remove all values not in [A-Z0-9] then I choosed to check each value manually step by step. You can notice that none of the constraints use the 11th char so it could be any value, so I used X at this position !

``````a = _ord(ord("0"))
b = _ord(ord("E"))
c = _ord(ord("6"))
d = _ord(ord("I"))
e = _ord(ord("W"))
f = _ord(ord("8"))
g = _ord(ord("B"))
h = _ord(ord("X"))
i = _ord(ord("N"))
j = _ord(ord("7"))
k = _ord(ord("X"))

m = _ord(ord("6"))
n = _ord(ord("K"))
o = _ord(ord("L"))
p = _ord(ord("7"))

print _mod(a + b, 36) == 14
print _mod(c + d, 36) == 24
print _mod(c - a, 36) == 6
print _mod(d + b + f, 36) == 4
print _mod(e + c + g, 36) == 13
print _mod(e + d + f, 36) == 22
print _mod(i + g + k, 36) == 31
print _mod(e + b + h, 36) == 7
print _mod(m + j + p, 36) == 20
print _mod(o + n + p, 36) == 12
print _mod(j + i + k, 36) == 27
print _mod(m + h + n, 36) == 23``````

``````switch :: ~/CTF/pico2018/keygen-me-2 » python solv2.py
True
True
True
True
True
True
True
True
True
True
True
True``````

And the key and flag are : 0E6IW8BXN7X6KL7 and picoCTF{c0n5tr41nt_50lv1nG_15_W4y_f45t3r_252103361}