Solution for the ESET BlackHat US Challenge 2012

1.  Introduction

On July 21st 2012 at 7AM (Las Vegas time) ESET published a crack-me for the BlackHat US 2012 edition. Rules were simple: find a valid couple of serial numbers for a given name before July 26^th 2012 2PM to maybe win $1000 and a BlackCard (that gives you a free entry for either the next BlackHat US or EU).

Figure 1: GUI of the crack-me

According to challenge's site Eloi Vanderbeken from Oppida was the only person to solve it in time and won the price even if he was not at BlackHat US:

Figure 2: Result of the challenge

This post explains how Eloi achieved to break it.

2.  First steps

The crack-me is packed with UPX, so we first unpack it by using the upx -d command to study it under IDA Pro 6.3.

We quickly noticed that it was created with the MFC library, which explains the large size of the binary (1Mo packed and 2M unpacked) and facilitates its analysis with IDA:

Figure 3: Light blue parts are MFC functions recognized by IDA

A quick look in the referenced text string reveals the address of the function in charge of serials verification:

Figure 4:localization of the verification function

To simplify its analysis, we import the labels generated by IDA in OllyDbg by using exporting them in a map file and importing the .map file with GoDup, an OllyDbg plugin :

Figure 5: IDA labels imported in OllyDbg

Now we have located verification functions we can start to study them.

3.  First part

A quick analysis shows us that the serial is base64 decoded and must be composed of at least 0x3F characters once base64 decoded. It is then verified with the following algorithm :

def scramble(t) :     j = 0     for i in xrange(64) :         c = t[i]%80         j = (t[c%80] + j)%80         t[j], t[i] = t[i], t[j] exitFun = badBoy serialDecoded = serial.decode("base64") padding = ("ESETNOD32@"*8)[len(name):] H = hash512(name+padding) if serialDecoded[:64][::-1] != H :     return exitFun() scrambledTab = H for i, c in enumerate(serialDecoded) :     scrambledTab[i%64] ^= c scramble(scrambledTab) if scrambledTab[68 : 72] != [0xA, 0xB, 0xC, 0xD] :     exitFun = badBoy     return exitFun() if hash512(scrambledTab)[:12] != [0xCA, 0x8A, 0x57, 0x12, 0x78, 0xB6, 0xCA, 0xEF, 0x78, 0x56, 0x34, 0x12] :     return exitFun() exitFun = goodBoy return exitFun()

Figure 6:  First check of the serial in pseudo-python

The first part of the check is easy to satisfy, we just need to encode in base64 the reversed hash of the padded name. The second part is a little bit harder, at first sight it seems that we need to find a preimage attack on the hash function to satisfy the last check and to reverse the scramble function to find a valid serial.

After studying the code of the hash function, we found that the hash function was WhirlPool (thanks to the substitution table) and we did not find any backdoor in the code. It had to be something else.

A careful reader might have seen that scrambledTab is initialized with a 64 bytes array  (the hash of the name) but is then considered as a 80 bytes array in the scramble function. After redefining scrambledTab as a 80 bytes array in IDA, we saw that exitFun became scrambledTab[76:80]:

Figure 6: IDA disassembly after scrambledTab was redefined

Moreover BadBoy and GoodBoy functions' addresses differ only by the least significant byte (0x40 for the BadBoy function, 0x20 for the GoodBoy one) so if we can use the scramble function to rewrite the badboy's address least significant byte to 0x20 and write the good values ([0xA, 0xB, 0xC, 0xD]) in scrambledTab[68:72] we will have the good boy message and you will pass the first check.

To achieve this goal we wrote a little "intelligent" bruteforcer which, given an initial table of 64 unknown bytes followed by 16 fixed bytes (remember we only control the 64 first bytes) and a list of couples (offset, value_to_set) corresponding to the desired final state of the table, tries to set the  right bytes at the right place and next tries to not overwrite them.

Complete code to generate a valid first serial is the following:

import sys from random import SystemRandom from base64 import b64encode try :   from whirlpool import Whirlpool except :   print "To work this keygen need the Whirpool implementation located here : http://www.bjrn.se/code/whirlpoolpy.txt"   sys.exit(0) sec_rnd = SystemRandom() print "name :" name = sys.stdin.readline().rstrip("\r\n") hash_name = [ord(c) for c in Whirlpool(name+("ESETNOD32@"*8)[len(name):]).digest()] def step1(k, i, j, to_set, to_keep) :   if i > 63 :     if not to_set :       return k     return None   if to_set :     to_set_cpy = list(to_set)     sec_rnd.shuffle(to_set_cpy)     for choice, (idx, v) in enumerate(to_set_cpy) :       if k[i] == v :         r = step2a(idx, k, i, j, to_set_cpy[:choice] + to_set_cpy[choice+1:] , to_keep)         if r is not None :           return r       elif k[i] is None :         k[i] = v         r = step2a(idx, k, i, j, to_set_cpy[:choice] + to_set_cpy[choice+1:] , to_keep)         if r is not None :           return r         k[i] = None   r = step2b(k, i, j, to_set, to_keep)   if r is not None :     return r   return None def step2a(idx, k, i, j, to_set, to_keep) :   c = k[i] % 80   kc = k[c]   if kc is None :     if (idx - j)%80 in to_keep :       return None     kc = (idx - j)%80     while kc < 0x100 :       k[c] = kc       to_keep.add(idx)       r = step3(k, i, idx, to_set, to_keep)       to_keep.remove(idx)       if r is not None :         return r       kc += 80     k[c] = None   elif (kc + j)%80 == idx :     to_keep.add(idx)     r = step3(k, i, idx, to_set, to_keep)     to_keep.remove(idx)     return r   else :     return None def step2b(k, i, j, to_set, to_keep) :   c = k[i]   if c is None :     vals = [c for c in xrange(0x100) if k[c%80] is not None and (k[c%80] + j)%80 not in to_keep]     sec_rnd.shuffle(vals)     for c in vals :       k[i] = c       r = step3(k, i, (k[c%80] + j)%80, to_set, to_keep)       if r is not None:         return r     vals = [c for c in xrange(0x100) if k[c%80] is None]     sec_rnd.shuffle(vals)     for c in vals :       k[i] = c       c = c % 80       vals2 = [kc for kc in xrange(0x100) if (kc + j)%80 not in to_keep]       sec_rnd.shuffle(vals2)       for kc in vals2 :         k[c] = kc         r = step3(k, i, (kc + j)%80, to_set, to_keep)         if r is not None :           return r       k[c] = None     k[i] = None   else :     c %= 80     kc = k[c]     if kc is None :       vals = [kc for kc in xrange(0x100) if (kc + j)%80 not in to_keep]       sec_rnd.shuffle(vals)       for kc in vals :         k[c] = kc         r = step3(k, i, (kc + j)%80, to_set, to_keep)         if r is not None :           return r       k[c] = None     elif (kc + j)%80 not in to_keep :       return step3(k, i, (kc + j)%80, to_set, to_keep)   return None def step3(k, i, j, to_set, to_keep) :   k[i], k[j] = k[j], k[i]   r = step1(k, i+1, j, to_set, to_keep)   if r is not None :     r[i], r[j] = r[j], r[i]     return r   k[i], k[j] = k[j], k[i]   return None # initial table k = [None]*64+[0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x40, 0x17, 0x40, 0x00] # couple of values to set to_set = [(0x44, 0xA), (0x45, 0xB), (0x46, 0xC), (0x47, 0xD), (0x4C, 0x20)] # addresses that have to be keep (not modified) to_keep = set((0x4D, 0x4E, 0x4F)) s = step1(k, 0, 0, to_set, to_keep) # unused values can be set to any value for i in xrange(len(s)) :   if s[i] is None :     s[i] = sec_rnd.randint(0, 0xFF) serial = "".join(chr(i) for i in hash_name[::-1]) serial += "".join(chr(a^b^c) for a, b, c in zip(hash_name, hash_name[::-1], s)) print "serial 1 :" print serial.encode("base64").replace("\n","")

Figure 7: Code to generate a valid first serial (Python 2.7)

If you want to personalize the generated serial by appending it a constant string, you can use one of the following code, the first one adds some constraints to the generated table and generates a serial with a minimal length; the second one appends bytes to the serial but permits to add an arbitrary long string:

egg = "ElV++ESET++=" egg_d = egg.decode("base64") padd = 64 - len(egg_d) list_egg = [hash_name[padd+i]^hash_name[::-1][padd+i]^ord(c) for i,c in enumerate(egg_d)] k = [None]*padd+list_egg+[0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x40, 0x17, 0x40, 0x00] to_set = [(0x44, 0xA), (0x45, 0xB), (0x46, 0xC), (0x47, 0xD), (0x4C, 0x20)] to_keep = set((0x4D, 0x4E, 0x4F)) s = step1(k, 0, 0, to_set, to_keep) for i in xrange(len(s)) :   if s[i] is None :     s[i] = sec_rnd.randint(0, 0xFF) serial = "".join(chr(i) for i in hash_name[::-1]) serial += "".join(chr(a^b^c) for a, b, c in zip(hash_name, hash_name[::-1], s)) serial = serial.encode("base64").replace("\n","") # multiple encoding are valid for the same value because some bits are ignored for the last symbol serial = serial[:-len(egg)]+egg print "serial 1 :" print serial

Figure 8: First solution, all generated serials end with ElV++ESET++ (Python 2.7)

egg = "+blabla+ESET+Nod32+BH2012+Oppida" egg_d = egg.decode("base64") k = [None]*64+[0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x40, 0x17, 0x40, 0x00] to_set = [(0x44, 0xA), (0x45, 0xB), (0x46, 0xC), (0x47, 0xD), (0x4C, 0x20)] to_keep = set((0x4D, 0x4E, 0x4F)) s = step1(k, 0, 0, to_set, to_keep) for i in xrange(len(s)) :   if s[i] is None :     s[i] = sec_rnd.randint(0, 0xFF) serial = "".join(chr(i) for i in hash_name[::-1]) # add padding (128 % 3 = 2) egg_d = chr(sec_rnd.randint(0, 0xFF) + egg_d for i, j in enumerate(hash_name + hash_name[::-1] + [ord(c) for c in egg_d]) :     s[i%64] ^= j serial += "".join(chr(i) for i in s[:64]) serial += egg_d serial = serial.encode("base64").replace("\n","") # multiple encoding are valid for the same value because some bits are ignored for the last symbol serial = serial[:-len(egg)]+egg print "serial 1 :" print serial

Figure 9: Second solution, all generated serials end with "+blabla+ESET+Nod32+BH2012+Oppida" (Python 2.7)

4.  Second part

The second part of the challenge takes place at address 0x0401C10. The serial must be composed of 12 uppercase hexadecimal characters. Those characters are used to transform a 64 bits value with the following algorithm:

def to_16b(qword) :     idx = 1     word = 0     for i in xrange(16) :         if qword & (1 << idx ) :             word |= 1 << i         idx = (idx + 29) % 64     return word def mutate(qword, word) :     idx = 1     for i in xrange(16) :         if word & (1 << i) :             qword |= 1 << idx         else :             qword &= ~(1 << idx)         idx = (idx + 29) % 64     return qword def shift(qword) :     qword_masked = qword & 7069181668496654033     nb_bits_set = 0     for i in xrange(64) :         if qword_masked & (1 << i) :             nb_bits_set += 1     return ((qword << 1) | (nb_bits_set & 1)) & ((1 << 64) - 1)     serial = "012345678ABC" qword = 8828098094971975552 for c in serial :     i = int(c,16)     word = to_16b(qword)     if word & (1 << i) :         word &= ~(1 << i)     else :         word |= (1 << i)     qword = mutate(qword, word)     qword = shift(qword) print hex(qword)

Figure 10: First part of the verification of the second serial : mutation of qword (Python 2.7)

Those operations can be simplified to get the following algorithm:

def shift(qword) :     qword_masked = qword & 7069181668496654033     nb_bits_set = 0     for i in xrange(64) :         if qword_masked & (1 << i) :             nb_bits_set += 1     return ((qword << 1) | (nb_bits_set & 1)) & ((1 << 64) - 1)     serial = "012345678ABC" qword = 8828098094971975552 int_to_idx = [1, 30, 59, 24, 53, 18, 47, 12, 41, 6, 35, 0, 29, 58, 23, 52] for c in serial :     qword ^= 1 << int_to_idx[int(c,16)]     qword = shift(qword) print hex(qword)

Figure 11: Simplified first part of the verification of the second serial : mutation of qword (Python 2.7)

After being transformed, qword must satisfy the following check:

qwordTable = [[4, 145, 249, 72, 19, 195, 74, 137],     [...]  [4611686018427387904L,   1195637156289680119L,   24621007439812200L,   43743323218066342L,   676995634570036126L,   1203597948695219397L,   1037036833364889864L,   130039954294608103L]] def has_same_set_bits(a, b) :     """ return 1 if all bits set in b are also set in a else 0"""     for i in xrange(64) :         if b & (1 << i) and not (a & 1 << i) :             return 0     return 1 r = 0 for i in xrange(64) :     nb_same_set_bits = 0     for j in xrange(8) :         nb_same_set_bits += has_same_set_bits(qword, qwordTable[i][j])     if nb_same_set_bits & 1 :         r |= 1 << i if r == 0x55BDEC8E23A0EF32 :     print "Good Boy" else :     print "BadBoy"

Figure 12: Verification of the mutated qword (Python 2.7)

To dump the qwordTable, we use the following simple IDA python script:

from pprint import pprint from idc import Qword qwordTable = [] for i in xrange(64) :   t = []   for j in xrange(8) :     t.append(Qword(0x560128 + i*8*8 + j*8))   qwordTable.append(t) pprint(qwordTable)

Figure 13: Code used to dump the table of qwords in IDA (Python 2.7)

It may exists an elegant solution for this problem but we didn't find it and we wanted to solve the crack-me as fast as possible so we decided to use the Microsoft Theorem Prover: Z3. It has a nice Python API, good reviews, free and easy to use; it is the perfect tool for this problem.

All we have to do is translate the different operations performed on the serial into Z3 equations and let Z3 find the answer for us.

Integers became bit vectors, different possible values are translated in OR equations. The following code gives a valid serial in less than 2 minutes:

check_v = 0x55BDEC8E23A0EF32 init_v = 8828098094971975552 bitvectors = [BitVecVal(init_v, 64)] solver = Solver() for i in xrange(12) :   bitvectors.append(BitVec('x_%d'%i, 64)) key = [] for i in xrange(12) :   key.append(Int("k%d"%i)) for i in xrange(1, 13) :   eq = False   for j, k in enumerate([1, 30, 59, 24, 53, 18, 47, 12, 41, 6, 35, 0, 29, 58, 23, 52]) :     sub_eq = (key[i-1] == j)     bv = (bitvectors[i-1] ^ BitVecVal(1 << k, 64))     bit = 0     for l in xrange(64) :       if 7069181668496654033 & (1 << l) :         bit = (LShR(bv, l) & 1) ^ bit     sub_eq = And(sub_eq, bitvectors[i] == ((bv << 1) | bit))     eq = Or(eq, sub_eq)   solver.append(eq) for i, t in enumerate(tt) :   bit = 0   for v in t :     has_same_set_bits = 1     for j in range(64) :       if v & (1 << j) :         has_same_set_bits = has_same_set_bits & (LShR(bitvectors[12], j) & 1)     bit ^= has_same_set_bits   if check_v & (1 << i) :     solver.add(bit == 1)   else :      solver.add(bit == 0)   solver.check() solution = solver.model() r = "" for i in xrange(12) :   r += "%X"%int(str(solution[key[i]])) print "serial2 :" print r

Figure 14: Code used to find a valid serial for the second part of the crack-me (Python 2.7)

It is faster to find a solution when boolean values are directly used instead of bit vectors (~30 sec versus ~100 sec) but it is also a little bit more tricky, the code doing this is given in the complete keygen source provided in Annex.

Different variations of the code gave us 3 different serials: 94A0353FA32B, 2BA52E7FAC23 and 966132348323.

5.  Conclusion

This crack-me intelligently mixed crypto, exploitation and use of specific tools, it wasn't too easy nor too hard for this kind of time constraint challenge and really interesting.

We want to thank ESET and all the people who participate to this challenge, both coders and organizers!

6.  Annex

import sys from random import SystemRandom from base64 import b64encode try :   from whirlpool import Whirlpool except :   print "To work this keygen need the Whirpool implementation located here : http://www.bjrn.se/code/whirlpoolpy.txt"   sys.exit(0) sec_rnd = SystemRandom() print "name :" name = sys.stdin.readline().rstrip("\r\n") hash_name = [ord(c) for c in Whirlpool(name+("ESETNOD32@"*8)[len(name):]).digest()] def step1(k, i, j, to_set, to_keep) :   global SOLUTION   if i > 63 :     if not to_set :       return k     return None   if to_set :     to_set_cpy = list(to_set)     sec_rnd.shuffle(to_set_cpy)     for choice, (idx, v) in enumerate(to_set_cpy) :       if k[i] == v :         r = step2a(idx, k, i, j, to_set_cpy[:choice] + to_set_cpy[choice+1:] , to_keep)         if r is not None :           return r       elif k[i] is None :         k[i] = v         r = step2a(idx, k, i, j, to_set_cpy[:choice] + to_set_cpy[choice+1:] , to_keep)         if r is not None :           return r         k[i] = None   r = step2b(k, i, j, to_set, to_keep)   if r is not None :     return r   return None def step2a(idx, k, i, j, to_set, to_keep) :   c = k[i] % 80   kc = k[c]   if kc is None :     if (idx - j)%80 in to_keep :       return None     kc = (idx - j)%80     while kc < 0x100 :       k[c] = kc       to_keep.add(idx)       r = step3(k, i, idx, to_set, to_keep)       to_keep.remove(idx)       if r is not None :         return r       kc += 80     k[c] = None   elif (kc + j)%80 == idx :     to_keep.add(idx)     r = step3(k, i, idx, to_set, to_keep)     to_keep.remove(idx)     return r   else :     return None def step2b(k, i, j, to_set, to_keep) :   c = k[i]   if c is None :     vals = [c for c in xrange(0x100) if k[c%80] is not None and (k[c%80] + j)%80 not in to_keep]     sec_rnd.shuffle(vals)     for c in vals :       k[i] = c       r = step3(k, i, (k[c%80] + j)%80, to_set, to_keep)       if r is not None:         return r     vals = [c for c in xrange(0x100) if k[c%80] is None]     sec_rnd.shuffle(vals)     for c in vals :       k[i] = c       c = c % 80       vals2 = [kc for kc in xrange(0x100) if (kc + j)%80 not in to_keep]       sec_rnd.shuffle(vals2)       for kc in vals2 :         k[c] = kc         r = step3(k, i, (kc + j)%80, to_set, to_keep)         if r is not None :           return r       k[c] = None     k[i] = None   else :     c %= 80     kc = k[c]     if kc is None :       vals = [kc for kc in xrange(0x100) if (kc + j)%80 not in to_keep]       sec_rnd.shuffle(vals)       for kc in vals :         k[c] = kc         r = step3(k, i, (kc + j)%80, to_set, to_keep)         if r is not None :           return r       k[c] = None     elif (kc + j)%80 not in to_keep :       return step3(k, i, (kc + j)%80, to_set, to_keep)   return None def step3(k, i, j, to_set, to_keep) :   k[i], k[j] = k[j], k[i]   r = step1(k, i+1, j, to_set, to_keep)   if r is not None :     r[i], r[j] = r[j], r[i]     return r   k[i], k[j] = k[j], k[i]   return None egg = "ElV++ESET++=" egg_d = egg.decode("base64") # fight against sexism in keygens ! # use B16B00B2 and B16BA112 with equal probability ! import struct egg_d = (struct.pack("<I", 0xB16B00B2) if sec_rnd.randint(0, 1) else struct.pack("<I", 0xB16BA112)) + egg_d padd = 64 - len(egg_d) list_egg = [hash_name[padd+i]^hash_name[::-1][padd+i]^ord(c) for i,c in enumerate(egg_d)] k = [None]*padd+list_egg+[0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x40, 0x17, 0x40, 0x00] to_set = [(0x44, 0xA), (0x45, 0xB), (0x46, 0xC), (0x47, 0xD), (0x4C, 0x20)] to_keep = set((0x4D, 0x4E, 0x4F)) s = step1(k, 0, 0, to_set, to_keep) for i in xrange(len(s)) :   if s[i] is None :     s[i] = sec_rnd.randint(0, 0xFF) serial = "".join(chr(i) for i in hash_name[::-1]) serial += "".join(chr(a^b^c) for a, b, c in zip(hash_name, hash_name[::-1], s)) serial = serial.encode("base64").replace("\n","") # multiple encoding are valid for the same value because some bits are ignored for the last symbol serial = serial[:-len(egg)]+egg print "serial 1 :" print serial tt = [     [0x4, 0x91, 0xF9, 0x48, 0x13, 0xC3, 0x4A, 0x89],     [0x80000, 0x30E099, 0xE36C82, 0x35CFAB, 0x94B829, 0x621DF1, 0x413F79, 0xD28998],     [0x8, 0xB5, 0x57, 0xB0, 0xB1, 0x80, 0x47, 0x83],     [0x200000000, 0xB5D4CE18F3, 0x8CFB75A1FA, 0x1CC4345974, 0x244C876646, 0xF1D67A37BD, 0x567DCE8EF, 0x71D88A2C6B],     [0x10000000, 0xEAA5839, 0x869CBEB, 0x72D6F13, 0x1AD663, 0xFEC707, 0x248AFA8, 0x681CB52],     [0x10, 0xA5, 0x6, 0x24, 0x29, 0x4D, 0xD, 0x8C],     [0x8000000000000, 0xF0AFDA2F1F6319, 0x54DC6F31E1DFD7, 0x2161D2BE0CC29F, 0xF3799D9A17CB9F, 0xE2B0EC0B44A77D, 0x548E26B440C7E0, 0x9362066CC80EA5],     [0x80, 0x4E, 0x2C, 0x75, 0x6C, 0x13, 0x67, 0x4B],     [0x100, 0x5D, 0xE0, 0x5F, 0x5, 0xEC, 0x67, 0x6F],     [0x800000000000000, 0x12BBC3C5DC54A38, 0x1CCD3437BF476CF, 0x75007C44E58937F, 0x21467EFC8A2F4FC, 0x1E98C57A31D1F52, 0x28CF95332617839, 0x56470EDC082144B],     [0x200, 0x5F, 0x1C, 0x15, 0x5C, 0x1BA, 0x1D7, 0x24],     [0x400, 0x13, 0x346, 0x152, 0x1FA, 0x35, 0xD0, 0x1EB],     [0x800, 0x23B, 0x12A, 0x6D0, 0x180, 0x5A8, 0x166, 0x128],     [0x8000000000, 0x2DFE120B8D, 0xDA2A736E, 0x49EA2BE641, 0x34D402DC99, 0x72F9F7DD9, 0x139B938691, 0x33650D8FAE],     [0x1000, 0xF30, 0xCCD, 0x627, 0xC24, 0x34E, 0x944, 0x72],     [0x1000000000000, 0xAA710830103040, 0xF8D9876FA33FAD, 0xE0872B7C409D25, 0x6C502ADD44EE49, 0x26A17C61A87597, 0x786F944EF0E02B, 0x9C476E3E0C8170],     [0x2000, 0x1E4, 0xFB1, 0x1CE3, 0x1F19, 0x1923, 0x5B5, 0x1E7F],     [0x4000, 0x13C6, 0x313D, 0x20E0, 0x17B6, 0x3E4, 0x313, 0x3FD5],     [0x8000, 0xC5D, 0x14AB, 0x4F1F, 0x4E79, 0x30AE, 0x1408, 0x3E1F],     [0x20000000000000, 0x5F8E3FF36DF7F1, 0x8D426F89260E03, 0x51A2E96DD21274, 0x6FE4A7A21C27C, 0xC60CA2A303E8AA, 0x4C88C6467883BB, 0x14D7CC45303AD5],     [0x10000, 0x94241F, 0x40C7E0, 0x369CC6, 0x5E1262, 0x9CCF74, 0xE02BD5, 0x82E8AF],     [0x20, 0xC2, 0x1B, 0x4B, 0x9E, 0x53, 0xD6, 0x17],     [0x20000, 0x525F3, 0x3C9E72, 0x5050A4, 0x352151, 0xC18A91, 0x19853E, 0xF464AB],     [0x100000, 0x279902, 0x495CA9, 0x2EAA39, 0x548EE, 0x4A118C, 0xED5F6E, 0xE212B],     [0x200000, 0xD5F694, 0x118702, 0x1A1231, 0x14F6D0, 0x4655E2, 0xD0AC93, 0xB53B1],     [0x400000, 0x41F14, 0x16F3C4, 0x8325F9, 0x932B7E, 0x900661, 0x23B3C8, 0x84205E],     [0x800000, 0x27F59, 0x253D0F, 0x3E894F, 0x15BB39, 0x5F3F45, 0x1BFE85, 0x771B46],     [0x8000000000000000, 0x82B96333035C10D, 0x7EA90FA43B6895B, 0xE781F2DBD9A06C, 0x1A037D0D66205D1, 0xE0978719A7CA63F, 0x6DFECA3318A6418, 0x6004A0795E97EA6],     [0x2, 0xB9, 0x79, 0xBC, 0x7D, 0x15, 0x60, 0x99],     [0x1000000, 0xD7F434, 0x89EB3C, 0xD686FE, 0xB97BF3, 0xBF565E, 0xCD9C32, 0xD5F19C],     [0x200000000000000, 0xD62782672B659B, 0x14AC89D5C0A4573, 0x1F24B67DC7065FE, 0x5BFBCAF9A26B49, 0x162670BAA8BFA51, 0x1F7D42DD6D0AEC0, 0x12A21173E4BCB43],     [0x2000000, 0xA0FA2E, 0x7E221F, 0x5B4103, 0x163DF66, 0x161AC76, 0x1667E40, 0xE9DFCB],     [0x400000000000, 0x2A635474528D, 0x272CA2F78E85, 0xD26BD767F6B, 0x2D5EFD63966D, 0x135444427BE2, 0xE49E6C649CC, 0x21FD11A032BC],     [0x4000000, 0x908322, 0x2D298B7, 0x1F5997, 0x79F0F1, 0x4BF061, 0x3B297C, 0x5B302C],     [0x8000000, 0x5D448D4, 0x283B776, 0x3145A19, 0x45C465, 0x69FF572, 0x7DEB365, 0x1F9214E],     [0x40000000, 0x192780D6, 0x2602A107, 0x13D0B078, 0x5C1351B, 0x2C436E84, 0xC8CF063, 0xA9A768F],     [0x100000000, 0x3069175096, 0xD28269BB14, 0x8727E70B5, 0xDA536BD5D8, 0xFA6622E8E6, 0xF696CD6F4A, 0xB8CC79C636],     [0x400000000, 0x43CC6D6C11, 0x9985B620E1, 0x8371C3A17, 0xBF670C33E, 0x806F4C464C, 0xB3383CE8B8, 0x822B885E10],     [0x800000000, 0xE65F7DC327, 0xD23F20538E, 0x739967CF65, 0x16A89332D3, 0xA7991DB287, 0x40C74ED44F, 0x267C979686],     [0x1000000000, 0x672D1A4176, 0x46F68AFEA2, 0x630665DBEC, 0xB4C085042, 0xCA7B912349, 0xA160ABD0A9, 0xCEC4B1E85E],     [0x2000000000, 0xDE6F99715E, 0x8DE175C718, 0x9E36A8FBDA, 0xCE7649EC86, 0xE09F1092E, 0x8B0C17265, 0xDE1EEB0098],     [0x4000000000, 0x3E37655239, 0xB8FFE5C49C, 0x95933F33D4, 0x38116C3E52, 0xBCAA64600C, 0x9B25DCCF0B, 0x89B17E2C],     [0x10000000000, 0xDED71D5774, 0x3D9408E914, 0xB656D2F967, 0xB0C1CADF8F, 0x43BED6FA3D, 0x4BB0D9A451, 0x76955E0E7D],     [0x20000000000, 0x5EAA80228A, 0x1F52F9E791D, 0x118BEB16970, 0x18F440E8778, 0x5DAD750C98, 0x1495CA088A7, 0xC6C2939013],     [0x40000000000, 0xF4930D48E2, 0x38F51A4F94C, 0x3B72170BF59, 0x2872194C90C, 0x16FBC07A0FC, 0x3071BC4ADF6, 0x382FCF15CEC],     [0x80000000000, 0x1C16C0D3F60, 0x2EA439BCB99, 0x4191CC0D086, 0x37EEFFDEC7, 0x1399B07940A, 0xE45E1ABC7F, 0x1805AA9CAA1],     [0x1, 0xF0, 0x28, 0xCC, 0xB6, 0xD4, 0x12, 0x6],     [0x100000000000, 0xC8F4FAEBDA4, 0xEBB413F2E37, 0xAC83562BC6C, 0x67713E39976, 0xFD5EEDAD058, 0x82D23735526, 0xCDFB1BC0DDB],     [0x200000000000, 0x11D42C06F1B6, 0x1D1E2E6E6223, 0x5539E7B941C, 0x758A21E70EC, 0xEE3DF953186, 0xEF69F8EE3DC, 0x1ECD77876261],     [0x800000000000, 0x200EBD4E62C8, 0x7885CD4584EE, 0x46E59ADA811, 0xB2F58DD756, 0x5F0889BEDD0D, 0x73DF76190650, 0x71DBD1F160D1],     [0x2000000000000, 0x91362730A633C, 0xB519E7BF5FDE90, 0xF51081D1D9B143, 0x40EA4B7E6C5451, 0x9157F00FE632B3, 0x7DB5001936A800, 0x406ED0911503C2],     [0x4000000000000, 0x5AD2DB864D68D1, 0x5387794E71CA27, 0x70FA8BAB871825, 0x58B7D3F4C4A474, 0x516E13F447158A, 0xB9B97B38870596, 0x2B4B74A2131B83],     [0x80000000, 0x6A2CA9CE, 0x5B80DEC2, 0x17FBFF2A, 0x28C7273D, 0x7874E025, 0xE9EAD5A, 0x252D552F],     [0x40000, 0x7086CA, 0xA0454B, 0xA18229, 0x235B43, 0x48BAE2, 0x90895, 0x8B740E],     [0x10000000000000, 0x6161E658A52B5C, 0xCA62896A2DAE8A, 0x242F88A65B2182, 0xE49F85CF3BC096, 0xE392473BBD42EF, 0x4A18407B9D7D6E, 0x678B046E512878],     [0x40000000000000, 0xF2811DE1B800C, 0xA7CADAEBB2743E, 0x1DE2659F77B6AC, 0x74950E9C892BB, 0x2E8156532E957D, 0x2E0FD11665C7A5, 0x96024A554AE450],     [0x40, 0x6, 0xB3, 0x80, 0x1F, 0xE, 0x82, 0x17],     [0x80000000000000, 0x45F6DF933C25A, 0x4FBCEB9CC00CF9, 0x6575D1B9C230CA, 0x4173E8D140E239, 0x2B95CAA25E3D1D, 0x7DD021CE354D59, 0x1A868E5B651C44],     [0x100000000000000, 0x73E560641E49A1, 0x14B3654EFEC16A, 0xC20A1CE5BF5431, 0xE8AB16961A64DC, 0xFC5AAA602EC41D, 0xD9CC3B32395B96, 0xE28C9F38890F0E],     [0x400000000000000, 0x5522500389A628, 0x2694003EF575A86, 0x13B9F036A0696A3, 0x1937BCEFB1621B, 0x200DFB8F91A8BB2, 0xBE6492FF025656, 0x202789F0C72B4FF],     [0x1000000000000000, 0x77AF02D6AB1DF3, 0x5659C5086E42E63, 0x284131A456DFD8E, 0xDB26FBB380976AC, 0xB175241CFECC18C, 0x660F1EFB8A20487, 0xFFFD90B934B8DF9],     [0x2000000000000000, 0x5B4C5AFA91EA2FC, 0xC781F620485C8B8, 0x1068D041963FF5A9, 0xAF1DABA44341845, 0x46577187503AD18, 0x1DAF83ACD5EBB96, 0x3DD97CE4685E29C],     [0x20000000, 0xEF4482F, 0x312765, 0x1A9BA833, 0xFE451C9, 0x6397B17, 0x16503A30, 0x12A2E425],     [0x4000000000000000, 0x1097C1A8ACE792F7, 0x5778AD02765668, 0x9B685219B53BA6, 0x9652BF15909839E, 0x10B409F5185E0CC5, 0xE644B8167B5D108, 0x1CDFEA6425690E7] ] check_v = 0x55BDEC8E23A0EF32 init_v = 8828098094971975552 try :   from z3 import * except :   print "unable to load Z3, here is a pre calculated serial 2 :"   print "966132348323"   sys.exit(0) from time import time start_time = time() def Xor(a,b) :   return Or(And(a,Not(b)), And(Not(a), b)) bits = [] solver = Solver() for i in xrange(13) :   bs = []   for j in xrange(64) :     bs.append(Bool("b%02d%02d"%(i, j)))   bits.append(bs) key = [] for i in xrange(12) :   key.append(Int("k%d"%i)) for i in xrange(64) :   if init_v & (1 << i) :     solver.append(bits[0][i])   else :     solver.append(Not(bits[0][i])) for i in xrange(1, 13) :   eq = False   for j, k in enumerate([1, 30, 59, 24, 53, 18, 47, 12, 41, 6, 35, 0, 29, 58, 23, 52]) :     sub_eq = (key[i-1] == j)     for l in xrange(63) :       if l != k :         sub_eq = And(sub_eq, bits[i][l+1] == bits[i-1][l])       else :         sub_eq = And(sub_eq, bits[i][l+1] == Not(bits[i-1][l]))     sub_sub_eq = False     for l in xrange(64) :       if 0x621AC745FB723ED1 & (1 << l) :         sub_sub_eq = Xor(sub_sub_eq, bits[i][l+1])     sub_eq = And(sub_eq, bits[i][0] == sub_sub_eq)     eq = Or(eq, sub_eq)   solver.append(eq) for i, t in enumerate(tt) :   bit = True if check_v & (1 << i) else False   eq = False   for v in t :     has_common_bit = True     for j in range(64) :       if v & (1 << j) :         has_common_bit = And(has_common_bit, bits[12][j])     eq = Xor(eq, has_common_bit)   if not bit :     eq = Not(eq)   solver.add(eq) solver.check() solution = solver.model() r = "" for i in xrange(12) :   r += "%X"%int(str(solution[key[i]])) print "serial 2 :" print r print print "(%.02f seconds)"%(time() - start_time)

Figure 15: Complete source of the keygen (Python 2.7)