# 50-fifty

[challenge_file](https://github.com/teambi0s/InCTF/raw/master/2018/Reversing/50-fifty/Handout/50-fifty.exe)

This challenge takes a string and an integer and does some checks on the inputs
Using Z3 solver we can solve those constraints

from z3 import *

#Xyz

#-------------------------------------------------------------------------------
a = [ BitVec("v%s"%i,32) for i in range(6)]
num=BitVec('num',32)

b=[70, 97, 90, 109, 107, 94]
for i in range(6):
	b[i]+=18


s=Solver()
s.add(num==((a[0]+a[1]+a[2]+a[3]+a[4]+a[5])%10))
for i in range(6):
	s.add(a[i]==b[i]^num)


s.check()

b=s.model()

name=''

for i in a:
	name+=chr(int(str(b[i])))

print("name: "+name)

v6 = b[num]

#-------------------------------------------------------------------------------

#xyz

v4=BitVec('v4',32)
v5=BitVec('v5',32)


s1=Solver()

s1.add(v5 == (v4/306783371))

str1='qcwuycj{~s'
str2='asgeiszknc'


for i in range(10):
	s1.add(ord(str2[i])==((v5+v6)^ord(str1[i])))


s1.check()

b=s1.model()
print("code: "+str(b[v4]))


#-------------------------------------------------------------------------------


#xyZ
s=Solver()


a = [ BitVec("a%s"%i,32) for i in range(32)]


arr=[0x7b,0x7c,0x71,0x66,0x74,0x69,0x6b,0x21
,0x26,0x7a,0x4d,0x23,0x66,0x4d,0x65,0x26
,0x61,0x4d,0x21,0x73,0x27,0x61,0x27,0x6b
,0x4d,0x60,0x23,0x75,0x7a,0x25,0x33,0x6f]

for i in range(32):
	s.add(a[i] == ((v6+v6) ^ arr[i]))

s.check()

aa = s.model()

print("flag: ",end='')
for i in a:
	print(chr(int(str(aa[i]))),end='')
print()

##### Flag: `inctf{y34h_1t_w4s_3a5s5y_r1gh7!}`

###### tags: `inctf` `Z3`