Orfeas Stefanos Thyfronitis Litos [ARCHIVE] on Nostr: 📅 Original date posted:2019-07-24 📝 Original message: -- The University of ...

📅 Original date posted:2019-07-24
📝 Original message:
--
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 <o.thyfronitis at ed.ac.uk>
To: Lloyd Fournier <lloyd.fourn at gmail.com>

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