From o.thyfronitis at ed.ac.uk Wed Jul 24 08:58:34 2019 From: o.thyfronitis at ed.ac.uk (Orfeas Stefanos Thyfronitis Litos) Date: Wed, 24 Jul 2019 09:58:34 +0100 Subject: [Lightning-dev] Fwd: Paper: A Composable Security Treatment of the Lightning Network In-Reply-To: References: Message-ID: -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. -------- Forwarded Message -------- Subject: Re: [Lightning-dev] Paper: A Composable Security Treatment of the Lightning Network Date: Thu, 18 Jul 2019 17:47:20 +0100 From: Orfeas Stefanos Thyfronitis Litos To: Lloyd Fournier Hi Lloyd, > Thanks for formally modelling lightning Thanks for the constructive questions. > I found F_PayNet to be rather difficult to follow I completely agree. F_PayNet is too complex for anyone's liking. Long story short, this was the result of: * staying in the UC model (easier said than done) * building on top of G_Ledger (with all its complexity) * the modelling of the entire LN as a single functionality (minimizing abstraction leak) * not depending on the `clock` functionality (thus not obstructing G_Ledger and other protocols that use it) * possibly many other reasons (such as me being a noob dev) FWIW, it's still much simpler than the real-world protocol Pi_LN (e.g. half its length). I'm currently exploring alternative models where e.g. there's one functionality per channel. It may make things more modular, but may also expose more gory details to the "user" of the functionality (i.e. the cryptographer who builds on top of those channels). > "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[?] In security proofs we usually let the Adversary be any polynomial machine. In particular, this includes the case where the Adversary does silly things, such as not fulfilling HTLCs. Sure, it's not a rational thing to do, but rationality is of interest in a game-theoretic analysis. (BTW, LN is a fine example of a protocol that requires both a cryptographic and a game-theoretic analysis, each of which could uncover different flaws.) We could restrict the adversary to always fulfilling the HTLCs it can, but that would immediately exile us from UC territory. > [Why not assume] (c) never happens because honest parties follow the > protocol and check each ledger update for malicious channel closes? If activated at the correct moment and with the correct command, honest parties indeed check the ledger. However, parties are activated by the Environment (another polynomial machine), which may simply refuse to activate them in time. This is why honest parties may end up being negligent. We could tie the advancement of the protocol to the clock functionality to avoid the above, but that would bring a big degree of coupling of LN with other protocols that use the clock. E.g. G_Ledger could stall because the Environment decided not to let some LN parties advance, which is very counterintuitive. > 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). Good point, it's not explained well enough in the main body, we should update the description (pp. 10-11). We indeed take care to have the exact same transactions end up on-chain in both worlds (otherwise the proof of security wouldn't work). F_PayNet checks at several moments that the ledger really contains the txs that would be there in the real world. The trick is that instead of having F_PayNet prepare all necessary transactions itself (i.e. "speak LN"), it forces the Simulator to do it by halting (and thus allowing the Environment to distinguish) in case it doesn't find the txs. > I don't understand this "receipt" mechanism. The receipt is to let the environment know which channels were successfully opened/closed and which payments were made. Importantly, it doesn't contain any keys. As such, it is unrelated to the keypair that can spend Alice's coins (the coins that Alice has before opening any channel). > In the ideal world, the ideal functionality should be the one with the > private key signing the funding transaction directly In the real world, Alice's key is created by the protocol instance when she receives REGISTER (Fig. 19, line 9), whereas in the ideal world, this key is created by the Simulator when it receives REGISTER from F_PayNet (Fig. 40, line 5). It's a bit counterintuitive on first thought, but F_PayNet shouldn't be managing private keys or doing signatures. It should just ensure that Alice's public key contains the promised coins upon channel closing. Note that our approach is different from that mentioned by Andrew Miller. Since we ensure that on-chain txs are the same in both worlds, we don't need to hide the ledger contents from the Environment. Let me know if I left anything unclear, or if you have further observations/corrections/questions. Best, Orfeas