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[1]. We'll solve it in two ways, the easy way which is bruteforce, and the longer way which is using z3.

1: https://0x80.org/challenges/keygenme_01

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.

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:

the final check is that every part equals the total sum divided by 4.


This function checks that numbers in position

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.

Proxied content from gemini://0x80.org/gemlog/2016-03-02-practice-z3-keygen.gmi.
Get a proper gemini browser and visit!

Gemini request details:

Original URL
Status code