aes128 cbc/ctr static IV attack with z3

aes-z3-excercise.py

from z3 import *
from binascii import unhexlify, hexlify
from itertools import chain

"""
Up for an excercise huh?

https://www.reddit.com/r/crypto/comments/y7c3m/key_recovery_on_aes_ctr_with_static_iv/

> The trivial version of this attack can be done when you that ciphertext_0 is the encryption of known plaintext plaintext_0. Then, to decrypt ciphertext_n you take ciphertext_n xor ciphertext_0 which equals plaintext_n xor plaintext_0. Since you know plaintext_0 already, you can compute (plaintext_n xor plaintext_0) xor plaintext_0 which cancels out the plaintext_0s leaving you with plaintext_n.
> The really basic thing you can do without any known plaintext is xor two ciphertexts together (which gives the same result as xoring the two corresponding plaintexts) and look for patterns/statistics in the results. If the high bit set very rarely in the output you're probably looking is probably text.
> If you do know that it's literally just plain text (ascii) that's encrypted, you can then iteratively guess a few bytes (max 2-3) of plaintext for one of the ciphertexts, using that to attempt decryption of those bytes in the other ciphertexts and see if the results make sense.
> Try decrypting these (AES128CTR, same key, fixed IV):
    5979e785be65e823ef60f8fd
    4f75e486f777a723ff7af8fc
    437de08ab263e83fff7bee8e
    486ee291f772ba28ea78f28e
"""

ex1 = unhexlify('5979e785be65e823ef60f8fd')
ex2 = unhexlify('4f75e486f777a723ff7af8fc')
ex3 = unhexlify('437de08ab263e83fff7bee8e')
ex4 = unhexlify('486ee291f772ba28ea78f28e')

shex = lambda s: str.join(' ', ["%02x" % ord(c) for c in s])
def ascii_diffpairs(diff):
    return [(chr(i), chr(i ^ diff)) for i in range(32, 128) if 32 <= i ^ diff < 128 and i < i ^ diff]
def arrxor(a1, a2):
    return [x ^ y for x, y in zip(a1, a2)]

solver = Solver()
Tu = BitVecs('Tu0 Tu1 Tu2 Tu3 Tu4 Tu5 Tu6 Tu7 Tu8 Tu9 Tua Tub', 8)
Tv = BitVecs('Tv0 Tv1 Tv2 Tv3 Tv4 Tv5 Tv6 Tv7 Tv8 Tv9 Tva Tvb', 8)
Tw = BitVecs('Tw0 Tw1 Tw2 Tw3 Tw4 Tw5 Tw6 Tw7 Tw8 Tw9 Twa Twb', 8)
Tz = BitVecs('Tz0 Tz1 Tz2 Tz3 Tz4 Tz5 Tz6 Tz7 Tz8 Tz9 Tza Tzb', 8)

for var in Tu + Tv + Tw + Tz:
    #-- isascii
    solver.add(var >= 32)
    # solver.add(var < 128)

for i, diff in enumerate(arrxor(ex1, ex2)):
    solver.add(Tu[i] ^ Tv[i] == diff)

for i, diff in enumerate(arrxor(ex2, ex3)):
    solver.add(Tv[i] ^ Tw[i] == diff)

for i, diff in enumerate(arrxor(ex3, ex4)):
    solver.add(Tw[i] ^ Tz[i] == diff)


issat = solver.check()
print(issat)

if issat == sat:
    m = solver.model()
    tostr = lambda arr: str.join('', map(chr, arr))
    print("Tu = %r; %r" % (tostr([m[v].as_long() for v in Tu]), [m[v] for v in Tu]))
    print("Tv = %r; %r" % (tostr([m[v].as_long() for v in Tv]), [m[v] for v in Tv]))
    print("Tw = %r; %r" % (tostr([m[v].as_long() for v in Tw]), [m[v] for v in Tw]))
    print("Tz = %r; %r" % (tostr([m[v].as_long() for v in Tz]), [m[v] for v in Tz]))

"""
[~] LD_LIBRARY_PATH=$Z3/bin PYTHONPATH=$Z3/bin/python python3 ~/aes-z3-excercise.py                                                                                                               ⌚ 15:15:33
sat
Tu = '@@@     @@@ '; [64, 64, 64, 32, 32, 32, 32, 32, 64, 64, 64, 32]
Tv = 'VLC#i2o PZ@!'; [86, 76, 67, 35, 105, 50, 111, 32, 80, 90, 64, 33]
Tw = 'ZDG/,& <P[VS'; [90, 68, 71, 47, 44, 38, 32, 60, 80, 91, 86, 83]
Tz = 'QWE4i7r+EXJS'; [81, 87, 69, 52, 105, 55, 114, 43, 69, 88, 74, 83]
"""




################################################################################
#
#-- ...... Wow. Holy whiskers!
#-- I didn't expect to get THAT in just 3 hours!
#-- Let's try again, this time with our own key.
#-- Cause that Reddit gentleman left his key undisclosed,
#-- and now I have that itch to __verity__ the result.
#
################################################################################
"""
>>> K = unhexlify("b7d23cb4ea7003e4f2d84681d57f43db")
>>> IV = '\0' * 16
>>>
>>> hexlify(AES.new(K, AES.MODE_CBC, IV).encrypt(Tu + '\0\0\0\0')[:12] )
'5394ff7f230f062bbed6451f'
>>> hexlify(AES.new(K, AES.MODE_CBC, IV).encrypt(Tv + '\0\0\0\0')[:12] )
'5498a1b2f8e9e414663f6cff'
>>> hexlify(AES.new(K, AES.MODE_CBC, IV).encrypt(Tw + '\0\0\0\0')[:12] )
'3f34cd7455b02e525b4a6ed9'
>>> hexlify(AES.new(K, AES.MODE_CBC, IV).encrypt(Tz + '\0\0\0\0')[:12] )
'62be3a3c4575bf0767b51ec2'
"""
myex1 = unhexlify('5394ff7f230f062bbed6451f')
myex2 = unhexlify('5498a1b2f8e9e414663f6cff')
myex3 = unhexlify('3f34cd7455b02e525b4a6ed9')
myex4 = unhexlify('62be3a3c4575bf0767b51ec2')

#-- now, I "don't" have the key, exactly as before!
#-- *I do have it ;) but in comments. The solver doesn't know it.

solver = Solver()
Qu = BitVecs('Qu0 Qu1 Qu2 Qu3 Qu4 Qu5 Qu6 Qu7 Qu8 Qu9 Qua Qub', 8)
Qv = BitVecs('Qv0 Qv1 Qv2 Qv3 Qv4 Qv5 Qv6 Qv7 Qv8 Qv9 Qva Qvb', 8)
Qw = BitVecs('Qw0 Qw1 Qw2 Qw3 Qw4 Qw5 Qw6 Qw7 Qw8 Qw9 Qwa Qwb', 8)
Qz = BitVecs('Qz0 Qz1 Qz2 Qz3 Qz4 Qz5 Qz6 Qz7 Qz8 Qz9 Qza Qzb', 8)

#-- just ^D-multicursor the shit out of the copypaste

for var in Qu + Qv + Qw + Qz:
    solver.add(var >= 32)
    # solver.add(var < 128)

for i, diff in enumerate(arrxor(ex1, ex2)):
    solver.add(Qu[i] ^ Qv[i] == diff)

for i, diff in enumerate(arrxor(ex2, ex3)):
    solver.add(Qv[i] ^ Qw[i] == diff)

for i, diff in enumerate(arrxor(ex3, ex4)):
    solver.add(Qw[i] ^ Qz[i] == diff)

issat = solver.check()
print(issat)
if issat == sat:
    m = solver.model()
    tostr = lambda arr: str.join('', map(chr, arr))
    print("Qu = %r; %r" % (tostr([m[v].as_long() for v in Qu]), [m[v] for v in Qu]))
    print("Qv = %r; %r" % (tostr([m[v].as_long() for v in Qv]), [m[v] for v in Qv]))
    print("Qw = %r; %r" % (tostr([m[v].as_long() for v in Qw]), [m[v] for v in Qw]))
    print("Qz = %r; %r" % (tostr([m[v].as_long() for v in Qz]), [m[v] for v in Qz]))

"""
sat
Qu = '@@@     @@@ '; [64, 64, 64, 32, 32, 32, 32, 32, 64, 64, 64, 32]
Qv = 'VLC#i2o PZ@!'; [86, 76, 67, 35, 105, 50, 111, 32, 80, 90, 64, 33]
Qw = 'ZDG/,& <P[VS'; [90, 68, 71, 47, 44, 38, 32, 60, 80, 91, 86, 83]
Qz = 'QWE4i7r+EXJS'; [81, 87, 69, 52, 105, 55, 114, 43, 69, 88, 74, 83]

FUCK YOU Z3

FUCK YOU STM SOLVING SHITTY CRYPTO

GO TO HELL YOU ARCANE MAGIC THIS IS BEYOND MY COMPREHENSION
"""


tokens = list(map(unhexlify, """
A559844F7209F7144334F13CD0B713A47D5AD10008410F358204C4DA5937379A
22988349266985AD51E1219E8476195F8F2167888E0D98582BC82EA31C080D6F
BA6EFD1D37D968906E1AE0FD52D9BD8A2D89B730AECD858683D803EDB3734CFE
2B19BD15EB2D69A4A49E31692313F4E4687D7F6419F5D265E857B4A11C9EDC75
""".strip().split()))

[
# unhexlify('18B8D4934B844477EA0AFECD698FEDD0B4883BFD3C31EA28A2B8190B13E4B0A5'),
# unhexlify('342870E7C04D90B78C0170D9EDA4F411BDF89DA04D506AC11848176E2B907E1F'),
# unhexlify('FFAC7182929353CE89C26F2ABC41A2CBB2394440B064F7B12DB5D2F79D99DE34'),
# unhexlify('F072C1E77511BBFD895575DD40E458DECD39B47FDF62401D59D4F30F648D7F25'),
# unhexlify('7AAB524093676E8281A74668CBB0D16DE9E240870FF2CE5EAD75D246D66FA7CE'),
]

nchars = min(8, len(tokens[0]))

names = list(reversed('k l m n p q r s t u'.split()))
def make_token_vars():
    family = names.pop()
    name = lambda i: 'Z%s%d' % (family, i)
    return [ BitVec(name(i), 8) for i in range(nchars) ]

solver = Solver()

Z = [make_token_vars() for token in tokens]
# print(Z)

# for var in chain(*Z): #-- i expected sum(Z) to kinda just work here >___>
#     solver.add(var >= 32)

for k, token in enumerate(tokens):
    if k == 0: continue
    A = Z[k-1]
    B = Z[k]
    for i, diff in enumerate(arrxor(tokens[k-1][:nchars], tokens[k][:nchars])):
        solver.add(A[i] ^ B[i] == diff)


print()

issat = solver.check()
print(issat)
if issat == sat:
    model = solver.model()
    tostr = lambda arr: str.join('', map(chr, arr))
    for i, token in enumerate(tokens):
        modelbytes = [model[v].as_long() for v in Z[i]]
        print("   token %s   " % hexlify(token[:nchars]))
        print("%s; %r" % (shex(tostr(modelbytes)), tostr(modelbytes)))

# print(solver.assertions()) #-- dump constraint AST; same as repr(solver)
# print(solver.statistics())


#-- .... Hello Z3!!!! You're awesome! //