CR2

#!/usr/bin/env ruby

# AlexCTF
# https://ctf.oddcoder.com/challenges
# CR2

require "z3"

msg = "
0529242a631234122d2b36697f13272c207f2021283a6b0c7908
2f28202a302029142c653f3c7f2a2636273e3f2d653e25217908
322921780c3a235b3c2c3f207f372e21733a3a2b37263b313012
2f6c363b2b312b1e64651b6537222e37377f2020242b6b2c2d5d
283f652c2b31661426292b653a292c372a2f20212a316b283c09
29232178373c270f682c216532263b2d3632353c2c3c2a293504
613c37373531285b3c2a72273a67212a277f373a243c20203d5d
243a202a633d205b3c2d3765342236653a2c7423202f3f652a18
2239373d6f740a1e3c651f207f2c212a247f3d2e65262430791c
263e203d63232f0f20653f207f332065262c3168313722367918
2f2f372133202f142665212637222220733e383f2426386b
"

msg = msg.tr("\n", "").scan(/../).map{|c| c.to_i(16)}

[26].each do |key_len|
  solver = Z3::Solver.new


  key = key_len.times.map{|j| Z3.Bitvec("k#{j}", 7) }
  key.each do |kj|
    solver.assert kj.unsigned_ge(" ".ord)
  end
  plaintext = msg.size.times.map{|i| Z3.Bitvec("p#{i}", 7)}

  "Dear Friend".chars.each_with_index do |pi, i|
    solver.assert plaintext[i] == pi.ord
  end
  "This time I understood my mistake and used".chars.each_with_index do |pi,i|
    solver.assert plaintext[i+5+6+2] == pi.ord
  end

  msg.size.times do |i|
    plain = plaintext[i]
    cipher = msg[i]
    solver.assert cipher == plain^key[i % key_len]
    solver.assert Z3.Or(
      plain == "\n".ord,
      plain == " ".ord,
      plain.unsigned_ge("a".ord) & plain.unsigned_le("z".ord),
      plain.unsigned_ge("A".ord) & plain.unsigned_le("Z".ord),
      # plain.unsigned_ge("0".ord) & plain.unsigned_le("9".ord),
      plain == ".".ord,
      plain == ",".ord,
      plain == "_".ord,
      # plain == "!".ord,
    )
    # "`%\\[]{}#^()<>*?/@\"'&=~+|;:".chars.each do |weird|
    #   solver.assert plain != weird.ord
    # end
  end
  while solver.satisfiable?
    puts "Solvable at key len #{key_len}"
    model = solver.model
    p plaintext.map{|pi| model[pi].to_s.to_i.chr}.join
    p key.map{|kj| model[kj].to_s.to_i.chr}.join
    puts ""
    solver.assert Z3.Or(*plaintext.map{|pi|
      pi != model[pi].to_s.to_i
    })
    # puts "Not solvable at key len #{key_len}"
  end
end