Re: [bitcoin-dev] TLA+ specification for Succint Atomic Swap

2020-06-01 Thread Dmitry Petukhov via bitcoin-dev
I've finished specifying the full Succint Atomic Swap contract in TLA+. I believe the specification [1] now covers all relevant behaviors of the participants. It even has an option to enable 'non-rational' behavior, so that it can be shown that the transactions that are there to punish bad

Re: [bitcoin-dev] TLA+ specification for Succint Atomic Swap

2020-05-14 Thread Ruben Somsen via bitcoin-dev
Hi Dmitry, >But it should be noted that it is not enough that Bob publishes success_tx before refund_tx_1 became valid. The success_tx needs to be confirmed before refund_tx_1 became valid. Agreed, my write-up would benefit from pointing this out more explicitly. Cheers, Ruben On Thu, May 14,

Re: [bitcoin-dev] TLA+ specification for Succint Atomic Swap

2020-05-14 Thread Dmitry Petukhov via bitcoin-dev
В Thu, 14 May 2020 07:31:13 +0200 Ruben Somsen wrote: > Hi Dmitry, > > >While refund_tx_1 is in the mempool, Bob gives success_tx to the > >friendly miner > > I see, so you're talking about prior to protocol completion, right > after Alice sends Bob the success_tx. The reason this is not an

Re: [bitcoin-dev] TLA+ specification for Succint Atomic Swap

2020-05-13 Thread Ruben Somsen via bitcoin-dev
Hi Dmitry, >While refund_tx_1 is in the mempool, Bob gives success_tx to the friendly miner I see, so you're talking about prior to protocol completion, right after Alice sends Bob the success_tx. The reason this is not an issue is because Alice and Bob both had to misbehave in order for this to

Re: [bitcoin-dev] TLA+ specification for Succint Atomic Swap

2020-05-13 Thread Dmitry Petukhov via bitcoin-dev
В Wed, 13 May 2020 21:03:17 +0200 Ruben Somsen wrote: > Or perhaps you're referring to the issue ZmnSCPxj pointed out after > that, where refund transaction #1 and the success transaction could > both become valid at the same time. It would make sense for the test > to pick up on that, but I

Re: [bitcoin-dev] TLA+ specification for Succint Atomic Swap

2020-05-13 Thread Ruben Somsen via bitcoin-dev
Hi Dmitry, Thanks for creating a specification for testing, I appreciate the interest! >The checking of the model encoded in the specification can successfully detect the violation of 'no mutual secret knowledge' invariant when one of the participant can bypass mempool and give the transaction