My simple cipher

Перед нами текст задания:

Кроме того, дано два файла.
cipher.py:

import sys
import random

key = sys.argv[1]
flag = '**CENSORED**'

assert len(key) == 13
assert max([ord(char) for char in key]) < 128
assert max([ord(char) for char in flag]) < 128

message = flag + "|" + key

random.seed(1)
encrypted = chr(random.randint(0, 128))

for i in range(0, len(message)):
  print 'enc:, encrypted', (encrypted, (encrypted[i]))
  encrypted += chr((ord(message[i]) +
                    ord(key[i % len(key)]) +
                    ord(encrypted[i])) % 128)

print(encrypted.encode('hex'))

encrypted.txt:

7c153a474b6a2d3f7d3f7328703e6c2d243a083e2e773c45547748667c1511333f4f745e

Из исходного кода очевидно, что ключ состоит из 13 символов и находится в конце зашифрованного текста, байты ключа и флага < 128, а сам флаг начинается с TWCTF{.
Понятно, что это можно инвертировать вручную, но мы просто использовали Z3 для получения флага.
Итак, мы знаем:

• флаг и ключ < 128 и >= 0
• флаг начинается с TWCTF{
• сообщение содержит символ |

Используем эти ограничения:

ciphertext = "7c153a474b6a2d3f7d3f7328703e6c2d243a083e2e773c45547748667c1511333f4f745e".decode("hex")

s = z3.Solver()
flag = [z3.Int("flag_" + str(i)) for i in range(len(ciphertext) - 15)]
key = [z3.Int("key_" + str(i)) for i in range(13)]
pipe = z3.Int("pipe")
s.add(pipe == ord("|"))
for var in flag:
	s.add(var < 128)
	s.add(var >= 0)
for i, c in enumerate("TWCTF{"):
	s.add(flag[i] == ord(c))
for var in key:
	s.add(var < 128)
	s.add(var >= 0)
message = flag + [pipe] + key
for i in range(1, len(ciphertext)):
	index = i - 1
	byte = ord(ciphertext[i])
	s.add((message[index] + key[index % 13] + ord(ciphertext[index])) % 128 == byte)

print(s.check())
print(s.model())
print("".join([chr(int(str(s.model()[var]))) for var in message]))

Запускаем скрипт и получаем исходное сообщение: TWCTF{Crypto-is-fun!}|ENJ0YHOLIDAY!
Фгаг — TWCTF{Crypto-is-fun!}