reverse学习总结-查表代换

一.easygui-查表代换-整体循环位移

是exe文件,先运行一下

猜测是输入flag让后验证的,

查壳是64位的,ida直接打开

int __stdcall WinMain(HINSTANCE hInstance, HINSTANCE hPrevInstance, LPSTR lpCmdLine, int nShowCmd)
{HWND Window; // rbxWNDCLASSW WndClass; // [rsp+60h] [rbp-A8h] BYREFstruct tagMSG Msg; // [rsp+B0h] [rbp-58h] BYREFWndClass.hInstance = hInstance;WndClass.style = 3;WndClass.lpfnWndProc = (WNDPROC)sub_140001490;*(_QWORD *)&WndClass.cbClsExtra = 0i64;WndClass.hIcon = LoadIconW(0i64, (LPCWSTR)0x7F00);WndClass.hCursor = LoadCursorW(0i64, (LPCWSTR)0x7F00);WndClass.lpszMenuName = 0i64;WndClass.hbrBackground = (HBRUSH)GetStockObject(0);WndClass.lpszClassName = ClassName;if ( RegisterClassW(&WndClass) ){Window = CreateWindowExW(0, ClassName, L"easygui", 0xCF0000u, 500, 200, 400, 400, 0i64, 0i64, hInstance, 0i64);ShowWindow(Window, nShowCmd);UpdateWindow(Window);while ( GetMessageW(&Msg, 0i64, 0, 0) ){TranslateMessage(&Msg);DispatchMessageW(&Msg);}return Msg.wParam;}else{MessageBoxW(0i64, "購*N\vz廭", ClassName, 0x10u);return 0;}
}

遇到了不熟悉的东西,先学习一下

WNDCLASS（或WNDCLASSW，用于Unicode应用程序）是一个结构体，用于定义Windows程序中的窗口类。在Win32 API中，每个窗口都属于一个窗口类，而每个窗口类都是通过WNDCLASS结构体定义的。这个结构体包含了窗口类的所有属性，这些属性会被用来创建和管理窗口。

以下是WNDCLASS结构体的成员及其用途：

style：指定窗口类的风格。可以是以下值的组合：
- CS_BYTEALIGNCLIENT：客户区数据按字节对齐。
- CS_BYTEALIGNWINDOW：窗口数据按字节对齐。
- CS_CLASSDC：类背景在显示器上绘制。
- CS_DBLCLKS：如果启用，窗口接受双击消息。
- CS_DROPSHADOW：窗口有阴影效果。
- CS_GLOBALCLASS：类是系统范围的。
- CS_HREDRAW：水平大小改变时重绘窗口。
- CS_NOCLOSE：窗口没有关闭按钮。
- CS_OWNDC：类拥有自己的设备上下文。
- CS_SAVEBITS：保存窗口的位图。
- CS_VREDRAW：垂直大小改变时重绘窗口。
lpfnWndProc：指向窗口过程的指针，窗口过程是处理窗口消息的函数。
cbClsExtra：应用程序可以定义的额外字节数，用于存储额外的类数据。
cbWndExtra：应用程序可以定义的额外字节数，用于存储额外的窗口数据。
hInstance：包含窗口类的模块的实例句柄。
hIcon：窗口类的图标句柄。
hCursor：窗口类的光标句柄。
hbrBackground：窗口类的背景画刷句柄。
lpszMenuName：窗口类菜单的名称。
lpszClassName：窗口类的名称。

下面的Window和Message和窗口和消息显示有关,我们也就不看了

猜测加密和sub_140001490函数有关

LRESULT __fastcall sub_140001490(HWND hWndParent, UINT Msg, WPARAM wParam, LPARAM lParam)
{char v4; // blHWND DlgItem; // raxunsigned int WindowTextW; // eaxbool v12; // dlbool v13; // clbool v14; // dlbool v15; // albool v16; // clbool v17; // albool v18; // dlbool v19; // albool v20; // clbool v21; // alchar v22; // dlchar v23; // alchar v24; // clchar v25; // alchar v26; // dlchar v27; // alchar v28; // clchar v29; // alchar v30; // dlchar v31; // alchar v32; // clchar v33; // alchar v34; // dlchar v35; // alchar v36; // clchar v37; // alchar v38; // dlchar v39; // alchar v40; // clchar v41; // alchar v42; // dlchar v43; // clchar v44; // alchar v45; // dlchar v46; // alchar v47; // clchar v48; // alchar v49; // dlchar v50; // alchar v51; // clchar v52; // alchar v53; // dlchar v54; // alchar v55; // clchar v56; // alchar v57; // dlchar v58; // alchar v59; // clchar v60; // alchar v61; // dlchar v62; // alchar v63; // clchar v64; // alchar v65; // dlchar v66; // alchar v67; // clchar v68; // alchar v69; // dlchar v70; // alchar v71; // clchar v72; // alchar v73; // dlchar v74; // alchar v75; // clchar v76; // alchar v77; // dlchar v78; // alchar v79; // clchar v80; // alchar v81; // dlchar v82; // alchar v83; // clchar v84; // alchar v85; // dlchar v86; // alchar v87; // clchar v88; // alchar v89; // dlchar v90; // alchar v91; // clHWND Window; // raxHWND v93; // raxchar v94[512]; // [rsp+70h] [rbp-90h] BYREFWCHAR String[104]; // [rsp+270h] [rbp+170h] BYREFv4 = 0;::wParam = (WPARAM)CreateFontW(18, 0, 0, 0, 400, 0, 0, 0, 1u, 0, 0, 0, 0x20u, L"Tahoma");if ( Msg == 1 ){if ( !IsDebuggerPresent() ){Window = CreateWindowExW(0,L"EDIT",0i64,0x50800000u,15,100,350,24,hWndParent,(HMENU)0x65,*(HINSTANCE *)(lParam + 8),0i64);SendMessageW(Window, 0x30u, ::wParam, 1i64);v93 = CreateWindowExW(0,L"BUTTON",L"verify",0x50000000u,120,170,100,30,hWndParent,(HMENU)0x66,*(HINSTANCE *)(lParam + 8),0i64);SendMessageW(v93, 0x30u, ::wParam, 1i64);return 0i64;}goto LABEL_96;}if ( Msg == 2 ){
LABEL_96:PostQuitMessage(0);return 0i64;}if ( Msg != 273 )return DefWindowProcW(hWndParent, Msg, wParam, lParam);if ( (_WORD)wParam == 102 ){DlgItem = GetDlgItem(hWndParent, 101);WindowTextW = GetWindowTextW(DlgItem, String, 100);sub_140001000(String, WindowTextW, v94);v12 = 0;if ( v94[1] == -57 )v12 = v94[0] == -33;v13 = 0;if ( v94[2] == 77 )v13 = v12;v14 = 0;v15 = v13;v16 = 0;if ( v94[3] == 20 )v14 = v15;v17 = v14;v18 = 0;if ( v94[4] == -63 )v16 = v17;v19 = v16;v20 = 0;if ( v94[5] == -20 )v18 = v19;v21 = v18;v22 = 0;if ( v94[6] == 8 )v20 = v21;v23 = v20;v24 = 0;if ( v94[7] == -28 )v22 = v23;v25 = v22;v26 = 0;if ( v94[8] == 95 )v24 = v25;v27 = v24;v28 = 0;if ( v94[9] == 63 )v26 = v27;v29 = v26;v30 = 0;if ( v94[10] == 3 )v28 = v29;v31 = v28;v32 = 0;if ( v94[11] == -76 )v30 = v31;v33 = v30;v34 = 0;if ( v94[12] == -112 )v32 = v33;v35 = v32;v36 = 0;if ( v94[13] == 74 )v34 = v35;v37 = v34;v38 = 0;if ( v94[14] == -71 )v36 = v37;v39 = v36;v40 = 0;if ( v94[15] == -113 )v38 = v39;v41 = v38;v42 = 0;if ( v94[16] == -113 )v40 = v41;if ( v94[17] == -6 )v42 = v40;v43 = 0;v44 = v42;v45 = 0;if ( v94[18] == 113 )v43 = v44;v46 = v43;v47 = 0;if ( v94[19] == 67 )v45 = v46;v48 = v45;v49 = 0;if ( v94[20] == -57 )v47 = v48;v50 = v47;v51 = 0;if ( v94[21] == -15 )v49 = v50;v52 = v49;v53 = 0;if ( v94[22] == -99 )v51 = v52;v54 = v51;v55 = 0;if ( v94[23] == -35 )v53 = v54;v56 = v53;v57 = 0;if ( v94[24] == 79 )v55 = v56;v58 = v55;v59 = 0;if ( v94[25] == -64 )v57 = v58;v60 = v57;v61 = 0;if ( v94[26] == 18 )v59 = v60;v62 = v59;v63 = 0;if ( v94[27] == 68 )v61 = v62;v64 = v61;v65 = 0;if ( v94[28] == 92 )v63 = v64;v66 = v63;v67 = 0;if ( v94[29] == -99 )v65 = v66;v68 = v65;v69 = 0;if ( v94[30] == -120 )v67 = v68;v70 = v67;v71 = 0;if ( v94[31] == 54 )v69 = v70;v72 = v69;v73 = 0;if ( v94[32] == 45 )v71 = v72;v74 = v71;v75 = 0;if ( v94[33] == 22 )v73 = v74;v76 = v73;v77 = 0;if ( v94[34] == 29 )v75 = v76;v78 = v75;v79 = 0;if ( v94[35] == -19 )v77 = v78;v80 = v77;v81 = 0;if ( v94[36] == -68 )v79 = v80;v82 = v79;v83 = 0;if ( v94[37] == -17 )v81 = v82;v84 = v81;v85 = 0;if ( v94[38] == -69 )v83 = v84;v86 = v83;v87 = 0;if ( v94[39] == 91 )v85 = v86;v88 = v85;v89 = 0;if ( v94[40] == -97 )v87 = v88;v90 = v87;v91 = 0;if ( v94[41] == 119 )v89 = v90;if ( v94[42] == -21 )v91 = v89;if ( v94[43] == 88 )v4 = v91;if ( v4 )MessageBoxW(hWndParent, L"Right!", L"Right!", 0x40u);elseMessageBoxW(hWndParent, L"Wrong!", L"Wrong!", 0x10u);}return 0i64;
}

见到了另一个函数sub_140001000

unsigned __int64 __fastcall sub_140001000(__int64 a1, int a2, void *a3)
{signed __int64 v4; // rbxint v6; // edisigned __int64 v7; // rsisigned __int64 i; // rcxsigned __int64 j; // rdxsigned __int64 k; // r11unsigned __int8 v11; // r9unsigned __int8 v12; // r10char v13; // clchar v14; // r8__int16 v15; // kr00_2__int64 v16; // r14int v17; // ebxint v18; // ecx__int64 v19; // rdx__int64 v20; // rax__int64 v21; // rdxint v22; // r8d_BYTE *v23; // rcxunsigned __int64 result; // raxint v25; // r8dsigned __int64 m; // r10int v27; // r9dchar v28[16]; // [rsp+20h] [rbp-E0h] BYREF__int128 v29[16]; // [rsp+30h] [rbp-D0h] BYREFchar Src[304]; // [rsp+130h] [rbp+30h] BYREFchar v31[256]; // [rsp+260h] [rbp+160h] BYREFv4 = a2;memset(Src, 0, 0x12Cui64);v6 = 0;v7 = v4;if ( (int)v4 > 0 ){for ( i = 0i64; i < v4; ++i )Src[i] = *(_BYTE *)(a1 + 2 * i);}v29[0] = (__int128)_mm_load_si128((const __m128i *)&xmmword_1400033C0);v29[1] = (__int128)_mm_load_si128((const __m128i *)&xmmword_1400033D0);v29[2] = (__int128)_mm_load_si128((const __m128i *)&xmmword_140003390);v29[3] = (__int128)_mm_load_si128((const __m128i *)&xmmword_1400033E0);v29[4] = (__int128)_mm_load_si128((const __m128i *)&xmmword_1400033B0);v29[5] = (__int128)_mm_load_si128((const __m128i *)&xmmword_140003400);v29[6] = (__int128)_mm_load_si128((const __m128i *)&xmmword_1400033F0);v29[7] = (__int128)_mm_load_si128((const __m128i *)&xmmword_1400033A0);if ( (int)v4 > 0 ){for ( j = 0i64; j < v4; ++j )Src[j] = *((_BYTE *)v29 + (unsigned __int8)Src[j]);for ( k = 0i64; k < v4; k += 4i64 ){v11 = Src[k + 3];v12 = Src[k + 2];v13 = ((unsigned __int8)Src[k] >> 3) | (32 * v11);v14 = 32 * Src[k + 1];Src[k + 1] = (32 * Src[k]) | ((unsigned __int8)Src[k + 1] >> 3);v15 = 32 * v12;Src[k + 2] = v14 | HIBYTE(v15);Src[k] = v13;Src[k + 3] = v15 | (v11 >> 3);}}v16 = 256i64;strcpy(v28, "easy_GUI");v17 = 0;memset(v31, 0, sizeof(v31));v18 = 0;v19 = 0i64;do{*((_BYTE *)v29 + v19) = v18;v20 = v18 & 7;++v19;++v18;Src[v19 + 303] = v28[v20];}while ( v18 < 256 );v21 = 0i64;do{v22 = *((unsigned __int8 *)v29 + v21);v17 = (v22 + v31[v21] + v17) % 256;v23 = (char *)v29 + v17;result = (unsigned __int8)*v23;*((_BYTE *)v29 + v21++) = result;*v23 = v22;--v16;}while ( v16 );v25 = 0;if ( v7 > 0 ){for ( m = 0i64; m < v7; ++m ){v6 = (v6 + 1) % 256;v27 = *((unsigned __int8 *)v29 + v6);v25 = (v27 + v25) % 256;*((_BYTE *)v29 + v6) = *((_BYTE *)v29 + v25);*((_BYTE *)v29 + v25) = v27;Src[m] ^= *((_BYTE *)v29 + (unsigned __int8)(v27 + *((_BYTE *)v29 + v6)));}return (unsigned __int64)memcpy(a3, Src, v7);}return result;
}

有明显的加密操作

1.进行换表加密

2.每4位为一组一加密,进行移位操作,自己右移3位和自己的前一位左移5位再按位异或,第一位和第四位交互,相当于这四个为一组,每组整体循环右移 3 位

3.进行rc4流加密

密文是sub_140001490函数处的v94

写脚本解决

#include <stdio.h>
#include <string.h>unsigned char sbox[256] = {0};
const unsigned char* key = (const unsigned char*)"easy_GUI";
unsigned char data[] = {223,199, 77, 20,193,236,  8,228, 95, 63,3 ,180,144, 74,185,143,143,250,113, 67,199,241,157,221, 79,192,18 ,68 , 92,157,136, 54, 45, 22, 29,237,188,239,187, 91,159,119,235, 88};void swap(unsigned char* a, unsigned char* b) {unsigned char tmp = *a;*a = *b;*b = tmp;
}void init_sbox(const unsigned char key[]) {for (unsigned int i = 0; i < 256; i++) sbox[i] = i;unsigned int keyLen = strlen((const char*)key);unsigned char Ttable[256] = {0};for (int i = 0; i < 256; i++) Ttable[i] = key[i % keyLen];for (int j = 0, i = 0; i < 256; i++) {j = (j + sbox[i] + Ttable[i]) % 256;swap(&sbox[i], &sbox[j]);}
}void RC4(unsigned char* data, unsigned int dataLen, const unsigned char key[]) {unsigned char k, i = 0, j = 0, t;init_sbox(key);for (unsigned int h = 0; h < dataLen; h++) {i = (i + 1) % 256;j = (j + sbox[i]) % 256;swap(&sbox[i], &sbox[j]);t = (sbox[i] + sbox[j]) % 256;k = sbox[t];data[h] ^= k;}
}int main(void) {unsigned int dataLen = sizeof(data) / sizeof(data[0]);RC4(data, dataLen, key);for (unsigned int i = 0; i < dataLen; i++) {printf("%d,", data[i]);}return 0;
}

111,129,166,197,99,172,75,199,143,41,135,164,39,170,166,105,79,39,174,236,39,46,231,169,105,135,46,229,47,36,230,111,68,135,169,137,79,38,71,33,171,1,167,174,

自己提取出密文,进行rc4解密

#include <stdio.h>
#include <string.h>
void change(unsigned char *m){int a=m[0];int b=m[1];int c=m[2];int d=m[3];m[0]=(a<<3)|(b>>5);m[1]=(b<<3)|(c>>5);m[2]=(c<<3)|(d>>5);m[3]=(d<<3)|(a>>5);
}
int main()
{unsigned char enc[]={111,129,166,197, 99,172, 75,199,143, 41,135,164, 39,170,166,105, 79, 39,174,236,39, 46,231,169,105,135, 46,229, 47, 36,230,111, 68,135,169,137, 79,38, 71, 33,171,  1,167,174,};int i;for(i=0;i<44;i+=4){change(enc+i);}int table[]={18, 66, 86, 4, 12, 35, 16, 124, 21, 84, 109, 22, 64, 108, 34, 70, 93, 106, 46, 23, 62, 37, 58, 47, 73, 126, 27, 68, 61, 123, 117, 14, 3, 20, 80, 127, 118, 38, 36, 105, 79, 43, 45, 103, 29, 100, 48, 26, 67, 0, 115, 53, 104, 9, 97, 17, 92, 49, 8, 33, 42, 51, 87, 72, 119, 44, 11, 15, 54, 91, 90, 57, 94, 101, 121, 25, 114, 116, 122, 65, 88, 31, 24, 5, 2, 82, 30, 50, 112, 28, 63, 81, 113, 77, 85, 60, 96, 98, 71, 39, 40, 10, 52, 120, 69, 74, 78, 13, 55, 75, 99, 56, 7, 59, 83, 111, 1, 125, 19, 110, 6, 95, 41, 89, 102, 107, 76, 32};for(i=0;i<44;i++){enc[i]=table[enc[i]];printf("%c",enc[i]);}return 0;
}

其中的查表代换我们先换表,

#include <stdio.h>
#include <string.h>
int main()
{int i;int t[]={49, 116, 84, 32, 3, 83, 120, 112, 58, 53, 101, 66, 4, 107, 31, 67, 6, 55, 0, 118, 33, 8, 11, 19, 82, 75, 47, 26, 89, 44, 86, 81, 127, 59, 14, 5, 38, 21, 37, 99, 100, 122, 60, 41, 65, 42, 18, 23, 46, 57, 87, 61, 102, 51, 68, 108, 111, 71, 22, 113, 95, 28, 20, 90, 12, 79, 1, 48, 27, 104, 15, 98, 63, 24, 105, 109, 126, 93, 106, 40, 34, 91, 85, 114, 9, 94, 2, 62, 80, 123, 70, 69, 56, 16, 72, 121, 96, 54, 97, 110, 45, 73, 124, 43, 52, 39, 17, 125, 13, 10, 119, 115, 88, 92, 76, 50, 77, 30, 36, 64, 103, 74, 78, 29, 7, 117, 25, 35};int tt[200];for(i=0;i<128;i++){tt[t[i]]=i;}for(i=0;i<128;i++){printf("%d,",tt[i]);}return 0;
}

flag{GU!_r3v3R5e_3nG1n3er1ng_i5_v3ry_s1mpl3}

知识点:

1.认识到了整体循环移位的加密操作,需要了解其代码和原理

2.查表代换的一个解密代码

(1)先进行换表,再带入原代码

要逆向这种查表代换，你需要知道两件事情：

查找表 table：你需要拥有原始的查找表，这样才能知道每个字节是如何被映射的。
查找表的逆：你需要查找表的逆，这样你才能将加密后的字节映射回原始字节。

(2)换表的时候找到的规律,简单理解一下

查表代换（Table Substitution）的原理基于一个简单的概念：将数据的每个元素（通常是字节）映射到另一个元素。这种映射是通过一个查找表（Lookup Table，简称LUT）实现的，其中每个输入值对应一个输出值。在加密过程中，原始数据中的每个字节都被查找表中的相应字节替换。以下是查表代换的基本原理和步骤：

### 1. 查找表的构建
查找表是一个数组，其中包含输入值到输出值的映射。例如，一个简单的查找表可能如下所示：
```c
char table[] = {0x13, 0x45, 0x67, 0x89, /* ... */};
```
在这个表中，输入字节（例如，0x00）被映射到表中的第1个元素（0x13），输入字节0x01被映射到第2个元素（0x45），依此类推。

### 2. 加密过程
在加密过程中，原始数据中的每个字节都被查找表中的相应字节替换。例如，如果原始数据是`0x01, 0x02, 0x03, 0x04`，那么加密后的数据将是`table[0x01], table[0x02], table[0x03], table[0x04]`。

### 3. 逆向查找表的构建
为了解密数据，你需要构建查找表的逆。逆表是一个数组，其中每个元素指向原始表中该元素的位置。例如，如果`table[0x01] = 0x45`，那么`inv_table[0x45] = 0x01`。

### 4. 解密过程
在解密过程中，加密数据中的每个字节都被逆查找表中的相应字节替换。这样，每个字节都回到了它原始的值。

### 为什么需要逆向查找表
查表代换是一种单向操作，因为它直接将每个输入映射到一个输出，没有提供任何信息来直接从输出回到输入。逆向查找表提供了这种能力，因为它反转了原始查找表的映射关系。

### 数学原理
查表代换可以看作是一种特殊的函数，其中每个输入值都映射到一个唯一的输出值。逆向查找表是这个函数的逆函数，它将每个输出值映射回唯一的输入值。

### 安全性
查表代换的安全性取决于查找表的复杂性和大小。一个简单的查找表很容易被破解，因为它只提供了有限的映射。更复杂的查找表，如在高级加密算法中使用的S盒，可以提供更强的安全性。

总结来说，查表代换的原理是通过一个预定义的映射表来替换数据中的每个元素，而逆向查找表则提供了从加密数据回到原始数据的能力。这种技术在密码学、数据压缩和图像处理等领域有广泛应用。

二.[ACTF新生赛2020]Universe_final_answer 1

ida打开,提示输入1v5,之后发现关键函数sub_860,跟进

__int64 __fastcall main(int a1, char **a2, char **a3)
{__int64 v4; // [rsp+0h] [rbp-A8h] BYREFchar v5[104]; // [rsp+20h] [rbp-88h] BYREFunsigned __int64 v6; // [rsp+88h] [rbp-20h]v6 = __readfsqword(0x28u);__printf_chk(1LL, "Please give me the key string:", a3);scanf("%s", v5);if ( sub_860(v5) ){sub_C50(v5, &v4);__printf_chk(1LL, "Judgement pass! flag is actf{%s_%s}\n", v5);}else{puts("False key!");}return 0LL;
}

是和方程有关,我们用python的z3解方程

bool __fastcall sub_860(char *a1)
{int v1; // ecxint v2; // esiint v3; // edxint v4; // r9dint v5; // r11dint v6; // ebpint v7; // ebxint v8; // r8dint v9; // r10dbool result; // alint v11; // [rsp+0h] [rbp-38h]v1 = a1[1];v2 = *a1;v3 = a1[2];v4 = a1[3];v5 = a1[4];v6 = a1[6];v7 = a1[5];v8 = a1[7];v9 = a1[8];result = 0;if ( -85 * v9 + 58 * v8 + 97 * v6 + v7 + -45 * v5 + 84 * v4 + 95 * v2 - 20 * v1 + 12 * v3 == 12613 ){v11 = a1[9];if ( 30 * v11 + -70 * v9 + -122 * v6 + -81 * v7 + -66 * v5 + -115 * v4 + -41 * v3 + -86 * v1 - 15 * v2 - 30 * v8 == -54400&& -103 * v11 + 120 * v8 + 108 * v7 + 48 * v4 + -89 * v3 + 78 * v1 - 41 * v2 + 31 * v5 - (v6 << 6) - 120 * v9 == -10283&& 71 * v6 + (v7 << 7) + 99 * v5 + -111 * v3 + 85 * v1 + 79 * v2 - 30 * v4 - 119 * v8 + 48 * v9 - 16 * v11 == 22855&& 5 * v11 + 23 * v9 + 122 * v8 + -19 * v6 + 99 * v7 + -117 * v5 + -69 * v3 + 22 * v1 - 98 * v2 + 10 * v4 == -2944&& -54 * v11 + -23 * v8 + -82 * v3 + -85 * v2 + 124 * v1 - 11 * v4 - 8 * v5 - 60 * v7 + 95 * v6 + 100 * v9 == -2222&& -83 * v11 + -111 * v7 + -57 * v2 + 41 * v1 + 73 * v3 - 18 * v4 + 26 * v5 + 16 * v6 + 77 * v8 - 63 * v9 == -13258&& 81 * v11 + -48 * v9 + 66 * v8 + -104 * v6 + -121 * v7 + 95 * v5 + 85 * v4 + 60 * v3 + -85 * v2 + 80 * v1 == -1559&& 101 * v11 + -85 * v9 + 7 * v6 + 117 * v7 + -83 * v5 + -101 * v4 + 90 * v3 + -28 * v1 + 18 * v2 - v8 == 6308 ){return 99 * v11 + -28 * v9 + 5 * v8 + 93 * v6 + -18 * v7 + -127 * v5 + 6 * v4 + -9 * v3 + -93 * v1 + 58 * v2 == -1697;}}return result;
}

python脚本

from z3 import *s = Solver()# 假设 a1 是一个包含至少10个元素的列表
a1 = [Int(f'a1_{i}') for i in range(104)]  # 创建一个长度为104的列表，初始化为Int变量# 赋值操作
v1 = a1[1]
v2 = a1[0]
v3 = a1[2]
v4 = a1[3]
v5 = a1[4]
v6 = a1[6]
v7 = a1[5]
v8 = a1[7]
v9 = a1[8]
v11 = a1[9]# 添加约束
s.add(-85 * v9 + 58 * v8 + 97 * v6 + v7 - 45 * v5 + 84 * v4 + 95 * v2 - 20 * v1 + 12 * v3 == 12613)
s.add(30 * v11 - 70 * v9 - 122 * v6 - 81 * v7 - 66 * v5 - 115 * v4 - 41 * v3 - 86 * v1 - 15 * v2 - 30 * v8 == -54400)
s.add(71 * v6 + (v7 * 128) + 99 * v5 - 111 * v3 + 85 * v1 + 79 * v2 - 30 * v4 - 119 * v8 + 48 * v9 - 16 * v11 == 22855)
s.add(-103 * v11 + 120 * v8 + 108 * v7 + 48 * v4 - 89 * v3 + 78 * v1 - 41 * v2 + 31 * v5 - (v6 * 64) - 120 * v9 == -10283)
s.add(5 * v11 + 23 * v9 + 122 * v8 - 19 * v6 + 99 * v7 - 117 * v5 - 69 * v3 + 22 * v1 - 98 * v2 + 10 * v4 == -2944)
s.add(-54 * v11 - 23 * v8 - 82 * v3 - 85 * v2 + 124 * v1 - 11 * v4 - 8 * v5 - 60 * v7 + 95 * v6 + 100 * v9 == -2222)
s.add(-83 * v11 - 111 * v7 - 57 * v2 + 41 * v1 + 73 * v3 - 18 * v4 + 26 * v5 + 16 * v6 + 77 * v8 - 63 * v9 == -13258)
s.add(81 * v11 - 48 * v9 + 66 * v8 - 104 * v6 - 121 * v7 + 95 * v5 + 85 * v4 + 60 * v3 - 85 * v2 + 80 * v1 == -1559)
s.add(101 * v11 - 85 * v9 + 7 * v6 + 117 * v7 - 83 * v5 - 101 * v4 + 90 * v3 - 28 * v1 + 18 * v2 - v8 == 6308)
s.add(99 * v11 - 28 * v9 + 5 * v8 + 93 * v6 - 18 * v7 - 127 * v5 + 6 * v4 - 9 * v3 - 93 * v1 + 58 * v2 == -1697)# 检查是否有解
if s.check() == sat:m = s.model()for i in range(104):print(f"a1[{i}] =", m[a1[i]].as_long())
else:print("No solution found.")

得到答案