-
Notifications
You must be signed in to change notification settings - Fork 0
/
tls_solver.py
103 lines (80 loc) · 4.22 KB
/
tls_solver.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
from z3 import*
f = [BitVec('f1%i'%i,8) for i in range(0,29)]
s = Solver()
#CoNGRAtS!T3N4CI0US
#C
s.add((f[12]-f[20]*f[3]-f[24]+f[11]+f[18]+f[12]^f[8])^67 == -3273)
s.add((f[13]-f[14]+f[15]-f[6]-f[20]^f[14]*f[6]^f[17]-f[26]^f[3])^67 == -11069)
s.add((f[18]+f[18]*f[1]*f[25]*f[8]*f[10]^f[16]+f[23]+f[5])^67 == -560840432)
#o
s.add((f[20]^f[16]*f[25]*f[14]+f[10]*f[12]-f[12]^f[13]*f[18]-f[9])^111 == 367670)
s.add((f[12]*f[7]+f[27]^f[0]-f[14]^f[15]*f[1]*f[24]-f[4]*f[3])^111 == -778883)
s.add((f[25]*f[14]-f[24]^f[9]+f[13]^f[5]*f[24]^f[11]^f[7]*f[28]*f[9])^111 == 5454)
#N
s.add((f[8]+f[11]^f[20]-f[23]*f[8]-f[25]*f[26]*f[4])^78 == -267633)
s.add((f[8]*f[23]^f[8]-f[24]-f[7]+f[11]-f[2]*f[23]-f[1]+f[0]-f[1]^f[3])^78 == -265)
s.add((f[27]-f[26]-f[4]*f[16]^f[3]-f[9]-f[2])^78 == 9592)
#G
s.add((f[2]+f[28]*f[21]+f[18]+f[5]^f[23]^f[3]*f[7]^f[11])^71 == 4575)
s.add((f[15]-f[26]+f[11]+f[21]+f[7]^f[27]*f[18]*f[5]+f[8]*f[15]+f[11])^71 == 879377)
s.add((f[19]-f[3]*f[0]*f[13]-f[15]-f[28]^f[19]*f[8])^71 == -404147)
#R
s.add((f[24]-f[13]-f[12]+f[25]*f[2]*f[11]*f[2]^f[3]*f[25]-f[5]*f[8])^82 == -35883964)
s.add((f[28]+f[5]-f[25]*f[4]+f[18]*f[15]+f[5]^f[19]-f[12]*f[0])^82 == -14927)
s.add((f[6]*f[28]+f[10]-f[14]+f[18]-f[28]^f[0]*f[4]^f[7]-f[6]^f[17]+f[3])^82 == -5840)
#A
s.add((f[10]*f[22]+f[0]^f[19]^f[0]-f[20]*f[0])^65 == -14527 )
s.add((f[4]-f[25]-f[1]+f[7]-f[12]^f[25]*f[0]-f[9])^65 == -2247)
s.add((f[1]*f[20]^f[21]^f[8]-f[9]^f[23]^f[19]+f[12]^f[16]+f[19]+f[12])^65 == -6923)
#t
s.add((f[25]*f[1]*f[27]^f[14]-f[21]-f[14]+f[5]*f[19]+f[3]+f[15]^f[6]-f[5])^116 == 220706)
s.add((f[28]-f[18]-f[13]^f[0]-f[19]+f[1]+f[6]^f[28]^f[5]*f[16]*f[18]*f[5])^116 == -158571284)
s.add((f[2]^f[13]-f[4]*f[9]+f[19]-f[6]+f[6]^f[10]+f[2])^116 == -8867)
#S
s.add((f[18]+f[1]^f[17]+f[19]*f[1]+f[4]-f[4]+f[12]*f[11]-f[5])^83 == 15778)
s.add((f[11]+f[6]*f[8]-f[11]-f[16]^f[24]-f[28]-f[12]*f[21]*f[6])^83 == -510999)
s.add((f[1]*f[20]^f[7]*f[19]+f[11]-f[26]*f[20]+f[11])^83 == 8113)
#!
s.add((f[23]+f[4]^f[16]*f[16]-f[11]^f[24]+f[17]*f[18]+f[12])^33 == 1080)
s.add((f[14]^f[12]-f[5]-f[26]-f[19]*f[2]^f[27]*f[9])^33 == -14013)
s.add((f[6]^f[2]+f[6]-f[5]*f[7]^f[17]-f[23]+f[6])^33 == -9068)
#T
s.add((f[18]+f[0]-f[24]^f[5]-f[0]+f[14]-f[13]-f[18]-f[4])^84 == -157)
s.add((f[6]*f[13]+f[22]+f[8]+f[9]*f[21]*f[13]-f[14]-f[16]-f[7])^84 == 806605)
s.add((f[22]-f[19]^f[28]-f[15]-f[7]^f[8]^f[28]-f[13]*f[16]-f[6])^84 == 13273)
#3
s.add((f[6]*f[0]^f[9]+f[5]+f[18]+f[9]-f[2]-f[8]+f[16]^f[1])^51 == 7926)
s.add((f[2]-f[15]^f[11]*f[25]-f[4]^f[16]*f[26]*f[5]+f[14]^f[2])^51 == -1258120)
s.add((f[22]^f[18]+f[23]-f[20]*f[12]+f[12]^f[8]*f[7]+f[17]*f[28]*f[5])^51 == -13215)
#N
s.add((f[25]*f[2]-f[2]*f[8]-f[1]*f[21]*f[4])^78 == -524776)
s.add((f[9]^f[18]^f[20]*f[2]*f[10]^f[24]+f[24]*f[5])^78 == 759268)
s.add((f[5]-f[24]*f[12]*f[5]*f[4]*f[5]^f[11])^78 == -514165330)
#4
s.add((f[26]-f[16]^f[3]^f[19]*f[1]-f[23]+f[12]+f[6])^52 == -9362)
s.add((f[15]-f[26]^f[26]+f[21]*f[17]-f[16]*f[7])^52 == -2360)
s.add((f[28]*f[17]^f[3]^f[28]*f[17]+f[5]-f[0]+f[17]^f[14]*f[11])^52 == 9181)
#C
s.add((f[4]+f[2]^f[23]+f[25]-f[2]+f[12]*f[28]-f[23]+f[9])^67 == 218)
s.add((f[9]+f[28]^f[23]^f[15]-f[14]^f[18]+f[13]^f[12])^67 == 146)
s.add((f[27]-f[17]-f[7]^f[7]+f[24]^f[1]^f[27]-f[6])^67 == 235)
#I
s.add((f[1]-f[2]^f[28]-f[4]-f[22]-f[7]+f[10]-f[15]*f[16]*f[2]+f[12]-f[1])^73 == 1452340)
s.add((f[6]*f[5]^f[23]-f[11]+f[16]+f[16]^f[5])^73 == 12835)
s.add((f[13]*f[21]*f[24]*f[14]+f[17]+f[16]*f[3])^73 == 47985902)
#0
s.add((f[21]-f[12]^f[4]*f[14]^f[26]-f[2]-f[23]^f[26]+f[7])^48 == 7893)
s.add((f[8]*f[9]*f[0]-f[2]*f[24]^f[8]*f[8]-f[3]*f[27]+f[22]^f[10])^48 == 796144)
s.add((f[6]+f[23]-f[8]^f[23]^f[15]+f[9]-f[25]-f[12]^f[3])^48 == 114)
#U
s.add((f[13]+f[13]*f[9]*f[24]*f[6]+f[23]*f[1]^f[11])^85 == 100004948)
s.add((f[20]^f[2]-f[24]^f[16]-f[16]-f[7]*f[19]^f[2])^85 == -8055)
s.add((f[14]-f[12]-f[14]^f[28]+f[1]^f[11]^f[21]*f[3]^f[26]*f[7])^85 == -4880)
#S
s.add((f[23]^f[7]+f[27]*f[4]^f[19]-f[18]-f[7]*f[3]^f[0])^83 == -2047)
s.add((f[0]^f[17]^f[13]+f[10]^f[18]+f[20]+f[21]*f[0])^83 == 4809)
s.add((f[3]+f[15]*f[16]-f[5]*f[23]^f[28]-f[1]+f[18]+f[6]^f[22]+f[7])^83 == 8052)
s.check()
m = s.model()
for j in range (0,29):
print(chr(int(str(m[f[j]]))), end='')