plaidctf23/04_mitm_mangle.ipynb

{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "import z3\n",
    "from css.mangle import mangle, mix, unmix, shift, unshift, table, reverse_table\n",
    "\n",
    "ks = [ z3.BitVec(f\"k{i}\", 8) for i in range(8) ]\n",
    "pts = [ z3.BitVec(f\"pt{i}\", 8) for i in range(8) ]\n",
    "cts = [ z3.BitVec(f\"ct{i}\", 8) for i in range(8) ]\n",
    "\n",
    "t = z3.Function(\"t\", z3.BitVecSort(8), z3.BitVecSort(8))\n",
    "rt = z3.Function(\"rt\", z3.BitVecSort(8), z3.BitVecSort(8))\n",
    "\n",
    "def tabulate(x):\n",
    "    return [t(z3.simplify(i)) for i in x]\n",
    "def untabulate(x):\n",
    "    return [rt(z3.simplify(i)) for i in x]\n",
    "\n",
    "def mangle_mitm(key, pts, cts):\n",
    "    fwd = pts\n",
    "\n",
    "    fwd = mix(key, fwd)\n",
    "    fwd = shift(fwd)\n",
    "    fwd = mix(key, fwd)\n",
    "    fwd = shift(fwd)\n",
    "    fwd = mix(key, fwd)\n",
    "    fwd = tabulate(fwd)\n",
    "    fwd = shift(fwd)\n",
    "    fwd = mix(key, fwd)\n",
    "\n",
    "    rev = cts\n",
    "    rev = unmix(key, rev)\n",
    "    rev = unshift(rev)\n",
    "    rev = unmix(key, rev)\n",
    "    rev = unshift(rev)\n",
    "    rev = untabulate(rev)\n",
    "\n",
    "    return fwd, rev\n",
    "\n",
    "fwd_sym, rev_sym = mangle_mitm(ks, pts, cts)\n",
    "\n",
    "def mitm_report(which):\n",
    "    fwd_sym_str = str(fwd_sym[which])\n",
    "    rev_sym_str = str(rev_sym[which])\n",
    "\n",
    "    print(f\"fwd[{which}] = (\\n{fwd_sym_str}\\n)\")\n",
    "    print(f\"rev[{which}] = (\\n{rev_sym_str}\\n)\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "fwd[0] = (\n",
      "t(pt0 ^ k7 ^ pt6 ^ k6 ^ pt5 ^ k0) ^\n",
      "t(pt7 ^ k6 ^ pt5 ^ k7 ^ pt6 ^ k5 ^ pt4) ^\n",
      "k0 ^\n",
      "0\n",
      ")\n",
      "rev[0] = (\n",
      "rt(k0 ^ ct7 ^ ct5 ^ ct3 ^ ct1 ^ k2 ^ k4 ^ k6 ^ ct0)\n",
      ")\n"
     ]
    }
   ],
   "source": [
    "mitm_report(0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "fwd[7] = (\n",
      "t(pt7 ^ k6 ^ pt5 ^ k7 ^ pt6 ^ k5 ^ pt4) ^\n",
      "k7 ^\n",
      "t(pt6 ^ k5 ^ pt4 ^ k6 ^ pt5 ^ k4 ^ pt3)\n",
      ")\n",
      "rev[7] = (\n",
      "rt(ct6 ^ ct4 ^ ct2 ^ ct0 ^ k1 ^ k3 ^ k5 ^ k7)\n",
      ")\n"
     ]
    }
   ],
   "source": [
    "mitm_report(7)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "demo_key = [27, 25, 196, 182, 180, 11, 79, 81]\n"
     ]
    }
   ],
   "source": [
    "from random import randbytes\n",
    "\n",
    "# Generate samples of ct = mangle(key, pt) of mangle from one shared key\n",
    "# Sweet spot seems to be around 32 samples\n",
    "n_samples = 32\n",
    "\n",
    "demo_key = list(randbytes(8))\n",
    "\n",
    "pts = [\n",
    "    list(randbytes(8))\n",
    "    for _ in range(n_samples)\n",
    "]\n",
    "cts = [\n",
    "    list(mangle(demo_key, i))\n",
    "    for i in pts\n",
    "]\n",
    "\n",
    "print(f\"{demo_key = }\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "sat\n",
      "known_k0   = 27\n",
      "known_k67  = 30\n",
      "known_k5   = 11\n",
      "known_k246 = 63\n"
     ]
    }
   ],
   "source": [
    "s = z3.Solver()\n",
    "\n",
    "for idx, table_i in enumerate(table):\n",
    "    s.add(t(idx) == table_i)\n",
    "for idx, reverse_table_i in enumerate(reverse_table):\n",
    "    s.add(rt(idx) == reverse_table_i)\n",
    "\n",
    "k0, k67, k5, k246 = z3.BitVecs(\"k0 k67 k5 k246\", 8)\n",
    "for pti, cti in zip(pts, cts):\n",
    "    pt0, pt1, pt2, pt3, pt4, pt5, pt6, pt7 = pti\n",
    "    ct0, ct1, ct2, ct3, ct4, ct5, ct6, ct7 = cti\n",
    "\n",
    "    # enforce mitm at byte 0\n",
    "    # all usages of key can be separated into 4 linear components\n",
    "    # key[0], key[6] ^ key[7], key[5] and key[2] ^ key[4] ^ key[6]\n",
    "    # brute force is only 32 bits\n",
    "    fwd = (\n",
    "        t(pt0 ^ pt5 ^ pt6 ^ k0 ^ k67) ^\n",
    "        t(pt4 ^ pt5 ^ pt6 ^ pt7 ^ k5 ^ k67) ^\n",
    "        k0\n",
    "    )\n",
    "    rev = rt(ct0 ^ ct1 ^ ct3 ^ ct5 ^ ct7 ^ k0 ^ k246)\n",
    "\n",
    "    s.add(fwd == rev)\n",
    "\n",
    "print(s.check())\n",
    "m = s.model()\n",
    "\n",
    "known_k0, known_k67, known_k5, known_k246 = [\n",
    "    m[ki].as_long()\n",
    "    for ki in [k0, k67, k5, k246]\n",
    "]\n",
    "print(f\"\"\"\\\n",
    "{known_k0   = }\n",
    "{known_k67  = }\n",
    "{known_k5   = }\n",
    "{known_k246 = }\"\"\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "sat\n",
      "known_k56  = 68\n",
      "known_k7   = 81\n",
      "known_k4   = 180\n",
      "known_k135 = 164\n"
     ]
    }
   ],
   "source": [
    "s = z3.Solver()\n",
    "\n",
    "for idx, table_i in enumerate(table):\n",
    "    s.add(t(idx) == table_i)\n",
    "for idx, reverse_table_i in enumerate(reverse_table):\n",
    "    s.add(rt(idx) == reverse_table_i)\n",
    "\n",
    "k56, k7, k4, k135 = z3.BitVecs(\"k56 k7 k4 k135\", 8)\n",
    "for pti, cti in zip(pts, cts):\n",
    "    pt0, pt1, pt2, pt3, pt4, pt5, pt6, pt7 = pti\n",
    "    ct0, ct1, ct2, ct3, ct4, ct5, ct6, ct7 = cti\n",
    "\n",
    "    # enforce mitm at byte 7\n",
    "    # 4 linear components, also 32 bit brute force\n",
    "    fwd = (\n",
    "        t(pt4 ^ pt5 ^ pt6 ^ pt7 ^ k56 ^ k7) ^\n",
    "        t(pt3 ^ pt4 ^ pt5 ^ pt6 ^ k4 ^ k56) ^\n",
    "        k7\n",
    "    )\n",
    "    rev = (\n",
    "        rt(ct0 ^ ct2 ^ ct4 ^ ct6 ^ k135 ^ k7)\n",
    "    )\n",
    "\n",
    "    s.add(fwd == rev)\n",
    "\n",
    "print(s.check())\n",
    "m = s.model()\n",
    "\n",
    "known_k56, known_k7, known_k4, known_k135 = [\n",
    "    m[ki].as_long()\n",
    "    for ki in [k56, k7, k4, k135]\n",
    "]\n",
    "\n",
    "print(f\"\"\"\\\n",
    "{known_k56  = }\n",
    "{known_k7   = }\n",
    "{known_k4   = }\n",
    "{known_k135 = }\"\"\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "sat\n",
      "derived_key = [27, 25, 196, 182, 180, 11, 79, 81]\n"
     ]
    }
   ],
   "source": [
    "s = z3.Solver()\n",
    "\n",
    "for idx, table_i in enumerate(table):\n",
    "    s.add(t(idx) == table_i)\n",
    "for idx, reverse_table_i in enumerate(reverse_table):\n",
    "    s.add(rt(idx) == reverse_table_i)\n",
    "\n",
    "s.add(known_k0 == ks[0])\n",
    "s.add(known_k4 == ks[4])\n",
    "s.add(known_k5 == ks[5])\n",
    "s.add(known_k56 ^ known_k5 == ks[6])\n",
    "s.add(known_k7 == ks[7])\n",
    "\n",
    "for pti, cti in zip(pts, cts):\n",
    "    # symbolic solve for the remaining 24 bits\n",
    "    fwd, rev = mangle_mitm(ks, pti, cti)\n",
    "    for fwdi, revi in zip(fwd, rev):\n",
    "        s.add(fwdi == revi)\n",
    "\n",
    "print(s.check())\n",
    "m = s.model()\n",
    "derived_key = [\n",
    "    m[ki].as_long()\n",
    "    for ki in ks\n",
    "]\n",
    "print(f\"{derived_key = }\")\n",
    "assert(derived_key == demo_key)"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "base",
   "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
}