嗯，等式很简单，你说散列是通过以下公式完成的：

v5 = serial[6] + serial[0] - serial[7] - serial[2];
LOBYTE(v5) = serial[1];
v8 = serial[3] + v5 - serial[4];
if ( v8 != serial[5] )
    goto FAIL;

我们可以使用 SMT 求解器（例如 Z3）来找出这些方程的可能键：

$> python
Python 2.7.13 (default, Jan 19 2017, 14:48:08) 
[GCC 6.3.0 20170118] on linux2
Type "help", "copyright", "credits" or "license" for more information.
>>> from z3 import *
>>> serial0 = BitVec('serial0', 8)
>>> serial1 = BitVec('serial1', 8)
>>> serial2 = BitVec('serial2', 8)
>>> serial3 = BitVec('serial3', 8)
>>> serial4 = BitVec('serial4', 8)
>>> serial5 = BitVec('serial5', 8)
>>> serial6 = BitVec('serial6', 8)
>>> serial7 = BitVec('serial7', 8)
>>> v5 = BitVec('v5', 16)
>>> v8 = BitVec('v8', 16)
>>> v5 = ((serial6 + serial0 - serial7 - serial2) & 0xff00) + serial1
>>> v8 = serial3 + v5 - serial4
>>> s = Solver()
>>> s.add(v8 == serial5)
>>> s.check()
sat
>>> s.model()
[serial3 = 0, serial1 = 0, serial4 = 0, serial5 = 0]
>>> 
>>> s.add(serial1 != 0)
>>> s.check()
sat
>>> s.model()
[serial1 = 128, serial3 = 172, serial5 = 0, serial4 = 44]

因为，我得到了一个退化的解决方案，所以我添加了serial1必须不同于零的约束。事实上，您可以根据需要添加任何约束（如果您愿意，您可以尝试强制序列在标准的可打印 ASCII 字符内（请注意，它可能没有解决方案！）。

通过 perror 和我最初的假设对答案进行了扩展

提供的输入字符串“abcdefgh”的结果将导致“b+de = f”

为输入字符串 z3 提供约束确实返回

这里的字符“a”作为第一个可能的模型（）是 perror 在他的回答中发布的一个稍微修改过的 python 脚本

:\>cat z3t.py
from z3 import *
s0,s1,s2,s3,s4,s5,s6,s7 = BitVecs( 's0 s1 s2 s3 s4 s5 s6 s7', 8)
v5,v8 = BitVecs ('v5 v8', 16)
v5 = ((s6 + s0 - s7 - s2) & 0xff00) | s1
v8 = s3 + v5 - s4
s = Solver()
s.add(v8 == s5,s0 == ord('a'),s1 == ord('b'),s2 == ord('c'),s3 == ord('d'))
s.add(s4 == ord('e'), s5 > 0x60,s6 == ord('g'),s7 == ord('h'))
s.check()
print chr((s.model()[s5]).as_long())


:\>python .\z3t.py
a