羊城杯202009re部分題解
阿新 • • 發佈:2020-09-14
login
pyinstaller 打包的exe檔案,反編譯為.py檔案,具體做法可以參考我的另一篇文章。pyinstaller打包的exe檔案反編譯為.py檔案
.py檔案原始碼:
# uncompyle6 version 3.7.3 # Python bytecode 3.7 (3394) # Decompiled from: Python 3.8.5 (tags/v3.8.5:580fbb0, Jul 20 2020, 15:57:54) [MSC v.1924 64 bit (AMD64)] # Embedded file name: login.py # Compiled at: 1995-09-28 00:18:56 # Size of source mod 2**32: 257 bytes import sys input1 = input('input something:') if len(input1) != 14: print('Wrong length!') sys.exit() else: code = [] for i in range(13): code.append(ord(input1[i]) ^ ord(input1[(i + 1)])) code.append(ord(input1[13])) a1 = code[2] a2 = code[1] a3 = code[0] a4 = code[3] a5 = code[4] a6 = code[5] a7 = code[6] a8 = code[7] a9 = code[9] a10 = code[8] a11 = code[10] a12 = code[11] a13 = code[12] a14 = code[13] if (a1 * 88 + a2 * 67 + a3 * 65 - a4 * 5 + a5 * 43 + a6 * 89 + a7 * 25 + a8 * 13 - a9 * 36 + a10 * 15 + a11 * 11 + a12 * 47 - a13 * 60 + a14 * 29 == 22748) & (a1 * 89 + a2 * 7 + a3 * 12 - a4 * 25 + a5 * 41 + a6 * 23 + a7 * 20 - a8 * 66 + a9 * 31 + a10 * 8 + a11 * 2 - a12 * 41 - a13 * 39 + a14 * 17 == 7258) & (a1 * 28 + a2 * 35 + a3 * 16 - a4 * 65 + a5 * 53 + a6 * 39 + a7 * 27 + a8 * 15 - a9 * 33 + a10 * 13 + a11 * 101 + a12 * 90 - a13 * 34 + a14 * 23 == 26190) & (a1 * 23 + a2 * 34 + a3 * 35 - a4 * 59 + a5 * 49 + a6 * 81 + a7 * 25 + (a8 << 7) - a9 * 32 + a10 * 75 + a11 * 81 + a12 * 47 - a13 * 60 + a14 * 29 == 37136) & (a1 * 38 + a2 * 97 + a3 * 35 - a4 * 52 + a5 * 42 + a6 * 79 + a7 * 90 + a8 * 23 - a9 * 36 + a10 * 57 + a11 * 81 + a12 * 42 - a13 * 62 - a14 * 11 == 27915) & (a1 * 22 + a2 * 27 + a3 * 35 - a4 * 45 + a5 * 47 + a6 * 49 + a7 * 29 + a8 * 18 - a9 * 26 + a10 * 35 + a11 * 41 + a12 * 40 - a13 * 61 + a14 * 28 == 17298) & (a1 * 12 + a2 * 45 + a3 * 35 - a4 * 9 - a5 * 42 + a6 * 86 + a7 * 23 + a8 * 85 - a9 * 47 + a10 * 34 + a11 * 76 + a12 * 43 - a13 * 44 + a14 * 65 == 19875) & (a1 * 79 + a2 * 62 + a3 * 35 - a4 * 85 + a5 * 33 + a6 * 79 + a7 * 86 + a8 * 14 - a9 * 30 + a10 * 25 + a11 * 11 + a12 * 57 - a13 * 50 - a14 * 9 == 22784) & (a1 * 8 + a2 * 6 + a3 * 64 - a4 * 85 + a5 * 73 + a6 * 29 + a7 * 2 + a8 * 23 - a9 * 36 + a10 * 5 + a11 * 2 + a12 * 47 - a13 * 64 + a14 * 27 == 9710) & (a1 * 67 - a2 * 68 + a3 * 68 - a4 * 51 - a5 * 43 + a6 * 81 + a7 * 22 - a8 * 12 - a9 * 38 + a10 * 75 + a11 * 41 + a12 * 27 - a13 * 52 + a14 * 31 == 13376) & (a1 * 85 + a2 * 63 + a3 * 5 - a4 * 51 + a5 * 44 + a6 * 36 + a7 * 28 + a8 * 15 - a9 * 6 + a10 * 45 + a11 * 31 + a12 * 7 - a13 * 67 + a14 * 78 == 24065) & (a1 * 47 + a2 * 64 + a3 * 66 - a4 * 5 + a5 * 43 + a6 * 112 + a7 * 25 + a8 * 13 - a9 * 35 + a10 * 95 + a11 * 21 + a12 * 43 - a13 * 61 + a14 * 20 == 27687) & (a1 * 89 + a2 * 67 + a3 * 85 - a4 * 25 + a5 * 49 + a6 * 89 + a7 * 23 + a8 * 56 - a9 * 92 + a10 * 14 + a11 * 89 + a12 * 47 - a13 * 61 - a14 * 29 == 29250) & (a1 * 95 + a2 * 34 + a3 * 62 - a4 * 9 - a5 * 43 + a6 * 83 + a7 * 25 + a8 * 12 - a9 * 36 + a10 * 16 + a11 * 51 + a12 * 47 - a13 * 60 - a14 * 24 == 15317): print('flag is GWHT{md5(your_input)}') print('Congratulations and have fun!') else: print('Sorry,plz try again...')
寫指令碼時需要用到z3這個工具,可以參考Z3Py在CTF逆向中的運用
from z3 import * import hashlib a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14 = BitVecs('a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14', 7) solve(a1 * 88 + a2 * 67 + a3 * 65 - a4 * 5 + a5 * 43 + a6 * 89 + a7 * 25 + a8 * 13 - a9 * 36 + a10 * 15 + a11 * 11 + a12 * 47 - a13 * 60 + a14 * 29 == 22748 , a1 * 89 + a2 * 7 + a3 * 12 - a4 * 25 + a5 * 41 + a6 * 23 + a7 * 20 - a8 * 66 + a9 * 31 + a10 * 8 + a11 * 2 - a12 * 41 - a13 * 39 + a14 * 17 == 7258 , a1 * 28 + a2 * 35 + a3 * 16 - a4 * 65 + a5 * 53 + a6 * 39 + a7 * 27 + a8 * 15 - a9 * 33 + a10 * 13 + a11 * 101 + a12 * 90 - a13 * 34 + a14 * 23 == 26190 , a1 * 23 + a2 * 34 + a3 * 35 - a4 * 59 + a5 * 49 + a6 * 81 + a7 * 25 + (a8 << 7) - a9 * 32 + a10 * 75 + a11 * 81 + a12 * 47 - a13 * 60 + a14 * 29 == 37136 , a1 * 38 + a2 * 97 + a3 * 35 - a4 * 52 + a5 * 42 + a6 * 79 + a7 * 90 + a8 * 23 - a9 * 36 + a10 * 57 + a11 * 81 + a12 * 42 - a13 * 62 - a14 * 11 == 27915 , a1 * 22 + a2 * 27 + a3 * 35 - a4 * 45 + a5 * 47 + a6 * 49 + a7 * 29 + a8 * 18 - a9 * 26 + a10 * 35 + a11 * 41 + a12 * 40 - a13 * 61 + a14 * 28 == 17298 , a1 * 12 + a2 * 45 + a3 * 35 - a4 * 9 - a5 * 42 + a6 * 86 + a7 * 23 + a8 * 85 - a9 * 47 + a10 * 34 + a11 * 76 + a12 * 43 - a13 * 44 + a14 * 65 == 19875 , a1 * 79 + a2 * 62 + a3 * 35 - a4 * 85 + a5 * 33 + a6 * 79 + a7 * 86 + a8 * 14 - a9 * 30 + a10 * 25 + a11 * 11 + a12 * 57 - a13 * 50 - a14 * 9 == 22784 , a1 * 8 + a2 * 6 + a3 * 64 - a4 * 85 + a5 * 73 + a6 * 29 + a7 * 2 + a8 * 23 - a9 * 36 + a10 * 5 + a11 * 2 + a12 * 47 - a13 * 64 + a14 * 27 == 9710 , a1 * 67 - a2 * 68 + a3 * 68 - a4 * 51 - a5 * 43 + a6 * 81 + a7 * 22 - a8 * 12 - a9 * 38 + a10 * 75 + a11 * 41 + a12 * 27 - a13 * 52 + a14 * 31 == 13376 , a1 * 85 + a2 * 63 + a3 * 5 - a4 * 51 + a5 * 44 + a6 * 36 + a7 * 28 + a8 * 15 - a9 * 6 + a10 * 45 + a11 * 31 + a12 * 7 - a13 * 67 + a14 * 78 == 24065 , a1 * 47 + a2 * 64 + a3 * 66 - a4 * 5 + a5 * 43 + a6 * 112 + a7 * 25 + a8 * 13 - a9 * 35 + a10 * 95 + a11 * 21 + a12 * 43 - a13 * 61 + a14 * 20 == 27687 , a1 * 89 + a2 * 67 + a3 * 85 - a4 * 25 + a5 * 49 + a6 * 89 + a7 * 23 + a8 * 56 - a9 * 92 + a10 * 14 + a11 * 89 + a12 * 47 - a13 * 61 - a14 * 29 == 29250 , a1 * 95 + a2 * 34 + a3 * 62 - a4 * 9 - a5 * 43 + a6 * 83 + a7 * 25 + a8 * 12 - a9 * 36 + a10 * 16 + a11 * 51 + a12 * 47 - a13 * 60 - a14 * 24 == 15317) A = [10,24,119,7,104,43,28,91,108,52,88,74,88,33] i = 12 while i >= 0: A[i] ^= A[i+1] i -= 1 for i in A: print(chr(i), end = '') a = b'U_G07_th3_k3y!' print(hashlib.md5(a).hexdigest())
需要注意的是,約束條件存在位移操作,所以不能用Int方法建立未知量,而是用BitVecs
方法,新增約束條件用solve
方法
附件下載 提取碼:k4n4
Bytecode
python位元組碼反彙編生成的虛擬碼,
4 0 LOAD_CONST 0 (3) 3 LOAD_CONST 1 (37) 6 LOAD_CONST 2 (72) 9 LOAD_CONST 3 (9) 12 LOAD_CONST 4 (6) 15 LOAD_CONST 5 (132) 18 BUILD_LIST 6 21 STORE_NAME 0 (en) 5 24 LOAD_CONST 6 (101) 27 LOAD_CONST 7 (96) 30 LOAD_CONST 8 (23) 33 LOAD_CONST 9 (68) 36 LOAD_CONST 10 (112) 39 LOAD_CONST 11 (42) 42 LOAD_CONST 12 (107) 45 LOAD_CONST 13 (62) 48 LOAD_CONST 7 (96) 51 LOAD_CONST 14 (53) 54 LOAD_CONST 15 (176) 57 LOAD_CONST 16 (179) 60 LOAD_CONST 17 (98) 63 LOAD_CONST 14 (53) 66 LOAD_CONST 18 (67) 69 LOAD_CONST 19 (29) 72 LOAD_CONST 20 (41) 75 LOAD_CONST 21 (120) 78 LOAD_CONST 22 (60) 81 LOAD_CONST 23 (106) 84 LOAD_CONST 24 (51) 87 LOAD_CONST 6 (101) 90 LOAD_CONST 25 (178) 93 LOAD_CONST 26 (189) 96 LOAD_CONST 6 (101) 99 LOAD_CONST 27 (48) 102 BUILD_LIST 26 105 STORE_NAME 1 (output) 7 108 LOAD_CONST 28 ('welcome to GWHT2020') 111 PRINT_ITEM 112 PRINT_NEWLINE 9 113 LOAD_NAME 2 (raw_input) 116 LOAD_CONST 29 ('please input your flag:') 119 CALL_FUNCTION 1 122 STORE_NAME 3 (flag) 10 125 LOAD_NAME 3 (flag) 128 STORE_NAME 4 (str) 12 131 LOAD_NAME 5 (len) 134 LOAD_NAME 4 (str) 137 CALL_FUNCTION 1 140 STORE_NAME 6 (a) 13 143 LOAD_NAME 6 (a) 146 LOAD_CONST 30 (38) 149 COMPARE_OP 0 (<) 152 POP_JUMP_IF_FALSE 173 14 155 LOAD_CONST 31 ('lenth wrong!') 158 PRINT_ITEM 159 PRINT_NEWLINE 15 160 LOAD_NAME 7 (exit) 163 LOAD_CONST 32 (0) 166 CALL_FUNCTION 1 169 POP_TOP 170 JUMP_FORWARD 0 (to 173) 17 >> 173 LOAD_NAME 8 (ord) 176 LOAD_NAME 4 (str) 179 LOAD_CONST 32 (0) 182 BINARY_SUBSCR 183 CALL_FUNCTION 1 186 LOAD_CONST 33 (2020) 189 BINARY_MULTIPLY 190 LOAD_NAME 8 (ord) 193 LOAD_NAME 4 (str) 196 LOAD_CONST 34 (1) 199 BINARY_SUBSCR 200 CALL_FUNCTION 1 203 BINARY_ADD 204 LOAD_CONST 33 (2020) 207 BINARY_MULTIPLY 208 LOAD_NAME 8 (ord) 211 LOAD_NAME 4 (str) 214 LOAD_CONST 35 (2) 217 BINARY_SUBSCR 218 CALL_FUNCTION 1 221 BINARY_ADD 222 LOAD_CONST 33 (2020) 225 BINARY_MULTIPLY 226 LOAD_NAME 8 (ord) 229 LOAD_NAME 4 (str) 232 LOAD_CONST 0 (3) 235 BINARY_SUBSCR 236 CALL_FUNCTION 1 239 BINARY_ADD 240 LOAD_CONST 33 (2020) 243 BINARY_MULTIPLY 244 LOAD_NAME 8 (ord) 247 LOAD_NAME 4 (str) 250 LOAD_CONST 36 (4) 253 BINARY_SUBSCR 254 CALL_FUNCTION 1 257 BINARY_ADD 258 LOAD_CONST 37 (1182843538814603) 261 COMPARE_OP 2 (==) 264 POP_JUMP_IF_FALSE 275 18 267 LOAD_CONST 38 ('good!continue\xe2\x80\xa6\xe2\x80\xa6') 270 PRINT_ITEM 271 PRINT_NEWLINE 272 JUMP_FORWARD 15 (to 290) 20 >> 275 LOAD_CONST 39 ('bye~') 278 PRINT_ITEM 279 PRINT_NEWLINE 21 280 LOAD_NAME 7 (exit) 283 LOAD_CONST 32 (0) 286 CALL_FUNCTION 1 289 POP_TOP 23 >> 290 BUILD_LIST 0 293 STORE_NAME 9 (x) 24 296 LOAD_CONST 40 (5) 299 STORE_NAME 10 (k) 25 302 SETUP_LOOP 128 (to 433) 305 LOAD_NAME 11 (range) 308 LOAD_CONST 41 (13) 311 CALL_FUNCTION 1 314 GET_ITER >> 315 FOR_ITER 114 (to 432) 318 STORE_NAME 12 (i) 26 321 LOAD_NAME 8 (ord) 324 LOAD_NAME 4 (str) 327 LOAD_NAME 10 (k) 330 BINARY_SUBSCR 331 CALL_FUNCTION 1 334 STORE_NAME 13 (b) 27 337 LOAD_NAME 8 (ord) 340 LOAD_NAME 4 (str) 343 LOAD_NAME 10 (k) 346 LOAD_CONST 34 (1) 349 BINARY_ADD 350 BINARY_SUBSCR 351 CALL_FUNCTION 1 354 STORE_NAME 14 (c) 28 357 LOAD_NAME 14 (c) 360 LOAD_NAME 0 (en) 363 LOAD_NAME 12 (i) 366 LOAD_CONST 4 (6) 369 BINARY_MODULO 370 BINARY_SUBSCR 371 BINARY_XOR 372 STORE_NAME 15 (a11) 29 375 LOAD_NAME 13 (b) 378 LOAD_NAME 0 (en) 381 LOAD_NAME 12 (i) 384 LOAD_CONST 4 (6) 387 BINARY_MODULO 388 BINARY_SUBSCR 389 BINARY_XOR 390 STORE_NAME 16 (a22) 30 393 LOAD_NAME 9 (x) 396 LOAD_ATTR 17 (append) 399 LOAD_NAME 15 (a11) 402 CALL_FUNCTION 1 405 POP_TOP 31 406 LOAD_NAME 9 (x) 409 LOAD_ATTR 17 (append) 412 LOAD_NAME 16 (a22) 415 CALL_FUNCTION 1 418 POP_TOP 32 419 LOAD_NAME 10 (k) 422 LOAD_CONST 35 (2) 425 INPLACE_ADD 426 STORE_NAME 10 (k) 429 JUMP_ABSOLUTE 315 >> 432 POP_BLOCK 33 >> 433 LOAD_NAME 9 (x) 436 LOAD_NAME 1 (output) 439 COMPARE_OP 2 (==) 442 POP_JUMP_IF_FALSE 453 34 445 LOAD_CONST 38 ('good!continue\xe2\x80\xa6\xe2\x80\xa6') 448 PRINT_ITEM 449 PRINT_NEWLINE 450 JUMP_FORWARD 15 (to 468) 36 >> 453 LOAD_CONST 42 ('oh,you are wrong!') 456 PRINT_ITEM 457 PRINT_NEWLINE 37 458 LOAD_NAME 7 (exit) 461 LOAD_CONST 32 (0) 464 CALL_FUNCTION 1 467 POP_TOP 39 >> 468 LOAD_NAME 5 (len) 471 LOAD_NAME 4 (str) 474 CALL_FUNCTION 1 477 STORE_NAME 18 (l) 40 480 LOAD_NAME 8 (ord) 483 LOAD_NAME 4 (str) 486 LOAD_NAME 18 (l) 489 LOAD_CONST 43 (7) 492 BINARY_SUBTRACT 493 BINARY_SUBSCR 494 CALL_FUNCTION 1 497 STORE_NAME 19 (a1) 41 500 LOAD_NAME 8 (ord) 503 LOAD_NAME 4 (str) 506 LOAD_NAME 18 (l) 509 LOAD_CONST 4 (6) 512 BINARY_SUBTRACT 513 BINARY_SUBSCR 514 CALL_FUNCTION 1 517 STORE_NAME 20 (a2) 42 520 LOAD_NAME 8 (ord) 523 LOAD_NAME 4 (str) 526 LOAD_NAME 18 (l) 529 LOAD_CONST 40 (5) 532 BINARY_SUBTRACT 533 BINARY_SUBSCR 534 CALL_FUNCTION 1 537 STORE_NAME 21 (a3) 43 540 LOAD_NAME 8 (ord) 543 LOAD_NAME 4 (str) 546 LOAD_NAME 18 (l) 549 LOAD_CONST 36 (4) 552 BINARY_SUBTRACT 553 BINARY_SUBSCR 554 CALL_FUNCTION 1 557 STORE_NAME 22 (a4) 44 560 LOAD_NAME 8 (ord) 563 LOAD_NAME 4 (str) 566 LOAD_NAME 18 (l) 569 LOAD_CONST 0 (3) 572 BINARY_SUBTRACT 573 BINARY_SUBSCR 574 CALL_FUNCTION 1 577 STORE_NAME 23 (a5) 45 580 LOAD_NAME 8 (ord) 583 LOAD_NAME 4 (str) 586 LOAD_NAME 18 (l) 589 LOAD_CONST 35 (2) 592 BINARY_SUBTRACT 593 BINARY_SUBSCR 594 CALL_FUNCTION 1 597 STORE_NAME 24 (a6) 46 600 LOAD_NAME 19 (a1) 603 LOAD_CONST 0 (3) 606 BINARY_MULTIPLY 607 LOAD_NAME 20 (a2) 610 LOAD_CONST 35 (2) 613 BINARY_MULTIPLY 614 BINARY_ADD 615 LOAD_NAME 21 (a3) 618 LOAD_CONST 40 (5) 621 BINARY_MULTIPLY 622 BINARY_ADD 623 LOAD_CONST 44 (1003) 626 COMPARE_OP 2 (==) 629 POP_JUMP_IF_FALSE 807 47 632 LOAD_NAME 19 (a1) 635 LOAD_CONST 36 (4) 638 BINARY_MULTIPLY 639 LOAD_NAME 20 (a2) 642 LOAD_CONST 43 (7) 645 BINARY_MULTIPLY 646 BINARY_ADD 647 LOAD_NAME 21 (a3) 650 LOAD_CONST 3 (9) 653 BINARY_MULTIPLY 654 BINARY_ADD 655 LOAD_CONST 45 (2013) 658 COMPARE_OP 2 (==) 661 POP_JUMP_IF_FALSE 807 48 664 LOAD_NAME 19 (a1) 667 LOAD_NAME 20 (a2) 670 LOAD_CONST 46 (8) 673 BINARY_MULTIPLY 674 BINARY_ADD 675 LOAD_NAME 21 (a3) 678 LOAD_CONST 35 (2) 681 BINARY_MULTIPLY 682 BINARY_ADD 683 LOAD_CONST 47 (1109) 686 COMPARE_OP 2 (==) 689 POP_JUMP_IF_FALSE 804 49 692 LOAD_NAME 22 (a4) 695 LOAD_CONST 0 (3) 698 BINARY_MULTIPLY 699 LOAD_NAME 23 (a5) 702 LOAD_CONST 35 (2) 705 BINARY_MULTIPLY 706 BINARY_ADD 707 LOAD_NAME 24 (a6) 710 LOAD_CONST 40 (5) 713 BINARY_MULTIPLY 714 BINARY_ADD 715 LOAD_CONST 48 (671) 718 COMPARE_OP 2 (==) 721 POP_JUMP_IF_FALSE 801 50 724 LOAD_NAME 22 (a4) 727 LOAD_CONST 36 (4) 730 BINARY_MULTIPLY 731 LOAD_NAME 23 (a5) 734 LOAD_CONST 43 (7) 737 BINARY_MULTIPLY 738 BINARY_ADD 739 LOAD_NAME 24 (a6) 742 LOAD_CONST 3 (9) 745 BINARY_MULTIPLY 746 BINARY_ADD 747 LOAD_CONST 49 (1252) 750 COMPARE_OP 2 (==) 753 POP_JUMP_IF_FALSE 798 51 756 LOAD_NAME 22 (a4) 759 LOAD_NAME 23 (a5) 762 LOAD_CONST 46 (8) 765 BINARY_MULTIPLY 766 BINARY_ADD 767 LOAD_NAME 24 (a6) 770 LOAD_CONST 35 (2) 773 BINARY_MULTIPLY 774 BINARY_ADD 775 LOAD_CONST 50 (644) 778 COMPARE_OP 2 (==) 781 POP_JUMP_IF_FALSE 795 52 784 LOAD_CONST 51 ('congraduation!you get the right flag!') 787 PRINT_ITEM 788 PRINT_NEWLINE 789 JUMP_ABSOLUTE 795 792 JUMP_ABSOLUTE 798 >> 795 JUMP_ABSOLUTE 801 >> 798 JUMP_ABSOLUTE 804 >> 801 JUMP_ABSOLUTE 807 >> 804 JUMP_FORWARD 0 (to 807) >> 807 LOAD_CONST 52 (None) 810 RETURN_VALUE
還原後的原始碼邏輯大概如下(dis模組可檢視python位元組碼反彙編虛擬碼,方便與題目校對):
import dis
def main():
en = [3, 37, 72, 9, 6, 132]
output = [101, 96, 23,68,112,42,107,62,96,53,176,179,98,53,67,29,41,120,60,106,51,101,178,189,101,48]
print('welcome to GWHT2020')
flag = input('please input your flag:')
str = flag
a = len(str)
if a < 38:
print('lenth wrong')
exit(0)
else:
if (((ord(str[0]) * 2020 + ord(str[1])) * 2020 + ord(str[2]))*2020 + ord(str[3])) * 2020 + ord(str[4]) == 1182843538814603:
print('good!continue\xe2\x80\xa6\xe2\x80\xa6')
else:
print('bye~')
exit(0)
x = []
k = 5
for i in range(13):
b = ord(str[k])
c = ord(str[k+1])
a11 = c ^ en[i%6]
a22 = b ^ en[i%6]
x.append(a11)
x.append(a22)
k = k + 2
if x == output:
print('good!continue\xe2\x80\xa6\xe2\x80\xa6')
else:
print('oh,you are wrong!')
exit(0)
l = len(str)
a1 = ord(str[l-7])
a2 = ord(str[l-6])
a3 = ord(str[l-5])
a4 = ord(str[l-4])
a5 = ord(str[l-3])
a6 = ord(str[l-2])
if a1 * 3 + a2 * 2 + a3 * 5 == 1003:
pass
else:
print('wrong')
if a1 * 4 + a2 * 7 + a3 * 9 == 2013:
pass
else:
print('wrong')
if a1 + a2 * 8 + a3 * 2 == 1109:
pass
else:
print('wrong')
if a4 * 3 + a5 * 2 + a6 * 5 == 671:
pass
else:
print('wrong')
if a4 * 4 + a5 * 7 + a6 * 9 == 1252:
pass
else:
print('wrong')
if a4 + a5 * 8 + a6 * 2 == 644:
print('congratulations!')
else:
print('wrong')
print(dis.dis(main))
main()
指令碼如下:
from z3 import *
a1 = Int('a1')
a2 = Int('a2')
a3 = Int('a3')
a4 = Int('a4')
a5 = Int('a5')
a6 = Int('a6')
s = Solver()
s.add(a1 * 3 + a2 * 2 + a3 * 5 == 1003)
s.add(a1 * 4 + a2 * 7 + a3 * 9 == 2013)
s.add(a1 + a2 * 8 + a3 * 2 == 1109)
s.add(a4 * 3 + a5 * 2 + a6 * 5 == 671)
s.add(a4 * 4 + a5 * 7 + a6 * 9 == 1252)
s.add(a4 + a5 * 8 + a6 * 2 == 644)
print(s.check())
m = s.model()
print ("traversing model...")
for d in m.decls():
print("{} = {}".format(d.name(), (m[d])))
a = [55,101,51,102,102,97]
for i in a:
print(chr(i))
a5 = 55
a2 = 101
a6 = 51
a3 = 102
a4 = 102
a1 = 97
for i in range(32,128):
for j in range(32,128):
for k in range(32,128):
for l in range(32,128):
for m in range(32,128):
if (((i * 2020 + j) * 2020 + k)*2020 + l) * 2020 + m == 1182843538814603:
print(i ,' ',j,' ',k,' ',l,' ',m)
exit(0)
# 第6~31個字元
output = [101, 96, 23,68,112,42,107,62,96,53,176,179,98,53,67,29,41,120,60,106,51,101,178,189,101,48]
k = 0
out_put = []
en = [3, 37, 72, 9, 6, 132]
for i in range(13):
out_put.append(output[k+1] ^ en[i%6])
out_put.append(output[k] ^ en[i%6])
k += 2
a = 'GWHT{'
flag = []
for i in a:
flag.append(ord(i))
for i in out_put:
flag.append(i)
flag.append(a1)
flag.append(a2)
flag.append(a3)
flag.append(a4)
flag.append(a5)
flag.append(a6)
for i in flag:
print(chr(i), end= '')
print('}')