plaidctf23/02_the_other_css_disk_a.ipynb

{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[240, 150, 0, 62, 234, 110, 177, 181]\n",
      "[236, 247, 121, 13, 52, 60, 10, 181]\n",
      "[240, 27, 101, 225, 163, 29, 157, 148]\n",
      "[6, 96, 115, 108, 181, 159, 107, 22]\n",
      "[16, 84, 34, 56, 198, 203, 125, 52]\n",
      "[231, 148, 41, 2, 11, 205, 176, 200]\n",
      "[44, 247, 96, 97, 104, 28, 81, 25]\n",
      "[181, 239, 145, 180, 153, 58, 200, 107]\n",
      "[7, 186, 235, 63, 143, 58, 177, 204]\n"
     ]
    }
   ],
   "source": [
    "from pwn import remote, context\n",
    "context.log_level = \"error\"\n",
    "\n",
    "def query(mangle_in):\n",
    "    r = remote(\"the-other-css.chal.pwni.ng\", 1996)\n",
    "    # challenge key is null, mangle is low bits set\n",
    "    r.sendline(bytes([0] * 8 + list(mangle_in)))\n",
    "    res = r.recv(8)\n",
    "    r.close()\n",
    "    return list(res)\n",
    "\n",
    "mangle_ins = [\n",
    "    [0, 0, 0, 0, 0, 0, 0, 0],\n",
    "    [1, 0, 0, 0, 0, 0, 0, 0],\n",
    "    [0, 1, 0, 0, 0, 0, 0, 0],\n",
    "    [0, 0, 1, 0, 0, 0, 0, 0],\n",
    "    [0, 0, 0, 1, 0, 0, 0, 0],\n",
    "    [0, 0, 0, 0, 1, 0, 0, 0],\n",
    "    [0, 0, 0, 0, 0, 1, 0, 0],\n",
    "    [0, 0, 0, 0, 0, 0, 1, 0],\n",
    "    [0, 0, 0, 0, 0, 0, 0, 1],\n",
    "]\n",
    "\n",
    "mangle_outs = [query(mangle_in) for mangle_in in mangle_ins]\n",
    "\n",
    "for mangle_out in mangle_outs:\n",
    "    print(mangle_out) "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [],
   "source": [
    "import z3\n",
    "from css.table import table\n",
    "\n",
    "def mix(key, value):\n",
    "    ret = value ^ z3.LShR(value, 8) ^ key\n",
    "    return ret\n",
    "\n",
    "def shift(value):\n",
    "    ret = value ^ (value << 56)\n",
    "    return ret\n",
    "\n",
    "def build_tabulate_one(solver):\n",
    "    tabulate_one = z3.Function(\"tabulate\", z3.BitVecSort(8), z3.BitVecSort(8))\n",
    "    for idx, table_i in enumerate(table):\n",
    "        solver.add(tabulate_one(idx) == table_i)\n",
    "    return tabulate_one\n",
    "\n",
    "def tabulate(value, name, tabulate_one, solver):\n",
    "    value_sym = z3.BitVec(name, 64)\n",
    "    solver.add(value_sym == value)\n",
    "    ret = []\n",
    "    for pos in reversed(range(0, 64, 8)):\n",
    "        ret.append(tabulate_one(z3.Extract(pos+7, pos, value_sym)))\n",
    "    ret = z3.Concat(*ret)\n",
    "    return ret\n",
    "\n",
    "def u8s_to_bitecval(x):\n",
    "    return z3.BitVecVal(int(bytes(x).hex(), 16), len(x) * 8)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "sat\n",
      "0bfb91847347be4a\n"
     ]
    }
   ],
   "source": [
    "s = z3.Solver()\n",
    "\n",
    "tabulate_one = build_tabulate_one(s)\n",
    "\n",
    "key = z3.BitVec(\"key\", 64)\n",
    "\n",
    "for idx, (mangle_in, mangle_out) in enumerate(zip(mangle_ins, mangle_outs)):\n",
    "    value = u8s_to_bitecval(mangle_in)\n",
    "    goal = u8s_to_bitecval(mangle_out)\n",
    "\n",
    "    value = mix(key, value)\n",
    "    value = shift(value)\n",
    "    value = mix(key, value)\n",
    "    value = shift(value)\n",
    "    value = mix(key, value)\n",
    "    value = tabulate(value, f\"one_{idx}\", tabulate_one, s)\n",
    "    value = shift(value)\n",
    "    value = mix(key, value)\n",
    "    value = tabulate(value, f\"two_{idx}\", tabulate_one, s)\n",
    "    value = shift(value)\n",
    "    value = mix(key, value)\n",
    "    value = shift(value)\n",
    "    value = mix(key, value)\n",
    "\n",
    "    s.add(value == goal)\n",
    "\n",
    "print(s.check())\n",
    "\n",
    "cipher_auth_key = hex(s.model()[key].as_long())[2:].zfill(16)\n",
    "print(cipher_auth_key)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [],
   "source": [
    "from css.mangle import mangle\n",
    "\n",
    "def bxor(a, b):\n",
    "    return bytes([i ^ j for i, j in zip(a, b)])\n",
    "def do_cipher_auth_key(x):\n",
    "    k = bytes.fromhex(cipher_auth_key)\n",
    "    return bxor(x, k)\n",
    "\n",
    "r = remote(\"the-other-css.chal.pwni.ng\", 1996)\n",
    "\n",
    "host_challenge = bytes([0] * 16)\n",
    "r.send(host_challenge)\n",
    "challenge_key = host_challenge[:8]\n",
    "encrypted_host_nonce = host_challenge[8:]\n",
    "host_mangling_key = do_cipher_auth_key(challenge_key)\n",
    "\n",
    "r.recv(8)\n",
    "\n",
    "host_nonce = do_cipher_auth_key(encrypted_host_nonce)\n",
    "\n",
    "player_challenge_key = r.recv(8)\n",
    "encrypted_player_nonce = r.recv(8)\n",
    "player_nonce = do_cipher_auth_key(encrypted_player_nonce)\n",
    "\n",
    "player_mangling_key = do_cipher_auth_key(player_challenge_key)\n",
    "response = mangle(player_mangling_key, do_cipher_auth_key(player_nonce))\n",
    "r.send(response)\n",
    "\n",
    "mangling_key = bxor(host_mangling_key, player_mangling_key)\n",
    "session_nonce = bxor(host_nonce, player_nonce)\n",
    "session_key = mangle(mangling_key, session_nonce)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "729it [01:14,  9.83it/s]\n"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "042d21becf5bb0e3\n"
     ]
    },
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "100%|██████████| 730/730 [01:25<00:00,  8.49it/s]\n"
     ]
    }
   ],
   "source": [
    "from tqdm import tqdm\n",
    "from itertools import count, cycle\n",
    "from css.cipher import Cipher\n",
    "from css.mode import Mode\n",
    "\n",
    "sectors = []\n",
    "for _ in tqdm(count()):\n",
    "    ct = b\"\"\n",
    "    try:\n",
    "        ct = r.recvn(8208, timeout=5)\n",
    "        sectors.append(ct)\n",
    "    except Exception:\n",
    "        ct = r.recv()\n",
    "        sectors.append(ct)\n",
    "    if len(ct) != 8208:\n",
    "        break\n",
    "\n",
    "stream_cipher = Cipher(session_key, Mode.Data)\n",
    "print(session_key.hex())\n",
    "\n",
    "decrypted_sectors = []\n",
    "for sector in tqdm(sectors):\n",
    "    sector = stream_cipher.decrypt(sector)\n",
    "    x, t = sector[:16], sector[16:]\n",
    "    decrypted_sectors.append(bxor(cycle(x), t))\n",
    "\n",
    "with open(\"diskA.iso\", \"wb\") as f:\n",
    "    for s in decrypted_sectors:\n",
    "        f.write(s)"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "sage",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.9.16"
  },
  "orig_nbformat": 4
 },
 "nbformat": 4,
 "nbformat_minor": 2
}