diff options
author | Ruben Somsen <rsomsen@gmail.com> | 2020-05-13 21:03:17 +0200 |
---|---|---|
committer | bitcoindev <bitcoindev@gnusha.org> | 2020-05-13 19:03:34 +0000 |
commit | 0b902affca089fff770582714ce6ec949e128f65 (patch) | |
tree | eb3c1f7242d98e71457df9cd46cfefab87f0f06b | |
parent | c7cf3e028e534b29a6518ac75dca5008bd9d5c8f (diff) | |
download | pi-bitcoindev-0b902affca089fff770582714ce6ec949e128f65.tar.gz pi-bitcoindev-0b902affca089fff770582714ce6ec949e128f65.zip |
Re: [bitcoin-dev] TLA+ specification for Succint Atomic Swap
-rw-r--r-- | f5/54cdf5861b5fbbf5e20659f64addeac2a88084 | 326 |
1 files changed, 326 insertions, 0 deletions
diff --git a/f5/54cdf5861b5fbbf5e20659f64addeac2a88084 b/f5/54cdf5861b5fbbf5e20659f64addeac2a88084 new file mode 100644 index 000000000..051282d36 --- /dev/null +++ b/f5/54cdf5861b5fbbf5e20659f64addeac2a88084 @@ -0,0 +1,326 @@ +Return-Path: <rsomsen@gmail.com> +Received: from hemlock.osuosl.org (smtp2.osuosl.org [140.211.166.133]) + by lists.linuxfoundation.org (Postfix) with ESMTP id A2CB7C016F + for <bitcoin-dev@lists.linuxfoundation.org>; + Wed, 13 May 2020 19:03:34 +0000 (UTC) +Received: from localhost (localhost [127.0.0.1]) + by hemlock.osuosl.org (Postfix) with ESMTP id 8ACCB89438 + for <bitcoin-dev@lists.linuxfoundation.org>; + Wed, 13 May 2020 19:03:34 +0000 (UTC) +X-Virus-Scanned: amavisd-new at osuosl.org +Received: from hemlock.osuosl.org ([127.0.0.1]) + by localhost (.osuosl.org [127.0.0.1]) (amavisd-new, port 10024) + with ESMTP id T-AwSgbHIITs + for <bitcoin-dev@lists.linuxfoundation.org>; + Wed, 13 May 2020 19:03:31 +0000 (UTC) +X-Greylist: domain auto-whitelisted by SQLgrey-1.7.6 +Received: from mail-ej1-f48.google.com (mail-ej1-f48.google.com + [209.85.218.48]) + by hemlock.osuosl.org (Postfix) with ESMTPS id 61208892AC + for <bitcoin-dev@lists.linuxfoundation.org>; + Wed, 13 May 2020 19:03:31 +0000 (UTC) +Received: by mail-ej1-f48.google.com with SMTP id e2so422485eje.13 + for <bitcoin-dev@lists.linuxfoundation.org>; + Wed, 13 May 2020 12:03:31 -0700 (PDT) +DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; + h=mime-version:references:in-reply-to:from:date:message-id:subject:to + :cc; bh=ByJxDnKZi4TtjZZKEld0PhoezZYTxk1pEna+TkZ+irc=; + b=oZGUcxRyqID0wOTkNf3r3VqyJPr/PFk0RxCmN5L5avLATh8ysBHwuqSbvEPuH4CIWy + QA/aZGAofdn+VvBS/b3UGzE2f34UN065DzLFkCA27MeNSIt0awC7LWhoSvFmJteBXJuu + bv8ImdnF7m87i6GLPUBsD0pV8EvEjF95mXQuJhrAYwHEa0PusGzWNqhZvFq44uXXr/gm + 0QwHxaEGXiqrCeMHWiCbQaNd9yZQV/nFsfPJGCgAZgLFHk8xdScNNVlkifiZQN4LeXBU + McuSnltvIC1k73xoqr8ljvDt8fkfEzWb4Xvl0PwDfMUKXnYQkhOUbSfG6k+p5sGunnev + aayQ== +X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; + d=1e100.net; s=20161025; + h=x-gm-message-state:mime-version:references:in-reply-to:from:date + :message-id:subject:to:cc; + bh=ByJxDnKZi4TtjZZKEld0PhoezZYTxk1pEna+TkZ+irc=; + b=DEAlWQ34+7tkKcT+kPu8qXuj7RXxgJE6rhbdIWpSRqkHMZUkK/VFmn+sNXPxfDqyhB + /Qntirx2dMWcy8trHfIxw9vyHk/DyX11POxYE7dWJR117v2foG7sH0iDbGGsXySMJVCM + KezMyLTz93/uhb0SYOVkD+2d2LpmhoEznmoOspIL16zvnsx53AL3yTBLvaqOmSayE1hD + vtHmjhTaeTN94WiZ9oYtO/9XFbx2z0LbYzrRMwol9fEHq5rySbObw9fmVQLawKo8pVgl + m8kd+sfT1j1xmRQ9i9/PxREo9iAqZB8IG4r9RdiDBuvPO+cp2LP7UYaQ3CNrRHVmVzLP + F62Q== +X-Gm-Message-State: AOAM5324EJfHcL8pI1wyjjyT3wllHQ7vhDKLTC9uXlYogCwXPhtAqQ44 + F7hwnNLQayvh5osm3mxsyMvawKlpGXuqBGKQCmXNzM+V +X-Google-Smtp-Source: ABdhPJzeJmURk8E5vlxYa+1NX0qapLtaKxCxbjH4MtI+IlUPnSZOz0m55Cww0DlwxQ/n62gDa22RoHuK9c8/gRmgc5s= +X-Received: by 2002:a17:906:7f0d:: with SMTP id + d13mr465780ejr.312.1589396609615; + Wed, 13 May 2020 12:03:29 -0700 (PDT) +MIME-Version: 1.0 +References: <20200513220222.24953c0a@simplexum.com> +In-Reply-To: <20200513220222.24953c0a@simplexum.com> +From: Ruben Somsen <rsomsen@gmail.com> +Date: Wed, 13 May 2020 21:03:17 +0200 +Message-ID: <CAPv7TjbZVYTztQLd2dxjzFajhPTg23iWtapkVBzz+z0q=pH2rw@mail.gmail.com> +To: Dmitry Petukhov <dp@simplexum.com> +Content-Type: multipart/alternative; boundary="00000000000052cd5705a58c3ccf" +X-Mailman-Approved-At: Wed, 13 May 2020 19:06:29 +0000 +Cc: Bitcoin Protocol Discussion <bitcoin-dev@lists.linuxfoundation.org> +Subject: Re: [bitcoin-dev] TLA+ specification for Succint Atomic Swap +X-BeenThere: bitcoin-dev@lists.linuxfoundation.org +X-Mailman-Version: 2.1.15 +Precedence: list +List-Id: Bitcoin Protocol Discussion <bitcoin-dev.lists.linuxfoundation.org> +List-Unsubscribe: <https://lists.linuxfoundation.org/mailman/options/bitcoin-dev>, + <mailto:bitcoin-dev-request@lists.linuxfoundation.org?subject=unsubscribe> +List-Archive: <http://lists.linuxfoundation.org/pipermail/bitcoin-dev/> +List-Post: <mailto:bitcoin-dev@lists.linuxfoundation.org> +List-Help: <mailto:bitcoin-dev-request@lists.linuxfoundation.org?subject=help> +List-Subscribe: <https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev>, + <mailto:bitcoin-dev-request@lists.linuxfoundation.org?subject=subscribe> +X-List-Received-Date: Wed, 13 May 2020 19:03:34 -0000 + +--00000000000052cd5705a58c3ccf +Content-Type: text/plain; charset="UTF-8" + +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 + +On Wed, May 13, 2020 at 7:07 PM Dmitry Petukhov via bitcoin-dev < +bitcoin-dev@lists.linuxfoundation.org> wrote: + +> The Succint Atomic Swap contract presented by Ruben Somsen recently has +> drawn much interest. +> +> I personally am interested in the smart contracts realizeable in the +> UTXO model, and also interested in applying formal methods to the +> design and implementation of such contracts. +> +> I think that having formal specifications for the contracts and to be +> able to machine-check the properties of these specifications is very +> valuable, as it can uncover the corner cases that might be difficult to +> uncover otherwise. +> +> The SAS contract is complex enough that it may benefit from formal +> specification and machine checking. +> +> I created a specification in TLA+ [1] specification language based on +> the explanation and the diagram given by Ruben. +> +> 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]) +> +> There's one transition that was unclear how to model, though: I did not +> understand what the destination of Alice&Bob cooperative spend of +> refund_tx#1 will be, so this transition is not modelled. +> +> I believe there can be more invariants and temporal properties of the +> model that can be checked. At the moment the temporal properties +> checking does not work, as I didn't master TLA+ enough yet. The safety +> invariants checking should work fine, though, but more work needed to +> devise and add the invariants. +> +> In the future, 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. The specification I present +> models the mempool, but in a simple way, without regards to the fees. +> +> The specification can be found in this github repository: +> https://github.com/dgpv/SASwap_TLAplus_spec +> +> There could be mistakes or omissions in the specified model, I hope +> that public review can help find these. +> +> It would be great to receive comments, suggestions and corrections, +> especially from people experienced in formal methods and TLA+, as this +> is only my second finished TLA+ spec and only my third project using +> formal methods (I created bitcoin transaction deserialization code in +> Ada/SPARK before that [3]). Please use the github issues or off-list +> mail to discuss if the matter is not interesting to the general +> bitcoin-dev list audience. +> +> [1] https://lamport.azurewebsites.net/tla/tla.html +> +> [2] +> +> https://lists.linuxfoundation.org/pipermail/bitcoin-dev/2020-May/017846.html +> +> [3] https://github.com/dgpv/spark-bitcoin-transaction-example +> _______________________________________________ +> bitcoin-dev mailing list +> bitcoin-dev@lists.linuxfoundation.org +> https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev +> + +--00000000000052cd5705a58c3ccf +Content-Type: text/html; charset="UTF-8" +Content-Transfer-Encoding: quoted-printable + +<div dir=3D"ltr">Hi Dmitry,<div><br></div><div>Thanks for creating a specif= +ication for testing, I appreciate the interest!</div><div><br></div><div>&g= +t;The checking of the model encoded in the specification can successfully d= +etect 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])</div><div><br></div><div>I'm not sure if I follow. The iss= +ue ZmnSCPxj described about bypassing the mempool was not a violation. It w= +as merely a "nuisance" strategy that causes Alice to have to abor= +t in three transactions. Also note that I subsequently pointed out in the t= +hread that this strategy does not work, because Alice is supposed to abort = +sooner than that if Bob still has not locked up any funds.</div><div><br></= +div><div>Or perhaps you're referring to the issue=20 + +ZmnSCPxj + + pointed out after that, where refund transaction #1 and the success transa= +ction 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 issu= +e (see my last reply in the thread).</div><div><br></div><div>>I did not= + understand what the destination of Alice&Bob cooperative spend of refu= +nd_tx#1 will be<br></div><div><br></div><div>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 purel= +y to ensure that Bob can spend the money before Alice once he receives her = +key at the end of the protocol.</div><div><br></div><div>If it helps, you c= +ould model this transaction as two separate transactions instead:</div><div= +>txA: 1 day absolute timelock to Alice & Bob (reveals secretAlice), whi= +ch can then be spent by</div><div>txB: +1 day relative timelock to Alice</d= +iv><div><br></div><div>This should be functionally equivalent. Also note th= +at 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.</div><di= +v><br></div><div>>it would be great to have an established framework for= + modelling of the behavior in Bitcoin-like blockchain networks. In particul= +ar, having a model of mempool-related behavior would help to reason about d= +ifficult RBF/CPFP issues<br></div><div><br></div><div>A laudable goal. Good= + luck with your efforts.</div><div><br></div><div>Cheers,</div><div>Ruben</= +div></div><br><div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_at= +tr">On Wed, May 13, 2020 at 7:07 PM Dmitry Petukhov via bitcoin-dev <<a = +href=3D"mailto:bitcoin-dev@lists.linuxfoundation.org">bitcoin-dev@lists.lin= +uxfoundation.org</a>> wrote:<br></div><blockquote class=3D"gmail_quote" = +style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);pa= +dding-left:1ex">The Succint Atomic Swap contract presented by Ruben Somsen = +recently has<br> +drawn much interest.<br> +<br> +I personally am interested in the smart contracts realizeable in the<br> +UTXO model, and also interested in applying formal methods to the<br> +design and implementation of such contracts.<br> +<br> +I think that having formal specifications for the contracts and to be<br> +able to machine-check the properties of these specifications is very<br> +valuable, as it can uncover the corner cases that might be difficult to<br> +uncover otherwise.<br> +<br> +The SAS contract is complex enough that it may benefit from formal<br> +specification and machine checking.<br> +<br> +I created a specification in TLA+ [1] specification language based on<br> +the explanation and the diagram given by Ruben.<br> +<br> +The checking of the model encoded in the specification can successfully<br> +detect the violation of 'no mutual secret knowledge' invariant when= + one<br> +of the participant can bypass mempool and give the transaction directly<br> +to the miner (this problem was pointed out by ZmnSCPxj in the original<br> +SAS thread [2])<br> +<br> +There's one transition that was unclear how to model, though: I did not= +<br> +understand what the destination of Alice&Bob cooperative spend of<br> +refund_tx#1 will be, so this transition is not modelled.<br> +<br> +I believe there can be more invariants and temporal properties of the<br> +model that can be checked. At the moment the temporal properties<br> +checking does not work, as I didn't master TLA+ enough yet. The safety<= +br> +invariants checking should work fine, though, but more work needed to<br> +devise and add the invariants.<br> +<br> +In the future, it would be great to have an established framework for<br> +modelling of the behavior in Bitcoin-like blockchain networks.<br> +In particular, having a model of mempool-related behavior would help to<br> +reason about difficult RBF/CPFP issues. The specification I present<br> +models the mempool, but in a simple way, without regards to the fees.<br> +<br> +The specification can be found in this github repository:<br> +<a href=3D"https://github.com/dgpv/SASwap_TLAplus_spec" rel=3D"noreferrer" = +target=3D"_blank">https://github.com/dgpv/SASwap_TLAplus_spec</a><br> +<br> +There could be mistakes or omissions in the specified model, I hope<br> +that public review can help find these.<br> +<br> +It would be great to receive comments, suggestions and corrections,<br> +especially from people experienced in formal methods and TLA+, as this<br> +is only my second finished TLA+ spec and only my third project using<br> +formal methods (I created bitcoin transaction deserialization code in<br> +Ada/SPARK before that [3]). Please use the github issues or off-list<br> +mail to discuss if the matter is not interesting to the general<br> +bitcoin-dev list audience.<br> +<br> +[1] <a href=3D"https://lamport.azurewebsites.net/tla/tla.html" rel=3D"noref= +errer" target=3D"_blank">https://lamport.azurewebsites.net/tla/tla.html</a>= +<br> +<br> +[2]<br> +<a href=3D"https://lists.linuxfoundation.org/pipermail/bitcoin-dev/2020-May= +/017846.html" rel=3D"noreferrer" target=3D"_blank">https://lists.linuxfound= +ation.org/pipermail/bitcoin-dev/2020-May/017846.html</a><br> +<br> +[3] <a href=3D"https://github.com/dgpv/spark-bitcoin-transaction-example" r= +el=3D"noreferrer" target=3D"_blank">https://github.com/dgpv/spark-bitcoin-t= +ransaction-example</a><br> +_______________________________________________<br> +bitcoin-dev mailing list<br> +<a href=3D"mailto:bitcoin-dev@lists.linuxfoundation.org" target=3D"_blank">= +bitcoin-dev@lists.linuxfoundation.org</a><br> +<a href=3D"https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev" = +rel=3D"noreferrer" target=3D"_blank">https://lists.linuxfoundation.org/mail= +man/listinfo/bitcoin-dev</a><br> +</blockquote></div> + +--00000000000052cd5705a58c3ccf-- + |