something fishy here in px1kcr-clarify.py

[themaddoctor]

If I remove these lines:

    if not s.solution(plaintext.get_byte(curChar), vp.get_byte(curChar), extra_constraints=[key == vk, ciphertext==ct]):
        print()
        IPython.embed()

then the program never finishes. It appears that the expected solution is built into the attack.

[stef]

it might be related to this bug: angr/claripy#241 (comment)

[themaddoctor]

But if we only remove "IPython.embed()", and replace ONLY the ct with the test ct, it also does not finish.

[stef]

it would be interesting to see how all those asserts work with a solver that has not seen any asserts before. so making a copy of the solver before the solution() and throw it away afterwards... it might be indeed that z3 somehow uses the extra constraints from the asserts to keep some internal state, which it should not...

[stef]

or alternatively use asserts with known good testvectors, do the final solve with an unrelated target vector.

[stef]

i'll try that. i'm afraid you are right that somehow the "the expected solution is built into the attack" by leaking through the asserts.

[themaddoctor]

I will stay tuned.
Thanks for your attention.

[stef]

hmm, it seems that if i solve for a different ciphertext (using a different key as well) while having the asserts for the original ciphertext/key in there the code in line 318:

sol = s.eval(key, 1, extra_constraints=[ciphertext == ct_test])

indeed times out, and thus it seems invalidates my attack.

what is strange though, is that (this was a few years ago) i seem to remember actually testing the attack by first building the model (which takes ~50 sec) and then feeding it different ciphertexts and it solved them each in about 4 sec while reusing the model. maybe my memory plays games with me, but until i can recover exactly how and why that worked back then, i guess i have to say that the attack is broken. :/

[stef]

however painful the (hopefully temporary) result, thank you for your feedback and your interest in all this, it is much appreciated.

[themaddoctor]

I am truly bummed. I was hoping to learn from this in anticipation of an upcoming challenge on MysteryTwister.

If you can find any old files from this attack, I have about three weeks that I can use to help figure it out.