z3，我的超人-week1-2021

复健失败.jpg
虽然这题大概不是这么解的，但还是记一下新学的姿势（）

crypto-对称之美

题目：

z3： https://github.com/Z3Prover/z3/releases/tag/z3-4.8.10
下载z3-4.8.10-x64-win.zip，配置环境变量

# Running this example on Windows:
# set PATH=%PATH%;MYZ3\bin
# set PYTHONPATH=MYZ3\bin\python
# python example.py

写个脚本：

c=b'D#M\x15!(#3\x15L#\x08V#<\x02n\x19GX;%2/L\x18"\x03V\'"\x13#\x15Z\x0c?m8\'Lf+F\x06#\'\x18:\x19Z\x1fl"%a\x08\x1e+\x11\x1f,)V,\x11X\x19".2a\t\r)\x0eV-:\x1e+\x02\x14r#8#oL8"\x0f\x05b-\x19;\x1cPX.(w5\x04\tj\t\x14(+\x15:\x03\x14\x0c$(:2\t\x00<\x03\x05nn|,\x05@X%9w"\r\x02j\x07\x1a1!V<\x15X\x198(w5\x03L)\t\x1a-<\x05n\x11Z\x1clG85\x04\t8F\x15-#\x06!\x03]\x0c%"9 \x00L>\x03\x15* \x1f?\x05Q\x0bbG\x0e.\x19L\'\x07\x0fb \x19:PF\x1d-!>;\tL#\x12Zb,\x03:PM\x179?w#\x1e\r#\x08VH\'\x05n\x12A\x0b5m .\x1e\x07#\x08\x11b,\x13&\x19Z\x1cl9?$L\x1f)\x03\x18\'=V:\x1f\x14\x0b)(<af\x03?\x12V17\x1b#\x15@\n5m )\t\x02j\x1f\x197n\x1a!\x1f_X-9w L\x1c+\x0f\x186\'\x18)^\x14r\x18%23\tL+\x14\x13b=\x138\x15F\x19 m%$\r\x1f%\x08\x05b(\x19<P@\x10%>ya8\x04/F|$\'\x04=\x04\x14\x11?m#)\r\x18j\x11\x13e<\x13n\x18U\n(` (\x1e\t.F\x02-n\x1a!\x1f_X*"%af\x05>HV\r;\x04n\x11Z\x1b%(95L\r$\x05\x131:\x19<\x03\x14\x15-4w/\x03\x18j\x0e\x174+V&\x11PXF,w/\r\x01/F\x10-<V\'\x04\x18X.8#a\x18\x04/\x1fV) \x139P@\x10-9w5\x04\t#\x14VH!\x01 PV\x17($22L\x1b/\x14\x13b,\x17=\x19W\x19 !.a\x1f\x15\'\x0b\x136<\x1f-\x11XTl,$af\x1b/\x14\x13b:\x1e!\x03QX#+w1\x03\x18/\x08\x02+/\x1an\x00F\x1d(,#.\x1e\x1fj\t\x04b>\x04+\t\x1aXF\x19?$\x1e\t,\t\x04\'bV:\x18]\x0bl.6,\tL#\x08V*/\x18*\t\x14\x0f$(#)\t\x1ejl\x15*!\x19=\x19Z\x1fl,w,\r\x18/JV!/\x02-\x18]\x16+m3(\x02\x02/\x14V-<VD\x11B\x17%)>/\x0bL(\x03\x1f,)V!\x1e\x14\x0c$(w,\t\x02?F\x19$n\x17n\x03Z\x19>!>/\x0b@jl\x1e7 \x11<\t\x14\x08-.<a\x03\nj\x11\x19.8\x13=P[\nl/2 \x1e\x1fkl"#%\x13n\x11\x14\x14#"<a\r\x18j\x1f\x197<V(\x11W\x1dl$9a\x18\x04/F\x1b+<\x04!\x02\x14r-#3a\x05\x01+\x01\x1f,+V/PX\x11"(w2\x18\x1e+\x0f\x11*:V*\x1fC\x16l9?$Lf\'\x0f\x12&"\x13`Pm\x179j;-L\x1f/\x03V !\x02&PG\x11(($a\x03\nj\x1f\x197<VD\x16U\x1b)m63\tL:\x14\x136:\x0fn\x03M\x15!(#3\x05\x0f+\nXb\x1a\x1e\'\x03\x14\x11?m]*\x02\x03=\x08V#=V,\x19X\x198(% \x00L9\x1f\x1b/+\x02<\t\x14\x19")w(\x18K9F|5&\x13<\x15\x14\x1a#9?a\x1f\x05.\x03\x05b+\x1f:\x18Q\nl>>%\tL%\x00V6&\x1f=P>\x1c%;>%\x05\x02-F\x1a+ \x13n\x11D\x08),%a\x01\x038\x03V-<V"\x15G\x0bl9?$L\x1f+\x0b\x13lD%!P\\\x1d>(w(\x1fL>\x0e\x13b(\x1a/\x17\x0eXF%0 \x01\t1>F0\x11\x1f{]U\'9\x1ed\'9]aR\x18&j\x10\x1b>Z\x01\x13\x0ef1$_8\x1b|'

from z3 import *

s = Solver()
key=[BitVec('key_%d' % i, 8) for i in range(16)]
cipher=[BitVec('cipher_%d' % i, 8) for i in range(len(c))]
plain=[BitVec('plain_%d' % i, 8) for i in range(len(c))]
for i in range(len(c)):
    s.add(key[i%16]<122,key[i%16]>48)
    s.add(cipher[i]==c[i])
    s.add(plain[i]==cipher[i]^key[i%16])
    s.add(Or(And(plain[i]>=0x20, plain[i]<=0x7E),plain[i]==0xA,plain[i]==0xD))
s.add(plain[-47]==ord('f'))
s.add(plain[-46]==ord('l'))
s.add(plain[-45]==ord('a'))
s.add(plain[-44]==ord('g'))
s.add(plain[-40]==ord('h'))
s.add(plain[-39]==ord('g'))
s.add(plain[-38]==ord('a'))
s.add(plain[-37]==ord('m'))
s.add(plain[-36]==ord('e'))
s.add(plain[-35]==ord('{'))
s.add(plain[-2]==ord('}'))
print(s.check())
m=s.model()

#test_key="".join(chr(int(obj_to_string(m[key[i]]))) for i in range(16))
#print("key=",test_key)
test_plain="".join(chr(int(obj_to_string(m[plain[i]]))) for i in range(len(c)))
f=open('111.txt','w')
f.write(test_plain)
f.close()

最后编辑于：2021.02.07 14:01:13