picoCTF 2018 - circuit123

Posted on October 17, 2018* in ctf-writeups

Table of Contents

Problem

Can you crack the key to decrypt map2 for us? The key to map1 is 11443513758266689915.

Hint

z3

Solution

Given the problem and the hint, it is clear that we can use z3 to solve this problem. We can create a z3 BitVec and pass it into the verify function to avoid writing a custom decrypter. Because we don't know the length of the bit vector, I used a conservative estimate of 128.

Jupyter Notebook