Published on: 2020-06-01T11:38:54+00:00
The author has completed the specification of the Succint Atomic Swap contract in TLA+. The specification covers all relevant behaviors of the participants and even has an option to enable 'non-rational' behavior. The model is capable of exhaustively checking safety properties and temporal properties. Additionally, the model can show hyperproperties, but automatic checking of hyperproperties is not yet available. The model has some limitations, like only having one miner and not modeling fees and mempool priorities. Despite these limitations, the author believes that TLA+ is a suitable tool for specifying and checking smart contract specifications.In an email exchange, Ruben Somsen points out to Dmitry Petukhov that it is important for Bob to confirm success_tx before refund_tx_1 becomes valid. Dmitry agrees and notes that this is unlikely to be a practical problem unless the original fee of success_tx is too small. Ruben also clarifies that Alice won't give her key until she learns secretBob because step 5 comes before step 6 in the diagram. Dmitry admits that he missed this and that he now made the `signers_map` into variable that can be changed to give Bob the ability to sign for Alice. However, he warns that this will add a bunch of new transactions to the model, each Alice&Bob spend having 'Bob unilateral override' case.A conversation between Ruben Somsen and Dmitry about the Lightning Network protocol was shared. They discuss the scenario when Bob gives success_tx to a friendly miner while refund_tx_1 is in the mempool. Ruben explains that this situation would not be an issue because both Alice and Bob had to misbehave for it to happen. Bob should have published the success_tx before refund_tx_1 became valid, and Alice should have sent the revoke_tx followed by refund_tx_2, revealing her secret only after Bob could no longer claim the BTC. Dmitry notes that it's crucial that success_tx is confirmed before refund_tx_1 becomes valid, but this is unlikely to be a practical problem since only Bob can spend success_tx unless the original fee of success_tx is too small. Ruben also corrects Dmitry's assumption that Bob will receive BTC, and the LTC can be locked forever. Ruben explains that Alice would not give her key until she learned secretBob, which occurs in step 6 of the diagram. Ruben then makes a change in the model, making the `signers_map` into a variable that can be changed to give Bob the ability to sign for Alice. This change enables step 6 to be modeled, but it adds several new transactions to the model.The conversation between Ruben and Dmitry revolves around the Lightning Network protocol and its potential issues. They discuss the issue of refund transaction #1 and the success transaction becoming valid at the same time. Ruben explains that this is not an issue because Alice and Bob would both have to misbehave for it to happen. They also discuss the possibility of Bob giving the success_tx to a friendly miner while refund_tx_1 is in the mempool, which could result in Bob receiving both LTC and BTC while Alice loses her BTC. Ruben clarifies that this won't happen if either of them doesn't want it to. Finally, they discuss the cooperative spend of refund_tx #1 by Alice and Bob, which is there to ensure that Bob can spend the money before Alice once he receives her key at the end of the protocol.In an email conversation, Ruben Somsen discusses an issue with the Lightning Network where Bob can potentially invalidate a transaction and take both LTC and BTC from Alice. The issue arises due to the fact that Bob cannot wait for Alice to broadcast refund_tx_1 before broadcasting success_tx, which would allow him to invalidate refund_tx_1 and take the BTC. However, Somsen believes this is not ultimately an issue. In response to a question about the destination of Alice and Bob's cooperative spend of refund_tx#1, Somsen explains that they can spend it right away or Alice can spend it a day later, after the tx has confirmed. The Alice & Bob condition is only there to ensure that Bob can spend the money before Alice once he receives her key at the end of the protocol. Somsen clarifies that the reason Alice gives Bob her key ("Alice") in step 5 of the diagram is to deny Alice from using refund_tx_1. Finally, there is a discussion about whether Bob could just spend the Alice&Bob output of the very first "commitment" transaction that locks BTC if Alice gives him her key before he shares secretBob via success_tx.Dmitry Petukhov has created a formal specification for the Succint Atomic Swap (SAS) contract presented by Ruben Somsen, using the TLA+ specification language.
Updated on: 2023-08-02T02:14:52.610003+00:00