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 directly to the miner (this problem was pointed out by ZmnSCPxj in the original SAS thread [2])
I'm not sure if I follow. The issue ZmnSCPxj described about bypassing the mempool was not a violation. It was merely a "nuisance" strategy that causes Alice to have to abort in three transactions. Also note that I subsequently pointed out in the thread that this strategy does not work, because Alice is supposed to abort sooner than that if Bob still has not locked up any funds.
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 believe that is ultimately also not an issue (see my last reply in the thread).
>I did not understand what the destination of Alice&Bob cooperative spend of refund_tx#1 will be
This transaction can be spent by Alice & Bob right away or by Alice a day later (in relative time, so the tx has to confirm first). The Alice & Bob condition is there purely to ensure that Bob can spend the money before Alice once he receives her key at the end of the protocol.
If it helps, you could model this transaction as two separate transactions instead:
txA: 1 day absolute timelock to Alice & Bob (reveals secretAlice), which can then be spent by
txB: +1 day relative timelock to Alice
This should be functionally equivalent. Also note that the protocol should fully function if refund tx #1 did not exist at all. It merely serves to save block space in certain refund scenarios.
>it would be great to have an established framework for modelling of the behavior in Bitcoin-like blockchain networks. In particular, having a model of mempool-related behavior would help to reason about difficult RBF/CPFP issues
A laudable goal. Good luck with your efforts.
Cheers,
Ruben