参考视频:

Jamiexu793的个人空间-Jamiexu793个人主页-哔哩哔哩视频

代码分析：

其主要内容在两个while循环中（从定义中可知flag位16个字符）。

看第二个循环，可知是比较result和经过第一个循环得到的v1比较（就是flag经过第一个循环后变成了result（v12））并且可以从开头看出v12=Qsw3sj_lz4_Ujw@l。

再看第一个循环，发现是凯撒密码（看了老半天），大写字母平移12位，小写字母平移8位，其他字符不变。

 

 

import z3
key="Qsw3sj_lz4_Ujw@l"solver=z3.Solver()varNames=[]
for i in key:o=ord(i)if o>64 and o<=90:x=z3.Int('v%d'%o)solver.add(x>64)solver.add(x<=90)solver.add(((x-51)%26+65)==o)varNames.append(x)elif o>96 and o<=122:x=z3.Int('v%d'%o)solver.add(x>96)solver.add(x<=122)solver.add(((x-79)%26+97)==o)varNames.append(x)else:x=z3.Int('v%d'%o)solver.add(x==o)varNames.append(x)
if solver.check()==z3.sat:model=solver.model()for i in varNames:print(chr(model[i].as_long()),end='')
#Cae3ar_th4_Gre@t
#ACTF{Cae3ar_th4_Gre@t}

ACTF{Cae3ar_th4_Gre@t}