Break XOR Cipher with Z3

In previous post, I showed how to break Caesar cipher with Z3.

This wasn't really all that exciting as Caesar cipher has only 26 possibilities, so it's triival to break with brute force, and you can even just display all possible answers and choose the right one manually.

So let's do something slightly more complicated - a 4 characetr XOR cipher. It has 4.3 billion possible keys, so solving it by brute force would be a hassle.

Writing solvers for XOR cipher is still fairly basic CTF exercise, but at least we're one step into not completely trivial territory.

The solver can handle XOR ciphers of arbitrary length as long as it's known.

The Challenge

The following plaintext from Wikipedia:

Cryptography, or cryptology is the practice and study of techniques for secure communication in the presence of adversarial behavior. More generally, cryptography is about constructing and analyzing protocols that prevent third parties or the public from reading private messages. Modern cryptography exists at the intersection of the disciplines of mathematics, computer science, information security, electrical engineering, digital signal processing, physics, and others. Core concepts related to information security (data confidentiality, data integrity, authentication, and non-repudiation) are also central to cryptography. Practical applications of cryptography include electronic commerce, chip-based payment cards, digital currencies, computer passwords, and military communications.

Random encryption

This program picks a random key, and runs XOR cipher on provided plaintext:

#!/usr/bin/env ruby

key_len = 4
key = key_len.times.map{ rand(256) }
text = STDIN.read.bytes
encrypted = (0...text.size).map{|i| text[i] ^ key[i % key_len]}.pack("C*")
print encrypted

The output is unprintable binary so I'm not including it here.

How to break Caesar Cipher with Z3

Z3 rules explaining XOR cipher are easier than for Caesar cipher, we just need to use 8-bit bit vectors instead of integers.

We add as a hard assumption that all characters are in printable range, either 0x0A (newline), or a printable ASCII character (0x20-0x7E).

So all we need is some rule how to decide which decoding is correct. And for that I'm just counting two most common characters in English text - space and lowercase "e". For longer keys, shorter texts, or something more complicated than English text we could include more rules, but this is enough.

Solver

#!/usr/bin/env ruby

require "z3"

class XorSolver
  def initialize(text)
    @key_len = 4
    @key = (0...@key_len).map{|i| Z3.Bitvec("k#{i}", 8) }
    @ct = text.bytes
  end

  def call
    @solver = Z3::Optimize.new
    # Variables for each plaintext letter
    @pt = (0...@ct.size).map{|i| Z3.Bitvec("pt#{i}", 8) }

    # This is how XOR cipher works
    (0...@pt.size).each do |i|
      @solver.assert @pt[i] == @ct[i] ^ @key[i % @key_len]
    end

    # All characters are newline (0x0A) or printable character (0x20-0x7E)
    @pt.each do |pti|
      @solver.assert Z3.Or(pti == 0x0A, pti.unsigned_ge(0x20))
      @solver.assert pti.unsigned_le(0x7E)
    end

    # Get as many space, and lowercase "e" as possible
    @pt.each do |pti|
      @solver.assert_soft pti == 0x20
      @solver.assert_soft pti == 'e'.ord
    end

    if @solver.satisfiable?
      model = @solver.model
      puts @pt.map{|pti| model[pti].to_s.to_i.chr}.join
    else
      puts "No solution found"
    end
  end
end

text = open(ARGV[0] || "encrypted.txt").read.b
XorSolver.new(text).call

Is it practical?

This is actually a reasonable way to write simple solvers for CTFs. They're not as performant as hand made solvers, but it's a lot more straightforward to write a Z3 solver than a hand made one. If you know encryption algorithm exactly, it's weak, and you have partial knowledge of the plaintext - situation that's essentially limited to easy CTFs - Z3 can be of some use.

Code

All code for this post is available on GitHub.