Skip to content

Instantly share code, notes, and snippets.

@rikaardhosein
Created October 4, 2015 20:14
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save rikaardhosein/57c91dcbdd9af7a6ab43 to your computer and use it in GitHub Desktop.
Save rikaardhosein/57c91dcbdd9af7a6ab43 to your computer and use it in GitHub Desktop.
from z3 import *
ciphertext = "320b1c5900180a034c74441819004557415b0e0d1a316918011845524147384f5700264f48091e4500110e41030d1203460b1d0752150411541b455741520544111d0000131e0159110f0c16451b0f1c4a74120a170d460e13001e120a1106431e0c1c0a0a1017135a4e381b16530f330006411953664334593654114e114c09532f271c490630110e0b0b".decode("hex")
length = len(ciphertext)
ct = [ ord(ciphertext[i]) for i in range(0,length) ]
def encrypt(s):
c = []
space = IntVal(0xa)
for i in range(0, length):
pos = space+i
idx = If( pos < (length-1), space+i, space)
val = Select(s,i) ^ Select(s, idx)
c.append(val)
space = If( (Select(s,i)&1) == 0, space+1, space-1)
return c
s = Solver()
A = Array('plaintext', IntSort(), BitVecSort(8))
solution = encrypt(A)
for i in range(0, length):
s.add(solution[i] == ct[i])
s.check()
k = s.model()
solution= k[A].as_list()
solution = solution[:len(solution)-1]
plaintext = {}
for t in solution:
idx = t[0].as_long()
val = t[1].as_long()
plaintext[idx] = chr(val)
print (''.join([plaintext[i] for i in range(0,length)]))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment