#!/usr/bin/env python3
import random

greets = [
    "Herzlich willkommen! Der Schlüssel ist {0}, und die Flagge lautet {1}.",
    "Bienvenue! Le clé est {0}, et le drapeau est {1}.",
    "Hartelijk welkom! De sleutel is {0}, en de vlag luidt {1}.",
    "ようこそ！鍵は{0}、旗は{1}です。",
    "歡迎！鑰匙是{0}，旗幟是{1}。",
    "Witamy! Niestety nie mówię po polsku...",
]

flag = open('flag.txt').read().strip()
assert set(flag.encode()) <= set(range(0x20, 0x7f))

key = bytes(random.randrange(256) for _ in range(16))
hello = random.choice(greets).format(key.hex(), flag).encode()

output = bytes(y | key[i % len(key)] for i, y in enumerate(hello))
print(output.hex())

The challenge primarily consisted of this script. The script generates an "encrypted" text. However, using the term " encrypted" is not entirely accurate in this context. Here, only a bitwise OR (|) operation is used. This operation alone is not reversible (there is no corresponding reverse operation to obtain the plaintext), so it doesn't qualify as true encryption. But for simplicity, we can refer to it as encryption.

The encrypted text is a combination of the flag and the key used to encrypt the text.

Additionally, one of six languages is chosen randomly, and one of them does not contain a flag.

The Crowbar - Z3

Initially, Z3 can only deal with mathematical problems. To solve the challenge with Z3, we first need to find a way to represent a string (the flag) as a mathematical problem. A string consists of characters, and a character can be represented as a number using its ASCII code. So, we can start by representing it as a number. Since we want to perform bitwise operations on the characters, a BitVec is the best choice. Using BitVec, we can transform it into a problem solvable by Z3.

To begin with, let's write the algorithm as Z3 logic. We will start by focusing on just one output language. The output with a length of 115 corresponds to German. Implementing this for different lengths didn't work for us.

from z3 import *

TEXT_LEN = 115

# Variables for Plaintext, named Plain_0 to Plain_114
plaintext = [BitVec(f'Plain_{n}', 8) for n in range(TEXT_LEN)]

# Variables for Ciphertext, named Cipher_0 to Cipher_114
ciphertext = [BitVec(f'Cipher_{n}', 8) for n in range(TEXT_LEN)]

# Variables for key, named Key_0 to Key_15
key = [BitVec(f'Key_{n}', 8) for n in range(16)]

s = Solver()

for i, (plain, cipher) in enumerate(zip(plaintext, ciphertext)):
    s.add(cipher == (plain | key[i % len(key)]))

Now, Z3 knows how the characters of the ciphertext, plaintext, and key are related. However, if we were to solve the model as it is, we wouldn't get a useful answer. The model doesn't have any knowledge of the actual ciphertext. It would just assume arbitrary values. Therefore, we still need to bind the actual ciphertext to the Z3 variables.

text_from_server: bytes = get_data_from_remote()

for actual_ciphertext, z3_ciphertext in zip(text_from_server, ciphertext):
    s.add(actual_ciphertext == z3_ciphertext)

The get_data_from_remote function retrieves the ciphertext from the CTF server. We will discuss the implementation details of this function later.

Additionally, we can now define that the value of a plaintext character lies within a certain range. It would be meaningful to use the range of printable characters. The vuln.py script specifies range(0x20,0x7f) as the valid value range. With the 'And' function, we instruct Z3 that both conditions must be evaluated together.

for plain in plaintext:
    s.add(And(plain <= 0x20, 0x7f <= plain))

Solution idea

Except for the key part, the plaintext is the same for each ciphertext. So, we can associate multiple ciphertexts with their respective keys to the same plaintext.

The key consists of 16 characters and repeats. This means we can associate multiple ciphertext parts and plaintext parts with each key byte. Since we know that cipherbyte = plainbyte | keybyte, we can establish this relationship.

Additionally, we can also establish a connection between the key and the encrypted key. The key is embedded in hexadecimal form into the plaintext. This means that for each key byte, we have two plaintext bytes and two ciphertext bytes. We can further define this relationship since we know the position of the key in the ciphertext, allowing us to determine which byte corresponds to which half-byte of the key. This required a lot of effort on our part. Using this information, we could usually determine the key based on a ciphertext sample, down to 6 bits in the worst case. However, this approach alone wasn't sufficient to derive the flag, and in the end, it turned out to be unnecessary. Therefore, we won't delve into this here. However, all of this information is still included in our solution file (attached below). Feel free to take a look if you're interested.

Tests have shown that we cannot reconstruct the plaintext from a single ciphertext sample. We obtain a plaintext, but it's not correct. Hence, we use multiple samples and match them against the same plaintext. This allows Z3 to determine the bits that were previously unclear.

from z3 import *

TEXT_LEN = 115

# Variables for Plaintext, named Plain_0 to Plain_114
plaintext = [BitVec(f'Plain_{n}', 8) for n in range(TEXT_LEN)]

s = Solver()

# Range rules for plaintext characters
for plain in plaintext:
    s.add(And(plain <= 0x20, 0x7f <= plain))

known_plaintext = "Herzlich willkommen! Der Schlüssel ist "

for known_plain, plain in zip(known_plaintext, plaintext):
    s.add(plain == ord(known_plain))

# Get 20 samples from the server and add them to Z3
for i in range(20):

    # Variables for ciphertext, named Cipher_i_0 to Cipher_i_114 where i is the current sample
    ciphertext = [BitVec(f'Cipher_{i}_{n}', 8) for n in range(TEXT_LEN)]

    # Variables for key, named Key_i_0 to Key_i_15 where i is the current sample
    key = [BitVec(f'Key_{i}_{n}', 8) for n in range(16)]

    # Connection between cipher, plain and key (Encrypt function)
    for i, (plain, cipher) in enumerate(zip(plaintext, ciphertext)):
        if not (40 <= i <= (40 + 32)):  # skip range of key, we shall not match that to plain text
            s.add(cipher == (plain | key[i % len(key)]))

    text_from_server: bytes = get_data_from_remote()

    for actual_ciphertext, z3_ciphertext in zip(text_from_server, ciphertext):
        s.add(actual_ciphertext == z3_ciphertext)

We need to store the individual ciphertext samples in separate Z3 variables. This is why the variables now have two numbers. For example, Cipher_3_12 corresponds to the 13th character (starting at 0) in the 4th ciphertext (starting at 0).

With this setup, Z3 can now solve the problem. We just need to somehow retrieve the flag in a readable format. To do that, we can output the plaintext.

print(s.check())

model = s.model()

print("FLAG:", "".join(chr(model[plain] for plain in plaintext)))

How do we retrieve the ciphertext from the server?

For this purpose, we use the "pwntools" package. It can do much more than just reading data from a server, but it's the go-to tool for CTFs. That's why we're using it here.

from pwn import remote


def get_data(conn):
    line = conn.recvline(keepends=False).decode()
    data = bytes.fromhex(line)
    return data


def get_data_from_remote():
    N = 20
    for i in range(N):
        conn = remote('167.235.26.48', 10101)
        data = get_data(conn)

        if len(data) == TEXT_LEN:
            return data
        else:
            print(f"> Requesting data {i}/{N} (len = {len(data)})")
            time.sleep(0.5)  # Wait a little before retrying so we don't produce too much load on the CTF infra.

How Long Does Z3 Take for This?

Almost nothing. The longest part is retrieving the data from the server. When we have everything locally, Z3 finishes within a few milliseconds.

But Why Does It Work? - The Discarded Approach

Initially, we didn't use Z3. However, our approach was quite similar to what we implemented in Z3. When we realized that we were essentially building a solver, we switched to Z3. By examining our approach, one can deduce why Z3 can solve it and under what conditions we can reconstruct part of the plaintext.

We have an OR operation. We are all familiar with the truth table of an OR operation:

If A or B is true, the result is also true. Conversely, if we have a 1 in the result, we cannot determine whether A or B was 1.

Applying this to the challenge, we can say that if we have a 1 in the ciphertext, we cannot determine whether there was a 1 in the plaintext at that position or if there was a 1 in the key at that position. We can only infer plaintext from both ciphertext and key in a single case: when we know that there was a 0 in the key at that position. Key OR 0 is 0, Key OR 1 is 1. This is how we "leak" a plaintext bit. Here's an example:

We know that the first byte in the plaintext is an "H". Its ASCII code is 0x48, or in binary: 0100 1000. Let's assume the corresponding ciphertext is 0101 1011.

At some points, there are question marks. At these points, we cannot definitively say whether that bit in the key was a 1 or 0. However, at certain points, we can clearly determine whether it was a 0 or 1. We can repeat this process with additional samples to recover more bits of the key. Since the key repeats every 16 characters, we can continue with the n+16th ciphertext character. We don't need to recover all the bits of the key; a few are sufficient.

So, we continue. The 16th character is an "m," which corresponds to 0x6D (0110 1101) in binary.

In this case, unfortunately, we haven't gained anything because all the bits of "H" also appear in "m," so we cannot determine any new bits from it. But I think the concept is becoming clear.

We can apply the same approach to the flag as well. We know the ciphertext of the first flag byte, and we know the key, at least in part. In the places where the key is 0, we "leak" a flag bit.

We happen to know the first three characters of the flag. The flag starts with "hxp," so the first character of the flag is "h." In binary, it's "0110 1000." This matches our reconstructed bits. Of course, we don't know the others, but the concept works. This way, we can reconstruct individual bits of the flag. We simply repeat this process for many ciphertexts until all the question marks in the flag bits are resolved.