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 characetrXOR 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 rubykey_len=4key=key_len.times.map{rand(256)}text=STDIN.read.bytesencrypted=(0...text.size).map{|i|text[i]^key[i%key_len]}.pack("C*")printencrypted

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 rubyrequire"z3"classXorSolverdefinitialize(text)@key_len=4@key=(0...@key_len).map{|i|Z3.Bitvec("k#{i}",8)}@ct=text.bytesenddefcall@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).eachdo|i|@solver.assert@pt[i]==@ct[i]^@key[i%@key_len]end# All characters are newline (0x0A) or printable character (0x20-0x7E)@pt.eachdo|pti|@solver.assertZ3.Or(pti==0x0A,pti.unsigned_ge(0x20))@solver.assertpti.unsigned_le(0x7E)end# Get as many space, and lowercase "e" as possible@pt.eachdo|pti|@solver.assert_softpti==0x20@solver.assert_softpti=='e'.ordendif@solver.satisfiable?model=@solver.modelputs@pt.map{|pti|model[pti].to_s.to_i.chr}.joinelseputs"No solution found"endendendtext=open(ARGV[0]||"encrypted.txt").read.bXorSolver.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.