Author: Ruben Somsen 2020-05-13 19:03:17
Published on: 2020-05-13T19:03:17+00:00
Dmitry Petukhov has created a formal specification for the Succint Atomic Swap (SAS) contract presented by Ruben Somsen, using the TLA+ specification language. The model encoded in the specification can successfully detect the violation of the 'no mutual secret knowledge' invariant when one participant bypasses mempool and gives the transaction directly to the miner. However, there is one transition that was unclear how to model - the destination of Alice and Bob's cooperative spend of refund_tx#1. Nevertheless, the temporal properties checking should work fine, but more work is needed to devise and add the invariants. In the future, an established framework for modelling the behavior in Bitcoin-like blockchain networks would be great. In particular, having a model of mempool-related behavior would help to reason about difficult RBF/CPFP issues. Dmitry believes that there can be more invariants and temporal properties of the model that can be checked. He hopes that public review can help find any mistakes or omissions in the specified model. Experienced people in formal methods and TLA+ are encouraged to give their comments, suggestions and corrections. They can use the github issues or off-list mail to discuss if the matter is not interesting to the general bitcoin-dev list audience.
Updated on: 2023-06-14T01:38:20.795903+00:00