## DEV Community

Tomasz Wegrzanowski

Posted on

# Break XOR 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) }
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