crypto writeup

忙着毕设没怎么打，平台也卡得不行，随便记录一下。

crypto_threshold

题目

import random
from sympy import nextprime
from Crypto.Util.number import *
from secret import flag
from gmpy2 import gcd

def lcg(seed,params):
    (m,c,n)=params
    s = seed % n
    while True:
        s = (m * s + c) % n
        yield s
    

seed = getPrime(128)
m = getPrime(128)
c = getPrime(128)
n = getPrime(129)

print(m,c,n)
key_stream = lcg(seed,(m,c,n))
num=[]
for _ in range(6):
	num.append(next(key_stream))
	
print(num)
secret =  next(key_stream)

e = nextprime(secret)
p = getPrime(1024)
q = getPrime(1024)


_lambda = ((p-1)*(q-1)) / gcd(p-1,q-1)

flag = bytes_to_long(flag)


print(_lambda)
print(p*q)
print(pow(flag,e,p*q))
        
'''
(315926151576125492949520250047736865439L, 204423972944032372640132172728460755543L, 375402477603617093440157245062608289367L)
[345100389799760820174075838471701328893L, 354616152072197410104284828964580660629L, 262223452907927780613453340112396026524L, 36884243358932605284421044617284274488L, 293840768243490066897038832083154668562L, 287868671713011127830359814204794790287L]
457872764421730558978217109311884057410311335293040789670930865953404030084212226269947268155086034859079522508205099945996505165612539895857134158846470122889806235716457030336629794120415334028017836171608283093853784030348654118118278878881245838363354935523654666907698225985634469947076411404657018958617661794208646954882326918608011132295868155254980231015984288966599987516188265570396237695988003707515471895679008794498548940902202079105268931791776841539932961070351617834137017590635300615537152347169984974533340989459692132455611998382465644967355506104871655788359202461542101480022365857889833055840
27472365865303833538693026558713043444618680117582447380255851957204241805052733576196836089305162091544771350492305996759790309936752393751428049530788207373388374142987421820197787647224920041681070170296496985631227041820919247087096732732874750301801296131419280014461893559138068196824584684279421137517391204355597563871480257589096606865035259322614687417246708249170470689983675108996118328359454354818425772935513344465778617739729440207409124134831968562495435786944862849412776010947330752600405451073822977981611026975129395818269513358936682934286140359273764118787152676411486767003233858544159511154941
7187920142528335824861143203876908084067528690298329755497671248322277194754277305701102880967402859593937177306927235921616059382304183094350022713118203435560220591865274025991334717202171313133285253575822615616032441398946742994706880814251670668924098240782583026655923033371628284132606950034409888896558825512875084001031123558055489119898334591442547695833103046341283479780998109787754685881665949269402489768629140076361688313079919123642491566639820702501701460474001196941883819620040361365999896847153131825439764785309224799365130821807533936571946283436139142085798584001786665762720472918598961576836
'''

安恒赛必有lcg…

step 1: 计算lcg参数

from Crypto.Util.number import *

def gcd(a,b): 
    if(b == 0): 
        return a 
    else: 
        return gcd(b,a % b) 

s =  [345100389799760820174075838471701328893, 354616152072197410104284828964580660629, 262223452907927780613453340112396026524, 36884243358932605284421044617284274488, 293840768243490066897038832083154668562, 287868671713011127830359814204794790287]
t = []
all_n = []
for i in range(6):
    t.append(s[i] - s[i - 1]) 

for i in range(4):
    all_n.append(gcd((t[i + 1] * t[i - 1] - t[i] * t[i]), (t[i + 2] * t[i] - t[i + 1] * t[i + 1]))) 

MMI = lambda A, n, s=1, t=0, N=0: (n < 2 and t % N or MMI(n, A % n, t, s - A // n * t, N or n), -1)[n < 1]
for n in all_n:
    n = abs(n)
    if n == 1:
        continue
    m = (s[2] - s[1]) * MMI((s[1] - s[0]), n) % n
    ani = MMI(m,n)
    c = (s[1] - m * s[0]) % n
    seed = (ani * (s[0] - c)) % n
    print("n = ",n)
    print("m = ",m)
    print("c = ",c)
    print("seed = ",seed)
    
# n =  375402477603617093440157245062608289367
# m =  315926151576125492949520250047736865439
# c =  204423972944032372640132172728460755543
# seed =  249693681622143659200648375306908850367

step 2: 计算公钥e

n =  375402477603617093440157245062608289367
m =  315926151576125492949520250047736865439
c =  204423972944032372640132172728460755543
seed =  249693681622143659200648375306908850367

import random
from sympy import nextprime
from Crypto.Util.number import *
from gmpy2 import *

def lcg(seed,params):
    (m,c,n)=params
    s = seed % n
    while True:
        s = (m * s + c) % n
        yield s

key_stream = lcg(seed,(m,c,n))
num=[]
for _ in range(6):
	num.append(next(key_stream))

secret =  next(key_stream)
e = nextprime(secret)

# e = 42571462274154625185979561328651991521

step 3: 解密m

import gmpy2
from Crypto.Util.number import * 
e = 42571462274154625185979561328651991521
n = 27472365865303833538693026558713043444618680117582447380255851957204241805052733576196836089305162091544771350492305996759790309936752393751428049530788207373388374142987421820197787647224920041681070170296496985631227041820919247087096732732874750301801296131419280014461893559138068196824584684279421137517391204355597563871480257589096606865035259322614687417246708249170470689983675108996118328359454354818425772935513344465778617739729440207409124134831968562495435786944862849412776010947330752600405451073822977981611026975129395818269513358936682934286140359273764118787152676411486767003233858544159511154941
gcdpq = 457872764421730558978217109311884057410311335293040789670930865953404030084212226269947268155086034859079522508205099945996505165612539895857134158846470122889806235716457030336629794120415334028017836171608283093853784030348654118118278878881245838363354935523654666907698225985634469947076411404657018958617661794208646954882326918608011132295868155254980231015984288966599987516188265570396237695988003707515471895679008794498548940902202079105268931791776841539932961070351617834137017590635300615537152347169984974533340989459692132455611998382465644967355506104871655788359202461542101480022365857889833055840
c = 7187920142528335824861143203876908084067528690298329755497671248322277194754277305701102880967402859593937177306927235921616059382304183094350022713118203435560220591865274025991334717202171313133285253575822615616032441398946742994706880814251670668924098240782583026655923033371628284132606950034409888896558825512875084001031123558055489119898334591442547695833103046341283479780998109787754685881665949269402489768629140076361688313079919123642491566639820702501701460474001196941883819620040361365999896847153131825439764785309224799365130821807533936571946283436139142085798584001786665762720472918598961576836

d = gmpy2.invert(e, gcdpq)
m = pow(c, d, n)
print(long_to_bytes(m))

# DASCTF{52476aa73c056a3c6cd620ab061fd079}

FeedBack

题目

from secret import flag
from string import hexdigits
import random
from functools import reduce

def cycle(c:list,a:list)->int:
    return reduce(lambda x,y: x+y,map(lambda x: x[0]*x[1],zip(c,a))) 

def enc(m:list,k:list)->list:
    for i in range(len(k)*2):
        m.append(cycle(m[i:i+len(k)],k))
    return m[len(k):]

if __name__ == "__main__":
    key=[ord(random.choice(hexdigits)) for i in range(len(flag))]
    c=enc(list(flag),key)
    print(c)

# [180320, 12795604, 913707946, 65244867544, 4658921499366, 332678259897680, 23755460291939729, 1696299282824525162, 121127152307279309992, 8649291534003765460181, 617617459134250473857819, 44102031285199767595231826, 3149180993372727865351695610, 224872656429052251931507068163, 16057416742916791898621189838002, 1146607313446549338631740275859490, 81875456824588820793005728503088789, 5846457066530480582594997088868317921, 417476268914312098171907310476576578536, 29810607197367740257089118506396936455267, 2128677406710643996313598469435818995764283, 152001851952900202233154866795341968398324618, 10853952282423997785255606215412380976089774602, 775045031593704366379150517314704054142878227755, 55343416422679709865626814221707233611767499083451, 3951891330799176591085237005754672086216649002044116, 282191561344334793283891774610663595748300192924237652, 20150371209182455377207293308509352961052348504530516058, 1438871729308714548579613052036192683042976990785336035213, 102745097443187470470063857372230471012050786200205019335560, 7336689458539737357933680339939811164938123954552946412371136, 523888862345101730958585832445722009143686030486587614405269619, 37409180481229224476184683624742923927721083153229315469794323846, 2671266531631899605156440693785360699681088880751785277451781995127, 190746356675660819059021289711194688989007498945709965975632125093772, 13620569925986012345710256811290898483914841356894501064938828451682289, 972600097542764210429602165761543702875470220807440912087468994318947199, 69450173882625967125859360885466807837084362724230554403206714010957033564, 4959208480970674965771932762141990438694621159829420665293248503741956497339, 354120765763611360372631234091033326236527919343510113669886900852817067794937, 25286599106731127999761204195099137001826484641202640190432847596126102129290177, 1805632869356683189091740036886552559813413339716342384679179468460652986832630119, 128934304100758873373068786008043012614625306314330902439450614878647840309940810799, 9206774564238985792239909901043542380389506567225353556524468058541750913201465442258, 657425488646345934124836595103998888905043390553798696290609052666406363868364633227987, 46944591735815161454850764823066332748372328488810515939042504343121621896260739496814215, 3352158885381868382186614128492698209211597671157972107257901283108688995314288195559935895, 239366640061152248661380413770610731951278310979044705869198442025229868870474962029566786828, 17092384440374810990148000504438682199862673994374786921479630475896214666270304948184067943963, 1220510952499186818225235173267171189892653750839095345581049972346091269304188809141591821528945, 87152672604981875905661244747737456527193455119785950165560211136820203006355054095176767065463607, 6223285687554056604834063330772248822879874758146969128122776216276580479221618865554693862254391145, 444384361274324240336894080988769378714126300500080707977898823502774400070423897702729938853457320554, 31732025566514505285832183071784730973330427403124198140983516899800427456134314554661472009492580417251]

cycle函数表示两个list中元素对应相乘再相加，即[a,b], [c,d]->ac+bd。因此可以依次列出54个方程，后27个方程解出27个未知元素的key，再根据key用前27个方程解出27个未知元素的flag。

step 1: 后27个方程计算key

from z3 import *

m = [180320, 12795604, 913707946, 65244867544, 4658921499366, 332678259897680, 23755460291939729, 1696299282824525162, 121127152307279309992, 8649291534003765460181, 617617459134250473857819, 44102031285199767595231826, 3149180993372727865351695610, 224872656429052251931507068163, 16057416742916791898621189838002, 1146607313446549338631740275859490, 81875456824588820793005728503088789, 5846457066530480582594997088868317921, 417476268914312098171907310476576578536, 29810607197367740257089118506396936455267, 2128677406710643996313598469435818995764283, 152001851952900202233154866795341968398324618, 10853952282423997785255606215412380976089774602, 775045031593704366379150517314704054142878227755, 55343416422679709865626814221707233611767499083451, 3951891330799176591085237005754672086216649002044116, 282191561344334793283891774610663595748300192924237652, 20150371209182455377207293308509352961052348504530516058, 1438871729308714548579613052036192683042976990785336035213, 102745097443187470470063857372230471012050786200205019335560, 7336689458539737357933680339939811164938123954552946412371136, 523888862345101730958585832445722009143686030486587614405269619, 37409180481229224476184683624742923927721083153229315469794323846, 2671266531631899605156440693785360699681088880751785277451781995127, 190746356675660819059021289711194688989007498945709965975632125093772, 13620569925986012345710256811290898483914841356894501064938828451682289, 972600097542764210429602165761543702875470220807440912087468994318947199, 69450173882625967125859360885466807837084362724230554403206714010957033564, 4959208480970674965771932762141990438694621159829420665293248503741956497339, 354120765763611360372631234091033326236527919343510113669886900852817067794937, 25286599106731127999761204195099137001826484641202640190432847596126102129290177, 1805632869356683189091740036886552559813413339716342384679179468460652986832630119, 128934304100758873373068786008043012614625306314330902439450614878647840309940810799, 9206774564238985792239909901043542380389506567225353556524468058541750913201465442258, 657425488646345934124836595103998888905043390553798696290609052666406363868364633227987, 46944591735815161454850764823066332748372328488810515939042504343121621896260739496814215, 3352158885381868382186614128492698209211597671157972107257901283108688995314288195559935895, 239366640061152248661380413770610731951278310979044705869198442025229868870474962029566786828, 17092384440374810990148000504438682199862673994374786921479630475896214666270304948184067943963, 1220510952499186818225235173267171189892653750839095345581049972346091269304188809141591821528945, 87152672604981875905661244747737456527193455119785950165560211136820203006355054095176767065463607, 6223285687554056604834063330772248822879874758146969128122776216276580479221618865554693862254391145, 444384361274324240336894080988769378714126300500080707977898823502774400070423897702729938853457320554, 31732025566514505285832183071784730973330427403124198140983516899800427456134314554661472009492580417251]

s = Solver()
a1 = [0] * 27
for i in range(27):
    a1[i] = Int('a1['+str(i)+']')

for i in range(0, 27):
    s.add(m[i+0] * a1[0] + m[i+1] * a1[1] + m[i+2] * a1[2] + m[i+3] * a1[3] + m[i+4] * a1[4] + m[i+5] * a1[5] + m[i+6] * a1[6] + m[i+7] * a1[7] + m[i+8] * a1[8] + m[i+9] * a1[9] + m[i+10] * a1[10] + m[i+11] * a1[11] + m[i+12] * a1[12] + m[i+13] * a1[13] + m[i+14] * a1[14] + m[i+15] * a1[15] + m[i+16] * a1[16] + m[i+17] * a1[17] + m[i+18] * a1[18] + m[i+19] * a1[19] + m[i+20] * a1[20] + m[i+21] * a1[21] + m[i+22] * a1[22] + m[i+23] * a1[23] + m[i+24] * a1[24] + m[i+25] * a1[25] + m[i+26] * a1[26] == m[i+27])
s.check()
print(s.model())

# a = [50,55,51,70,57,68,100,54,49,55,55,66,97,52,65,48,50,52,66,53,49,98,53,102,102,99,70]

step 2: 生成约束

start = 0
with open('1.txt', 'w') as f:
    for j in range(27):
        c = 0
        s = 's.add( '
        for i in range(start, 27):
            s += 'a[{0}] * x[{1}] + '.format(str(c), str(i))
            c += 1

        for i in range(0, start):
            s += 'a[{0}] * m[{1}] + '.format(str(c), str(i))
            c += 1

        res = s[:-2] + '== m[{0}] )'.format(str(start)) + '\n'
        f.write(res)
        start += 1

f.close()

step 3: 前27个方程计算flag

from z3 import *

a = [50,55,51,70,57,68,100,54,49,55,55,66,97,52,65,48,50,52,66,53,49,98,53,102,102,99,70]
m = [180320, 12795604, 913707946, 65244867544, 4658921499366, 332678259897680, 23755460291939729, 1696299282824525162, 121127152307279309992, 8649291534003765460181, 617617459134250473857819, 44102031285199767595231826, 3149180993372727865351695610, 224872656429052251931507068163, 16057416742916791898621189838002, 1146607313446549338631740275859490, 81875456824588820793005728503088789, 5846457066530480582594997088868317921, 417476268914312098171907310476576578536, 29810607197367740257089118506396936455267, 2128677406710643996313598469435818995764283, 152001851952900202233154866795341968398324618, 10853952282423997785255606215412380976089774602, 775045031593704366379150517314704054142878227755, 55343416422679709865626814221707233611767499083451, 3951891330799176591085237005754672086216649002044116, 282191561344334793283891774610663595748300192924237652, 20150371209182455377207293308509352961052348504530516058, 1438871729308714548579613052036192683042976990785336035213, 102745097443187470470063857372230471012050786200205019335560, 7336689458539737357933680339939811164938123954552946412371136, 523888862345101730958585832445722009143686030486587614405269619, 37409180481229224476184683624742923927721083153229315469794323846, 2671266531631899605156440693785360699681088880751785277451781995127, 190746356675660819059021289711194688989007498945709965975632125093772, 13620569925986012345710256811290898483914841356894501064938828451682289, 972600097542764210429602165761543702875470220807440912087468994318947199, 69450173882625967125859360885466807837084362724230554403206714010957033564, 4959208480970674965771932762141990438694621159829420665293248503741956497339, 354120765763611360372631234091033326236527919343510113669886900852817067794937, 25286599106731127999761204195099137001826484641202640190432847596126102129290177, 1805632869356683189091740036886552559813413339716342384679179468460652986832630119, 128934304100758873373068786008043012614625306314330902439450614878647840309940810799, 9206774564238985792239909901043542380389506567225353556524468058541750913201465442258, 657425488646345934124836595103998888905043390553798696290609052666406363868364633227987, 46944591735815161454850764823066332748372328488810515939042504343121621896260739496814215, 3352158885381868382186614128492698209211597671157972107257901283108688995314288195559935895, 239366640061152248661380413770610731951278310979044705869198442025229868870474962029566786828, 17092384440374810990148000504438682199862673994374786921479630475896214666270304948184067943963, 1220510952499186818225235173267171189892653750839095345581049972346091269304188809141591821528945, 87152672604981875905661244747737456527193455119785950165560211136820203006355054095176767065463607, 6223285687554056604834063330772248822879874758146969128122776216276580479221618865554693862254391145, 444384361274324240336894080988769378714126300500080707977898823502774400070423897702729938853457320554, 31732025566514505285832183071784730973330427403124198140983516899800427456134314554661472009492580417251]

s = Solver()
x = [0] * 27
for i in range(27):
    x[i] = Int('x['+str(i)+']')

s.add( a[0] * x[0] + a[1] * x[1] + a[2] * x[2] + a[3] * x[3] + a[4] * x[4] + a[5] * x[5] + a[6] * x[6] + a[7] * x[7] + a[8] * x[8] + a[9] * x[9] + a[10] * x[10] + a[11] * x[11] + a[12] * x[12] + a[13] * x[13] + a[14] * x[14] + a[15] * x[15] + a[16] * x[16] + a[17] * x[17] + a[18] * x[18] + a[19] * x[19] + a[20] * x[20] + a[21] * x[21] + a[22] * x[22] + a[23] * x[23] + a[24] * x[24] + a[25] * x[25] + a[26] * x[26] == m[0] )
s.add( a[0] * x[1] + a[1] * x[2] + a[2] * x[3] + a[3] * x[4] + a[4] * x[5] + a[5] * x[6] + a[6] * x[7] + a[7] * x[8] + a[8] * x[9] + a[9] * x[10] + a[10] * x[11] + a[11] * x[12] + a[12] * x[13] + a[13] * x[14] + a[14] * x[15] + a[15] * x[16] + a[16] * x[17] + a[17] * x[18] + a[18] * x[19] + a[19] * x[20] + a[20] * x[21] + a[21] * x[22] + a[22] * x[23] + a[23] * x[24] + a[24] * x[25] + a[25] * x[26] + a[26] * m[0] == m[1] )
s.add( a[0] * x[2] + a[1] * x[3] + a[2] * x[4] + a[3] * x[5] + a[4] * x[6] + a[5] * x[7] + a[6] * x[8] + a[7] * x[9] + a[8] * x[10] + a[9] * x[11] + a[10] * x[12] + a[11] * x[13] + a[12] * x[14] + a[13] * x[15] + a[14] * x[16] + a[15] * x[17] + a[16] * x[18] + a[17] * x[19] + a[18] * x[20] + a[19] * x[21] + a[20] * x[22] + a[21] * x[23] + a[22] * x[24] + a[23] * x[25] + a[24] * x[26] + a[25] * m[0] + a[26] * m[1] == m[2] )
s.add( a[0] * x[3] + a[1] * x[4] + a[2] * x[5] + a[3] * x[6] + a[4] * x[7] + a[5] * x[8] + a[6] * x[9] + a[7] * x[10] + a[8] * x[11] + a[9] * x[12] + a[10] * x[13] + a[11] * x[14] + a[12] * x[15] + a[13] * x[16] + a[14] * x[17] + a[15] * x[18] + a[16] * x[19] + a[17] * x[20] + a[18] * x[21] + a[19] * x[22] + a[20] * x[23] + a[21] * x[24] + a[22] * x[25] + a[23] * x[26] + a[24] * m[0] + a[25] * m[1] + a[26] * m[2] == m[3] )
s.add( a[0] * x[4] + a[1] * x[5] + a[2] * x[6] + a[3] * x[7] + a[4] * x[8] + a[5] * x[9] + a[6] * x[10] + a[7] * x[11] + a[8] * x[12] + a[9] * x[13] + a[10] * x[14] + a[11] * x[15] + a[12] * x[16] + a[13] * x[17] + a[14] * x[18] + a[15] * x[19] + a[16] * x[20] + a[17] * x[21] + a[18] * x[22] + a[19] * x[23] + a[20] * x[24] + a[21] * x[25] + a[22] * x[26] + a[23] * m[0] + a[24] * m[1] + a[25] * m[2] + a[26] * m[3] == m[4] )
s.add( a[0] * x[5] + a[1] * x[6] + a[2] * x[7] + a[3] * x[8] + a[4] * x[9] + a[5] * x[10] + a[6] * x[11] + a[7] * x[12] + a[8] * x[13] + a[9] * x[14] + a[10] * x[15] + a[11] * x[16] + a[12] * x[17] + a[13] * x[18] + a[14] * x[19] + a[15] * x[20] + a[16] * x[21] + a[17] * x[22] + a[18] * x[23] + a[19] * x[24] + a[20] * x[25] + a[21] * x[26] + a[22] * m[0] + a[23] * m[1] + a[24] * m[2] + a[25] * m[3] + a[26] * m[4] == m[5] )
s.add( a[0] * x[6] + a[1] * x[7] + a[2] * x[8] + a[3] * x[9] + a[4] * x[10] + a[5] * x[11] + a[6] * x[12] + a[7] * x[13] + a[8] * x[14] + a[9] * x[15] + a[10] * x[16] + a[11] * x[17] + a[12] * x[18] + a[13] * x[19] + a[14] * x[20] + a[15] * x[21] + a[16] * x[22] + a[17] * x[23] + a[18] * x[24] + a[19] * x[25] + a[20] * x[26] + a[21] * m[0] + a[22] * m[1] + a[23] * m[2] + a[24] * m[3] + a[25] * m[4] + a[26] * m[5] == m[6] )
s.add( a[0] * x[7] + a[1] * x[8] + a[2] * x[9] + a[3] * x[10] + a[4] * x[11] + a[5] * x[12] + a[6] * x[13] + a[7] * x[14] + a[8] * x[15] + a[9] * x[16] + a[10] * x[17] + a[11] * x[18] + a[12] * x[19] + a[13] * x[20] + a[14] * x[21] + a[15] * x[22] + a[16] * x[23] + a[17] * x[24] + a[18] * x[25] + a[19] * x[26] + a[20] * m[0] + a[21] * m[1] + a[22] * m[2] + a[23] * m[3] + a[24] * m[4] + a[25] * m[5] + a[26] * m[6] == m[7] )
s.add( a[0] * x[8] + a[1] * x[9] + a[2] * x[10] + a[3] * x[11] + a[4] * x[12] + a[5] * x[13] + a[6] * x[14] + a[7] * x[15] + a[8] * x[16] + a[9] * x[17] + a[10] * x[18] + a[11] * x[19] + a[12] * x[20] + a[13] * x[21] + a[14] * x[22] + a[15] * x[23] + a[16] * x[24] + a[17] * x[25] + a[18] * x[26] + a[19] * m[0] + a[20] * m[1] + a[21] * m[2] + a[22] * m[3] + a[23] * m[4] + a[24] * m[5] + a[25] * m[6] + a[26] * m[7] == m[8] )
s.add( a[0] * x[9] + a[1] * x[10] + a[2] * x[11] + a[3] * x[12] + a[4] * x[13] + a[5] * x[14] + a[6] * x[15] + a[7] * x[16] + a[8] * x[17] + a[9] * x[18] + a[10] * x[19] + a[11] * x[20] + a[12] * x[21] + a[13] * x[22] + a[14] * x[23] + a[15] * x[24] + a[16] * x[25] + a[17] * x[26] + a[18] * m[0] + a[19] * m[1] + a[20] * m[2] + a[21] * m[3] + a[22] * m[4] + a[23] * m[5] + a[24] * m[6] + a[25] * m[7] + a[26] * m[8] == m[9] )
s.add( a[0] * x[10] + a[1] * x[11] + a[2] * x[12] + a[3] * x[13] + a[4] * x[14] + a[5] * x[15] + a[6] * x[16] + a[7] * x[17] + a[8] * x[18] + a[9] * x[19] + a[10] * x[20] + a[11] * x[21] + a[12] * x[22] + a[13] * x[23] + a[14] * x[24] + a[15] * x[25] + a[16] * x[26] + a[17] * m[0] + a[18] * m[1] + a[19] * m[2] + a[20] * m[3] + a[21] * m[4] + a[22] * m[5] + a[23] * m[6] + a[24] * m[7] + a[25] * m[8] + a[26] * m[9] == m[10] )
s.add( a[0] * x[11] + a[1] * x[12] + a[2] * x[13] + a[3] * x[14] + a[4] * x[15] + a[5] * x[16] + a[6] * x[17] + a[7] * x[18] + a[8] * x[19] + a[9] * x[20] + a[10] * x[21] + a[11] * x[22] + a[12] * x[23] + a[13] * x[24] + a[14] * x[25] + a[15] * x[26] + a[16] * m[0] + a[17] * m[1] + a[18] * m[2] + a[19] * m[3] + a[20] * m[4] + a[21] * m[5] + a[22] * m[6] + a[23] * m[7] + a[24] * m[8] + a[25] * m[9] + a[26] * m[10] == m[11] )
s.add( a[0] * x[12] + a[1] * x[13] + a[2] * x[14] + a[3] * x[15] + a[4] * x[16] + a[5] * x[17] + a[6] * x[18] + a[7] * x[19] + a[8] * x[20] + a[9] * x[21] + a[10] * x[22] + a[11] * x[23] + a[12] * x[24] + a[13] * x[25] + a[14] * x[26] + a[15] * m[0] + a[16] * m[1] + a[17] * m[2] + a[18] * m[3] + a[19] * m[4] + a[20] * m[5] + a[21] * m[6] + a[22] * m[7] + a[23] * m[8] + a[24] * m[9] + a[25] * m[10] + a[26] * m[11] == m[12] )
s.add( a[0] * x[13] + a[1] * x[14] + a[2] * x[15] + a[3] * x[16] + a[4] * x[17] + a[5] * x[18] + a[6] * x[19] + a[7] * x[20] + a[8] * x[21] + a[9] * x[22] + a[10] * x[23] + a[11] * x[24] + a[12] * x[25] + a[13] * x[26] + a[14] * m[0] + a[15] * m[1] + a[16] * m[2] + a[17] * m[3] + a[18] * m[4] + a[19] * m[5] + a[20] * m[6] + a[21] * m[7] + a[22] * m[8] + a[23] * m[9] + a[24] * m[10] + a[25] * m[11] + a[26] * m[12] == m[13] )
s.add( a[0] * x[14] + a[1] * x[15] + a[2] * x[16] + a[3] * x[17] + a[4] * x[18] + a[5] * x[19] + a[6] * x[20] + a[7] * x[21] + a[8] * x[22] + a[9] * x[23] + a[10] * x[24] + a[11] * x[25] + a[12] * x[26] + a[13] * m[0] + a[14] * m[1] + a[15] * m[2] + a[16] * m[3] + a[17] * m[4] + a[18] * m[5] + a[19] * m[6] + a[20] * m[7] + a[21] * m[8] + a[22] * m[9] + a[23] * m[10] + a[24] * m[11] + a[25] * m[12] + a[26] * m[13] == m[14] )
s.add( a[0] * x[15] + a[1] * x[16] + a[2] * x[17] + a[3] * x[18] + a[4] * x[19] + a[5] * x[20] + a[6] * x[21] + a[7] * x[22] + a[8] * x[23] + a[9] * x[24] + a[10] * x[25] + a[11] * x[26] + a[12] * m[0] + a[13] * m[1] + a[14] * m[2] + a[15] * m[3] + a[16] * m[4] + a[17] * m[5] + a[18] * m[6] + a[19] * m[7] + a[20] * m[8] + a[21] * m[9] + a[22] * m[10] + a[23] * m[11] + a[24] * m[12] + a[25] * m[13] + a[26] * m[14] == m[15] )
s.add( a[0] * x[16] + a[1] * x[17] + a[2] * x[18] + a[3] * x[19] + a[4] * x[20] + a[5] * x[21] + a[6] * x[22] + a[7] * x[23] + a[8] * x[24] + a[9] * x[25] + a[10] * x[26] + a[11] * m[0] + a[12] * m[1] + a[13] * m[2] + a[14] * m[3] + a[15] * m[4] + a[16] * m[5] + a[17] * m[6] + a[18] * m[7] + a[19] * m[8] + a[20] * m[9] + a[21] * m[10] + a[22] * m[11] + a[23] * m[12] + a[24] * m[13] + a[25] * m[14] + a[26] * m[15] == m[16] )
s.add( a[0] * x[17] + a[1] * x[18] + a[2] * x[19] + a[3] * x[20] + a[4] * x[21] + a[5] * x[22] + a[6] * x[23] + a[7] * x[24] + a[8] * x[25] + a[9] * x[26] + a[10] * m[0] + a[11] * m[1] + a[12] * m[2] + a[13] * m[3] + a[14] * m[4] + a[15] * m[5] + a[16] * m[6] + a[17] * m[7] + a[18] * m[8] + a[19] * m[9] + a[20] * m[10] + a[21] * m[11] + a[22] * m[12] + a[23] * m[13] + a[24] * m[14] + a[25] * m[15] + a[26] * m[16] == m[17] )
s.add( a[0] * x[18] + a[1] * x[19] + a[2] * x[20] + a[3] * x[21] + a[4] * x[22] + a[5] * x[23] + a[6] * x[24] + a[7] * x[25] + a[8] * x[26] + a[9] * m[0] + a[10] * m[1] + a[11] * m[2] + a[12] * m[3] + a[13] * m[4] + a[14] * m[5] + a[15] * m[6] + a[16] * m[7] + a[17] * m[8] + a[18] * m[9] + a[19] * m[10] + a[20] * m[11] + a[21] * m[12] + a[22] * m[13] + a[23] * m[14] + a[24] * m[15] + a[25] * m[16] + a[26] * m[17] == m[18] )
s.add( a[0] * x[19] + a[1] * x[20] + a[2] * x[21] + a[3] * x[22] + a[4] * x[23] + a[5] * x[24] + a[6] * x[25] + a[7] * x[26] + a[8] * m[0] + a[9] * m[1] + a[10] * m[2] + a[11] * m[3] + a[12] * m[4] + a[13] * m[5] + a[14] * m[6] + a[15] * m[7] + a[16] * m[8] + a[17] * m[9] + a[18] * m[10] + a[19] * m[11] + a[20] * m[12] + a[21] * m[13] + a[22] * m[14] + a[23] * m[15] + a[24] * m[16] + a[25] * m[17] + a[26] * m[18] == m[19] )
s.add( a[0] * x[20] + a[1] * x[21] + a[2] * x[22] + a[3] * x[23] + a[4] * x[24] + a[5] * x[25] + a[6] * x[26] + a[7] * m[0] + a[8] * m[1] + a[9] * m[2] + a[10] * m[3] + a[11] * m[4] + a[12] * m[5] + a[13] * m[6] + a[14] * m[7] + a[15] * m[8] + a[16] * m[9] + a[17] * m[10] + a[18] * m[11] + a[19] * m[12] + a[20] * m[13] + a[21] * m[14] + a[22] * m[15] + a[23] * m[16] + a[24] * m[17] + a[25] * m[18] + a[26] * m[19] == m[20] )
s.add( a[0] * x[21] + a[1] * x[22] + a[2] * x[23] + a[3] * x[24] + a[4] * x[25] + a[5] * x[26] + a[6] * m[0] + a[7] * m[1] + a[8] * m[2] + a[9] * m[3] + a[10] * m[4] + a[11] * m[5] + a[12] * m[6] + a[13] * m[7] + a[14] * m[8] + a[15] * m[9] + a[16] * m[10] + a[17] * m[11] + a[18] * m[12] + a[19] * m[13] + a[20] * m[14] + a[21] * m[15] + a[22] * m[16] + a[23] * m[17] + a[24] * m[18] + a[25] * m[19] + a[26] * m[20] == m[21] )
s.add( a[0] * x[22] + a[1] * x[23] + a[2] * x[24] + a[3] * x[25] + a[4] * x[26] + a[5] * m[0] + a[6] * m[1] + a[7] * m[2] + a[8] * m[3] + a[9] * m[4] + a[10] * m[5] + a[11] * m[6] + a[12] * m[7] + a[13] * m[8] + a[14] * m[9] + a[15] * m[10] + a[16] * m[11] + a[17] * m[12] + a[18] * m[13] + a[19] * m[14] + a[20] * m[15] + a[21] * m[16] + a[22] * m[17] + a[23] * m[18] + a[24] * m[19] + a[25] * m[20] + a[26] * m[21] == m[22] )
s.add( a[0] * x[23] + a[1] * x[24] + a[2] * x[25] + a[3] * x[26] + a[4] * m[0] + a[5] * m[1] + a[6] * m[2] + a[7] * m[3] + a[8] * m[4] + a[9] * m[5] + a[10] * m[6] + a[11] * m[7] + a[12] * m[8] + a[13] * m[9] + a[14] * m[10] + a[15] * m[11] + a[16] * m[12] + a[17] * m[13] + a[18] * m[14] + a[19] * m[15] + a[20] * m[16] + a[21] * m[17] + a[22] * m[18] + a[23] * m[19] + a[24] * m[20] + a[25] * m[21] + a[26] * m[22] == m[23] )
s.add( a[0] * x[24] + a[1] * x[25] + a[2] * x[26] + a[3] * m[0] + a[4] * m[1] + a[5] * m[2] + a[6] * m[3] + a[7] * m[4] + a[8] * m[5] + a[9] * m[6] + a[10] * m[7] + a[11] * m[8] + a[12] * m[9] + a[13] * m[10] + a[14] * m[11] + a[15] * m[12] + a[16] * m[13] + a[17] * m[14] + a[18] * m[15] + a[19] * m[16] + a[20] * m[17] + a[21] * m[18] + a[22] * m[19] + a[23] * m[20] + a[24] * m[21] + a[25] * m[22] + a[26] * m[23] == m[24] )
s.add( a[0] * x[25] + a[1] * x[26] + a[2] * m[0] + a[3] * m[1] + a[4] * m[2] + a[5] * m[3] + a[6] * m[4] + a[7] * m[5] + a[8] * m[6] + a[9] * m[7] + a[10] * m[8] + a[11] * m[9] + a[12] * m[10] + a[13] * m[11] + a[14] * m[12] + a[15] * m[13] + a[16] * m[14] + a[17] * m[15] + a[18] * m[16] + a[19] * m[17] + a[20] * m[18] + a[21] * m[19] + a[22] * m[20] + a[23] * m[21] + a[24] * m[22] + a[25] * m[23] + a[26] * m[24] == m[25] )
s.add( a[0] * x[26] + a[1] * m[0] + a[2] * m[1] + a[3] * m[2] + a[4] * m[3] + a[5] * m[4] + a[6] * m[5] + a[7] * m[6] + a[8] * m[7] + a[9] * m[8] + a[10] * m[9] + a[11] * m[10] + a[12] * m[11] + a[13] * m[12] + a[14] * m[13] + a[15] * m[14] + a[16] * m[15] + a[17] * m[16] + a[18] * m[17] + a[19] * m[18] + a[20] * m[19] + a[21] * m[20] + a[22] * m[21] + a[23] * m[22] + a[24] * m[23] + a[25] * m[24] + a[26] * m[25] == m[26] )

s.check()
print(s.model())

# [125, 95, 121, 115, 64, 101, 95, 111, 115, 95, 115, 105, 95, 107, 99, 97, 66, 100, 101, 101, 70, 95, 123, 103, 97, 108, 102]

x = [125, 95, 121, 115, 64, 101, 95, 111, 115, 95, 115, 105, 95, 107, 99, 97, 66, 100, 101, 101, 70, 95, 123, 103, 97, 108, 102]
flag = ''.join([chr(i) for i in x])[::-1]
print(flag)

# flag{_FeedBack_is_so_e@sy_}