<div dir="ltr">Hi Orfeas,<div><br></div><div>Thanks for formally modelling lightning and posting your paper here. I&#39;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:</div><div><br></div><div>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, </div><div><br></div><div>&quot;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&quot;</div><div><br></div><div> Why not assume that (b) never happens because a malicious party never wants to lose the funds from a party they&#39;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. </div><div><br></div><div>2. In both your paper and [1] I am not convinced that the ideal and real worlds aren&#39;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. </div><div><br></div><div>3. On a related note, I don&#39;t understand this &quot;receipt&quot; 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&#39;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&#39;t understand.</div><div><br>Cheers</div><div><br></div><div>LL</div><div><br></div><div>[1] <a href="https://arxiv.org/pdf/1702.05812.pdf" target="_blank">https://arxiv.org/pdf/1702.05812.pdf</a></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Jul 10, 2019 at 6:44 PM Orfeas Stefanos Thyfronitis Litos &lt;<a href="mailto:o.thyfronitis@ed.ac.uk" target="_blank">o.thyfronitis@ed.ac.uk</a>&gt; wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi all,<br>
<br>
The promise for fast, scalable, user-friendly and trustless use of<br>
bitcoin that the Lightning Network offers motivated us to author a paper<br>
where we formalize LN in the cryptographic framework of Universal<br>
Composition and prove its security. It can be found here:<br>
<a href="https://eprint.iacr.org/2019/778" rel="noreferrer" target="_blank">https://eprint.iacr.org/2019/778</a><br>
<br>
We believe that a formal proof of security was needed to specify the<br>
exact operating parameters that safeguard the funds and transactions of<br>
users against arbitrary attackers, to abstract, modularize and validate<br>
the underlying cryptography that is used in LN, to incorporate LN in the<br>
body of cryptographic protocols that have been abstracted within the<br>
Universal Composition framework (and thus can be safely composed and run<br>
in parallel) and to increase the trust of the wider community to LN. We<br>
view this work as a small contribution to the amazing effort that the<br>
Lightning community has expended both on the theoretical and the<br>
practical front throughout the last years.<br>
<br>
The paper is authored by my PhD supervisor Prof. Aggelos Kiayias and me.<br>
Any feedback will be greatly appreciated.<br>
<br>
Best regards,<br>
Orfeas Stefanos Thyfronitis Litos<br>
<br>
-- <br>
The University of Edinburgh is a charitable body, registered in<br>
Scotland, with registration number SC005336.<br>
<br>
_______________________________________________<br>
Lightning-dev mailing list<br>
<a href="mailto:Lightning-dev@lists.linuxfoundation.org" target="_blank">Lightning-dev@lists.linuxfoundation.org</a><br>
<a href="https://lists.linuxfoundation.org/mailman/listinfo/lightning-dev" rel="noreferrer" target="_blank">https://lists.linuxfoundation.org/mailman/listinfo/lightning-dev</a><br>
</blockquote></div>