从一道Crypto题目认识z3

writeup crypto

字数统计: 1,785阅读时长: 8 min

 2018/08/23  Share

1	文章首发于安全客 https://www.anquanke.com/post/id/156915

前言

最近在看Crypto，一直听闻z3的强大，近日终于体验了一次，做一下记录

题干分析

题目直接给出了密文生成文本：

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

json.dump({ key: globals()[key] for key in "Mmxyzpq" }, open('crypted', 'w'))

题目的意思很简单：
1.生成两个随机大素数m,M
2.利用m再生成3个随机大数a,b,c
3.再利用a,b,c,m生成3个随机大数x,y,z
4.类RSA，将flag用公钥a加密，模数为M
5.类RSA，将flag用公钥b加密，模数为M
（注：这里不准确，并不是真RSA，说公钥和模数是方便类比）
然后我们已知的信息为

{
"p": 240670121804208978394996710730839069728700956824706945984819015371493837551238, 
"q": 63385828825643452682833619835670889340533854879683013984056508942989973395315, 
"M": 349579051431173103963525574908108980776346966102045838681986112083541754544269, 
"z": 213932962252915797768584248464896200082707350140827098890648372492180142394587, 
"m": 282832747915637398142431587525135167098126503327259369230840635687863475396299, 
"x": 254732859357467931957861825273244795556693016657393159194417526480484204095858, 
"y": 261877836792399836452074575192123520294695871579540257591169122727176542734080
}

所以想解决这个问题的关键点应该在于a和b，毕竟其他的信息都给出了，除了a和b

解题思考（1）

如果我们得到了a和b，应该如何解决这道题呢？
乍一看，很困难，两个密文p和q都是利用类RSA的算法得到的，而M是大素数，强行突破肯定不容易
但这里讲到RSA，相信大家都知道RSA的共模攻击，那这里的题目是不是很相似呢？
我们先看看什么是RSA共模攻击：
这里简单给大家推导一下，如果RSA不知道是什么的话，建议先谷歌学一下概念
首先是基本条件，我们有：

那么根据贝祖等式:

我们一定可以得到

那么我们将最初的两个等式进行变形

我们将其相乘

则得到

到此，我们可以在不知道私钥的情况下，得到明文
我们再回到这道题目里

我们同样可以得到

又根据贝祖等式

我们能有结果为

故此我们又得到一个隐形的约束条件：

解题思考2

我们如何求出a和b？
我们有如下约束条件

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

此时，我们知道x,y,z,m
按照道理说，这里的约束条件，在不做任何思考的条件下，我们可以用如下方法爆破出来

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

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

但是这显然是一种极其不理智的做法，因为解题概率极低
这里就要用到一个神奇了：SMT约束求解器Z3

Z3快速入门

z3安装

1	sudo pip install z3-solver

即可安装成功

简单介绍

我们看这样一个三元一次方程组的问题

那么我们如何利用z3约束迅速求解呢？
脚本如下

from z3 import *

x = Int('x')
y = Int('y')
z = Int('z')
s = Solver()
s.add(y==2*x-7)
s.add(5*x+3*y+2*z==3)
s.add(3*x+z==7)
print s.check()
print s.model()

可以轻松得到结果

1
2
3

sat
[x = 2, z = 1, y = -3]
[Finished in 0.3s]

这里简单解释一下

1
2
3

x = Int('x')
y = Int('y')
z = Int('z')

用于定于类型，包括整数、浮点数、BitVector、数组等
然后是

1	s = Solver()

用Solver()创建求解器
紧接着

1
2
3

s.add(y==2*x-7)
s.add(5*x+3*y+2*z==3)
s.add(3*x+z==7)

我们使用add()为变量之间增加约束条件
最后

1 2	print s.check() print s.model()

使用check()检查约束条件是否ok，并使用model()列出求解结果
这里再给出更多python z3 api文档

1	http://z3prover.github.io/api/html/namespacez3py.html

求解step1

现在有了z3这样强大的约束求解器，我们可以尝试计算出a,b了
我们有约束条件

以及

1	a, b, c = [(sympy.randprime(2256, 2257) % m) for _ in range(3)]

这样一来，我们可以写出相应的约束解决脚本

from z3 import *
from primefac import *

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

a, b, c = BitVecs('a b c', 262)
s = Solver()
s.add(UGT(a, pow(2, 256, m)))
s.add(ULT(a, pow(2, 257, m)))
s.add(UGT(b, pow(2, 256, m)))
s.add(ULT(b, pow(2, 257, m)))
s.add(UGT(c, pow(2, 256, m)))
s.add(ULT(c, pow(2, 257, m)))
s.add(x == (a + b * 3) % m)
s.add(y == (b - c * 5) % m)
s.add(z == (a + c * 8) % m)
while s.check() == sat:
    A,B= s.model()[a].as_long(),s.model()[b].as_long()
    if gcd(A,B) == 1:
        print A,B
        break

这里有几点申明一下：
1.这里使用的是BitVecs，而不是Int，因为类型为 Int（注意这里的 Int 可不是 C/C++ 里面包含上下界的 int，Z3 中的 Int 对应的就是数学中的整数，Z3 中的 BitVector 才对应到 C/C++ 中的 int），这样我们才能实现一些无符号和有符号二进制运算
2.关于a, b, c = BitVecs('a b c', 262)的范围选262的原因如下
我们在计算中有一步

a + c * 8

这应该是在运算中可能生成的最大值，而我们知道

1	a, b, c = [(sympy.randprime(2256, 2257) % m) for _ in range(3)]

所以这里我们假设a和c都是2**257
估计极限最大值为

1	print len(bin(pow(2,257)*9)[2:])

发现是261bit
故此我们选择262bit就不会溢出，导致check()无法通过
3.由于是约束条件，这里可能出现多组值，而根据之前我们的推算，我们需要gcd(a,b)=1，所以这一点加入约束中
运行脚本后，我们可以得到一组值：

1 2	a = 176268455401080975226023429120782206814426280508931609844850047979724152864469 b = 214709966595887251005567190400910974312839914267660095937082916625495667341329

求解step2

这里根据之前我们推导出的公式：

可以得到flag的脚本为：

import primefac
import libnum

M=349579051431173103963525574908108980776346966102045838681986112083541754544269
p=240670121804208978394996710730839069728700956824706945984819015371493837551238
q=63385828825643452682833619835670889340533854879683013984056508942989973395315
a=176268455401080975226023429120782206814426280508931609844850047979724152864469
b=214709966595887251005567190400910974312839914267660095937082916625495667341329
s1,s2,tmp = libnum.xgcd(a, b)
if s1<0:
    s1 = - s1
    p = primefac.modinv(p, M)
    if p<0:
        p+=M
elif s2<0:
    s2 = - s2
    q = primefac.modinv(q, M)
    if q<0:
        q+=M
m=(pow(p,s1,M)*pow(q,s2,M)) % M
print libnum.n2s(m)

注：这里s1或者s2会有一个为负数，这里的负数不是负值，是逆元的意思
运行即可得到flag

1	FLAG{Math is simple, right? OwO}

后记

从这个题重温了不少数论的相关知识，以及一些优雅的crypto库，还算对得起数论老师了（逃）

参考链接

https://zhuanlan.zhihu.com/p/30548907
https://www.cnblogs.com/ZHijack/p/9001860.html

点击赞赏二维码，您的支持将鼓励我继续创作！

Next Post

RSA之拒绝套路(1)
Previous Post

2018 WhiteHat writeup

CATALOG

1. 前言
2. 题干分析
3. 解题思考（1）
4. 解题思考2
5. Z3快速入门
1. 5.1. z3安装
2. 5.2. 简单介绍
6. 求解step1
7. 求解step2
8. 后记
9. 参考链接

