<unnamed>

Public Key

npub1dsqlkhn7edxc34rey35udpgsjdxqceh7m2xlvqte8uur2eukq45q63xycd

Profile Code

nprofile1qqsxcq0mtelvknvg63ujg6wxs5gfxnqvvmld4r0kq9un7wp4v7tq26qpzpmhxue69uhkummnw3ezumrpdejqq9qtrm

Publishing to

nostr.land

Last Notes

2023-06-09 12:55:27 GMT

- reply

📅 Original date posted:2019-07-17
📝 Original message:
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 <lloyd.fourn at gmail.com<mailto:lloyd.fourn at 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 <o.thyfronitis at ed.ac.uk<mailto: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<mailto:Lightning-dev at lists.linuxfoundation.org>
https://lists.linuxfoundation.org/mailman/listinfo/lightning-dev
--
Andrew Miller
University of Illinois at Urbana-Champaign
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.linuxfoundation.org/pipermail/lightning-dev/attachments/20190717/ef5a4974/attachment-0001.html>