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.
Top comments (0)