Find the secret key for this function

Originally Posted by mr.exodia

My code for solving (see here on how to install z3py):

from z3 import *

key = BitVec('key', 64)
solve((key * key * key * key * key * key * key) == 0x90de757572b51cd3)

Output:

[key = 16721472531635646971]
0xE80E9AAC619831FB

I still don't get it

Can anyone explain me the mathematical way to calculate this ?

I always come up to a different result.

Like:

0xE80E9AAC619831FB ^7 = 0x80BE33B7E7E4CB02B42B9C6FDF0D774CC0645D8992D29738EC470B848F80CFA482BA62D01E70C65E397E7EFE6F190D1990DE757572B51CD3

or something like that

Where is my "think failure" ?

- Seth