1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208
 from Crypto.Util.number import * from pwn import * from hashlib import * from Crypto.Cipher import AES import z3
def sym_xoroshiro128plus(solver, sym_s0, sym_s1, mask, result): s0 = sym_s0 s1 = sym_s1 sym_r = (sym_s0 + sym_s1)
condition = z3.Bool('c0x%0.16x' % result) solver.add(z3.Implies(condition, (sym_r & mask) == result & mask))
s1 ^= s0 sym_s0 = z3.RotateLeft(s0, 55) ^ s1 ^ (s1 << 14) sym_s1 = z3.RotateLeft(s1, 36)
return sym_s0, sym_s1, condition
def find_seed(results_with_masks): start_s0, start_s1 = z3.BitVecs('start_s0 start_s1', 64) sym_s0 = start_s0 sym_s1 = start_s1 solver = z3.Solver() conditions = []
for result, mask in results_with_masks: sym_s0, sym_s1, condition = sym_xoroshiro128plus(solver, sym_s0, sym_s1, mask, result) conditions.append(condition)
if solver.check(conditions) == z3.sat: model = solver.model()
return (model[start_s0].as_long(), model[start_s1].as_long())
else: return None
class PRNG(object): def __init__(self, seed1,seed2): self.seed1 = seed1 self.seed2 = seed2 @staticmethod def rotl(x, k): return ((x << k) & 0xffffffffffffffff)  (x >> 64  k) def next(self): s0 = self.seed1 s1 = self.seed2 result = (s0 + s1) & 0xffffffffffffffff
s1 ^= s0 self.seed1 = self.rotl(s0, 55) ^ s1 ^ ((s1 << 14) & 0xffffffffffffffff) self.seed2 = self.rotl(s1, 36)
return result
def crt(list_a, list_m): try: assert len(list_a) == len(list_m) except: print "[+] Length of list_a should be equal to length of list_m" return 1 for i in range(len(list_m)): for j in range(len(list_m)): if GCD(list_m[i], list_m[j])!= 1 and i!=j: print "[+] Moduli should be pairwise coprime" return 1 M = 1 for i in list_m: M *= i list_b = [M/i for i in list_m] assert len(list_b) == len(list_m) try: assert [GCD(list_b[i], list_m[i]) == 1 for i in range(len(list_m))] list_b_inv = [int(inverse(list_b[i], list_m[i])) for i in range(len(list_m))] except: print "[+] Encountered an unusual error while calculating inverse using gmpy2.invert()" return 1 x = 0 for i in range(len(list_m)): x += list_a[i]*list_b[i]*list_b_inv[i] return x % M
def brute_dlp(g,a,p): x=1 while(True): if pow(g,x,p)==a: return x else: x+=1
def pohlig_hellman_pp(g, y, p, q, e): try: assert (p1) % q == 0 except: print "[] Error! q**e not a factor of p1" return 1
a = 0
b_j = y alpha = pow(g, (p1)/q, p) for j in range(e): y_i = pow(b_j, (p1)/(q**(j+1)), p) a_j = brute_dlp(alpha, y_i, p) a += a_j*(q**j)
multiplier = pow(g, a_j*(q**j), p) assert GCD(multiplier, p) == 1 b_j = (b_j * inverse(multiplier, p)) % p return a
def pohlig_hellman(g, y, p, list_q, list_e): x_list = [pohlig_hellman_pp(g, y, p, list_q[i], list_e[i]) for i in range(len(list_q))] mod_list = [list_q[i]**list_e[i] for i in range(len(list_q))] return crt(x_list, mod_list)
def left_right(num): num = (((num & 2863311530) >> 1)  ((num & 1431655765) << 1)) num = (((num & 3435973836) >> 2)  ((num & 858993459) << 2)) num = (((num & 4042322160) >> 4)  ((num & 252645135) << 4)) num = (((num & 4278255360) >> 8)  ((num & 16711935) << 8)) return((num >> 16)  (num << 16))
def fix1(x): b = bin(x)[2:][::1] flag = True i =32 while(flag): ans = int(b[:i],2) if left_right(ans)==x: return ans i+=1
def exploit(a): ph = pohlig_hellman(g,a,p,x,y) assert pow(g,ph,p)==a a = ph/(2**64) b = ph%(2**64) a = fix1(a) b = fix1(b) ran = (a << 32) + b return ran
def decrypt(ct,key): key = sha256(long_to_bytes(key)).digest() aes = AES.new(key,AES.MODE_CBC,md5(key).digest()) ct = aes.decrypt(ct.decode('hex')) return ct
def decrypt_from_seed(seed): genr = PRNG(seed[0],seed[1]) for i in range(7): key = genr.next() flag = decrypt(fl,key) if 'inctf' in flag: return flag
def create_list(l): lis = [] for i in l: lis.append((i,0xffffffffffffffff)) return lis
if __name__ == "__main__":
g = 2 p = 7199773997391911030609999317773941274322764333428698921736339643928346453700085358802973900485592910475480089726140708102474957429903531369589969318716771L x = [2, 5, 109, 7963, 8539, 20641, 38833, 39341, 46337, 51977, 54319, 57529] y = [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
io = remote('18.218.190.20',3197) lis = [] print io.recv() if io.can_recv(): io.recv() io.recvuntil("> ") for i in range(6): io.sendline('1') s = io.recvuntil('> ').split() so=s[5].split("'") c1 = eval(so[1]) exp = exploit(c1) print exp lis.append(exp) io.sendline('2') io.recvuntil('flag:') fg = io.recv().split() fl = fg[0] sed = find_seed(create_list(lis[:5])) print decrypt_from_seed(sed)
