首页
社区
课程
招聘
问答 CTF 排行榜 知识库 工具下载 看雪峰会 看雪商城 证书查询
  1. 看雪社区
  2. 密码应用
    3. 发新帖
[原创]密码学中的z3约束求解器
2020-10-25 18:52 9056

[原创]密码学中的z3约束求解器

happi0 活跃值
1
2020-10-25 18:52
9056

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
#!/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))

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

1
flag{cc7490e-78ab-11e9-b422-8ba97e5da1fd}

[培训]《安卓高级研修班(网课)》月薪三万计划，掌握调试、分析还原ollvm、vmp的方法，定制art虚拟机自动化脱壳的方法

收藏
点赞・1
打赏
分享
最新回复 (1)
默NJ
雪    币： 2124
活跃值： (4181)
能力值： ( LV2，RANK：10 )
在线值：
发帖
回帖
粉丝
私信
默NJ 2020-12-7 13:40
2 楼
0
所以z3的优势是啥哦,
游客
登录 | 注册 方可回帖
　回帖　 表情 雪币赚取及消费
高级回复
返回