# How to use smt solvers in order to restrict the possible key search where a portion of the private key and a portion of the public key hash is known?

I’m in the following situation :

• I’ve a portion/first bytes of a private secp256k1 security key such as it would take minutes to fully recover it through Pollard’s Kangaroo if I had the public key.
• While I don’t have the public key, I do have the first 20 bytes of it’s sha256 (and nothing else as the key was never used so I don’t even know if it’s the compressed or the uncompressed key).

So currently either I have to brute force all possible 260 keys which looks economically infeasible or I have to brute force sha256 through an asic in order to find a preimage of the public key’s.
This means either the private key portion or either the partial sha256 is useless to restrict the search space…

Given using sat solvers for Bitcoin mining (so finding pre‑images in a specific case) showed mixed results, my idea would be to use smt/sat solving for restricting the search space using both the partial hash along with the first private key’s bytes. Currently, I’m not looking at making it more efficient than bruteforcing, but just to get it working.

There’re 2 ways to do it : either to search for the private key directly or search for the public key which then can be reversed quickly using Pollard’s kangaroo.

• Incrementing a private key by 1 leads to incrementing the public key by 0xBAAEDCE6AF48A03BBFD25E8CD0364141 ($$G$$ of secp256k1). This means there’s a range of public keys, but unless the Koblitz curve can be converted to a more useful curve, I fail to see how to use this type of information for formalizing into a useful way for at least a smt solver.
• As retrieving a private key from a public key is the same as solving the discrete logarithm, I fail to see how to express a formula that would allow a smt/sat solver to restrict the sha256 search space using the restricted private key search space (since the first private key bytes are known).

Any thoughts on how to mathematically link the 2 informations for a smt/sat solver for shrinking the brute force search space ?

• Your question about incrementing by one was competently answered. It is only polite to accept that answer. Apr 16 at 18:16
• @kodlu depending on that question I wanted to know the faster method for ꜰᴘɢᴀ in the previous question where space is an issue… That’s why I didn’t accept the answer yet. Apr 16 at 20:52
• The value you show is not the point $G$ for secp256k1; if it only the low bits of the y-coordinate. You can add numbers by doing the low bits and high bits separately (as long as you do both) but that doesn't work for EC point addition, which is NOT numeric addition at all; you must use the full value of both coordinates and the Weierstrass formula(s). Apr 16 at 23:50
• @dave_thompson_085 as far I understand, it’s a translation. When you multiply for getting the public key, you use a scalar instead of a point and thus the value of G I wrote. Apr 16 at 23:57
• I don't know what you mean by translation, but the private key $d$ is a scalar; the generator $G$ is a point, and the public key produced by point multiplication (not numeric multiplication) $Q = d \cdot G$ is also a point Apr 18 at 1:32

## 1 Answer

search for the public key which then…

That's infeasible if we hash public keys that are not chosen according to what's known of the private key. It would require about $$2^{160}$$ hashes to find one which first 20 bytes are as desired (and then there's a mere one chance in $$2^{96}$$ we found the public key for the desired private key).

This leaves as the only option: trying private keys, for each computing the matching public key, and from that computing and testing the first 20 bytes of the hash. This will succeed after $$2^b$$ private keys processed for $$b$$ unknown private key bits (and an expected $$2^{b-1}$$ attempts). As discussed there, the cost is dominated by one addition of the generator point $$G$$ and one near complete SHA-256 per additional private key tested.

use SMT/SAT solving…

Because the private-key to public-key function and the public-key to hash function are one-way, the best that could be hoped (absent an improbable cryptanalytic breakthrough) is that the solver's heuristic manages to find a way to select the unknown private key bits as "master" unknowns, and performs essentially a brute force search with cost $$\mathcal O(2^b)$$. But don't bet on that! For all (SAT) solvers I practice, the size of the input problem will grow as $$\mathcal O(2^b)$$, and the cost will grow so much faster that the approach is doomed.

how to express a formula that would allow a SMT/SAT solver to restrict the sha256 search space using the restricted private key search space

We can build a function $$g$$ which on input the $$(x,y)$$ coordinates of $$Q$$ outputs $$Q+G$$ per point addition, that we can restrict to $$Q\not\in\{G,-G,\infty\}$$. We can make a function $$h$$ which on input the coordinates of $$Q$$ outputs a bit telling if the first 160 bits of the SHA-256 of $$Q$$ are as expected. From this we can construct a function which on externally computed $$Q_0=d\,G$$ (expressed as $$(x,y)$$ coordinates) computes $$Q_1=f(Q_0)$$, $$Q_2=f(Q_1)$$, $$Q_3=f(Q_2)$$, $$h_0=h(Q_0)$$, $$h_1=h(Q_1)$$, $$h_2=h(Q_2)$$, $$h_3=h(Q_3)$$, and the expression $$h_0\vee h_1\vee h_2\vee h_3$$. If that later condition is satisfiable, the desired private key is $$d+h_1+2h_2+3h_3$$, solving our problem with $$b=2$$ unknown private key bits. With pure SAT, the size of the input problem grows exponentially with $$b$$, but that would not be the case for more sophisticated input formats, e.g. with Quantified Boolean Formula (that I never personally used). Whatever, that's in essence brute force re-expressed as satisfiability, and doomed to be slow.

• Benchmarks say that 256 H100 ɢᴘᴜs programmed in ᴄᴜᴅᴀ are able to generate 80 billion key/hash per second for brute force (using only the hash for verification and not for restricting the possible keys). 2⁶⁰ key pairs seems possible but economically too much… [edited for readability by moderator] Apr 17 at 15:29
• @user2284570: 80 billion hash/s for 256 GPUs seems in the right ballpark. If you have reasons to believe the problem is more easily solvable (like it's a CTF that others have solved), double-check what the « portion/first bytes of a private secp256k1 security key » exactly is. More often than not, in secp256k1/cryptocurrencies contexts, that's not high-order bits of a 256-bit private key $d$ in the ECDSA sense. In particular, in WIF format, the last 5 characters (at least) are redundant. So you might need to explore a smaller key interval than you estimated!
– fgrieu
Apr 18 at 13:54
• Again, it’s the least significant bits that are unknown. P2PKH transactions can send money to any sha256 hash of a public key (compressed or uncompressed). Based on this, I fail to see any restrictions on what private keys can be used, nor do I see restrictions in the source des bruteforce software (unless the known truncated hash can used to restrict the buteforce’s search space and not only for checking whether the result is valid). Apr 18 at 14:38
• @user2284570: I do trust that « it’s the least significant bits that are unknown », but evaluating how many of those bits are unknown depends on how these have been lost and the format of the private key at time of that loss. I very much doubt that a competently devised CTF intended to be solved with the help of some part of the hash of the public key would remove the low-order 60 bits of the 256-bit private key $d$. As you point out, that's too much. OTOH, loosing the last/low order 10 or 11 character of a WIF key would imply much less work.
– fgrieu
Apr 18 at 16:37
• It was hex encoded private keys. Current cuda software designed on purpose are trying the full unknown bits search. Unless there re can be something made clever, I only see the sha256 preimage through solvers as the way to have less than 2<sup>lost bits</sup> to search. Apr 18 at 23:00