A keygen challenge (z3+brute)
On one of the previous CTFs that I played a keygen me binary is given, you can download it from here. We'll solve it in two ways, the easy way which is bruteforce, and the longer way which is using z3.
Let us start to understand what the binary does. We start from main. At the beginning of main it initializes a bunch of pointers to functions.
those functions are called in sequence to check the serial number. They take a char * and return either 1 or 0. If all of them passed then the serial number is valid, otherwise it's not.
Let's take a look at each function.
- The first 3 functions are simple all they do is check if the serial number is in the requested format which is 19 characters long, consist of numbers, and has - at positions 4,9, and 14.
Decompilation of the function is :
This is a simple check that does the following :
We have 4 parts, each part is the sum of the previous numbers in the serial number divided by the part number. eg:
- part1 is the sum of the first 4 numbers divided by 1
- part2 is the sum of the first 8 numbers divided by 2
- and so on..
the final check is that every part equals the total sum divided by 4.
This function checks that numbers in position
- 0,1,2,3 are not equal to 5,6,7,8
- 5,6,7,8 are not equal to 10,11,12,13
- 10,11,12,13 are not equal to 15,16,17,18
Using z3 we can generate all possible solutions by adding the constrains to a solver and it will solve them.
This will generate all possible solutions. It was running while I was writing this, and so far it generated
41K unique valid keys :p. The easy and quick way of solving this will be just decompile the check functions and run them while generating the parts of the serial randomly from a digit charset.