Points: 150

Solves: ???

Description:

I do declare this to challenge to be at least mildly engaging, and certainly useful going forwards

flag format: TUCTF{…}

Given:

A file with a set of restrictions in Prolog that the keys have to satisfy in order to pass the check.

# Solution

(by L0rdComm4nder)

## TLDR

The prolog code encodes a series of constraints that are easily encoded in Z3

## Description

Looking at the given files one notices the existence of two important functions `tokenizer` and `checkkey`.

The `tokenizer` function basically transforms character codes into the corresponding characters `0` to `9` and a few others `( ) , - &`.

The `checkkey` function checks the validity of the generated keys.

These constraints are easily encoded in Z3 and we know that a key should be of the form `(XX,XX-XX,XX&XX,XX-XX,XX)` and satisfy some conditions.

``````#!/usr/bin/env python3
from z3 import *
from pwn import *

SERVER = "grammarlesson.tuctf.com"
PORT = 6661

s = Solver()
flag = [Int('flag%d' % i) for i in range(25)]
p = [Int('p%d' % i) for i in range(8)]
q = [Int('q%d' % i) for i in range(8)]
o = [Int('o%d' % i) for i in range(8)]

def is_digit(x):

is_digit(flag[1])
is_digit(flag[2])
is_digit(flag[4])
is_digit(flag[5])

is_digit(flag[7])
is_digit(flag[8])
is_digit(flag[10])
is_digit(flag[11])

s.add(q[0] + q[1] == o[0])

is_digit(flag[13])
is_digit(flag[14])
is_digit(flag[16])
is_digit(flag[17])

is_digit(flag[19])
is_digit(flag[20])
is_digit(flag[22])
is_digit(flag[23])

s.add(q[2] + q[3] == o[1])

s.add(o[0] * o[1] == 82944)

def hack(x):
if x>=0 and x<=9:
return chr(x +48)
else:
return chr(x)

chan = remote(SERVER, PORT, timeout=9999)
chan.recvuntil(': ')

rounds=0
while z3.sat == s.check():
rounds += 1
m = s.model()
plaint = "".join([ hack(int(repr(m[flag[i]]))) for i in range(len(flag)) ])
print plaint
chan.sendline(plaint)
if rounds == 10:
break
chan.recvuntil(': ')
block = []
for i in range(len(flag)):
block.append( flag[i] != m[flag[i]])

chan.interactive()
``````

Running the above script, and submitting the 10 first retrieved flags one gets

``````(99,99-99,99&92,38-10,16)
(88,88-88,80&81,97-09,35)
(88,75-78,88&80,86-08,64)
(88,77-58,88&80,77-08,91)
(88,77-58,88&80,77-08,82)
(88,77-58,88&80,07-08,98)
(88,67-68,88&80,66-08,84)
(88,67-38,88&80,76-08,86)
(88,67-92,88&80,56-08,88)
(88,67-92,88&80,46-08,89)
TUCTF{Gr4mm3r_1s_v3ry_imp0rtAnT!_4ls0_Pr0log_iz_c00l!}
``````