Use an SMT solver to make better CoinJoins

[csH7KmCC9]

(this is a duplicate of the issue filed for JoinMarket, but reposted here because it is also relevant).

Please see this proof-of-concept. This sets up an example CoinJoin, encodes the CoinJoin constraints into a satisfiability modulo theories problem, and uses PySMT with an off-the-shelf SMT solver e.g. from Microsoft.

The key advantages of this approach are:

• There is no more guessing and fuzziness about tx fees
• We can use it to put more outputs (i.e. change outputs) into a non-singleton anonymity set, potentially improving the privacy of makers

Consider the default CoinJoin example from my repo. We have four inputs from three parties, in amounts 1BTC (from the taker who is doing a sweep), 1.3BTC (from the second party), and two inputs totaling 1.4BTC (from the third party). In the current implementation, we might get CoinJoin outputs like (party, amount): [(1, 99997329), (2, 99997329), (3, 99997329), (2, 30002682), (3, 40002676)], which includes two outputs that are uniquely identifiable.

In contrast, here is the solution found by the SMT-based approach: [(1, 99997329), (2, 99997329), (3, 99997329), (2, 9999994), (3, 9999994), (3, 9999994), (2, 20002688), (3, 20002688)], which includes zero outputs that are uniquely identifiable. Of course, subsequent behavior of the maker could reveal the association between outputs, but a similar approach can be taken to use an SMT solver to choose the least-revealing set of UTXOs for a maker to use for a given offer.

Note that this is just a proof-of-concept, and the final implementation probably should not take the extreme of trying to minimize unique outputs at all costs, as the extra outputs primarily cost the taker but give privacy benefits to the makers. Of course there will need to be some protocol tweaks, too, to enable the communication to the taker of more than one change address per maker.

[lontivero]

Thank you very much for sharing this. We are currently working on the WabiSabi coinjoin protocol which needs to find the best way to break outputs and it could be good to take a look at this technology too. Ping: @nothingmuch

[csH7KmCC9]

It's my pleasure. I would like to participate in these discussions. Maybe I can identify a way that this approach can be helpful.

I would also like to point out a related project implementing the problem encoding, solving, and optimization procedure for what I am currently calling "community joins" but what are probably better called "perfect CoinJoins".

In these CoinJoins, no output is uniquely identifiable. Each participant offers inputs and a maximum fee contribution, and a solver determines the best way to use the offered inputs to create a perfect CoinJoin with no uniquely-identifiable outputs. Not all offered inputs are always used. Solutions are scored according to how much they improve anonymity and are iteratively optimized. Fee contributions are pro-rated according to the number of that party's offered inputs that are actually consumed, and if the math works out, parties can even end up with a negative fee contribution (i.e. you can sometimes--but not reliably--even earn satoshis by participating). The total number of outputs, and the total number of outputs for each party, are also constrained to limit UTXO fragmentation.

More and different applications, constraints, and optimization procedures are possible. I hope that we can together come up with more ideas on how best to apply SMT-based methods to improve CoinJoin privacy.

For example, the further combination of CoinJoin outputs as inputs to subsequent transactions reduces the anonymity set of those combined UTXOs. This is true both in "perfect CoinJoins" and in current-style CoinJoins. I believe there is an opportunity to apply an SMT-based method to UTXO selection in order to enforce certain anonymity set guarantees and avoid harming rather than improving the size of the outputs' anonymity sets. But this needs more careful thought; I don't have a proof-of-concept ready for this :).