TLA+ specification for Succint Atomic Swap



Summary:

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.


Updated on: 2023-06-14T01:38:34.600114+00:00