Re: [Lightning-dev] Paper: A Composable Security Treatment of the Lightning Network
This is a really great question. You are totally right to notice that on-chain transactions are a difference between the real and ideal world and hence can lead to distinguishability... this is something we're actively working on clarifying for Sprites/SaUCy. To give a somewhat fuzzy answer of how we're approaching it: The environment is not really the "adversary", instead it's a placeholder for *honest parties* running arbitrary other protocols. I like thinking of the environment as an "app store wallet" that runs apps like lightning in a protected sandbox. While we can't prevent the adversary from seeing the transactions in the real world, we do in fact have to prevent the environment from enumerating all the transactions created by the user for security to make sense. Basically the environment needs to only run subprotocols that are isolated from each other, i.e. cannot interfere with or observe other subprotocols' on-chain transactions. Just like UC is only applicable for "subroutine respecting protocols", we need to define a similar constraint like "smart contract isolation respecting protocols" for blockchain UC to make sense. This too is a somewhat fuzzy answer we're hoping to clarify soon. Also I'm only responding since you mentioned Sprites, Orfeas may have a completely different approach / it may be handled in their paper some other way. > 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. On Wed, Jul 17, 2019 at 1:12 PM Lloyd Fournier mailto:lloyd.fo...@gmail.com>> wrote: 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 mailto:o.thyfroni...@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
Re: [Lightning-dev] Paper: A Composable Security Treatment of the Lightning Network
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.thyfroni...@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@lists.linuxfoundation.org > https://lists.linuxfoundation.org/mailman/listinfo/lightning-dev > ___ Lightning-dev mailing list Lightning-dev@lists.linuxfoundation.org https://lists.linuxfoundation.org/mailman/listinfo/lightning-dev
[Lightning-dev] Paper: A Composable Security Treatment of the Lightning Network
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@lists.linuxfoundation.org https://lists.linuxfoundation.org/mailman/listinfo/lightning-dev
