z3 python z3.If всегда False (keygen)

Я хочу сгенерировать кейген на питоне с помощью z3. вот функция проверки:

def f(a):
    a = ord(a)
    if a <= 47 or a > 57:
        if a <= 64 or a > 98:
            exit()
        else:
            return a - 55
    else:
        return a - 48


def validate(key):
    if len(key) != 16:
        return False

    for k in key:
        if f(k)%2== 0:
            return False
    return True

Я пытался написать решатель для этого

from z3 import *
solver = Solver()

def f_z3(a):
    return If(
        Or(a<=47, a>57),
        If(
            Or(a<=64, a>98),
            False, #  exit()???
            a -55
        ),
        a -48
    )

key = IntVector("key", 16)
for k in key:
    solver.add(f_z3(k)%2==0)

solver.check()
print(solver.model())

и вот вывод

[key__1 = 48,
 key__10 = 48,
 key__9 = 48,
 key__15 = 48,
 key__6 = 48,
 key__8 = 48,
 key__4 = 48,
 key__0 = 48,
 key__14 = 48,
 key__11 = 48,
 key__7 = 48,
 key__5 = 48,
 key__2 = 48,
 key__12 = 48,
 key__13 = 48,
 key__3 = 48]

Который возвращает ключ «0000000000000000», но проверка («00000000000000000») возвращает False.

Я знаю, что проблема в функции f_z3, я не знаю, как выразить exit() внутри if, я всегда хочу что-то False. Но вместо этого я просто возвращаю False.

Любая идея, как решить эту проблему?


python reverse key-generator z3
person Nazime Lakehal    schedule 06.10.2018    source источник

Ответы (2)


arrow_upward
2
arrow_downward

Есть две проблемы с вашим кодом:

  1. Как вы заметили, замена exit на False неверна в функции f_z3. (Версия Python здесь просто странная, потому что в некоторых случаях она возвращает логическое значение, а в других просто умирает. Но это не относится к делу.) Во всех других ветвях вы возвращаете целое число, а в этом вы возвращаете логическое значение. В z3 вы всегда хотите возвращать один и тот же тип; целое число. Так что выберите что-то, что приведет к тому, что случай в конечном итоге даст False. Поскольку позже вы проверяете четность, подойдет любое нечетное число. Произнесите 1; поэтому измените его, чтобы при вызове exit производилось 1 вместо False.

  2. Пока вы проверяете, код Python возвращает False, если результат четный; так что вам нужно утверждать, что правильно. В настоящее время вы делаете solver.add(f_z3(k)%2==0), вместо этого вы должны потребовать, чтобы модуль был нечетным, например: solver.add(f_z3(k)%2!=0).

С этими двумя модификациями у вас будет следующий код:

from z3 import *
solver = Solver()

def f_z3(a):
    return If(
        Or(a<=47, a>57),
        If(
            Or(a<=64, a>98),
            1,
            a -55
        ),
        a -48
    )

key = IntVector("key", 16)
for k in key:
    solver.add(f_z3(k)%2!=0)

solver.check()
print(solver.model())

При запуске это производит:

[key__1 = 49,
 key__10 = 49,
 key__9 = 49,
 key__15 = 49,
 key__6 = 49,
 key__8 = 49,
 key__4 = 49,
 key__0 = 49,
 key__14 = 49,
 key__11 = 49,
 key__7 = 49,
 key__12 = 49,
 key__5 = 49,
 key__2 = 49,
 key__13 = 49,
 key__3 = 49]

который предлагает действительный ключ "1111111111111111".

person alias    schedule 06.10.2018

arrow_upward
0
arrow_downward

Второй пункт я не заметил, в первом я был более сконцентрирован. возврат 1 не решает мои грехи проблемы, я просто упростил реальную проблему с помощью меньшего примера. Я хочу общее решение для этого шаблона.

def f(x):
   if condition(x):
       exit()
   else:
       return g(x) # return something in relation with x

Я нашел этот шаблон, который работает сейчас

def f_z3(x):
    global solver
    solver.add(Not(condition(x))
    return g(x)

Так что моя первая функция будет что-то вроде

def f_z3(a):
    global solver
    # sins we have two nested condition we have to add an And
    solver.add(
        Not(
            And(
                Or(a<=47, a>57),
                Or(a<=64, a>98)
            )
        )
    )
    return If(
        Or(a<=47, a>57),
        a-55,
        a - 48
    )

Я все еще ищу лучший подход для решения такого рода шаблонов, что-то, что говорит условию If всегда False.

person Nazime Lakehal    schedule 07.10.2018
comment
Похоже, у вас есть «предварительные условия», когда функция f может быть вызвана. Это предполагает, что бремя обеспечения соблюдения этого лежит на вызывающем абоненте; поэтому ограничение должно перейти к вызывающей стороне. - person alias; 07.10.2018