Recently Updated
Dec 15: Paper and Pen
Challenge
applying bitwise equations on decimals
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
We've captured a strange message. It looks like it is encrypted somehow ...
iw, hu, fv, lu, dv, cy, og, lc, gy, fq, od, lo, fq, is, ig, gu, hs, hi, ds, cy, oo, os, iu, fs, gu, lh, dq, lv, gu, iw, hv, gu, di, hs, cy, oc, iw, gc
We've also intercepted what seems to be a hint to the key:
bytwycju + yzvyjjdy ^ vugljtyn + ugdztnwv | xbfziozy = bzuwtwol
^ ^ ^ ^ ^
wwnnnqbw - uclfqvdu & oncycbxh | oqcnwbsd ^ cgyoyfjg = vyhyjivb
& & & & &
yzdgotby | oigsjgoj | ttligxut - dhcqxtfw & szblgodf = sfgsoxdd
+ + + + +
yjjowdqh & niiqztgs + ctvtwysu & diffhlnl - thhwohwn = xsvuojtx
- - - - -
nttuhlnq ^ oqbctlzh - nshtztns ^ htwizvwi + udluvhcz = syhjizjq
= = = = =
fjivucti zoljwdfl sugvqgww uxztiywn jqxizzxq
Note:
assume q != 0
a letter is a decimal digit is a letter
each digit has exactly two different letter representations
C-like operator precedence
Solution
This was another tough one, after the deadline ended a hint was given to use Z3 theorem prover, which was very helpful.
We installed the Z3 python library:
1
pip install https://pypi.python.org/packages/source/a/angr-z3/angr-z3-4.4.2.tar.gz
And created the following script
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
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
from z3 import *
from string import maketrans
init('/usr/local/lib/libz3.so')
solver = Solver()
# create bitvector for each variable
b,c,d,f,g,h,i,j,l,n,o,q,s,t,u,v,w,x,y,z = BitVecs('b c d f g h i j l n o q s t u v w x y z',32)
# variables must be between 0 and 9
solver.add(b>=0,c>=0,d>=0,f>=0,g>=0,h>=0,i>=0,j>=0,l>=0,n>=0,o>=0,q>=0,s>=0,t>=0,u>=0,v>=0,w>=0,x>=0,y>=0,z>=0)
solver.add(b<10,c<10,d<10,f<10,g<10,h<10,i<10,j<10,l<10,n<10,o<10,q<10,s<10,t<10,u<10,v<10,w<10,x<10,y<10,z<10)
# we know q isnt zero
solver.add(q!=0)
# no more than two letters can represent the same value
# NOTE: this can definitely be done better, but could not find correct way to specify it quickly..
# autogenerated this list of constraints, for all combination of 3 variables they can not all represent same value
solver.add(Not(And(b==c,c==d)))
solver.add(Not(And(b==c,c==f)))
solver.add(Not(And(b==c,c==g)))
[..]
solver.add(Not(And(w==x,x==z)))
solver.add(Not(And(w==y,y==z)))
solver.add(Not(And(x==y,y==z)))
# Add all the equations
# bytwycju + yzvyjjdy ^ vugljtyn + ugdztnwv | xbfziozy = bzuwtwol
solver.add(
(((b*pow(10,7)+y*pow(10,6)+t*pow(10,5)+w*pow(10,4)+y*pow(10,3)+c*pow(10,2)+j*pow(10,1)+u)
+
(y*pow(10,7)+z*pow(10,6)+v*pow(10,5)+y*pow(10,4)+j*pow(10,3)+j*pow(10,2)+d*pow(10,1)+y))
^
((v*pow(10,7)+u*pow(10,6)+g*pow(10,5)+l*pow(10,4)+j*pow(10,3)+t*pow(10,2)+y*pow(10,1)+n)
+
(u*pow(10,7)+g*pow(10,6)+d*pow(10,5)+z*pow(10,4)+t*pow(10,3)+n*pow(10,2)+w*pow(10,1)+v)))
|
(x*pow(10,7)+b*pow(10,6)+f*pow(10,5)+z*pow(10,4)+i*pow(10,3)+o*pow(10,2)+z*pow(10,1)+y)
==
(b*pow(10,7)+z*pow(10,6)+u*pow(10,5)+w*pow(10,4)+t*pow(10,3)+w*pow(10,2)+o*pow(10,1)+l)
)
# wwnnnqbw - uclfqvdu & oncycbxh | oqcnwbsd ^ cgyoyfjg = vyhyjivb
solver.add(
(((w*pow(10,7)+w*pow(10,6)+n*pow(10,5)+n*pow(10,4)+n*pow(10,3)+q*pow(10,2)+b*pow(10,1)+w )
-
(u*pow(10,7)+c*pow(10,6)+l*pow(10,5)+f*pow(10,4)+q*pow(10,3)+v*pow(10,2)+d*pow(10,1)+u ))
&
(o*pow(10,7)+n*pow(10,6)+c*pow(10,5)+y*pow(10,4)+c*pow(10,3)+b*pow(10,2)+x*pow(10,1)+h ))
|
((o*pow(10,7)+q*pow(10,6)+c*pow(10,5)+n*pow(10,4)+w*pow(10,3)+b*pow(10,2)+s*pow(10,1)+d )
^
(c*pow(10,7)+g*pow(10,6)+y*pow(10,5)+o*pow(10,4)+y*pow(10,3)+f*pow(10,2)+j*pow(10,1)+g ))
==
(v*pow(10,7)+y*pow(10,6)+h*pow(10,5)+y*pow(10,4)+j*pow(10,3)+i*pow(10,2)+v*pow(10,1)+b )
)
# yzdgotby | oigsjgoj | ttligxut - dhcqxtfw & szblgodf = sfgsoxdd
solver.add(
(y*pow(10,7)+z*pow(10,6)+d*pow(10,5)+g*pow(10,4)+o*pow(10,3)+t*pow(10,2)+b*pow(10,1)+y )
|
(o*pow(10,7)+i*pow(10,6)+g*pow(10,5)+s*pow(10,4)+j*pow(10,3)+g*pow(10,2)+o*pow(10,1)+j )
|
(((t*pow(10,7)+t*pow(10,6)+l*pow(10,5)+i*pow(10,4)+g*pow(10,3)+x*pow(10,2)+u*pow(10,1)+t )
-
(d*pow(10,7)+h*pow(10,6)+c*pow(10,5)+q*pow(10,4)+x*pow(10,3)+t*pow(10,2)+f*pow(10,1)+w ))
&
(s*pow(10,7)+z*pow(10,6)+b*pow(10,5)+l*pow(10,4)+g*pow(10,3)+o*pow(10,2)+d*pow(10,1)+f ))
==
(s*pow(10,7)+f*pow(10,6)+g*pow(10,5)+s*pow(10,4)+o*pow(10,3)+x*pow(10,2)+d*pow(10,1)+d )
)
# nttuhlnq ^ oqbctlzh - nshtztns ^ htwizvwi+udluvhcz = syhjizjq
solver.add(
(n*pow(10,7)+t*pow(10,6)+t*pow(10,5)+u*pow(10,4)+h*pow(10,3)+l*pow(10,2)+n*pow(10,1)+q )
^
((o*pow(10,7)+q*pow(10,6)+b*pow(10,5)+c*pow(10,4)+t*pow(10,3)+l*pow(10,2)+z*pow(10,1)+h )
-
(n*pow(10,7)+s*pow(10,6)+h*pow(10,5)+t*pow(10,4)+z*pow(10,3)+t*pow(10,2)+n*pow(10,1)+s ))
^
((h*pow(10,7)+t*pow(10,6)+w*pow(10,5)+i*pow(10,4)+z*pow(10,3)+v*pow(10,2)+w*pow(10,1)+i )
+
(u*pow(10,7)+d*pow(10,6)+l*pow(10,5)+u*pow(10,4)+v*pow(10,3)+h*pow(10,2)+c*pow(10,1)+z ))
==
(s*pow(10,7)+y*pow(10,6)+h*pow(10,5)+j*pow(10,4)+i*pow(10,3)+z*pow(10,2)+j*pow(10,1)+q )
)
# nttuhlnq ^ oqbctlzh - nshtztns ^ htwizvwi + udluvhcz = syhjizjq
solver.add(
(n*pow(10,7)+t*pow(10,6)+t*pow(10,5)+u*pow(10,4)+h*pow(10,3)+l*pow(10,2)+n*pow(10,1)+q )
^
((o*pow(10,7)+q*pow(10,6)+b*pow(10,5)+c*pow(10,4)+t*pow(10,3)+l*pow(10,2)+z*pow(10,1)+h )
-
(n*pow(10,7)+s*pow(10,6)+h*pow(10,5)+t*pow(10,4)+z*pow(10,3)+t*pow(10,2)+n*pow(10,1)+s ))
^
((h*pow(10,7)+t*pow(10,6)+w*pow(10,5)+i*pow(10,4)+z*pow(10,3)+v*pow(10,2)+w*pow(10,1)+i )
+
(u*pow(10,7)+d*pow(10,6)+l*pow(10,5)+u*pow(10,4)+v*pow(10,3)+h*pow(10,2)+c*pow(10,1)+z ))
==
(s*pow(10,7)+y*pow(10,6)+h*pow(10,5)+j*pow(10,4)+i*pow(10,3)+z*pow(10,2)+j*pow(10,1)+q )
)
# bytwycju ^ wwnnnqbw & yzdgotby + yjjowdqh - nttuhlnq = fjivucti
solver.add(
(b*pow(10,7)+y*pow(10,6)+t*pow(10,5)+w*pow(10,4)+y*pow(10,3)+c*pow(10,2)+j*pow(10,1)+u )
^
((w*pow(10,7)+w*pow(10,6)+n*pow(10,5)+n*pow(10,4)+n*pow(10,3)+q*pow(10,2)+b*pow(10,1)+w )
&
((y*pow(10,7)+z*pow(10,6)+d*pow(10,5)+g*pow(10,4)+o*pow(10,3)+t*pow(10,2)+b*pow(10,1)+y )
+
(y*pow(10,7)+j*pow(10,6)+j*pow(10,5)+o*pow(10,4)+w*pow(10,3)+d*pow(10,2)+q*pow(10,1)+h )
-
(n*pow(10,7)+t*pow(10,6)+t*pow(10,5)+u*pow(10,4)+h*pow(10,3)+l*pow(10,2)+n*pow(10,1)+q )))
==
(f*pow(10,7)+j*pow(10,6)+i*pow(10,5)+v*pow(10,4)+u*pow(10,3)+c*pow(10,2)+t*pow(10,1)+i )
)
# yzvyjjdy ^ uclfqvdu & oigsjgoj + niiqztgs - oqbctlzh = zoljwdfl
solver.add(
(y*pow(10,7)+z*pow(10,6)+v*pow(10,5)+y*pow(10,4)+j*pow(10,3)+j*pow(10,2)+d*pow(10,1)+y )
^
((u*pow(10,7)+c*pow(10,6)+l*pow(10,5)+f*pow(10,4)+q*pow(10,3)+v*pow(10,2)+d*pow(10,1)+u )
&
((o*pow(10,7)+i*pow(10,6)+g*pow(10,5)+s*pow(10,4)+j*pow(10,3)+g*pow(10,2)+o*pow(10,1)+j )
+
(n*pow(10,7)+i*pow(10,6)+i*pow(10,5)+q*pow(10,4)+z*pow(10,3)+t*pow(10,2)+g*pow(10,1)+s )
-
(o*pow(10,7)+q*pow(10,6)+b*pow(10,5)+c*pow(10,4)+t*pow(10,3)+l*pow(10,2)+z*pow(10,1)+h )))
==
(z*pow(10,7)+o*pow(10,6)+l*pow(10,5)+j*pow(10,4)+w*pow(10,3)+d*pow(10,2)+f*pow(10,1)+l )
)
# vugljtyn ^ oncycbxh & ttligxut + ctvtwysu - nshtztns = sugvqgww
solver.add(
(v*pow(10,7)+u*pow(10,6)+g*pow(10,5)+l*pow(10,4)+j*pow(10,3)+t*pow(10,2)+y*pow(10,1)+n )
^
((o*pow(10,7)+n*pow(10,6)+c*pow(10,5)+y*pow(10,4)+c*pow(10,3)+b*pow(10,2)+x*pow(10,1)+h )
&
((t*pow(10,7)+t*pow(10,6)+l*pow(10,5)+i*pow(10,4)+g*pow(10,3)+x*pow(10,2)+u*pow(10,1)+t )
+
(c*pow(10,7)+t*pow(10,6)+v*pow(10,5)+t*pow(10,4)+w*pow(10,3)+y*pow(10,2)+s*pow(10,1)+u )
-
(n*pow(10,7)+s*pow(10,6)+h*pow(10,5)+t*pow(10,4)+z*pow(10,3)+t*pow(10,2)+n*pow(10,1)+s )))
==
(s*pow(10,7)+u*pow(10,6)+g*pow(10,5)+v*pow(10,4)+q*pow(10,3)+g*pow(10,2)+w*pow(10,1)+w )
)
# ugdztnwv ^ oqcnwbsd & dhcqxtfw + diffhlnl - htwizvwi = uxztiywn
solver.add(
(u*pow(10,7)+g*pow(10,6)+d*pow(10,5)+z*pow(10,4)+t*pow(10,3)+n*pow(10,2)+w*pow(10,1)+v )
^
((o*pow(10,7)+q*pow(10,6)+c*pow(10,5)+n*pow(10,4)+w*pow(10,3)+b*pow(10,2)+s*pow(10,1)+d )
&
( (d*pow(10,7)+h*pow(10,6)+c*pow(10,5)+q*pow(10,4)+x*pow(10,3)+t*pow(10,2)+f*pow(10,1)+w )
+
(d*pow(10,7)+i*pow(10,6)+f*pow(10,5)+f*pow(10,4)+h*pow(10,3)+l*pow(10,2)+n*pow(10,1)+l )
-
(h*pow(10,7)+t*pow(10,6)+w*pow(10,5)+i*pow(10,4)+z*pow(10,3)+v*pow(10,2)+w*pow(10,1)+i )))
==
(u*pow(10,7)+x*pow(10,6)+z*pow(10,5)+t*pow(10,4)+i*pow(10,3)+y*pow(10,2)+w*pow(10,1)+n )
)
# xbfziozy ^ cgyoyfjg & szblgodf + thhwohwn - udluvhcz = jqxizzxq
solver.add(
(x*pow(10,7)+b*pow(10,6)+f*pow(10,5)+z*pow(10,4)+i*pow(10,3)+o*pow(10,2)+z*pow(10,1)+y )
^
((c*pow(10,7)+g*pow(10,6)+y*pow(10,5)+o*pow(10,4)+y*pow(10,3)+f*pow(10,2)+j*pow(10,1)+g )
&
((s*pow(10,7)+z*pow(10,6)+b*pow(10,5)+l*pow(10,4)+g*pow(10,3)+o*pow(10,2)+d*pow(10,1)+f )
+
(t*pow(10,7)+h*pow(10,6)+h*pow(10,5)+w*pow(10,4)+o*pow(10,3)+h*pow(10,2)+w*pow(10,1)+n )
-
(u*pow(10,7)+d*pow(10,6)+l*pow(10,5)+u*pow(10,4)+v*pow(10,3)+h*pow(10,2)+c*pow(10,1)+z )))
==
(j*pow(10,7)+q*pow(10,6)+x*pow(10,5)+i*pow(10,4)+z*pow(10,3)+z*pow(10,2)+x*pow(10,1)+q )
)
#find solution
print(solver.check())
print(solver.model())
#translate message
msg='iw hu fv lu dv cy og lc gy fq od lo fq is ig gu hs hi ds cy oo os iu fs gu lh dq lv gu iw hv gu di hs cy oc iw gc'
fromstring='bcdfghijlnoqstuvwxyz'
tostring=''+str(solver.model()[b])+str(solver.model()[c])+str(solver.model()[d])+str(solver.model()[f])+str(solver.model()[g])+str(solver.model()[h])+str(solver.model()[i])+str(solver.model()[j])+str(solver.model()[l])+str(solver.model()[n])+str(solver.model()[o])+str(solver.model()[q])+str(solver.model()[s])+str(solver.model()[t])+str(solver.model()[u])+str(solver.model()[v])+str(solver.model()[w])+str(solver.model()[x])+str(solver.model()[y])+str(solver.model()[z])
mytrans=maketrans(fromstring,tostring)
print msg.translate(mytrans)
We run this and find the solution!!
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
sat
[x = 1,
z = 0,
c = 3,
v = 9,
s = 9,
q = 5,
l = 8,
g = 3,
b = 5,
f = 6,
i = 8,
o = 7,
j = 0,
u = 2,
h = 7,
w = 4,
n = 1,
d = 6,
y = 2,
t = 4]
84 72 69 82 69 32 73 83 32 65 76 87 65 89 83 32 79 78 69 32 77 79 82 69 32 87 65 89 32 84 79 32 68 79 32 73 84 33
The translated message converted to ASCII reads:
1
THERE IS ALWAYS ONE MORE WAY TO DO IT!
Flag
HV15-U3bA-BKhc-gNqN-Hit6-C1fK