Dojo challenge #4 - Exploit Script

exploit.py

#!/usr/bin/env python
# @SakiiR

import z3

def format_chunks(m, chunks):
    return "-".join([f"{int(str(m[c])):04d}" for c in chunks])

def doit_twice(s, chunks):
    try:
        while True:
            if s.check() == z3.sat:
                m = s.model()
                # Prints the serial
                print(format_chunks(m, chunks))

                # Adds a constraints forcing z3 to find the next solution
                s.add(
                    z3.And(
                        chunks[0] != m[chunks[0]],
                        chunks[1] != m[chunks[1]],
                        chunks[2] != m[chunks[2]],
                        chunks[3] != m[chunks[3]],
                    )
                )
            else:
                return
    except KeyboardInterrupt:
        print("\nExiting ...")
        return

def main():

    s = z3.Solver()

    chunks = [z3.Int(f"chunk[{_}]") for _ in range(4)]

    for _ in range(4):
        s.add(chunks[_] >= 0)
        s.add(chunks[_] <= 9999)

    s.add(
        z3.And(
            chunks[0] % 3 == 0,
            chunks[2] % 9 == 0,
            chunks[1] % 5 == 0,
            chunks[3] % 8 == 0,
            chunks[0] == chunks[1] + chunks[3],
            chunks[1] == (chunks[2] - chunks[3] - 42),
            ((chunks[1] * 3) + chunks[0] - chunks[2]) == chunks[3],
        )
    )

    doit_twice(s, chunks)

if __name__ == "__main__":
    main()