马的，我的密码学是真的弱阿，就这个题我都要看一天，是真的服了，不过是真的学到好多， 主要说一下程序流程， 首先输入32个数字，然后用其中的三个数字，作为种子，使用线性同余发生器生成伪随机数 在此说一下线性同余发生器，因为我是真的不知道 就是这玩意，(记住这个是四个字节)然后与flag xor ，生成64个方程，每个都是4个字节， 然后传进4个方程，des加密，前面两个（8个字节）合并组成密钥，后面两个是明文（8个字节），后面再放回原处，进行比较， 其中des加密 还是分奇偶的，要当心溢出， //2 | 0x8000000000000000 看官方的wp，还学会了z3的一些新的用法， yield,fromhex…以前我都是手打flag, 原来可以这么写(没错，我就是怎么菜)
flag = [Bitvec(('x%d' %i),8) for i in range(32)] m = s.model() str = [chr(m[flag[i]].as_long()) for i in range(32)]