引自大佬：z3约束求解器 | happi0 (gitee.io)

z3简介:

  • 官方: z3是由微软公司开发的一个优秀的SMT求解器（也就定理证明器），它能够检查逻辑表达式的可满足性。
  • 人话: 解方程

通过下面一道题来展示z3的优势

题目:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
#!/usr/bin/env python3
import sympy
import json

m = sympy.randprime(2**257, 2**258)                                     
M = sympy.randprime(2**257, 2**258)                                     
a, b, c = [(sympy.randprime(2**256, 2**257) % m) for _ in range(3)]     

x = (a + b * 3) % m
y = (b - c * 5) % m
z = (a + c * 8) % m

flag = int(open('flag', 'rb').read().strip().hex(), 16)
p = pow(flag, a, M)                                 
q = pow(flag, b, M)                             //类似rsa加密,可以考虑共模攻击

json.dump({ key: globals()[key] for key in "Mmxyzpq" }, open('crypted', 'w'))
1
2
3
4
5
6
7
8
9
p = 240670121804208978394996710730839069728700956824706945984819015371493837551238,
q = 63385828825643452682833619835670889340533854879683013984056508942989973395315,

M = 349579051431173103963525574908108980776346966102045838681986112083541754544269,
m = 282832747915637398142431587525135167098126503327259369230840635687863475396299,

x = 254732859357467931957861825273244795556693016657393159194417526480484204095858,
y = 261877836792399836452074575192123520294695871579540257591169122727176542734080
z = 213932962252915797768584248464896200082707350140827098890648372492180142394587,

解题:

题目思路比较简单,只需要求得a和b来充当最后类似rsa加密的e1和e2

即可采用共模攻击解的flag

于是先求a,b,c

常规思路:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
#!/usr/bin/python

m = 282832747915637398142431587525135167098126503327259369230840635687863475396299
x = 254732859357467931957861825273244795556693016657393159194417526480484204095858
y = 261877836792399836452074575192123520294695871579540257591169122727176542734080
z = 213932962252915797768584248464896200082707350140827098890648372492180142394587

min = 2**256 % m
max = 2**257 % m

if min > max:
    min,max = max,min

for a in range(min,max):
    for b in range(min,max):
        for c in range(min,max):
            if x == (a + b * 3) % m and y == (b - c * 5) % m and z == (a + c * 8) % m:
                print(a)
                print(b)
                break

算到是应该能算出来,不过时间等不起,所以我们换一种工具

思路2:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
#!/usr/bin/python
from z3 import *
import gmpy2

z=213932962252915797768584248464896200082707350140827098890648372492180142394587
m=282832747915637398142431587525135167098126503327259369230840635687863475396299
x=254732859357467931957861825273244795556693016657393159194417526480484204095858
y=261877836792399836452074575192123520294695871579540257591169122727176542734080

a,b,c = Ints('a b c')
s = Solver()

min = 2**256 % m
max = 2**257 % m

if max < min:
    max,min = min,max

s.add(x == (a + 3*b) % m )
s.add(y == (b - 5*c) % m )
s.add(z == (a + 8*c) % m )

s.add( min < a , a < max)
s.add( min < b , b < max)

if s.check() == sat:
    A,B= s.model()[a].as_long(),s.model()[b].as_long()
    print(A,B)

可以秒解出a和b的值,然后一个简单的共模攻击

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
#!/usr/bin/python2

import gmpy2
from Crypto.Util.number import long_to_bytes

c1 = 240670121804208978394996710730839069728700956824706945984819015371493837551238
c2 = 63385828825643452682833619835670889340533854879683013984056508942989973395315
n = 349579051431173103963525574908108980776346966102045838681986112083541754544269
e1 = 176268455401080975226023429120782206814426280508931609844850047979724152864469
e2 = 214709966595887251005567190400910974312839914267660095937082916625495667341329


_, r, s = gmpy2.gcdext(e1, e2)

m = pow(c1, r, n) * pow(c2, s, n) % n
print long_to_bytes(m)

得到flag

1
FLAG{Math is simple, right? OwO}

用法:

下载

1
pip install z3-solver

变量初始化

变量有以下几种:

  • 包括整数
  • 浮点数
  • 位向量
  • 数组

相比其他,在密码学里整型比较常用

1
2
a = Int('a')
b,c,d = Ints('b c d')

创建对象:

创建一个解的对象。

1
s=solver()

为解增加一个限制条件

1
s.add(条件)

check()，检查解是否存在，如果存在，会返回”sat”

1
eg: s.check()

输出解得结果

1
2
3
if s.check()==sat:
    result=s.modul()
print(result)

一道题练练手:

题目:

[GUET-CTF 2019]BabyRSA

1
2
3
4
5
6
7
8
9
10
11
p+q :
0x1232fecb92adead91613e7d9ae5e36fe6bb765317d6ed38ad890b4073539a6231a6620584cea5730b5af83a3e80cf30141282c97be4400e33307573af6b25e2ea
(p+1)(q+1):
0x5248becef1d925d45705a7302700d6a0ffe5877fddf9451a9c1181c4d82365806085fd86fbaab08b6fc66a967b2566d743c626547203b34ea3fdb1bc06dd3bb765fd8b919e3bd2cb15bc175c9498f9d9a0e216c2dde64d81255fa4c05a1ee619fc1fc505285a239e7bc655ec6605d9693078b800ee80931a7a0c84f33c851740
e :
0xe6b1bee47bd63f615c7d0a43c529d219
d:
0x2dde7fbaed477f6d62838d55b0d0964868cf6efb2c282a5f13e6008ce7317a24cb57aec49ef0d738919f47cdcd9677cd52ac2293ec5938aa198f962678b5cd0da344453f521a69b2ac03647cdd8339f4e38cec452d54e60698833d67f9315c02ddaa4c79ebaa902c605d7bda32ce970541b2d9a17d62b52df813b2fb0c5ab1a5
enc_flag:
0x50ae00623211ba6089ddfae21e204ab616f6c9d294e913550af3d66e85d0c0693ed53ed55c46d8cca1d7c2ad44839030df26b70f22a8567171a759b76fe5f07b3c5a6ec89117ed0a36c0950956b9cde880c575737f779143f921d745ac3bb0e379c05d9a3cc6bf0bea8aa91e4d5e752c7eb46b2e023edbc07d24a7c460a34a9a
### 解题:

普通解法:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
#!/usr/bin/python
import gmpy2
from Crypto.Util.number import long_to_bytes

p_add_q = 0x1232fecb92adead91613e7d9ae5e36fe6bb765317d6ed38ad890b4073539a6231a6620584cea5730b5af83a3e80cf30141282c97be4400e33307573af6b25e2ea #p+q
p_add_1_mul_q_add_1 = 0x5248becef1d925d45705a7302700d6a0ffe5877fddf9451a9c1181c4d82365806085fd86fbaab08b6fc66a967b2566d743c626547203b34ea3fdb1bc06dd3bb765fd8b919e3bd2cb15bc175c9498f9d9a0e216c2dde64d81255fa4c05a1ee619fc1fc505285a239e7bc655ec6605d9693078b800ee80931a7a0c84f33c851740 #(p+1) * (q+1)
e = 0xe6b1bee47bd63f615c7d0a43c529d219
d = 0x2dde7fbaed477f6d62838d55b0d0964868cf6efb2c282a5f13e6008ce7317a24cb57aec49ef0d738919f47cdcd9677cd52ac2293ec5938aa198f962678b5cd0da344453f521a69b2ac03647cdd8339f4e38cec452d54e60698833d67f9315c02ddaa4c79ebaa902c605d7bda32ce970541b2d9a17d62b52df813b2fb0c5ab1a5
c = 0x50ae00623211ba6089ddfae21e204ab616f6c9d294e913550af3d66e85d0c0693ed53ed55c46d8cca1d7c2ad44839030df26b70f22a8567171a759b76fe5f07b3c5a6ec89117ed0a36c0950956b9cde880c575737f779143f921d745ac3bb0e379c05d9a3cc6bf0bea8aa91e4d5e752c7eb46b2e023edbc07d24a7c460a34a9a

#---------get p and q--------
p_mul_q = p_add_1_mul_q_add_1 -p_add_q - 1   # p * q
p_sub_q = gmpy2.iroot(p_add_q ** 2 - 4 * p_mul_q,2)[0] # p-q

q = (p_add_q + p_sub_q) // 2
p = p_add_q - q

#---------check q and p-----
assert (p+1)*(q+1) == p_add_1_mul_q_add_1

#--------solve-------------
n = q*p
phi = (p-1) * (q-1)

d = gmpy2.invert(e,phi)
m = gmpy2.powmod(c,d,n)
print(long_to_bytes(m))

使用z3:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
#!/usr/bin/python
import gmpy2
from Crypto.Util.number import long_to_bytes
from z3 import *

tmp1 = 0x1232fecb92adead91613e7d9ae5e36fe6bb765317d6ed38ad890b4073539a6231a6620584cea5730b5af83a3e80cf30141282c97be4400e33307573af6b25e2ea
tmp2 = 0x5248becef1d925d45705a7302700d6a0ffe5877fddf9451a9c1181c4d82365806085fd86fbaab08b6fc66a967b2566d743c626547203b34ea3fdb1bc06dd3bb765fd8b919e3bd2cb15bc175c9498f9d9a0e216c2dde64d81255fa4c05a1ee619fc1fc505285a239e7bc655ec6605d9693078b800ee80931a7a0c84f33c851740
e = 0xe6b1bee47bd63f615c7d0a43c529d219
d = 0x2dde7fbaed477f6d62838d55b0d0964868cf6efb2c282a5f13e6008ce7317a24cb57aec49ef0d738919f47cdcd9677cd52ac2293ec5938aa198f962678b5cd0da344453f521a69b2ac03647cdd8339f4e38cec452d54e60698833d67f9315c02ddaa4c79ebaa902c605d7bda32ce970541b2d9a17d62b52df813b2fb0c5ab1a5
c = 0x50ae00623211ba6089ddfae21e204ab616f6c9d294e913550af3d66e85d0c0693ed53ed55c46d8cca1d7c2ad44839030df26b70f22a8567171a759b76fe5f07b3c5a6ec89117ed0a36c0950956b9cde880c575737f779143f921d745ac3bb0e379c05d9a3cc6bf0bea8aa91e4d5e752c7eb46b2e023edbc07d24a7c460a34a9a

s = Solver()
p,q = Ints('p q')
s.add(p+q == tmp1)
s.add((p+1) * (q+1) == tmp2)
assert s.check() == sat
p = s.model()[p].as_long()
q = s.model()[q].as_long()
n = q*p

phi = (p-1) * (q-1)

d = gmpy2.invert(e,phi)
m = gmpy2.powmod(c,d,n)
print(long_to_bytes(m))
#flag{cc7490e-78ab-11e9-b422-8ba97e5da1fd}

其实这道题,z3的优势完全发不出来,不过至少写脚本简单了不少

有时z3解不出来，可以尝试sympy中的sovle函数：

如求解f1，f2：

1
2
3
4
5
6
import sympy
f1=sympy.Symbol('f1')
f2=sympy.Symbol('f2')
solved_value=sympy.solve([f1+f2-c1,f1 ** 3+f2 ** 3-c2], [f1,f2])  求解：f1 + f2 = c1,f1 ** 3 + f2 ** 3 = c2
f1=solved_value[0][0]
f2=solved_value[0][1]

应用：

有时可以用于逆向爆破输入。

题目：输入的数据进行一系列运算后等于一个密文：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
from z3 import *
v10=[0]*25
v12=[0]*25
v11=[0]*25

v10[0] = 126
v10[1] = 225
v10[2] = 62
v10[3] = 40
v10[4] = 216;
v10[5] = 253;
v10[6] = 20;
v10[7] = 124;
v10[8] = 232;
v10[9] = 122;
v10[10] = 62;
v10[11] = 23;
v10[12] = 100;
v10[13] = 161;
v10[14] = 36;
v10[15] = 118;
v10[16] = 21;
v10[17] = 184;
v10[18] = 26;
v10[19] = 142;
v10[20] = 59;
v10[21] = 31;
v10[22] = 186;
v10[23] = 82;
v10[24] = 79;
v12[0] = 63998;
v12[1] = 33111;
v12[2] = 67762;
v12[3] = 54789;
v12[4] = 61979;
v12[5] = 69619;
v12[6] = 37190;
v12[7] = 70162;
v12[8] = 53110;
v12[9] = 68678;
v12[10] = 63339;
v12[11] = 30687;
v12[12] = 66494;
v12[13] = 50936;
v12[14] = 60810;
v12[15] = 48784;
v12[16] = 30188;
v12[17] = 60104;
v12[18] = 44599;
v12[19] = 52265;
v12[20] = 43048;
v12[21] = 23660;
v12[22] = 43850;
v12[23] = 33646;
v12[24] = 44270;

x = Solver()
flag = [Real('%d'%i) for i in range(32)]  //flag是输入，对输入*v10后的结果等于v12，因此可以这样定义来求解输入。

for i in range(5):
    for j in range(5):
        for k in range(5):
            v11[5 * i + j] += flag[5 * i + k] * v10[5 * k + j]

for i in range(25):
    x.add(v11[i] == v12[i])


if x.check() == sat:
    model = x.model()
    s = ''
    for i in range(25):
        s += chr((model[flag[i]].as_long().real) & 0x7f)  # 0-127(0x00-0x7f)
    print(s)

两种声明方法：

1
2
flag = [Int('flag{}'.format(i)) for i in range(22)]
flag = [Int('flag[%s]' % i) for i in range(0x22)]  //每个是flag[i]