Lloyd Fournier [ARCHIVE] on Nostr: 📅 Original date posted:2019-07-17 📝 Original message: Hi Orfeas, Thanks for ...
📅 Original date posted:2019-07-17
📝 Original message:
Hi Orfeas,
Thanks for formally modelling lightning and posting your paper here. I've
taken a brief look at the paper so far. I am a UC novice and have no
academic background so please take that into account when interpreting my
comments. In general, I am glad that you are taking the approach to model
the protocol relative to the G_ledger functionality which seems like the
right thing to do (from my amateurish view). The questions/comments I have
are:
1. When modelling things in UC the ideal functionalities should be as
simple and intuitive as possible. I found F_PayNet to be rather difficult
to follow as compared to the Sprites paper [1]. For example,
"F_PayNet checks that for each payment the charged party was one of the
following: (a) the one that initiated the payment, (b) a malicious party or
(c) an honest party that is negligent"
Why not assume that (b) never happens because a malicious party never
wants to lose the funds from a party they've corrupted and (c) never
happens because honest parties follow the protocol and check each ledger
update for malicious channel closes. Real world protocols always realise
ideal functionalities under some assumptions and these two things seem like
pretty reasonable things to include in your assumptions rather than
cluttering up your ideal functionality.
2. In both your paper and [1] I am not convinced that the ideal and real
worlds aren't easily distinguishable from each other by an Environment that
just looks at the transactions in the blockchain (G_ledger). For example,
the lightning protocol makes heavy use of pay-to-script-hash where as ideal
functionalities have no need for this. F_PayNet can just send normal
transactions. I think it would be a great idea to describe how you ensure
that the transactions that make it onto the blockchain after an execution
in the real world are indistinguishable from the ideal world.
3. On a related note, I don't understand this "receipt" mechanism. In your
protocol description of OpenChannel, Alice uses her private key which owns
UTXO(s) with x coins to create the funding transaction. This means she
received that private key as input to the execution of the protocol so that
she is able to do this (why don't you explicitly include this private key
in the OpenChannel message?). In the ideal world, the ideal functionality
should be the one with the private key signing the funding transaction
directly (in the ideal world the parties are dummy ITMs which just send
their input to the ideal functionality). But instead there is this receipt
thing which I don't understand.
Cheers
LL
[1] https://arxiv.org/pdf/1702.05812.pdf
On Wed, Jul 10, 2019 at 6:44 PM Orfeas Stefanos Thyfronitis Litos <
o.thyfronitis at ed.ac.uk> wrote:
> Hi all,
>
> The promise for fast, scalable, user-friendly and trustless use of
> bitcoin that the Lightning Network offers motivated us to author a paper
> where we formalize LN in the cryptographic framework of Universal
> Composition and prove its security. It can be found here:
> https://eprint.iacr.org/2019/778
>
> We believe that a formal proof of security was needed to specify the
> exact operating parameters that safeguard the funds and transactions of
> users against arbitrary attackers, to abstract, modularize and validate
> the underlying cryptography that is used in LN, to incorporate LN in the
> body of cryptographic protocols that have been abstracted within the
> Universal Composition framework (and thus can be safely composed and run
> in parallel) and to increase the trust of the wider community to LN. We
> view this work as a small contribution to the amazing effort that the
> Lightning community has expended both on the theoretical and the
> practical front throughout the last years.
>
> The paper is authored by my PhD supervisor Prof. Aggelos Kiayias and me.
> Any feedback will be greatly appreciated.
>
> Best regards,
> Orfeas Stefanos Thyfronitis Litos
>
> --
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
> _______________________________________________
> Lightning-dev mailing list
> Lightning-dev at lists.linuxfoundation.org
> https://lists.linuxfoundation.org/mailman/listinfo/lightning-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.linuxfoundation.org/pipermail/lightning-dev/attachments/20190718/06565966/attachment-0001.html>;
📝 Original message:
Hi Orfeas,
Thanks for formally modelling lightning and posting your paper here. I've
taken a brief look at the paper so far. I am a UC novice and have no
academic background so please take that into account when interpreting my
comments. In general, I am glad that you are taking the approach to model
the protocol relative to the G_ledger functionality which seems like the
right thing to do (from my amateurish view). The questions/comments I have
are:
1. When modelling things in UC the ideal functionalities should be as
simple and intuitive as possible. I found F_PayNet to be rather difficult
to follow as compared to the Sprites paper [1]. For example,
"F_PayNet checks that for each payment the charged party was one of the
following: (a) the one that initiated the payment, (b) a malicious party or
(c) an honest party that is negligent"
Why not assume that (b) never happens because a malicious party never
wants to lose the funds from a party they've corrupted and (c) never
happens because honest parties follow the protocol and check each ledger
update for malicious channel closes. Real world protocols always realise
ideal functionalities under some assumptions and these two things seem like
pretty reasonable things to include in your assumptions rather than
cluttering up your ideal functionality.
2. In both your paper and [1] I am not convinced that the ideal and real
worlds aren't easily distinguishable from each other by an Environment that
just looks at the transactions in the blockchain (G_ledger). For example,
the lightning protocol makes heavy use of pay-to-script-hash where as ideal
functionalities have no need for this. F_PayNet can just send normal
transactions. I think it would be a great idea to describe how you ensure
that the transactions that make it onto the blockchain after an execution
in the real world are indistinguishable from the ideal world.
3. On a related note, I don't understand this "receipt" mechanism. In your
protocol description of OpenChannel, Alice uses her private key which owns
UTXO(s) with x coins to create the funding transaction. This means she
received that private key as input to the execution of the protocol so that
she is able to do this (why don't you explicitly include this private key
in the OpenChannel message?). In the ideal world, the ideal functionality
should be the one with the private key signing the funding transaction
directly (in the ideal world the parties are dummy ITMs which just send
their input to the ideal functionality). But instead there is this receipt
thing which I don't understand.
Cheers
LL
[1] https://arxiv.org/pdf/1702.05812.pdf
On Wed, Jul 10, 2019 at 6:44 PM Orfeas Stefanos Thyfronitis Litos <
o.thyfronitis at ed.ac.uk> wrote:
> Hi all,
>
> The promise for fast, scalable, user-friendly and trustless use of
> bitcoin that the Lightning Network offers motivated us to author a paper
> where we formalize LN in the cryptographic framework of Universal
> Composition and prove its security. It can be found here:
> https://eprint.iacr.org/2019/778
>
> We believe that a formal proof of security was needed to specify the
> exact operating parameters that safeguard the funds and transactions of
> users against arbitrary attackers, to abstract, modularize and validate
> the underlying cryptography that is used in LN, to incorporate LN in the
> body of cryptographic protocols that have been abstracted within the
> Universal Composition framework (and thus can be safely composed and run
> in parallel) and to increase the trust of the wider community to LN. We
> view this work as a small contribution to the amazing effort that the
> Lightning community has expended both on the theoretical and the
> practical front throughout the last years.
>
> The paper is authored by my PhD supervisor Prof. Aggelos Kiayias and me.
> Any feedback will be greatly appreciated.
>
> Best regards,
> Orfeas Stefanos Thyfronitis Litos
>
> --
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
> _______________________________________________
> Lightning-dev mailing list
> Lightning-dev at lists.linuxfoundation.org
> https://lists.linuxfoundation.org/mailman/listinfo/lightning-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.linuxfoundation.org/pipermail/lightning-dev/attachments/20190718/06565966/attachment-0001.html>;