Rating: 4.5
tl;dr:
1. Notice output depends only on 2 bits of the state, and after some shifts one of them is known
2. Ask Z3 to solve the correspondence
https://github.com/p4-team/ctf/tree/master/2019-03-23-0ctf-quals/crypto_lfsr
Could someone explain how to get past the fact that we have multiple LFSRs in a bit more detail? I can see we can easily recover the state with a single LFSR, but when we have multiple we no longer know the output bits, and the writeup somewhat glosses over this and just plugs it into Z3. What's actually happening here?
Thanks!
