2019强网杯

Author Avatar
Xzhah 6月 04, 2019
  • 在其它设备中阅读本文章

[TOC]

JustRE

思路

前十个输入类似SMC，需要将特定函数开头写为特定值。后十六个输入是3DES加密，密文和密钥都可以提取，S盒也没变，直接用3DES库函数解就行

得到前十位(在一开始满足的有多组，全都打印出来从其中选出y值为0x18181818的组合，因为y是两位的重复，在z3中也限制了，但是会出现其他不重复的解)

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
from z3 import *
def get_models(s):
    while s.check() == sat:
        m = s.model()
        yield m
        s.add(Or([sym() != m[sym] for sym in m.decls()]))
x=BitVec('x', 32)
y = BitVec('y',32)
#z = Int('z')

s = Solver()
s.add(y==0x18181818)
s.add(((y+0x78B09135)&0xffffffff)^x==0x83ec8b55)
s.add(((y+0xE78DBAE5)&0xffffffff)^(x+0x00000001)==0xec81f0e4)
s.add(And(y&0xff == (y>>8)&0xff),(y&0xff == (y>>16)&0xff),(y&0xff == (y>>24)&0xff))
for m in get_models(s):
    serial = [m[x].as_long(), m[y].as_long()]
    
    key = ''
    key=hex(m[x].as_long())+hex(m[y].as_long())[2:4]
    print key

得到后十六位

1
2
from Crypto.Cipher import DES3
DES3.new(key='AFSAFCEDYCXCXACNDFKDCQXC').decrypt('507CA9E68709CEFA20D50DCF90BB976C'.decode('hex'))