circuit123

circuit123

Reversing - 800 points

Challenge

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

decrypt.py

map1.txt

map2.txt

Hint

Have you heard of z3?

Solution

Solution is simply to convert the verify() function into constrain equations in Z3

---

Running the solver. I ensured it worked for map1.txt first, and then I moved on to solve map2.txt

$ export DYLD_LIBRARY_PATH=$DYLD_LIBRARY_PATH:$(pwd)/bin
$ export PYTHONPATH=$(pwd)/bin/python
$ python solve.py
sequence 1011001101001100110110000111001011110101010001011111011101101001111010100110001001110111011010000101001000101110110110001010010110011001100111101001011010111100111101110100011001101011101110100011001100111101110101111010111101011110100011010111101000110011001111010010110101111001111100111110011110111010001100101001011010111100111101110101111010001101011110100011001101011101001010111010111101011110101111010001101011110101111010001101011110100011001100111110101110100101010010110101110100101100111110101111010111101011110011111010111010010101110101111010111101000110100000100110011110100101010010101110101111010111101000110010111010111101011110101111010111101011110100011010111101011110101111010111101000110010100101011101011110101111010111101011110100011001010010101110101111010111101000110101111010111101000110011010111100111110101110111010001100101110101111010001101011110100011010001100110011110100101101011101001010100101101011110011110100101101011110101110111010001100110101111001111101011101110101111010110000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
key 219465169949186335766963147192904921805

Plug into the decryptor and get the flag

$ python decrypt.py 219465169949186335766963147192904921805 map2.txt
Attempting to decrypt map2.txt...
Congrats the flag for map2.txt is: picoCTF{36cc0cc10d273941c34694abdb21580d__aw350m3_ari7hm37ic__}

Flag

picoCTF{36cc0cc10d273941c34694abdb21580d__aw350m3_ari7hm37ic__}