2016 Boston Key Party HMAC_CRC Writeup

hmac_crc - 5 - 15 solves : crypto: We're trying a new mac here at BKP---HMAC-CRC.
The hmac (with our key) of "zupe zecret" is '0xa57d43a032feb286'.  What's the 
hmac of "BKPCTF"? https://s3.amazonaws.com/bostonkeyparty/2016/0c7433675c3c555a \
fb77271d6a549bf5d941d2ab

That download gives us hmac.py and I added some comments and debug prints in hmac2.py.

somewhat de-confusing HMAC

The motivation of that weird HMAC formula is apparent when you look at ways of combining a key with hash(msg) that do NOT work, thanks to the Wikipedia article. If we do MAC = hash(key|msg) then we can the hash algorithms' internal state so that it would output MAC and continue hashing on some appended data to msg, forging a MAC for msg'. If we do MAC = hash(msg|key) then a collision found in hash() is also a collision in the MAC, since msg' will be constructible such that hash(msg)==hash(msg') and the internal state of the hash algorithm will be identical before consuming the key. Concatenating the key to the front and back, even when the keys are different has some more nuanced issues that I don't understand and don't matter for now. The final good design is HMAC = hash(key|hash(key|msg)) with some padding.

an algebra attack?

The challenge is the vanilla HMAC algorithm but using weak hash function CRC. The layman's explanation of CRC is that by treating the input data as a polynomial over a finite field, and finding the remainder after division by an irreducible polynomial in that field, the result is pretty good at detecting errors. The divider polynomial used here is the monster 11110111111110110011111000111011111010001001110000011010111110111 which represents the coefficients over GF(2), with left side MSB being the x^64 coeff. I checked that this was irreducible in pari/gp before continuing, suspecting maybe some weakness in the divider might be needed to solve the challenge:

? p = (x^64 + x^63 + x^62 + x^61 + x^59 + x^58 + x^57 + x^56 + x^55 + x^54 + x^53 + x^52 + x^50 + x^49 + x^46 + x^45 + x^44 + x^43 + x^42 + x^38 + x^37 + x^36 + x^34 + x^33 + x^32 + x^31 + x^30 + x^28 + x^24 + x^21 + x^20 + x^19 + x^13 + x^12 + x^10 + x^8 + x^7 + x^6 + x^5 + x^4 + x^2 + x + 1)*Mod(1,2)
? lift(factor(p))
%3 =
[x^64 + x^63 + x^62 + x^61 + x^59 + x^58 + x^57 + x^56 + x^55 + x^54 + x^53 + x^52 + x^50 + x^49 + x^46 + x^45 + x^44 + x^43 + x^42 + x^38 + x^37 + x^36 + x^34 + x^33 + x^32 + x^31 + x^30 + x^28 + x^24 + x^21 + x^20 + x^19 + x^13 + x^12 + x^10 + x^8 + x^7 + x^6 + x^5 + x^4 + x^2 + x + 1 1]

crc in reverse?

Don't worry! You don't need to know shit about polynomials and fields to work with CRC. Study crc() in hmac.py until you can imagine that large bit string in CRC_POLY travelling left-to-write across the input bits, being XOR'd in everytime the current input bit is 1. Once the CRC_POLY bumps up against the right side of the input, the current running result is taken as the remainder.

It's tempting to think that you can work it backwards, and when the number of unknown bits is <= n for an n-bit CRC, you are right. But keep in mind that you are not necessarily revealing INPUT bits during this process, you're revealing what those bits were during a temporary time of CRC calculation. The input bit could have been anything, and a more significant input bit could have caused the divider poly to change its lesser significant bit neighbors after an XOR. I wasted a large time seduced by the idea that the outer CRC could be worked backwards to reveal part of it's input: the 64-bit inner CRC result, and then from this the inner CRC result could be worked backwards to reveal it's input: the 64-bit key. But I was merely revealing what those bits were amid the CRC calculation, when the divider reached them. I was revealing the values AFTER the key bits to the left had affected them.

alright, this is cool

When I realized the above natural path of attack would fail, I started to appreciate the disturbing reality of this challenge. We're faced with a completely invertible function, but it's cleverly chained (inner CRC result is concatenated and fed to outer CRC) so that the invertibility evaporates before our eyes!

If I challenged you to compute the 64 bit input KEY that results in a given 64 bit output CRC, you'd have no problem. You'd also have no problem for crc(crc(KEY)); working backwards twice. But crc(KEY|crc(KEY)) magically inflates the input to the outer CRC beyond 64-bits, losing invertibility. Yet the input size to the entire system remains only 64-bits; the KEY is simply reused. I sat shocked by this for a while, and am still hoping someone solved the problem in a way that makes it not true.

down to the bits

So how to solve it? If you look carefully, every computation in this entire algorithm is XOR. Even the conditional "if current bit b_i is 1, then XOR in the poly" can be written unconditionally as an XOR of b_i for each of the bits that would have been flipped by applying poly, due to the property that XOR with 0 is an identity function. If each of the 64 output bits can be written as an expression of the input bits where the only operator is XOR, then we're in a completely determined linear system over GF(2). That's fancy talk for it being solvable, using the same technique taught in linear algebra where you reduce rows in a matrix.

Guess what? These equations are a bit big, so let's write a program to keep track of them rather than work them out by hand. See gen_equations.py which takes into account minor details like key padding and CRC initial value. With k_i naming each key bit, the final system is:

1^k₁₀^k₁₃^k₁₆^k₁₉^k₂₄^k₂₅^k₂₇^k₃^k₃₁^k₃₂^k₃₄^k₃₅^k₃₆^k₃₇^k₄₁^k₄₂^k₄₄^k₄₅^k₄₆^k₄₈^k₄₉^k₅₁^k₅₃^k₅₆^k₅₈^k₅₉^k₆^k₆₀^k₆₂^k₇=1 1^k₁₀^k₁₂^k₁₃^k₁₅^k₁₆^k₁₈^k₁₉^k₂^k₂₃^k₂₅^k₂₆^k₂₇^k₃^k₃₀^k₃₂^k₃₃^k₃₇^k₄₀^k₄₂^k₄₃^k₄₆^k₄₇^k₄₉^k₅^k₅₀^k₅₁^k₅₂^k₅₃^k₅₅^k₅₆^k₅₇^k₆₀^k₆₁^k₆₂^k₆₃^k₇^k₉=0 1^k₁^k₁₀^k₁₁^k₁₂^k₁₃^k₁₄^k₁₅^k₁₆^k₁₇^k₁₈^k₁₉^k₂^k₂₂^k₂₆^k₂₇^k₂₉^k₃^k₃₄^k₃₅^k₃₇^k₃₉^k₄^k₄₄^k₅₀^k₅₂^k₅₃^k₅₄^k₅₅^k₅₈^k₆₁^k₇^k₈^k₉=1 k₀^k₁^k₁₁^k₁₂^k₁₄^k₁₅^k₁₇^k₁₈^k₁₉^k₂^k₂₁^k₂₄^k₂₆^k₂₇^k₂₈^k₃₁^k₃₂^k₃₃^k₃₅^k₃₇^k₃₈^k₄₁^k₄₂^k₄₃^k₄₄^k₄₅^k₄₆^k₄₈^k₅₂^k₅₄^k₅₆^k₅₇^k₅₈^k₅₉^k₆₂^k₆₃^k₈^k₉=0 1^k₀^k₁^k₁₀^k₁₁^k₁₃^k₁₄^k₁₆^k₁₇^k₁₈^k₂₀^k₂₃^k₂₅^k₂₆^k₂₇^k₃₀^k₃₁^k₃₂^k₃₄^k₃₆^k₃₇^k₄₀^k₄₁^k₄₂^k₄₃^k₄₄^k₄₅^k₄₇^k₅₁^k₅₃^k₅₅^k₅₆^k₅₇^k₅₈^k₆₁^k₆₂^k₆₃^k₇^k₈=0 1^k₀^k₁₂^k₁₅^k₁₇^k₂₂^k₂₆^k₂₇^k₂₉^k₃^k₃₀^k₃₂^k₃₃^k₃₄^k₃₇^k₃₉^k₄₀^k₄₃^k₄₅^k₄₈^k₄₉^k₅₀^k₅₁^k₅₂^k₅₃^k₅₄^k₅₅^k₅₇^k₅₈^k₅₉^k₆₁^k₆₃^k₉=1 1^k₁₀^k₁₁^k₁₃^k₁₄^k₁₉^k₂^k₂₁^k₂₄^k₂₆^k₂₇^k₂₈^k₂₉^k₃^k₃₃^k₃₄^k₃₅^k₃₇^k₃₈^k₃₉^k₄₁^k₄₅^k₄₆^k₄₇^k₅₀^k₅₂^k₅₄^k₅₇^k₅₉^k₆^k₇^k₈=0 1^k₁^k₁₂^k₁₆^k₁₈^k₁₉^k₂^k₂₀^k₂₃^k₂₄^k₂₆^k₂₈^k₃^k₃₁^k₃₃^k₃₅^k₃₈^k₄₀^k₄₁^k₄₂^k₄₈^k₅^k₅₉^k₆₀^k₆₂^k₆₃^k₉=1 k₀^k₁^k₁₀^k₁₁^k₁₃^k₁₅^k₁₆^k₁₇^k₁₈^k₂^k₂₂^k₂₃^k₂₄^k₃^k₃₀^k₃₁^k₃₅^k₃₆^k₃₉^k₄^k₄₀^k₄₂^k₄₄^k₄₅^k₄₆^k₄₇^k₄₈^k₄₉^k₅₁^k₅₃^k₅₆^k₆^k₆₀^k₆₁^k₆₃^k₇^k₈=0 1^k₀^k₁^k₁₂^k₁₃^k₁₄^k₁₅^k₁₇^k₁₉^k₂^k₂₁^k₂₂^k₂₃^k₂₄^k₂₅^k₂₇^k₂₉^k₃₀^k₃₁^k₃₂^k₃₆^k₃₇^k₃₈^k₃₉^k₄₂^k₄₃^k₄₇^k₄₉^k₅^k₅₀^k₅₁^k₅₂^k₅₃^k₅₅^k₅₆^k₅₈^k₉=1 1^k₀^k₁^k₁₀^k₁₁^k₁₂^k₁₄^k₁₈^k₁₉^k₂₀^k₂₁^k₂₂^k₂₃^k₂₅^k₂₆^k₂₇^k₂₈^k₂₉^k₃^k₃₀^k₃₂^k₃₄^k₃₈^k₄^k₄₄^k₄₅^k₅₀^k₅₂^k₅₃^k₅₄^k₅₅^k₅₆^k₅₇^k₅₈^k₅₉^k₆^k₆₀^k₆₂^k₇^k₈=1 k₀^k₁₁^k₁₆^k₁₇^k₁₈^k₂^k₂₀^k₂₁^k₂₂^k₂₆^k₂₈^k₂₉^k₃₂^k₃₃^k₃₄^k₃₅^k₃₆^k₄₁^k₄₂^k₄₃^k₄₅^k₄₆^k₄₈^k₅^k₅₂^k₅₄^k₅₅^k₅₇^k₆₀^k₆₁^k₆₂^k₉=1 1^k₁^k₁₃^k₁₅^k₁₇^k₂₀^k₂₁^k₂₄^k₂₈^k₃^k₃₃^k₃₆^k₃₇^k₄^k₄₀^k₄₆^k₄₇^k₄₈^k₄₉^k₅₄^k₅₈^k₆^k₆₁^k₆₂^k₇^k₈=1 k₀^k₁₂^k₁₄^k₁₆^k₁₉^k₂^k₂₀^k₂₃^k₂₇^k₃^k₃₂^k₃₅^k₃₆^k₃₉^k₄₅^k₄₆^k₄₇^k₄₈^k₅^k₅₃^k₅₇^k₆^k₆₀^k₆₁^k₆₃^k₇=1 1^k₁^k₁₀^k₁₁^k₁₅^k₁₆^k₁₈^k₂^k₂₂^k₂₄^k₂₅^k₂₆^k₂₇^k₃^k₃₂^k₃₆^k₃₇^k₃₈^k₄^k₄₁^k₄₂^k₄₇^k₄₈^k₄₉^k₅^k₅₁^k₅₂^k₅₃^k₅₈^k₇=0 1^k₀^k₁^k₁₃^k₁₄^k₁₅^k₁₆^k₁₇^k₁₉^k₂^k₂₁^k₂₃^k₂₆^k₂₇^k₃₂^k₃₄^k₄^k₄₀^k₄₂^k₄₄^k₄₅^k₄₇^k₄₉^k₅₀^k₅₂^k₅₃^k₅₆^k₅₇^k₅₈^k₅₉^k₆₀^k₆₂^k₇^k₉=1 1^k₀^k₁^k₁₂^k₁₃^k₁₄^k₁₅^k₁₆^k₁₈^k₂₀^k₂₂^k₂₅^k₂₆^k₃^k₃₁^k₃₃^k₃₉^k₄₁^k₄₃^k₄₄^k₄₆^k₄₈^k₄₉^k₅₁^k₅₂^k₅₅^k₅₆^k₅₇^k₅₈^k₅₉^k₆^k₆₁^k₈=0 k₀^k₁₁^k₁₂^k₁₃^k₁₄^k₁₅^k₁₇^k₁₉^k₂^k₂₁^k₂₄^k₂₅^k₃₀^k₃₂^k₃₈^k₄₀^k₄₂^k₄₃^k₄₅^k₄₇^k₄₈^k₅^k₅₀^k₅₁^k₅₄^k₅₅^k₅₆^k₅₇^k₅₈^k₆₀^k₇=1 1^k₁^k₁₁^k₁₂^k₁₄^k₁₈^k₁₉^k₂₀^k₂₃^k₂₅^k₂₇^k₂₉^k₃^k₃₂^k₃₄^k₃₅^k₃₆^k₃₉^k₄^k₄₅^k₄₇^k₄₈^k₅₀^k₅₁^k₅₄^k₅₅^k₅₇^k₅₈^k₆₀^k₆₂^k₆₃^k₇=0 1^k₀^k₁₁^k₁₆^k₁₇^k₁₈^k₂^k₂₂^k₂₅^k₂₆^k₂₇^k₂₈^k₃₂^k₃₃^k₃₆^k₃₇^k₃₈^k₄₁^k₄₂^k₄₅^k₄₇^k₄₈^k₅₀^k₅₁^k₅₄^k₅₇^k₅₈^k₆₀^k₆₁^k₆₃^k₇=0 1^k₁^k₁₃^k₁₅^k₁₇^k₁₉^k₂₁^k₂₆^k₃^k₃₄^k₄₀^k₄₂^k₄₅^k₄₇^k₄₈^k₅₀^k₅₁^k₅₇^k₅₈^k₆₃^k₇=0 1^k₀^k₁₀^k₁₂^k₁₃^k₁₄^k₁₈^k₁₉^k₂^k₂₀^k₂₄^k₂₇^k₃^k₃₁^k₃₂^k₃₃^k₃₄^k₃₅^k₃₆^k₃₇^k₃₉^k₄₂^k₄₅^k₄₇^k₄₈^k₅₀^k₅₁^k₅₃^k₅₇^k₅₈^k₅₉^k₆₀^k₇=0 1^k₁^k₁₀^k₁₁^k₁₂^k₁₆^k₁₇^k₁₈^k₂^k₂₃^k₂₄^k₂₅^k₂₆^k₂₇^k₃^k₃₀^k₃₃^k₃₇^k₃₈^k₄₂^k₄₅^k₄₇^k₄₈^k₅₀^k₅₁^k₅₂^k₅₃^k₅₇^k₆₀^k₆₂^k₇^k₉=1 1^k₀^k₁^k₁₀^k₁₁^k₁₅^k₁₆^k₁₇^k₂^k₂₂^k₂₃^k₂₄^k₂₅^k₂₆^k₂₉^k₃₂^k₃₆^k₃₇^k₄₁^k₄₄^k₄₆^k₄₇^k₄₉^k₅₀^k₅₁^k₅₂^k₅₆^k₅₉^k₆^k₆₁^k₆₃^k₈^k₉=1 1^k₀^k₁^k₁₀^k₁₄^k₁₅^k₁₆^k₂₁^k₂₂^k₂₃^k₂₄^k₂₅^k₂₈^k₃₁^k₃₅^k₃₆^k₄₀^k₄₃^k₄₅^k₄₆^k₄₈^k₄₉^k₅^k₅₀^k₅₁^k₅₅^k₅₈^k₆₀^k₆₂^k₆₃^k₇^k₈^k₉=1 k₀^k₁₃^k₁₄^k₁₅^k₂₀^k₂₁^k₂₂^k₂₃^k₂₄^k₂₇^k₃₀^k₃₄^k₃₅^k₃₉^k₄^k₄₂^k₄₄^k₄₅^k₄₇^k₄₈^k₄₉^k₅₀^k₅₄^k₅₇^k₅₉^k₆^k₆₁^k₆₂^k₇^k₈^k₉=0 k₁₀^k₁₂^k₁₄^k₁₆^k₂₀^k₂₁^k₂₂^k₂₃^k₂₄^k₂₅^k₂₆^k₂₇^k₂₉^k₃₁^k₃₂^k₃₃^k₃₅^k₃₆^k₃₇^k₃₈^k₄₂^k₄₃^k₄₅^k₄₇^k₅^k₅₁^k₅₉^k₆₁^k₆₂^k₆₃^k₈=1 k₁₀^k₁₁^k₁₅^k₁₆^k₂₀^k₂₁^k₂₂^k₂₃^k₂₆^k₂₇^k₂₈^k₃^k₃₀^k₄^k₄₅^k₄₈^k₄₉^k₅₀^k₅₁^k₅₃^k₅₆^k₅₉^k₆^k₆₁^k₉=0 k₁₃^k₁₄^k₁₅^k₁₆^k₂^k₂₀^k₂₁^k₂₂^k₂₄^k₂₆^k₂₉^k₃₁^k₃₂^k₃₄^k₃₅^k₃₆^k₃₇^k₄₁^k₄₂^k₄₅^k₄₆^k₄₇^k₅^k₅₀^k₅₁^k₅₂^k₅₃^k₅₅^k₅₆^k₅₉^k₆^k₆₂^k₇^k₈^k₉=0 k₁^k₁₂^k₁₃^k₁₄^k₁₅^k₁₉^k₂₀^k₂₁^k₂₃^k₂₅^k₂₈^k₃₀^k₃₁^k₃₃^k₃₄^k₃₅^k₃₆^k₄^k₄₀^k₄₁^k₄₄^k₄₅^k₄₆^k₄₉^k₅^k₅₀^k₅₁^k₅₂^k₅₄^k₅₅^k₅₈^k₆^k₆₁^k₇^k₈=0 1^k₀^k₁₀^k₁₁^k₁₂^k₁₄^k₁₆^k₁₈^k₂₀^k₂₂^k₂₅^k₂₉^k₃₀^k₃₁^k₃₃^k₃₆^k₃₇^k₃₉^k₄^k₄₀^k₄₁^k₄₂^k₄₃^k₄₆^k₅^k₅₀^k₅₄^k₅₆^k₅₇^k₅₈^k₅₉^k₆₂^k₆₃=0 1^k₁₁^k₁₅^k₁₆^k₁₇^k₂₁^k₂₅^k₂₇^k₂₈^k₂₉^k₃₀^k₃₁^k₃₄^k₃₇^k₃₈^k₃₉^k₄^k₄₀^k₄₄^k₄₆^k₄₈^k₅₁^k₅₅^k₅₇^k₅₉^k₆^k₆₀^k₆₁^k₇^k₉=0 k₁₃^k₁₄^k₁₅^k₁₉^k₂₀^k₂₅^k₂₆^k₂₈^k₂₉^k₃₀^k₃₁^k₃₂^k₃₃^k₃₄^k₃₅^k₃₈^k₃₉^k₄₁^k₄₂^k₄₃^k₄₄^k₄₆^k₄₇^k₄₈^k₄₉^k₅^k₅₀^k₅₁^k₅₃^k₅₄^k₆₂^k₇^k₈=0 k₁₀^k₁₂^k₁₄^k₁₆^k₁₈^k₂₈^k₂₉^k₃^k₃₀^k₃₃^k₃₅^k₃₆^k₃₈^k₄^k₄₀^k₄₃^k₄₄^k₄₇^k₅₀^k₅₁^k₅₂^k₅₆^k₅₈^k₅₉^k₆₀^k₆₁^k₆₂=0 1^k₁₀^k₁₁^k₁₅^k₁₆^k₁₇^k₁₉^k₂^k₂₄^k₂₅^k₂₈^k₂₉^k₃₁^k₃₆^k₃₉^k₄₁^k₄₃^k₄₄^k₄₅^k₄₈^k₅₀^k₅₃^k₅₅^k₅₆^k₅₇^k₆^k₆₁^k₆₂^k₆₃^k₇^k₉=1 k₁^k₁₀^k₁₄^k₁₅^k₁₆^k₁₈^k₂₃^k₂₄^k₂₇^k₂₈^k₃₀^k₃₅^k₃₈^k₄₀^k₄₂^k₄₃^k₄₄^k₄₇^k₄₉^k₅^k₅₂^k₅₄^k₅₅^k₅₆^k₆^k₆₀^k₆₁^k₆₂^k₈^k₉=1 1^k₀^k₁₀^k₁₄^k₁₅^k₁₆^k₁₇^k₁₉^k₂₂^k₂₃^k₂₄^k₂₅^k₂₆^k₂₉^k₃^k₃₁^k₃₂^k₃₅^k₃₆^k₃₉^k₄^k₄₃^k₄₄^k₄₅^k₄₉^k₅^k₅₄^k₅₅^k₅₆^k₅₈^k₆^k₆₁^k₆₂^k₆₃^k₈^k₉=0 1^k₁₃^k₁₄^k₁₅^k₁₆^k₁₈^k₂^k₂₁^k₂₂^k₂₃^k₂₄^k₂₅^k₂₈^k₃^k₃₀^k₃₁^k₃₄^k₃₅^k₃₈^k₄^k₄₂^k₄₃^k₄₄^k₄₈^k₅^k₅₃^k₅₄^k₅₅^k₅₇^k₆₀^k₆₁^k₆₂^k₇^k₈^k₉=0 k₁^k₁₂^k₁₃^k₁₄^k₁₅^k₁₇^k₂^k₂₀^k₂₁^k₂₂^k₂₃^k₂₄^k₂₇^k₂₉^k₃^k₃₀^k₃₃^k₃₄^k₃₇^k₄^k₄₁^k₄₂^k₄₃^k₄₇^k₅₂^k₅₃^k₅₄^k₅₆^k₅₉^k₆^k₆₀^k₆₁^k₇^k₈=1 k₀^k₁^k₁₁^k₁₂^k₁₃^k₁₄^k₁₆^k₁₉^k₂^k₂₀^k₂₁^k₂₂^k₂₃^k₂₆^k₂₈^k₂₉^k₃^k₃₂^k₃₃^k₃₆^k₄₀^k₄₁^k₄₂^k₄₆^k₅^k₅₁^k₅₂^k₅₃^k₅₅^k₅₈^k₅₉^k₆^k₆₀^k₆₃^k₇=0 k₀^k₁^k₁₁^k₁₂^k₁₅^k₁₆^k₁₈^k₂^k₂₀^k₂₁^k₂₂^k₂₄^k₂₈^k₃^k₃₄^k₃₆^k₃₇^k₃₉^k₄^k₄₀^k₄₂^k₄₄^k₄₆^k₄₈^k₄₉^k₅^k₅₀^k₅₂^k₅₃^k₅₄^k₅₆^k₅₇^k₆₀^k₆₃^k₇=1 1^k₀^k₁^k₁₀^k₁₁^k₁₄^k₁₅^k₁₇^k₁₉^k₂^k₂₀^k₂₁^k₂₃^k₂₇^k₃^k₃₃^k₃₅^k₃₆^k₃₈^k₃₉^k₄^k₄₁^k₄₃^k₄₅^k₄₇^k₄₈^k₄₉^k₅₁^k₅₂^k₅₃^k₅₅^k₅₆^k₅₉^k₆^k₆₂^k₆₃=1 1^k₀^k₁^k₁₀^k₁₃^k₁₄^k₁₆^k₁₈^k₁₉^k₂^k₂₀^k₂₂^k₂₆^k₃^k₃₂^k₃₄^k₃₅^k₃₇^k₃₈^k₄₀^k₄₂^k₄₄^k₄₆^k₄₇^k₄₈^k₅^k₅₀^k₅₁^k₅₂^k₅₄^k₅₅^k₅₈^k₆₁^k₆₂^k₉=1 1^k₀^k₁^k₁₀^k₁₂^k₁₅^k₁₆^k₁₇^k₁₈^k₂^k₂₁^k₂₄^k₂₇^k₃^k₃₂^k₃₃^k₃₅^k₃₉^k₄^k₄₂^k₄₃^k₄₄^k₄₇^k₄₈^k₅₀^k₅₄^k₅₆^k₅₇^k₅₈^k₅₉^k₆^k₆₁^k₆₂^k₇^k₈^k₉=1 1^k₀^k₁^k₁₀^k₁₁^k₁₃^k₁₄^k₁₅^k₁₇^k₁₉^k₂^k₂₀^k₂₃^k₂₄^k₂₅^k₂₆^k₂₇^k₃₅^k₃₆^k₃₇^k₃₈^k₄₃^k₄₄^k₄₅^k₄₇^k₄₈^k₅^k₅₁^k₅₅^k₅₇^k₅₉^k₆₁^k₆₂^k₈^k₉=1 1^k₀^k₁^k₁₂^k₁₄^k₁₈^k₂₂^k₂₃^k₂₆^k₂₇^k₃^k₃₁^k₃₂^k₄^k₄₁^k₄₃^k₄₅^k₄₇^k₄₈^k₄₉^k₅₀^k₅₁^k₅₃^k₅₄^k₅₉^k₆^k₆₁^k₆₂^k₆₃^k₈^k₉=1 1^k₀^k₁₁^k₁₃^k₁₇^k₂^k₂₁^k₂₂^k₂₅^k₂₆^k₃^k₃₀^k₃₁^k₄₀^k₄₂^k₄₄^k₄₆^k₄₇^k₄₈^k₄₉^k₅^k₅₀^k₅₂^k₅₃^k₅₈^k₆₀^k₆₁^k₆₂^k₇^k₈=1 k₁^k₁₀^k₁₂^k₁₆^k₂^k₂₀^k₂₁^k₂₄^k₂₅^k₂₉^k₃₀^k₃₉^k₄^k₄₁^k₄₃^k₄₅^k₄₆^k₄₇^k₄₈^k₄₉^k₅₁^k₅₂^k₅₇^k₅₉^k₆^k₆₀^k₆₁^k₆₃^k₇=0 1^k₀^k₁^k₁₁^k₁₅^k₁₉^k₂₀^k₂₃^k₂₄^k₂₈^k₂₉^k₃^k₃₈^k₄₀^k₄₂^k₄₄^k₄₅^k₄₆^k₄₇^k₄₈^k₅^k₅₀^k₅₁^k₅₆^k₅₈^k₅₉^k₆^k₆₀^k₆₂^k₉=1 1^k₀^k₁₀^k₁₄^k₁₈^k₁₉^k₂^k₂₂^k₂₃^k₂₇^k₂₈^k₃₇^k₃₉^k₄^k₄₁^k₄₃^k₄₄^k₄₅^k₄₆^k₄₇^k₄₉^k₅^k₅₀^k₅₅^k₅₇^k₅₈^k₅₉^k₆₁^k₈=0 k₁^k₁₃^k₁₇^k₁₈^k₂₁^k₂₂^k₂₆^k₂₇^k₃^k₃₆^k₃₈^k₄^k₄₀^k₄₂^k₄₃^k₄₄^k₄₅^k₄₆^k₄₈^k₄₉^k₅₄^k₅₆^k₅₇^k₅₈^k₆₀^k₇^k₉=1 k₀^k₁₀^k₁₂^k₁₃^k₁₇^k₁₉^k₂^k₂₀^k₂₁^k₂₄^k₂₆^k₂₇^k₃₁^k₃₂^k₃₄^k₃₆^k₃₉^k₄₃^k₄₆^k₄₇^k₄₉^k₅₁^k₅₅^k₅₇^k₅₈^k₆₀^k₆₂^k₆₃^k₇^k₈=1 1^k₁^k₁₀^k₁₁^k₁₂^k₁₃^k₁₈^k₂₀^k₂₃^k₂₄^k₂₆^k₂₇^k₃^k₃₀^k₃₂^k₃₃^k₃₄^k₃₆^k₃₇^k₃₈^k₄₁^k₄₄^k₄₉^k₅₀^k₅₁^k₅₃^k₅₄^k₅₇^k₅₈^k₆₀^k₆₁^k₆₃^k₉=0 1^k₀^k₁₀^k₁₁^k₁₂^k₁₇^k₁₉^k₂^k₂₂^k₂₃^k₂₅^k₂₆^k₂₉^k₃₁^k₃₂^k₃₃^k₃₅^k₃₆^k₃₇^k₄₀^k₄₃^k₄₈^k₄₉^k₅₀^k₅₂^k₅₃^k₅₆^k₅₇^k₅₉^k₆₀^k₆₂^k₈^k₉=0 1^k₁^k₁₁^k₁₃^k₁₈^k₁₉^k₂₁^k₂₂^k₂₇^k₂₈^k₃^k₃₀^k₃₇^k₃₉^k₄₁^k₄₄^k₄₅^k₄₆^k₄₇^k₅₂^k₅₃^k₅₅^k₆^k₆₀^k₆₁^k₆₂^k₈^k₉=1 k₀^k₁₀^k₁₂^k₁₇^k₁₈^k₂^k₂₀^k₂₁^k₂₆^k₂₇^k₂₉^k₃₆^k₃₈^k₄₀^k₄₃^k₄₄^k₄₅^k₄₆^k₅^k₅₁^k₅₂^k₅₄^k₅₉^k₆₀^k₆₁^k₆₃^k₇^k₈=0 1^k₁^k₁₀^k₁₁^k₁₃^k₁₇^k₂₀^k₂₄^k₂₆^k₂₇^k₂₈^k₃^k₃₁^k₃₂^k₃₄^k₃₆^k₃₉^k₄^k₄₁^k₄₃^k₄₆^k₄₈^k₄₉^k₅₀^k₅₆^k₉=1 1^k₀^k₁₂^k₁₃^k₂^k₂₃^k₂₄^k₂₆^k₃₀^k₃₂^k₃₃^k₃₄^k₃₆^k₃₇^k₃₈^k₄₀^k₄₁^k₄₄^k₄₆^k₄₇^k₅₁^k₅₃^k₅₅^k₅₆^k₅₈^k₅₉^k₆^k₆₀^k₆₂^k₇^k₈^k₉=0 k₁^k₁₀^k₁₁^k₁₂^k₁₃^k₁₆^k₁₉^k₂₂^k₂₃^k₂₄^k₂₇^k₂₉^k₃^k₃₃^k₃₄^k₃₉^k₄₀^k₄₁^k₄₂^k₄₃^k₄₄^k₄₈^k₄₉^k₅^k₅₀^k₅₁^k₅₂^k₅₃^k₅₄^k₅₅^k₅₆^k₅₇^k₆₀^k₆₁^k₆₂^k₆₃^k₈=0 1^k₀^k₁₁^k₁₂^k₁₃^k₁₅^k₁₆^k₁₈^k₁₉^k₂^k₂₁^k₂₂^k₂₃^k₂₄^k₂₅^k₂₆^k₂₇^k₂₈^k₃^k₃₁^k₃₃^k₃₄^k₃₅^k₃₆^k₃₇^k₃₈^k₃₉^k₄^k₄₀^k₄₃^k₄₄^k₄₅^k₄₆^k₄₇^k₅₀^k₅₂^k₅₄^k₅₅^k₅₈^k₆^k₆₁^k₉=0 k₁^k₁₁^k₁₂^k₁₃^k₁₄^k₁₅^k₁₆^k₁₇^k₁₈^k₁₉^k₂^k₂₀^k₂₁^k₂₂^k₂₃^k₂₆^k₃₀^k₃₁^k₃₃^k₃₈^k₃₉^k₄₁^k₄₃^k₄₈^k₅^k₅₄^k₅₆^k₅₇^k₅₈^k₅₉^k₆^k₆₂^k₇^k₈=0 k₀^k₁^k₁₀^k₁₁^k₁₂^k₁₃^k₁₄^k₁₅^k₁₆^k₁₇^k₁₈^k₁₉^k₂₀^k₂₁^k₂₂^k₂₅^k₂₉^k₃₀^k₃₂^k₃₇^k₃₈^k₄^k₄₀^k₄₂^k₄₇^k₅^k₅₃^k₅₅^k₅₆^k₅₇^k₅₈^k₆^k₆₁^k₇=1 1^k₀^k₁₁^k₁₂^k₁₄^k₁₅^k₁₇^k₁₈^k₂₀^k₂₁^k₂₅^k₂₇^k₂₈^k₂₉^k₃₂^k₃₄^k₃₅^k₃₉^k₄^k₄₂^k₄₄^k₄₅^k₄₈^k₄₉^k₅^k₅₁^k₅₂^k₅₃^k₅₄^k₅₅^k₅₇^k₅₈^k₅₉^k₆₂^k₆₃^k₇^k₉=1 k₁₁^k₁₄^k₁₇^k₂₀^k₂₅^k₂₆^k₂₈^k₃₂^k₃₃^k₃₅^k₃₆^k₃₇^k₃₈^k₄^k₄₂^k₄₃^k₄₅^k₄₆^k₄₇^k₄₉^k₅₀^k₅₂^k₅₄^k₅₇^k₅₉^k₆₀^k₆₁^k₆₃^k₇^k₈=0

You might notice that we can rid the left side the equations of constants by XOR'ing, and that the terms can be sorted. This is taken care of in gen_equations.py before producing the pari/gp matrix declarations. Equation matrix as A and column vector of desired values as B:

A=[ 0,1,0,1,1,1,0,1,0,0,1,0,1,0,1,1,0,1,1,1,0,1,1,0,0,0,1,1,1,1,0,1,1,0,0,0,1,0,1,1,0,0,0,0,1,0,0,1,0,0,1,0,0,1,0,0,1,1,0,0,1,0,0,0;1,1,1,1,0,0,1,1,1,0,1,1,1,1,1,0,1,1,0,0,1,1,0,1,0,0,1,0,0,0,1,1,0,1,0,0,1,1,1,0,1,0,0,0,1,1,0,1,1,0,1,1,0,1,1,0,1,0,1,0,1,1,0,0;0,0,1,0,0,1,0,0,1,1,1,1,0,1,0,0,0,0,0,1,0,0,0,0,1,0,1,0,1,1,0,0,0,0,1,0,1,1,0,0,0,1,0,0,1,1,1,1,1,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0;1,1,0,0,1,1,1,1,0,1,0,1,0,0,0,1,0,1,1,1,1,1,1,0,0,1,1,0,1,0,1,1,1,0,0,1,1,1,0,1,0,0,1,0,1,1,1,0,1,1,0,1,1,0,1,1,0,0,0,0,0,1,1,1;1,1,1,0,0,1,1,1,1,0,1,0,1,0,0,0,1,0,1,1,1,1,1,1,0,0,1,1,0,1,0,1,1,1,0,0,1,1,1,0,1,0,0,1,0,1,1,1,0,1,1,0,1,1,0,1,1,0,0,0,0,0,1,1;1,0,1,0,1,1,1,0,1,1,1,1,1,1,1,1,0,0,1,0,1,0,0,1,1,0,1,0,0,1,1,1,0,1,1,0,1,1,0,0,0,1,0,0,0,0,1,0,1,0,0,1,0,0,1,0,0,0,0,0,1,0,0,1;0,0,0,0,1,0,1,0,0,1,0,1,0,1,0,0,1,1,1,0,0,0,1,0,1,1,1,0,1,1,1,0,0,0,1,1,1,1,0,1,0,0,1,0,1,0,0,0,0,1,1,0,1,1,0,1,1,1,0,0,1,1,0,0;1,1,0,1,1,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,1,1,1,0,1,0,0,1,0,1,0,1,0,0,1,0,1,0,1,1,0,0,1,1,1,0,1,0,0,0,1,0,0,1,0,0,0,1,0,1,1,1,0;1,0,1,1,0,0,0,1,0,0,1,0,1,0,1,1,1,1,1,1,0,1,0,1,1,0,0,1,1,0,0,0,1,1,0,0,0,0,0,1,1,1,0,0,0,1,1,1,1,0,1,0,1,1,0,1,1,1,0,1,1,1,1,1;0,0,0,0,0,1,0,1,1,0,1,1,1,1,1,0,1,0,0,0,1,1,0,0,1,1,1,1,0,0,0,1,1,1,1,0,1,0,1,1,1,1,1,0,1,0,1,0,1,1,1,1,0,0,1,0,0,0,1,0,0,1,1,1;0,1,0,1,1,1,1,1,1,1,1,1,0,1,0,0,0,0,1,1,0,0,0,0,0,1,0,0,0,1,0,1,0,1,1,1,1,1,1,0,1,1,1,1,1,1,0,0,0,1,0,1,1,1,0,1,1,1,0,1,1,0,1,1;0,1,1,1,0,0,1,0,1,1,0,1,0,0,0,1,0,1,1,0,1,1,1,0,0,0,0,1,1,1,1,1,0,0,1,1,0,1,0,0,0,1,1,1,0,1,1,1,0,0,0,0,1,0,1,0,0,0,1,0,0,1,0,1;0,1,1,0,0,1,0,0,0,1,0,0,0,0,1,1,1,1,0,0,0,0,0,1,0,0,1,1,0,0,1,0,0,0,0,1,0,0,0,1,0,0,1,1,0,0,1,0,1,0,1,0,0,0,0,1,1,1,0,1,1,0,1,0;1,0,1,1,0,0,1,0,0,0,1,0,0,0,0,1,1,1,1,0,0,0,0,0,1,0,0,1,1,0,0,1,0,0,0,0,1,0,0,0,1,0,0,1,1,0,0,1,0,1,0,1,0,0,0,0,1,1,1,0,1,1,0,1;0,0,0,0,0,1,0,0,0,0,1,1,1,0,1,1,1,0,0,0,0,1,1,0,0,1,1,1,0,0,0,1,0,0,0,0,1,1,1,1,0,1,0,0,0,1,0,1,1,0,0,0,1,1,0,0,1,0,1,1,1,1,1,0;0,1,0,1,1,1,1,1,0,0,1,1,0,1,1,0,1,0,1,1,0,1,0,1,0,0,0,0,0,1,0,1,0,0,0,0,1,1,0,0,1,0,1,0,1,0,1,1,1,1,1,0,0,0,1,0,1,0,0,1,0,1,1,1;0,0,1,0,1,1,1,1,1,0,0,1,1,0,1,1,0,1,0,1,1,0,1,0,1,0,0,0,0,0,1,0,1,0,0,0,0,1,1,0,0,1,0,1,0,1,0,1,1,1,1,1,0,0,0,1,0,1,0,0,1,0,1,1;0,0,0,1,0,1,1,1,1,1,0,0,1,1,0,1,1,0,1,0,1,1,0,1,0,1,0,0,0,0,0,1,0,1,0,0,0,0,1,1,0,0,1,0,1,0,1,0,1,1,1,1,1,0,0,0,1,0,1,0,0,1,0,1;1,1,0,1,0,1,1,0,1,1,0,0,1,1,0,1,1,0,1,0,0,0,0,0,1,0,0,1,1,1,0,1,0,0,1,0,1,0,1,0,1,0,0,1,1,1,0,0,0,1,0,1,1,0,0,0,1,0,0,1,1,0,1,0;1,0,1,1,0,1,1,0,0,1,0,0,1,1,0,1,1,0,1,0,0,1,1,0,0,1,1,1,0,0,1,1,0,0,0,1,1,1,1,0,0,1,0,0,0,1,1,1,0,0,0,0,1,0,0,0,1,0,0,0,0,1,0,1;1,0,0,0,0,1,1,0,0,0,0,0,1,1,0,1,1,0,1,0,0,1,0,1,0,0,0,0,0,1,0,0,0,0,0,0,0,1,0,0,0,0,1,0,1,0,1,0,1,0,1,0,0,0,0,0,1,0,0,0,1,0,1,0;0,0,0,1,1,1,1,0,0,0,1,0,1,1,0,1,1,0,1,0,0,1,0,0,1,0,1,1,1,1,1,1,1,0,0,0,1,0,0,1,0,0,0,1,1,1,0,0,0,1,1,1,0,1,0,0,1,0,0,0,1,1,0,1;0,1,0,1,0,0,1,0,0,0,1,1,1,1,0,1,1,0,1,0,0,1,0,0,0,1,1,0,0,0,1,0,0,1,0,0,1,1,1,1,1,0,0,0,0,1,1,1,0,0,0,1,1,1,1,0,1,0,0,0,1,1,1,0;1,0,1,0,1,0,0,1,0,0,0,1,1,1,1,0,1,1,0,1,0,0,1,0,0,0,1,1,0,0,0,1,0,0,1,0,0,1,1,1,1,1,0,0,0,0,1,1,1,0,0,0,1,1,1,1,0,1,0,0,0,1,1,1;1,1,0,1,0,1,0,0,1,0,0,0,1,1,1,1,0,1,1,0,1,0,0,1,0,0,0,1,1,0,0,0,1,0,0,1,0,0,1,1,1,1,1,0,0,0,0,1,1,1,0,0,0,1,1,1,1,0,1,0,0,0,1,1;0,1,1,0,1,0,1,0,0,1,0,0,0,1,1,1,1,0,1,1,0,1,0,0,1,0,0,0,1,1,0,0,0,1,0,0,1,0,0,1,1,1,1,1,0,0,0,0,1,1,1,0,0,0,1,1,1,1,0,1,0,0,0,1;1,1,1,0,1,0,0,0,0,0,0,0,1,0,0,0,1,0,1,0,1,1,0,0,0,1,1,1,1,0,1,1,1,0,1,0,1,1,1,1,1,1,1,1,0,0,0,1,0,1,0,1,0,1,0,1,0,0,1,0,0,0,0,0;0,0,1,0,1,0,0,1,0,0,1,0,1,1,1,1,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,1,1,1,0,0,1,1,1,1,0,0,0,1,1,0,0,0,1,1,1,0,0,1,0,1,1,0,0,0;0,1,0,0,1,0,0,1,1,0,1,1,1,1,0,0,1,1,1,0,0,1,1,0,0,0,1,1,1,1,0,1,1,0,1,0,0,1,0,1,0,1,1,1,0,0,0,1,1,1,1,0,0,0,1,1,1,1,1,0,0,1,0,0;0,0,1,0,0,1,0,0,1,1,0,1,1,1,1,0,0,1,1,1,0,0,1,1,0,0,0,1,1,1,1,0,1,1,0,1,0,0,1,0,1,0,1,1,1,0,0,0,1,1,1,1,0,0,0,1,1,1,1,1,0,0,1,0;1,1,0,0,1,1,1,1,0,1,0,0,0,1,0,0,0,1,0,0,1,1,1,1,1,0,1,1,0,0,1,0,1,1,1,0,0,0,1,0,0,1,0,1,0,1,0,1,0,1,0,1,1,1,0,0,0,0,1,1,0,0,0,1;0,0,1,1,1,0,1,0,1,0,0,0,1,0,0,1,0,1,0,1,0,0,0,1,1,1,1,0,0,1,0,0,1,1,1,1,1,0,1,0,0,0,1,0,0,0,1,1,1,0,0,0,1,0,1,0,1,1,0,1,0,0,0,0;0,1,0,0,0,0,0,0,0,1,1,0,1,1,1,1,1,1,0,1,1,1,1,0,1,1,0,0,1,1,1,1,1,1,1,1,0,1,1,0,0,0,0,1,1,0,0,0,1,1,1,0,0,0,0,1,1,0,1,0,0,0,0,0;0,1,1,1,1,1,0,1,0,0,0,1,1,1,0,0,1,0,0,1,1,0,0,1,0,1,0,1,1,0,1,0,0,1,1,1,0,0,0,0,0,0,0,0,0,1,0,1,0,1,0,1,0,1,0,0,0,0,0,1,1,0,0,0;1,1,1,0,0,0,1,1,1,0,1,0,0,1,0,1,0,0,1,1,1,0,1,0,1,0,0,1,0,0,0,0,1,0,1,1,0,0,1,1,0,0,0,0,1,0,1,1,1,0,0,0,1,1,1,0,1,1,0,0,0,1,0,0;0,1,1,1,0,0,0,1,1,1,0,1,0,0,1,0,1,0,0,1,1,1,0,1,0,1,0,0,1,0,0,0,0,1,0,1,1,0,0,1,1,0,0,0,0,1,0,1,1,1,0,0,0,1,1,1,0,1,1,0,0,0,1,0;1,1,1,0,0,1,0,1,1,1,0,0,0,0,1,0,0,0,1,1,1,0,0,0,1,0,0,1,1,0,0,1,1,0,1,0,0,1,1,1,1,1,0,0,1,0,1,1,1,1,0,0,0,1,1,1,0,1,1,1,1,0,0,1;0,1,1,1,0,0,1,0,1,1,1,0,0,0,0,1,0,0,0,1,1,1,0,0,0,1,0,0,1,1,0,0,1,1,0,1,0,0,1,1,1,1,1,0,0,1,0,1,1,1,1,0,0,0,1,1,1,0,1,1,1,1,0,0;0,0,1,1,1,0,0,1,0,1,1,1,0,0,0,0,1,0,0,0,1,1,1,0,0,0,1,0,0,1,1,0,0,1,1,0,1,0,0,1,1,1,1,1,0,0,1,0,1,1,1,1,0,0,0,1,1,1,0,1,1,1,1,0;1,0,0,1,1,1,0,0,1,0,1,1,1,0,0,0,0,1,0,0,0,1,1,1,0,0,0,1,0,0,1,1,0,0,1,1,0,1,0,0,1,1,1,1,1,0,0,1,0,1,1,1,1,0,0,0,1,1,1,0,1,1,1,1;1,0,0,1,0,0,1,1,0,1,1,1,0,1,1,1,0,1,0,1,0,1,0,1,1,0,1,1,0,1,0,0,0,0,0,1,0,0,0,1,0,1,1,1,0,1,0,1,1,0,0,1,1,0,0,0,1,0,1,1,1,1,1,1;1,1,0,0,1,0,0,1,1,0,1,1,1,0,1,1,1,0,1,0,1,0,1,0,1,1,0,1,1,0,1,0,0,0,0,0,1,0,0,0,1,0,1,1,1,0,1,0,1,1,0,0,1,1,0,0,0,1,0,1,1,1,1,1;0,1,1,0,0,1,0,0,1,1,0,1,1,1,0,1,1,1,0,1,0,1,0,1,0,1,1,0,1,1,0,1,0,0,0,0,0,1,0,0,0,1,0,1,1,1,0,1,0,1,1,0,0,1,1,0,0,0,1,0,1,1,1,1;0,1,1,0,1,1,1,1,0,1,0,0,0,1,0,1,1,0,0,1,1,1,0,0,1,0,0,0,1,0,1,1,0,0,0,0,1,0,0,1,0,0,1,0,0,1,1,1,1,0,0,1,0,1,1,1,1,1,0,1,1,1,1,1;0,1,1,0,1,0,1,0,1,0,0,0,1,0,0,1,1,0,1,1,1,0,0,0,0,1,1,1,1,0,0,0,0,0,0,0,1,1,1,1,1,0,0,1,1,0,1,0,1,1,1,0,1,1,1,1,0,0,1,0,0,1,1,1;1,1,1,0,1,0,0,0,0,1,1,0,1,1,1,1,1,0,1,0,1,0,1,0,0,0,0,0,0,0,0,1,1,0,0,0,1,1,0,0,1,1,0,0,0,1,0,0,0,1,0,1,0,0,1,1,0,1,0,1,1,0,1,1;0,1,1,1,0,1,0,0,0,0,1,1,0,1,1,1,1,1,0,1,0,1,0,1,0,0,0,0,0,0,0,0,1,1,0,0,0,1,1,0,0,1,1,0,0,0,1,0,0,0,1,0,1,0,0,1,1,0,1,0,1,1,0,1;1,0,1,1,1,0,1,0,0,0,0,1,1,0,1,1,1,1,1,0,1,0,1,0,1,0,0,0,0,0,0,0,0,1,1,0,0,0,1,1,0,0,1,1,0,0,0,1,0,0,0,1,0,1,0,0,1,1,0,1,0,1,1,0;0,1,0,1,1,1,0,1,0,0,0,0,1,1,0,1,1,1,1,1,0,1,0,1,0,1,0,0,0,0,0,0,0,0,1,1,0,0,0,1,1,0,0,1,1,0,0,0,1,0,0,0,1,0,1,0,0,1,1,0,1,0,1,1;0,0,1,0,1,1,1,0,1,0,0,0,0,1,1,0,1,1,1,1,1,0,1,0,1,0,1,0,0,0,0,0,0,0,0,1,1,0,0,0,1,1,0,0,1,1,0,0,0,1,0,0,0,1,0,1,0,0,1,1,0,1,0,1;0,0,0,1,0,1,1,1,0,1,0,0,0,0,1,1,0,1,1,1,1,1,0,1,0,1,0,1,0,0,0,0,0,0,0,0,1,1,0,0,0,1,1,0,0,1,1,0,0,0,1,0,0,0,1,0,1,0,0,1,1,0,1,0;1,1,0,1,0,1,1,0,1,0,0,0,1,0,1,0,1,1,0,0,1,0,0,0,1,0,0,1,0,1,0,1,1,0,0,0,1,1,0,1,0,0,1,1,1,0,1,0,0,0,1,1,0,1,0,1,1,0,0,0,0,1,0,1;1,0,1,1,0,1,1,0,0,1,1,0,1,1,1,0,0,0,0,1,0,0,1,0,0,1,1,1,0,1,1,1,0,1,0,0,1,1,0,1,1,0,0,1,0,1,0,0,0,0,1,1,1,1,1,0,0,0,0,0,1,0,1,0;0,1,0,1,1,0,1,1,0,0,1,1,0,1,1,1,0,0,0,0,1,0,0,1,0,0,1,1,1,0,1,1,1,0,1,0,0,1,1,0,1,1,0,0,1,0,1,0,0,0,0,1,1,1,1,1,0,0,0,0,0,1,0,1;0,1,1,1,0,0,0,0,1,0,1,1,0,0,0,0,1,1,1,1,0,0,1,0,1,0,1,0,0,0,0,0,0,1,0,1,1,0,0,0,0,1,1,0,1,1,0,0,0,0,1,0,1,0,1,1,0,1,0,0,1,0,1,0;1,0,1,1,1,0,0,0,0,1,0,1,1,0,0,0,0,1,1,1,1,0,0,1,0,1,0,1,0,0,0,0,0,0,1,0,1,1,0,0,0,0,1,1,0,1,1,0,0,0,0,1,0,1,0,1,1,0,1,0,0,1,0,1;0,0,0,0,0,0,0,1,0,0,0,0,0,1,1,1,0,1,0,0,1,0,1,0,1,0,0,1,0,1,0,1,1,0,0,1,1,1,0,1,0,0,0,1,0,0,1,0,0,0,1,0,1,1,1,0,0,0,0,1,1,0,1,0;0,1,0,1,1,1,0,1,1,0,1,0,1,0,0,0,1,1,0,1,0,0,1,1,0,1,1,1,0,1,1,1,0,1,0,0,0,1,0,1,1,0,0,0,0,0,0,0,0,0,1,1,0,0,1,1,1,1,0,0,0,1,0,1;1,1,1,1,0,0,1,1,1,1,1,1,1,1,1,1,0,0,0,1,1,1,1,1,1,0,0,0,0,1,1,0,0,0,1,0,1,0,0,1,1,1,0,0,1,0,0,1,0,0,1,1,1,1,0,1,0,0,1,0,1,0,1,0;0,0,1,0,0,1,0,0,1,1,0,1,0,1,0,0,1,1,1,1,1,0,0,1,1,1,1,1,1,1,1,0,1,0,0,1,1,1,1,1,1,1,1,0,1,1,0,1,1,0,1,1,1,0,1,0,0,1,0,1,1,1,0,1;0,1,0,0,1,1,1,1,0,1,0,0,0,0,0,1,0,0,0,0,1,0,1,0,1,1,0,0,0,0,1,0,1,1,0,0,0,1,0,0,1,1,1,1,1,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,0,1,1,0;0,0,1,0,0,1,1,1,1,0,1,0,0,0,0,0,1,0,0,0,0,1,0,1,0,1,1,0,0,0,0,1,0,1,1,0,0,0,1,0,0,1,1,1,1,1,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,0,1,1;1,1,0,0,1,1,1,0,1,1,1,1,1,0,1,1,0,0,1,1,0,1,0,0,1,0,0,0,1,1,0,1,0,0,1,1,1,0,1,0,0,0,1,1,0,1,1,0,1,1,0,1,1,0,1,0,1,0,1,1,0,0,0,1;1,0,1,1,1,0,1,0,0,1,0,1,0,1,1,0,1,1,1,0,1,1,0,0,0,1,1,1,1,0,1,1,0,0,0,1,0,1,1,0,0,0,0,1,0,0,1,0,0,1,0,0,1,0,0,1,1,0,0,1,0,0,0,0 ]*Mod(1,2)
B=[ 0;1;0;0;1;0;1;0;0;0;0;1;0;1;1;0;1;1;1;1;1;1;0;0;0;0;1;0;0;0;1;1;0;0;0;1;1;1;1;0;1;0;0;0;0;0;0;0;0;1;1;1;1;1;0;0;0;1;0;1;0;1;0;0 ]*Mod(1,2)

is that your final answer?

And then solve by inverting and multiplying:

? solution = A^-1 * B
? lift(solution)~
%9 =
[1 0 1 0 1 1 1 0 0 1 0 1 0 1 1 0 0 0 0 1 0 1 1 1 0 1 1 1 0 0 0 0 0 0 1 1 1 0 1 0 1 1 0 0 1 1 1 0 1 1 0 1 1 1 0 0 1 0 0 0 1 0 0 0]

Which are the bits of 0xAE 0x56 0x17 0x70 0x3A 0xCE 0xDC 0x88. When these values are supplied by key.txt and run hmac.py, you'll see that the HMAC of "zupe zecret" ends up being computed as 0xa57d43a032feb286 as given, and thus we're left to read the HMAC of "BKPCTF" which is 0xd2db2b8b9002841f, the final answer.