[原创]密码学中的z3约束求解器
发表于:
2020-10-25 18:52
官方: z3是由微软公司开发的一个优秀的SMT求解器（也就定理证明器），它能够检查逻辑表达式的可满足性。
人话: 解方程
通过下面一道题来展示z3的优势
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
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
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
算到是应该能算出来,不过时间等不起,所以我们换一种工具
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
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
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
2
a = Int('a')
b,c,d = Ints('b c d')
创建一个解的对象。
为解增加一个限制条件
check()，检查解是否存在，如果存在，会返回"sat"
输出解得结果
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
import gmpy2
from Crypto.Util.number import long_to_bytes
p_add_q = 0x1232fecb92adead91613e7d9ae5e36fe6bb765317d6ed38ad890b4073539a6231a6620584cea5730b5af83a3e80cf30141282c97be4400e33307573af6b25e2ea
p_add_1_mul_q_add_1 = 0x5248becef1d925d45705a7302700d6a0ffe5877fddf9451a9c1181c4d82365806085fd86fbaab08b6fc66a967b2566d743c626547203b34ea3fdb1bc06dd3bb765fd8b919e3bd2cb15bc175c9498f9d9a0e216c2dde64d81255fa4c05a1ee619fc1fc505285a239e7bc655ec6605d9693078b800ee80931a7a0c84f33c851740
e = 0xe6b1bee47bd63f615c7d0a43c529d219
d = 0x2dde7fbaed477f6d62838d55b0d0964868cf6efb2c282a5f13e6008ce7317a24cb57aec49ef0d738919f47cdcd9677cd52ac2293ec5938aa198f962678b5cd0da344453f521a69b2ac03647cdd8339f4e38cec452d54e60698833d67f9315c02ddaa4c79ebaa902c605d7bda32ce970541b2d9a17d62b52df813b2fb0c5ab1a5
c = 0x50ae00623211ba6089ddfae21e204ab616f6c9d294e913550af3d66e85d0c0693ed53ed55c46d8cca1d7c2ad44839030df26b70f22a8567171a759b76fe5f07b3c5a6ec89117ed0a36c0950956b9cde880c575737f779143f921d745ac3bb0e379c05d9a3cc6bf0bea8aa91e4d5e752c7eb46b2e023edbc07d24a7c460a34a9a
p_mul_q = p_add_1_mul_q_add_1 -p_add_q - 1
p_sub_q = gmpy2.iroot(p_add_q ** 2 - 4 * p_mul_q,2)[0]
q = (p_add_q + p_sub_q) // 2
p = p_add_q - q
assert (p+1)*(q+1) == p_add_1_mul_q_add_1
n = q*p
phi = (p-1) * (q-1)
d = gmpy2.invert(e,phi)
m = gmpy2.powmod(c,d,n)
print(long_to_bytes(m))
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
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))
其实这道题,z3的优势完全发不出来,不过至少写脚本简单了不少
1
flag{cc7490e-78ab-11e9-b422-8ba97e5da1fd}
[培训]内核驱动高级班，冲击BAT一流互联网大厂工作，每周日13:00-18:00直播授课
