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
| from z3 import *
num=[BitVec("num[%d]"%i,8) for i in range(13)]
solver=Solver()
solver.add(num[0] + 52296 + num[1] - 26211 + num[2] - 11754 + (num[3] ^ 41236)
+ num[4] * 63747 + num[5] - 52714 + num[6] - 10512 + num[7] * 12972 + num[8] +
45505 + num[9] - 21713 + num[10] - 59122 + num[11] - 12840 + (num[12] ^ 21087)
== 12702282 )
solver.add( num[0] - 25228 + (num[1] ^ 20699) + (num[2] ^ 8158) + num[3] -
65307 + num[4] * 30701 + num[5] * 47555 + num[6] - 2557 + (num[7] ^ 49055) +
num[8] - 7992 + (num[9] ^ 57465) + (num[10] ^ 57426) + num[11] + 13299 +
num[12] - 50966 == 9946829 )
solver.add( num[0] - 64801 + num[1] - 60698 + num[2] - 40853 + num[3] - 54907
+ num[4] + 29882 + (num[5] ^ 13574) + (num[6] ^ 21310) + num[7] + 47366 +
num[8] + 41784 + (num[9] ^ 53690) + num[10] * 58436 + num[11] * 15590 +
num[12] + 58225 == 2372055 )
solver.add( num[0] + 61538 + num[1] - 17121 + num[2] - 58124 + num[3] + 8186 +
num[4] + 21253 + num[5] - 38524 + num[6] - 48323 + num[7] - 20556 + num[8] *
56056 + num[9] + 18568 + num[10] + 12995 + (num[11] ^ 39260) + num[12] + 25329
== 6732474 )
solver.add( num[0] - 42567 + num[1] - 17743 + num[2] * 47827 + num[3] - 10246
+ (num[4] ^ 16284) + num[5] + 39390 + num[6] * 11803 + num[7] * 60332 +
(num[8] ^ 18491) + (num[9] ^ 4795) + num[10] - 25636 + num[11] - 16780 +
num[12] - 62345 == 14020739 )
solver.add( num[0] - 10968 + num[1] - 31780 + (num[2] ^ 31857) + num[3] - 61983
+ num[4] * 31048 + num[5] * 20189 + num[6] + 12337 + num[7] * 25945 + (num[8]
^ 7064) + num[9] - 25369 + num[10] - 54893 + num[11] * 59949 + (num[12] ^
12441) == 14434062 )
solver.add( num[0] + 16689 + num[1] - 10279 + num[2] - 32918 + num[3] - 57155
+ num[4] * 26571 + num[5] * 15086 + (num[6] ^ 22986) + (num[7] ^ 23349) +
(num[8] ^ 16381) + (num[9] ^ 23173) + num[10] - 40224 + num[11] + 31751 +
num[12] * 8421 == 7433598 )
solver.add( num[0] + 28740 + num[1] - 64696 + num[2] + 60470 + num[3] - 14752
+ (num[4] ^ 1287) + (num[5] ^ 35272) + num[6] + 49467 + num[7] - 33788 +
num[8] + 20606 + (num[9] ^ 44874) + num[10] * 19764 + num[11] + 48342 +
num[12] * 56511 == 7989404 )
solver.add( (num[0] ^ 28978) + num[1] + 23120 + num[2] + 22802 + num[3] * 31533
+ (num[4] ^ 39287) + num[5] - 48576 + (num[6] ^ 28542) + num[7] - 43265 +
num[8] + 22365 + num[9] + 61108 + num[10] * 2823 + num[11] - 30343 + num[12] +
14780 == 3504803 )
solver.add( num[0] * 22466 + (num[1] ^ 55999) + num[2] - 53658 + (num[3] ^
47160) + (num[4] ^ 12511) + num[5] * 59807 + num[6] + 46242 + num[7] + 3052 +
(num[8] ^ 25279) + num[9] + 30202 + num[10] * 22698 + num[11] + 33480 +
(num[12] ^ 16757) == 11003580 )
solver.add( num[0] * 57492 + (num[1] ^ 13421) + num[2] - 13941 + (num[3] ^
48092) + num[4] * 38310 + num[5] + 9884 + num[6] - 45500 + num[7] - 19233 +
num[8] + 58274 + num[9] + 36175 + (num[10] ^ 18568) + num[11] * 49694 +
(num[12] ^ 9473) == 25546210 )
solver.add( num[0] - 23355 + num[1] * 50164 + (num[2] ^ 34618) + num[3] + 52703
+ num[4] + 36245 + num[5] * 46648 + (num[6] ^ 4858) + (num[7] ^ 41846) +
num[8] * 27122 + (num[9] ^ 42058) + num[10] * 15676 + num[11] - 31863 +
num[12] + 62510 == 11333836 )
solver.add( num[0] * 30523 + (num[1] ^ 7990) + num[2] + 39058 + num[3] * 57549
+ (num[4] ^ 53440) + num[5] * 4275 + num[6] - 48863 + (num[7] ^ 55436) +
(num[8] ^ 2624) + (num[9] ^ 13652) + num[10] + 62231 + num[11] + 19456 +
num[12] - 13195 == 13863722)
enc =[132,47,180,7,216,45,68,6,39,246,124,2,243,137,58,172,53,200,99,91,83,13,171
,80,108,235,179,58,176,28,216,36,11,80,39,162,97,58,236,130,123,176,24,212,56,89,72]
solver.add(num[0]^enc[0]==ord('h'))
solver.add(num[1]^enc[1]==ord('g'))
solver.add(num[2]^enc[2]==ord('a'))
solver.add(num[3]^enc[3]==ord('m'))
solver.add(num[4]^enc[4]==ord('e'))
print(solver.check())
for i in num:
print(solver.model()[i],end=",")
key=[236,72,213,106,189,86,62,53,120,199,15,93,133]
for i in range(len(enc)):
print(chr(enc[i]^key[i%len(key)]),end='')
|
