前言
最近在看密码学的题目，一直听说过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不知道是什么的话，建议先谷歌学一下概念
首先是基本条件，我们有：
c_1 equiv m^{e_1} text{ } mod text{ } n
c_2 equiv m^{e_2} text{ } mod text{ } n
gcd(e1,e2) = 1那么根据贝祖等式:
ax+by = gcd(a,b) = d我们一定可以得到
e1s1+e2s2 = 1那么我们将最初的两个等式进行变形
c_1^{s_1} equiv m^{e_1s_1} text{ } mod text{ } n
c_2^{s_2} equiv m^{e_2s_2} text{ } mod text{ } n我们将其相乘c_1^{s_1}c_2^{s_2} text{ } mod text{ } n equiv m^{e_1s_1+e_2s_2} text{ } mod text{ } n
则得到
c_1^{s_1}c_2^{s_2} text{ } mod text{ } n equiv m^{1} text{ } mod text{ } n到此，我们可以在不知道私钥的情况下，得到明文
我们再回到这道题目里
p equiv flag^{a} text{ } mod text{ } M
q equiv flag^{b} text{ } mod text{ } M我们同样可以得到
p^{s1}q^{s2} text{ } mod text{ } M equiv flag^{as_1+bs_2} text{ } mod text{ } M又根据贝祖等式
ax+by = gcd(a,b) = d我们能有结果为
p^{s1}q^{s2} text{ } mod text{ } M equiv flag^{d} text{ } mod text{ } M
d = gcd(a,b)故此我们又得到一个隐形的约束条件：
gcd(a,b)=1解题思考（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安装
sudo pip install z3-solver
即可安装成功
简单介绍
我们看这样一个三元一次方程组的问题
begin{cases}
y=2x-7
5x+3y+2z=3
3*x+z=7
end{cases}
那么我们如何利用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()
可以轻松得到结果
sat
[x = 2, z = 1, y = -3]
[Finished in 0.3s]
这里简单解释一下
x = Int('x')
y = Int('y')
z = Int('z')
用于定于类型，包括整数、浮点数、BitVector、数组等
然后是
s = Solver()
用Solver()创建求解器
紧接着
s.add(y==2*x-7)
s.add(5*x+3*y+2*z==3)
s.add(3*x+z==7)
我们使用add()为变量之间增加约束条件
最后
print s.check()
print s.model()
使用check()检查约束条件是否ok，并使用model()列出求解结果
这里再给出更多python z3 api文档
http://z3prover.github.io/api/html/namespacez3py.html
求解step1
现在有了z3这样强大的约束求解器，我们可以尝试计算出a,b了
我们有约束条件
begin{cases}
x=(a + b 3) text{ } mod text{ } m
y=(b - c 5) text{ } mod text{ } m
z=(a + c * 8) text{ } mod text{ } m
gcd(a,b)=1
end{cases}以及
a, b, c = [(sympy.randprime(2**256, 2**257) % 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
这应该是在运算中可能生成的最大值，而我们知道
a, b, c = [(sympy.randprime(2**256, 2**257) % m) for _ in range(3)]
所以这里我们假设a和c都是2**257
估计极限最大值为
print len(bin(pow(2,257)*9)[2:])
发现是261bit
故此我们选择262bit就不会溢出，导致check()无法通过
3.由于是约束条件，这里可能出现多组值，而根据之前我们的推算，我们需要gcd(a,b)=1，所以这一点加入约束中
运行脚本后，我们可以得到一组值：
a = 176268455401080975226023429120782206814426280508931609844850047979724152864469
b = 214709966595887251005567190400910974312839914267660095937082916625495667341329
求解step2
这里根据之前我们推导出的公式：
flag^{1} text{ } mod text{ } M equiv p^{s1}*q^{s2} text{ } mod text{ } M可以得到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
FLAG{Math is simple, right? OwO}
后记
从这个题重温了不少数论的相关知识，以及一些优雅的crypto库，还算对得起数论老师了（逃）
https://zhuanlan.zhihu.com/p/30548907
https://www.cnblogs.com/ZHijack/p/9001860.html