Tags: bruteforce-bytebybyte z3 smt reversing math crypto saturation brute-force bruteforce python python3 


In my write-up (see link) I'm describing this challenge in full. It also includes the challenge files for download and the description contains many images. The challenge contains three parts:
1. understanding stream-cipher and decrypting the beginning of the Python code
2. understanding the Python code and continuing the stream cipher to decode the rest of the Python code and decoding the hint image
3. reversing the PRNG bootstrap code to get the IV (password), which is the flag; I first tried some intelligent brute-forcing and later Z3

I didn't solve this challenge on time (actually one day too late), so no points for our team, but it's still a very interesting challenge.

I never used SAT or SMT before, so solving this, I definetely learned something new.

Original writeup (https://e4ch.blogspot.com/2018/01/insomnihack-teaser-2018-ctf.html).