Winning the War by (Strategically) Losing Battles: Settling the Complexity of Grundy-Values in Undirected Geography

I.   Introduction

Blockchain technologies are emerging as a revolutionary paradigm to perform secure decentralized financial applications. Nevertheless, a widespread adoption of cryptocurrencies, such as Bitcoin ^[1] and Ethereum ^[2], is severely hindered by their inherent limitations on transaction throughput ^[3],[4]. For instance, while Bitcoin can support tens of transactions per second and the confirmation time is about an hour, traditional credit networks like Visa can comfortably handle up to 47,000 transactions per second.

Off-chain protocols ^[5] are recognized as one of the most promising scalability solutions, achieving a seemingly contradictory property: the bulk of transactions is performed off-chain, and yet in a secure fashion. The idea is to leverage the blockchain only in case of disputes, resorting otherwise to off-chain, peer-to-peer transactions. Bitcoin's Lightning Network ^[6] is the most widely adopted off-chain instantiation, hosting at the time of writing bitcoins worth more than 170M USD, in a total of more than 27,000 nodes and more than 76,000 channels. In a nutshell, parties deposit money in a shared address, called channel, and can later on perform arbitrarily many off-chain transactions with each other by redistributing the deposit on the channel. In the end, the channel can be closed and the latest state (i.e., deposit distribution) is posted on-chain. Off-chain transactions are not limited to the end-point of the channel, but they can be routed over paths of channels (so-called multi-hop payments). Besides such payment channel networks, an entire ecosystem of off-chain protocols ^[5] (virtual channels, watchtowers, payment-channel hubs, state channels, side-chains, etc.) is under development for Bitcoin ^[7]–^[12], Ethereum ^[13]–^[16], as well as other cryptocurrencies ^[17].

The cryptographic protocols underlying these off-chain constructions are rather sophisticated and, most importantly, rely on game-theoretic arguments to discourage malicious behavior. For instance, the Lightning Network relies on a punishment mechanism to disincentivize parties to publish old states on-chain and on an unlocking mechanism where parties first pay a neighbor and then retrieve the paid amount from the other to ensure the atomicity of multi-hop payments (i.e., either all channels are consistently updated or none is).

Off-chain protocols are typically subject to rigorous security analyses, which however concentrate on cryptographic properties and do not capture the game-theoretic ones. In particular, most protocols are proven secure in the Universal Composability framework ^[18], proving that the cryptographic realization simulates the ideal functionality. This framework, however, was developed to reason about security in the classical honest/Byzantine setting: in particular, the ideal functionality has to model all possible parties' behavior, rational and irrational, otherwise it would not be simulatable, but reasoning on whether or not certain behavior is rational is outside of the model and thus left to informal arguments. This is not just a theoretical issue, but a practical one, as there is the risk to let attacks pass undetected: for instance, the Wormhole attack ^[7] constitutes a rational behavior in the Lightning Network, which is thus admitted in any faithful model thereof although it undermines its incentive mechanism. The first step towards closing this gap in cryptographic proofs is to come up with a faithful game-theoretic model for off-chain protocols in order to reason about security in the presence of rational parties. We address this challenge in this paper, advocating the use of Extensive Form Games (EFGs) for the game-theoretic security analysis of off-chain protocols. In particular, we introduce two instances of EFGs to model the closing and the routing of the Lightning Network.

A. Related Work

A game-theoretic model for off-chain protocols is initiated and introduced in ^[19]. This work suffers, however, from several limitations, which make it unsuitable to conduct faithful security analyses. Firstly, the game model considers only honest closing of channels, i.e., all deviations - such as posting an old state - are ignored: this makes it impossible to reason about the security of basic channel operations. Secondly, the pay-offs are represented as constants, which neglects the dependency of the channel's balance on its security properties. Further, fees are not considered at all, thereby ignoring their impact on Lightning protocols. For instance, the routing game to model the security of multi-hop payments fails to capture already identified attacks in payment channel networks, like the Wormhole attack ^[7] that targets the fee distribution among players. Additionally, Lightning is vulnerable to the Griefing attack ^[20], where a significant amount of money is locked. In our work, we overcome the aforementioned limitations, by defining a stronger closing phase model, by aligning the utilities to the monetary outcome, by considering all possible deviations of parties during closing, and by revising the relevant security properties. We demonstrate the importance of precision in game-theoretic protocol models by modeling the Wormhole attack, as well as the Griefing attack.

Our work further complements other game-theoretic advancements in the area, most prominently the following lines of research.

1. Incentivizing Watchtowers: A major drawback of payment channel protocols is that channel participants must frequently be online and watch the blockchain to prevent cheating. To alleviate this issue, the parties can employ third parties, or so-called watchtowers, to act on their behalf in case their counterparty misbehaves. Correctly aligning the incentives of watchtowers to yield a secure payment channel protocol is, however, challenging. This is the main focus of several works ^{[11],[15],[16],[21]}. As their objective is to incentivize external parties, their models does not apply in our work.
2. Payment Channel Network Creation Games: Avarikioti et al. ^[22],[23] study payment channel networks as network creation games. Their goal is to determine which channels a rational node should establish to maximize its profit. Ersoy et al. ^[24] undertake a similar task; they formulate the same problem as an optimization problem, show it is NP-hard, and present a greedy algorithm to approximate it. Similarly to our work, all these works assume rational participants. However, we aim to model the security of the protocols, in contrast to these works that study the network creation problem graph-theoretically.
3. Blockchains with Rational Players: Blockchains incentivize miners to participate in the network via monetary rewards ^[1]. Therefore, analyzing blockchains under the lens of rational participants is critical for the security of the consensus layer. There are multiple works in this direction: Badertscher et al. ^[25] present a rational analysis of the Bitcoin protocol. Eyal and Garay ^[26] introduce an attack on the Nakamoto consensus, effectively demonstrating that rational miners will not faithfully follow the Bitcoin protocol. This attack is generalized in ^[27],[28]. Consequently, Kiayias et al. ^[29] analyze how miners can deviate from the protocol to optimize their expected outcome. Later, Chen et al. ^[30] investigate the reward allocation schemes in longest-chain protocols and identify Bitcoin's allocation rule as the only one that satisfies a specific set of desired properties. On a different note, several works study the dynamics of mining pools from a game-theoretic perspective ^[31],[32] or introduce network attacks that may increase the profit of rational miners ^[33],[34]. An overview of game-theoretic works on blockchain protocols can be found in ^[35].

All these works, however, focus on the consensus layer (Layer-1) of blockchains and as both the goals and assumptions are different from the application layer (Layer-2), the models introduced there cannot be employed for our purposes. For instance, payment channel protocols occur off-chain and thus game-based cryptographic assumptions of the blockchain do not apply. In addition, consensus protocols investigate the expected reward of miners which is a probabilistic problem, whereas we ask if any honest player could lose money, which depends on the behavior of the other players and is fundamentally deterministic.

Game-based definitions have also been proposed for the security analysis of smart contracts ^[36],[37]. These models, however, target an on-chain setting and are thus not suitable to reason about the specifics of off-chain constructions (e.g., closing games, routing games, etc.).

B. Our Contributions

In this work, we take the first steps towards closing the gap between security and game-theoretic analysis of off-chain protocols. Specifically, we introduce the first game-theoretic models that are expressive enough to reason about the security of off-chain protocols. We model off-chain protocols as games and then analyze whether or not certain security properties are satisfied. The design of our models is driven by two principles: (a) all possible actions should be represented and (b) the utility function should mirror the monetary outcome realistically. We aim to ensure that honest participants do not suffer any damage (P1), whereas deviating from the protocol yields a worse outcome for the adversary (P2) We will use weak immunity (Definition II.4) to implement (P1), and collusion resilience (Definition III.8) together with practicality (Definition III.7) for (P2). While we believe that our approach of implementing principles (a) and (b) is easily extensible to other off-chain protocols, in this work we focus on the Bitcoin Lightning Network, which constitutes the most widely adopted off-chain protocol. Our technical contributions can be summarized as follows:

• We refine existing game-theoretical concepts in order to reason about the security of off-chain protocols (Section III).
• We introduce the Closing Game $G_{c}$, the first game-theoretic security model that accurately captures the closing phase of Lightning channels, encapsulating arbitrary deviations from the protocol specification (Section IV).
• We perform a detailed security analysis of $G_{c}$, formalize folklore security corner cases of Lightning, and present the strategy that rational parties should follow to close their channels in order to maximize their expected out-come relative to the current and previous distribution states (Section V).
• We identify limitations in prior work ^[19] on game-based modeling of multi-hop payments, putting forward a new game-based definition that is precise enough to cover the Wormhole and the Griefing attack (Section VI). We further show how to model Fulgor protocol ^[38], a variant of Lightning's routing that prevents the Wormhole attack. Our formalization leverages game theory concepts introduced in Section III and Section IV, thereby demonstrating the theoretical expressiveness of our framework to analyze complex protocols..

In conclusion, our work brings game-theoretical foundations to enforce security of off-chain protocols, by providing a rigorous analysis over security properties expressed through formal requirements over game strategies. We believe, the provided rigor in our paper opens up new venues for automating security analysis via game-theoretic arguments, a challenge which we aim to tackle in future work.¹

II.   Background and Preliminaries

A. Payment Channel Networks

A payment channel ^[8] can be seen as an escrow (or multi-signature), into which two parties Alice $A$ and Bob $B$ transfer their initial coins with the guarantee that their coins are not locked forever and the agreed balance can be withdrawn at any time. After that, $A$ and $B$ can pay each other off-chain by signing and exchanging messages that reflect the updated balances in the escrow. These signatures can be used at any time to close the channel and distribute the coins on-chain according to the last channel state. In order to discourage parties from posting an old state on-chain, a punishment mechanism is in place. In particular, in Lightning ^[6], once $A$ closes the channel, she has to wait a mutually agreed time before getting her coins. Meanwhile, $B$ has the opportunity to withdraw all the coins in the channel (by posting a so-called revocation transaction), including the ones assigned to $A$, if the state posted on-chain by $A$ is not the last one they mutually agreed on. Such a punishment mechanism is of game-theoretic nature: parties can indeed post an old state on-chain, yet they are discouraged to do so.

In particular, Lightning payment channels operate as follows: First, Alice and Bob create a funding transaction where they input their respective coins; the funding transaction has a single output that can only be spent if both $A$ and $B$ provide their signature (2-out-of-2 multi-signature). Then, the two parties create the first commitment transaction, i.e., a transaction that spends the output of the funding transaction and returns the initial coins to both parties. In other words, the input of the commitment transaction is the output of the funding transaction while the output of the first commitment transaction is two-fold: the first output returns the coins to $A$ and the second output to $B$. However, the commitment transaction each party holds is not the same. Specifically, the commitment transaction of $A$ has an additional spending condition, a timelock $t$ that signifies the revocation period and is pre-agreed between the two parties; in $A$'s commitment transaction $B$'s output is spendable immediately. Symmetrically, in $B$'s commitment transaction $B$'s output has a timelock $t$ while $A$'s output is spendable immediately. Note that a timelock $t$ is a condition that allows the coins of the output to be spent on-chain only after time $t$ has elapsed from the publication of the transaction. After $A$ and $B$ sign and exchange the respective first commitment transactions, they proceed to signing the funding transaction and publishing it on-chain. This order is important to avoid hostage situations². As soon as the funding transaction is securely published on-chain, $A$ and $B$ can transact off-chain by creating every time a new commitment transaction that depicts the current balance of the joint capital among the two parties. Every time a new commitment transaction is created, the parties reveal a secret to their counterparty that allows their counterparty to spend their own coins immediately (e.g., $A$ can spend $B$'s coins from the previous commitment) if the previous commitment transaction appears on chain (revocation transaction). To close a Lightning channel, the two parties can either collaborate and spend the output of the funding transaction, or each of them can close the channel unilaterally by publishing the last commitment transaction. Since the commitment transactions each party hold have a timelock, in case of cheating, i.e., publication of a previous commitment transaction on-chain, the counterpart can immediately spend the cheating party's coins, claiming all the coins of the channel, thus punish the cheating party for misbehaving.

Technically, $A$ and $B$ do not just lock their initial funds but also a certain small amount which will be used as a fee for the closing transaction of the channel. Note that every on-chain transaction requires such a fee $f$. The fee for the opening transaction is paid upon the opening of the channel and is thus irrelevant to our consideration. However, in case $A$ posts an old state on-chain and $B$ performs the revocation transaction - which is an on-chain transaction - to prove it, $B$ has to carry the additional transaction fee alone. These facts have an important impact on our game-theoretic models.

In the following, we refer to honest closing when a party unilaterally closes the channel by posting the last commitment transaction or when the parties close collaboratively, where both parties sign to spend the funding transaction output directly.

Fig. 1.Fig. 1. Routing in lightning using htlcs.

Off-chain transactions are not limited to the end-points of a channel, as they can be performed whenever sender and receiver are connected by a path of channels with enough capacity. The cryptographic approach to do so exploits hash-time-locked-contracts (HTLC) ^[12]. Assume players $A$ and $B$ do not share a channel. Instead, $A$ has a channel with $E_{1};\ E_{1}$ has a channel with $I;\ I$ has a channel with $E_{2}$; and $E_{2}$ has a channel with $B$, as illustrated in Figure 1. Player $A$ can now send an amount $m$ to player $B$ via the intermediaries $E_{1},I$ and $E_{2}$, where each intermediary charges a fee $f$ for the routing service, hence $A$ should pay $m+3f$. The core idea is that $A$ pays $E_{1},\ E_{1}$ pays $I$, and so forth, until $B$ gets paid.

A key security property in multi-hop payments is atomicity: either all payments are successful, and the deposit in each channel is updated accordingly, or none is. To achieve this property, the Lighting protocol proceeds as follows. First, the receiver $B$ generates a secret $x$ and sends its hash $h(x)=y$ to the sender $A$ (see action 1 in Figure 1). Then $A$ creates an HTLC for $E_{1}$, where she locks $m+3f$ with lock $y$ and time-out $t_{1}$. That means only $E_{1}$ can claim the money and only by providing a value whose hash is $y$ within time $t_{1}$ (action 2 in Figure 1). Although $E_{1}$ does not know such a value yet and can therefore not unlock, $E_{1}$ can nevertheless proceed by creating another HTLC for $I$ also locked with $y$ and a time-out $t_{2}$ (action 3 in Figure 1). Thereafter, $I$ and $E_{2}$ continue in the same way (actions 4 - 5 in Figure 1). Actions 1 - 5 of Figure 1 are called the locking phase . Note that in order to allow everybody to unlock their HTLCs in the subsequent steps, the time-outs have to be decreasing $t_{1} > t_{2} > t_{3} > t_{4}$. Once $B$ receives the conditional payment, he can reveal $x$ to $E_{2}$ and the conditional payment is unlocked (action 6 in Figure 1). The others can now unlock the HTLCs one after the other from right to left (actions 7 - 9 in Figure 1), which is called the unlocking phase . Finally, $A$ paid $m+3f,\ B$ received $m$ and each intermediary was rewarded with $f$.

We note that atomicity is achieved by a game-theoretic argument: intermediaries can, in principle, stop the protocol either in the locking phase or in the unlocking phase. In the former, they would lose the transaction fee $f$, while in the latter, they would lose the payment amount $m, m+f, m+2f$ respectively. Thus, they are incentivized to act once they have committed to participate.

a) The Wormhole Attack

The aforementioned routing protocol is proven to be vulnerable to the Wormhole attack ^[7], which is depicted in Figure 2. The attack is as follows: $E_{1}$ and $E_{2}$ collude, and bypass $I$ in the unlocking phase, thus stealing $I^{\prime}\mathrm{s}$ participation reward $f$. Until actions 6 in Figure 1 and Figure 2, the behavior is identical. Then, $E_{2}$, knowing $x$, forwards $x$ to $E_{1}$ (offline) instead of unlocking the HTLC from $I$ (action 7 in Figure 2). This way, $E_{1}$ can unlock $A^{\prime}\mathrm{s}$ HTLC and claim the money (action 8), but $I$ will never be able to unlock. After a certain time the remaining HTLCs time-out and the locked money returns to the creators.

Fig. 2.Fig. 2. Wormhole attack in lightning.

Therefore, the parties $A$ and $B$ are not affected. However, $E_{1}$ and $E_{2}$ collectively earn $3f$ instead of the $2f$ they deserve, stealing the fee $f$ from $I$, who locked resources in the locking phase of the protocol. This attack undermines the incentive of intermediaries to route payments.

b) The Griefing Attack

It describes the scenario when a player, assume $B$ for simplicity, ignores the proposed payment and refuses to proceed ^[20]. This way, money is locked in the conditional payments for a considerable amount of time. While ^[40] studies the Griefing attack through probabilistic modelling and ^[41] provides mitigation techniques, to the best of our knowledge there is no formal security analysis of this attack at present. Our work addresses this limitation and shows that Lightning's routing module is indeed susceptible to the Griefing attack.

In the sequel we consider the behavior as illustrated in Figure 1 as the only honest routing behavior.

B. Game-Theoretic Definitions

We now introduce the game-theoretic concepts relevant for our formalization. We denote real numbers by $\mathbb{R}$ and tuples as $\sigma=(\sigma_{1},\ldots,\sigma_{n})$. We write $\sigma[\sigma_{i}^{\prime}/\sigma_{i}]$ to denote the tuple resulting from substituting $\sigma_{i}$ by $\sigma_{i}^{\prime}$ in $\sigma$, that is $\sigma[\sigma_{i}^{\prime}/\sigma_{i}]= (\sigma_{1},\ldots,\sigma_{i-1},\sigma_{i}^{\prime},\sigma_{i+1},\ldots,\sigma_{n})$. We understand games as static objects in which finitely many players can choose finitely many times from a finite set of actions. A game yields a certain positive or negative utility for each player. We briefly overview the very common Normal Form Games, also called Strategic Games ^[42], in which each player chooses an action only once , called strategy.

In what follows we fix an arbitrary game $\Gamma$ and give all definitions relative to it. To formalize an optimal outcome on game strategies, we use Nash Equilibria.

Another important concept is weakly dominated strategies , expressing the strategies a rational player would not play since they yield worse utilities.

Applying Definition II.2, the joint strategies $(C,C),\ (U,\Im)$ and $(\Im, U)$are Nash Equilibria: for each of these joint strategies, neither $A$nor $B$can deviate in order to increase their own utility. Comparing the second and the third row of Table I, we see that $A$'s utility is always as least as good in the second row as it is in the third row. Hence, strategy $C$weakly dominates strategy $\Im$for player $A$, by Definition II.3; the same property also holds for player B. By comparing the other pairs of rows/columns of Table I, we see that there is no other weak dominance in $\Gamma_{C}$.

C. Game-Theoretic Security Properties of Off-Chain Protocols

We now present existing game-theoretic concepts ^[19],[42] implying security properties of off-chain protocols. In Section III, we extend these concepts towards another type of games, called Extensive Form Games, enabling our security analysis in Section IV. We focus on two security properties ensuring that (P1) honest players do not suffer damage, and (P2) subgroups of rational players do not deviate from a respective strategy. A protocol is compliant to these properties, if the strategy implementing the intended behavior satisfies them; we call such a strategy an honest strategy .

(P1) No Honest Loss . As the utility function of a game is supposed to display the monetary and intrinsic value of a certain joint strategy, property (P1) is expressed using weak immune strategies defined next.

(P2) No Deviation . Even though the concept of Nash Equilibria seems to be a good candidate to ensure (P2) at first glance, they have two crucial shortcomings. First, a Nash Equilibrium only ensures that a single player cannot profit from deviating, but does not imply that two or more players cannot do so. Second, there might be Nash Equilibria, which are weakly dominated by another strategy for a specific player. Such Nash Equilibria will therefore not be played by rational parties and hence should not be considered to satisfy (P2).

The solution proposed for NFGs in ^[19] is to consider strategies $\sigma$ compliant to (P2), if they are both strongly resilient (fixing the former shortcoming) and practical (fixing the latter) as defined subsequently.

Strong resilience extends Nash Equilibria by considering deviations of multiple players.

We note that in games with two players (i.e. two-player games), strong resilience and Nash Equilibrium are identical. As such, in $\Gamma_{C}$ from Table I, the joint strategies $(C,C),\ (U,\Im)$ and $(\Im, U)$ of Example II.1 are also strongly resilient.

To define practicality of a strategy, we first introduce the concept of iterated deletion of weakly dominated strategies (IDWDS) .

Definition II.6 (Iterated Deletion of Weakly Dominated Strategies - IDWDS)

The iterated deletion of weakly dominated s trategies (IDWDS) of an $NFG\ \Gamma$is defined as iteratively rewriting $\Gamma$by omitting all weakly dominated strategies of all players. This is repeated until no strategy is weakly dominated any more. The resulting game $\Gamma^{\prime}$is thus a subgame of $\Gamma$.

Table II Nfg $\Gamma_{C}^{\prime}$ obtained from idwds over table I.

Note that, when IDWDS is applied to a game $\Gamma$, then every Nash Equilibrium of the resulting game $\Gamma^{\prime}$ is also a Nash Equilibrium of $\Gamma$. Since all weakly dominated strategies of every player are removed at each step, the generated game is unique. Details and proofs can be found in ^[42].

We now define practical strategies, in order to ensure that no single strategy is weakly dominated at any iteration.

Note that there are no weakly dominated strategies in $\Gamma_{C}^{\prime}$. Thus, any Nash Equilibrium of $\Gamma_{C}^{\prime}$is also practical strategy of $\Gamma_{C}$. By comparing utilities, we derive that the only Nash Equilibrium of $\Gamma_{C}^{\prime}$is the joint strategy $(C,C)$.

An alternative approach for expressing (P2) is by requiring a strategy $\sigma$ to be both a strong Nash Equilibrium (a property similar to SR ) and practical, instead of SR and practical.

A detailed comparison of the various concepts ensuring (P2) including their strengths and weaknesses, is given in Section III.

III.   Efg-Based Modeling of Off-Chain Protocols

So far we considered games in which each party takes only one action. We now extend our definitions to handle adaptive strategies, i.e., games in which parties take several actions and choose at each step which action to take based on the actions previously chosen by other parties. As we will see, this is necessary for faithfully modeling off-chain protocols and overcoming the limitations of previous work ^[19]. For that, we overview the concept of extensive form games (EFGs) in Section III-A. We show how to lift NFG-based security definitions to EFGs in Section III-B. Finally, we show that these definitions do not yet suffice to yield an accurate security model of off-chain protocols, and introduce a refined security definition based on the concept of collusion resilience in Section III-C.

A. Extensive Form Games (efg)

To formalize strategies where players make multiple choices one after the other, we advocate the usage of Extensive Form Games (EFGs) ^[42], which extend NFGs as follows.

• The set $\mathscr{H}$of histories is a set of sequences of actions with

1. $\emptyset\in \mathscr{H}$;
2. if the action sequence $(a_{k})_{k=1}^{K}\in \mathscr{H}$ and $L < K$, then also $(a_{k})_{k=1}^{L}\in \mathscr{H}$;
3. a history is terminal $(a_{k})_{k=1}^{K}\in\mathscr{T}$, if there is no action $a_{K+1}$with $(a_{k})_{k=1}^{K+1}\in \mathscr{H}$.

• The next player function $P$

1. assigns the next player $p\in N$to every non-terminal history $(a_{k})_{k=1}^{K}\in \mathscr{H}\backslash \mathscr{T}$, that is $P((a_{k})_{k=1}^{K})=p$;
2. after a non-terminal history $h=(a_{k})_{k=1}^{K}\in \mathscr{H}$it is player $P(h)^{\prime}s\ turn$to choose an action from the action set $A(h)=\{a:(h,a)\in \mathscr{H}\}$.

$A$ strategy of player $p$is a function $\sigma_{p}$mapping every $h\in \mathscr{H}$with $P(h)=p$to an action from $A(h)$. Formally , $$\begin{equation*}\sigma_{p}:\{h\in \mathscr{H}:P(h)=p\}\rightarrow\{a:(h,a)\in \mathscr{H},\forall h\in \mathscr{H}\},\end{equation*}$$ such that $\sigma_{p}(h)\in A(h)$. The set of all strategies of a player $p$ is $\mathscr{S}_{p}$, and the set of all joint strategies is $\mathscr{S}=\times _{p\in N}\mathscr{S}_{p}$.

Note that the set of terminal histories $\mathscr{T}$ is uniquely determined by $\mathscr{H}$ and therefore does not explicitly occur in the tuple $\Gamma$. Since histories $h$ are just sequences of actions $h=(a_{k})_{k=1}^{K}=(a_{1},\ldots,a_{K})$, we denote histories by the variable $h$, the abstract sequence $(a_{k})_{k=1}^{K}$, or the explicit sequence $(a_{1}, \ldots,a_{K})$, depending on the context in which they are used. We note that EFGs can conveniently be represented as trees, as described below.

Let us illustrate EFGs and their tree-based representation through the following example.

Fig. 3.Fig. 3. An efg $\Gamma_{E}$.

As depicted in the tree-based representation of Figure 3, we note that the utility of joint strategies in an EFG is uniquely determined by their associated history (i.e., path). In the context of EFGs, the concept of Nash Equilibria remains as given in Definition II.2. In addition to Nash Equilibria, another useful concept for EFGs is the Subgame Perfect Equilibrium , which we will use to characterize the strategies played in practice by rational parties. To this end, we first introduce the notion of subgames of EFGs. A subgame of an EFGs can be seen as a subtree determined by a certain history (i.e., whose root note is the last history node), and is formalized below.

By adjusting the concept of Nash Equilibrium to subgames, we derive the following property of joint strategies.

B. Efg Extensions for Security Properties

While EFGs enable us to incorporate choices made at different times yielding different options for the next player, they come with the following limitation. The intended (i.e., honest) behaviors in off-chain protocols only specify a terminal history (i.e., a path from root to leaf), rather than a strategy. For instance, an honest history may specify to close the channel collaboratively, but it does not capture a player's behavior once a player deviated. To address this limitation, we introduce the following notion of an extended strategy in EFGs.

While EFGs can in principle be translated to NFGs, as explained in ^[43], analyzing the security properties (P1)-(P2)over the translated NFGs may yield unexpected results. We shortly exemplify this point in Example III.4, but similar issues occur also in larger games. We thus lift NFG-based definitions to EFGs, enabling the analysis of (P1) and (P2). Since EFGs have a utility function just as NFGs do, which assigns values after the game, the NFG concepts of weak immunity, strong resilience and sNE remain the same for EFGs.

Practicality in NFGs, however, relies on IDWDS, which fails to incorporate the sequential nature of EFGs, and hence must be adjusted for EFGs. This is because NFG actions happen simultaneously, while EFG players choose their actions sequentially. We first present an example to showcase that applying the NFG definition of practicality to an EFG, by using its translation to an NFG, leads to overlooking rational strategies.

Example III.4

Let us consider the $EFG\ \Gamma_{E}$from Figure 3 with two players $A$and B. The compact translation of $\Gamma_{E}$to an $NFG\ \Gamma_{N}$is given in Table III. Histories of Figure 3, where players choose twice, such as $(b,d,f)$, are translated to Table III as the joint strategy $(b;f,d)$. Hence, the $NFG$strategy $b;f$of player $A$means choosing action $b$first, and, if A gets to choose again , $A$takes $f$. Player $A^{\prime}s$strategies are displayed in the rows, whereas player $B^{\prime}s$are shown in the columns of Table III. Strategy $d;g$for example denotes choosing $d$in the first turn and $g$in the second turn, unless the game ends before. For readability, strategies with identical utilities in any case are merged together, e.g., having only a instead of both $a;e$ and $a;f$.

Table III Compact view of $\Gamma_{E}$, TRANSLATED TO AN NFG $\Gamma_{N}$.

According to definition of practicality for NFGs (see Definition II.7), the only practical strategy in $\Gamma_{N}$ is $(a, d;i)$, which results in a utility of (2,2). This is because for $A$strategy $b;e$weakly dominates $b;f$and for $B$strategy $d;i$weakly dominates both $c$ and $d;g$. After deleting those (in blue), the red strategy $b;e\ of\ A$becomes weakly dominated by $a$. Thus, after removing $b;e$only the joint strategy $(a,d;i)$remains and is therefore a Nash Equilibrium of the resulting game .

However, in the $EFG\ \Gamma_{E}$the comparison of strategies has a certain order, as not all choices are made simultaneously. Thus, when it comes to $B$choosing between option $c$ and $d$, choosing $c$is also a rational action because in any case $B$gets utility 1. This is the case, since the subgame following after $d$, will end in the subgame perfect and practical (1,1), if played by rational players. Following this argumentation, we claim that $(b;e,c)$, yielding history $(b,c)$should also be considered rational and thus practical .

Example III.4 demonstrates that it is advisable to adapt the NFG concept of practicality for EFGs, and that a näive application can be problematic since information may be lost during the transformation from EFG to NFG ^[42]. We therefore propose to use subgame perfect equilibria for comparing EFG strategies, and define practicality for EFGs as follows.

C. Security Strategies for Off-Chain Protocols

We now leverage the previously introduced EFG-based definitions (Section III-B1) to faithfully model the security of off-chain protocols. In particular, we propose the novel concept of collusion resilience for addressing (P2), and compare it to existing formalizations of property (P2).

In ^[19], strong resilience and practicality were used to model the no deviation property of (P2): We identify unwanted properties of strong resilience and we thus investigate variations of it. Specifically, we show that strong Nash Equilibria do not imply strong resilience nor vice-versa (Lemma III.1), and therefore define the collusion resilience property of a joint strategy. Intuitively, collusion resilience considers the sum of the utilities of the deviating parties, since rational players may collude or be controlled by the same entity.

In addition, we also consider a slight adaption of strong resilience, $\mathsf{SR}_{\subseteq}$, where the deviation of the entire set of players $N$ is also allowed, as it is for sNE.

We now formalize how the resilience properties relate to each other, which motivates our definition of (P2).

The next example further motivates why we decided to formalize (P2) in terms of collusion resilience .

Let us study $\Gamma_{1}$first. There are three players $P_{1}$on the left , $P_{2}$in the “3rd dimension” who only has one possible strategy, and $P_{3}$at the top. Let us consider the joint strategy $\sigma=(H_{1},H_{2},H_{3})$. Since $P_{2}$does not have another choice , $P_{2}$can never deviate. Player $P_{1}$deviating alone yields the same utility as $\sigma$and is thus irrelevant. The same holds for $P_{3}$. The only deviation that makes a difference, is if $P_{1}$ and $P_{3}$change strategy together to $(D_{1},H_{2},D_{3})$. By doing so , $P_{1}$profits and receives 5 instead of 1, but $P_{3}$looses by getting -2 instead of 1. Thus , $P_{3}$does not have an incentive to do so, unless the two players collude for their mutual benefit and share their payoffs. This way they receive 1.5 each instead of 1 each, which poses a serious thread to $\sigma$and should thus not be considered satisfying (P2). However , $(H_{1},H_{2},H_{3})$ is $sNE$since $P_{3}$has no incentive in deviating with $P_{1}$, if their utilities are not shared, but it is not $CR$since $$\begin{align*}2 & = u_{P_{1}}(H_{1}, H_{2}, H_{3})+ u_{P_{3}}(H_{1}, H_{2}, H_{3}) \tag{9}\\ & < u_{P_{1}}(D_{1}, H_{2}, D_{3})+ u_{P_{3}}(D_{1}, H_{2}, D_{3})=3. \tag{10}\end{align*}$$

In the similar game $\Gamma_{2}$, on the contrary , $P_{3}$has no incentive in deviating from $\sigma=(H_{1},H_{2},H_{3})$together with $P_{1}$, also if their utilities are shared. Such a deviation yields 0.5 each, instead of 1 each in $\sigma$. Hence, there is no incentive to change strategy for one or more players and therefore $(H_{1},H_{2},H_{3})$should be considered satisfying (P2). Nevertheless, according to Definition II.5, $(H_{1},H_{2},H_{3})$is not $SR$since at least one of the deviating parties $P_{1}, P_{3}$profits from choosing $(D_{1},H_{2},D_{3})$, although $P_{3}$has no reason to play along. However, in $\Gamma_{2},(H_{1},H_{2},H_{3})$ is $CR$as $$\begin{align*}2 & = u_{P_{1}}(H_{1}, H_{2}, H_{3})+ u_{P_{3}}(H_{1}, H_{2}, H_{3}) \tag{11}\\ & \geq u_{P_{1}}(D_{1}, H_{2}, D_{3})+ u_{P_{3}}(D_{1}, H_{2}, D_{3})=1. \tag{12}\end{align*}$$

We conclude this section by defining secure game strategies/histories, as follows.

When discussing security in the setting of EFGs, we are interested mainly in assessing whether a history is secure, as the protocol only defines an honest history instead of a full strategy. By applying Definition III.5, we state the following security characterization.

We note that we do not have to find a secure extended strategy for the history to be secure, as aiming for one joint secure strategy in an EFG would be unnecessarily restrictive. Instead, our goal is to make sure that rational parties follow the honest history, no matter what their actual strategy is. In particular, an honest player follows the honest history by default, a rational player does so because of practicality and collusion resistance. Weak immunity further ensures that honest players as well as rational one cannot be damaged by Byzantine players while following the honest history. Hence, the strategy each player has in mind does not matter, since in a secure protocol weak immune, practical, and collusion resistant, strategies are overlapping along the honest history. This is the case because in Definition III.11 we require $\sigma_{1},\sigma_{2}$, and $\sigma_{3}$ to all yield the same history, namely $\beta$. We can therefore admit that an honest player has a weak immune strategy in mind, while a rational player has a practical one, as long as these overlap on the honest history.

IV.   Closing Games of Off-Chain Protocols

We now define a new two-player EFG, called the Closing Game $G_{c}$, in order to model closing phase properties of off-chain protocols, in particular of the Lightning Network. As explained in Section II-A, to close a channel a party can unilaterally publish a channel state on-chain, which does not necessarily have to be the latest one. The one who closes, however, has to wait a certain amount of time until the money can be used. Meanwhile, the other party can steal all the money from the channel in case the state published on-chain is not the latest one: this ensures that rational players close their channel only with the latest state. Alternatively, the parties can collaboratively sign a new transaction to split the money. In this case no one has to wait.

Our closing game overcomes the limitations of previous work ^[19] in representing dishonest closing attempts, by modeling how closing can be achieved after a failed collaborative closing attempt and by also considering the additional fee $f$ to be paid in a revocation transaction.

To the best of our knowledge, our closing game $G_{c}$ is the most accurate model for the security analysis of off-chain protocols, notably of the Lightning Network. In our model of the closing phase we make the following assumptions for $a$ channel between $A$ and $B$ at the moment where the closing phase is initiated.

• The fair split of the channel's funds is $a\rightarrow A, b\rightarrow B$ and $a > 0, b > 0$.
• The benefit of closing the channel is $\alpha$. Closing a channel yields a benefit, since it unlocks assets.
• The opportunity cost of having to wait for one's funds upon closing is $\varepsilon$.
• When both players agree to update the channel we assume $a$ fair deal in the background which yields a profit of $\rho$ for both parties.
• Publishing a revocation transaction on-chain costs a fee $f > 0$.

Further, to properly model utilities in the closing game $G_{c}$, we define the following total order, which is crucial for analyzing security properties of $G_{c}$. For capturing total order properties in the setting of $G_{c}$, we extend the set $\mathbb{R}$ of real numbers by the infinitesimal numbers $\alpha,\ \varepsilon$ and $\rho$.

In general, unlocking funds gives additional financial freedom even if there is some processing delay; therefore, we choose $\varepsilon\prec\alpha$ in Definition IV.1. Additionally, once the parties initiate the closing phase, it is reasonable to assume that no potential update significantly benefits both parties. In contrast, both parties are interested in avoiding the opportunity cost, i.e., the cost of having to wait for their funds upon closing, therefore, we set $\rho\prec\varepsilon$ in Definition IV.1.

Based on the utility ordering of Definition IV.1, we introduce our Closing Game for Player $A$ below.

Note that the utility function $u$ of $G_{c}(A)$ in Figure 4 assigns player $p\in N$ the money player $p$ received minus the money player $p$ deserved based on the latest channel state. The values of closing $(\alpha)$, updating $(\rho)$ and waiting $(-\varepsilon)$ are also considered in Figure 4. As discussed in Section II-A, the fee needed for the closing transaction is assumed to have been reserved among the locked funds in the channel all the time and is spent upon closing, therefore not affecting the players' channel balance.

The closing game for player $B,\ G_{c}(B)$ is defined similarly to $G_{c}(A)$, with the roles of $A$ and $B$ being swapped in Definition IV.2. Based on the closing games $G_{c}(A)$ and $G_{c}(B)$, we consider the closing phase in an off-chain channel as given in Figure 5 and defined below.

Fig. 4.Fig. 4. Closing game $G_{c}(A)$.

V.   Closing Games for Secure Lightning Channels

We now show that the closing games from Definition IV.2 precisely capture secure closing phases in Lightning channels ^[6]. Namely, the following two terminal histories of closing games model the honest behavior of Lightning: (i) history $(H)$ from Figure 4 represents unilateral honest closing of $A$, yielding utility $(\alpha-\varepsilon, \alpha)$; and (ii) history $(C_{h},S)$ captures the attempt of $A$ to close collaboratively and honestly, while $B$ signs, with a utility of $(\alpha, \alpha)$. Our security analysis focuses on these two honest histories of Lightning channels.³

Fig. 5.Fig. 5. Closing phase $\Gamma_{C}$.

In the following, the values $d_{A}$ (resp. $d_{B}$) defined in Table VI (line $D$) represent the difference of funds between the latest state and the old one that is dishonestly posted on chain by $A$ (resp. $B$). In other words, if $(a,b)$ is the latest state, the one posted on chain is $(a+d_{A},b-d_{A})$ (resp. $(a-d_{B},b+d_{B})$), thus enabling dishonest closing attempts of profit $d_{A}$ for $A$ (resp. $d_{B}$ for $B$). The values $p_{A,B}$ (Table VI, lines $U^{+}, U^{-}$) and $c$ (Table VI, line $C_{c}$) can respectively be chosen by $A$ and $B$ at the time of the action and do not depend on previous distribution states. Based on this setting, we derive the security properties (P1) and (P2) of Lightning channels as given below. The omitted proofs are given in ^[39].

Further, to ensure the security property (P2) of “no deviation”, we require that $$\begin{align*}&a- p_{B}+ d_{A}\geq f\ \ \text{and} \tag{15}\\ &b- p_{A}+ d_{B}\geq f. \tag{16}\end{align*}$$

To understand the in equations (15)–(16) consider the history $(C_{h}, \mathfrak{I}, U^{-}, \mathfrak{A}, D)$ in Figure 4, respectively $S_{1}^{\prime}$. This history formalizes the case where $A$ attempts honest collaborative closing (action $C_{h}$) and $B$ ignores it (action $\Im$). Then $A$ proposes an update (action $U^{-}$) from state $(a,b)$ to state $(a-p_{B},b+p_{B})$ and $B$ agrees (action $\mathfrak{A}$). Finally, $A$ closes dishonestly (action $D)$ using the old distribution state $(a-p_{B}+d_{A},b+p_{B}-d_{A})$. Let us also study the options $B$ has. By ignoring $A^{\prime}\mathrm{s}$ behavior (action $\Im$), $B$ receives $b+p_{B}-d_{A}$ instead of the fair amount $b+p_{B}$, leaving $B$ with a loss of $d_{A}$. By publishing the revocation transaction (action $P$), $B$ receives $a+b$ but has to pay the fee $f$ for pushing it on the blockchain, which leads to a win of $a-p_{B}-f$. Therefore, the win should be greater than the loss; hence $$\begin{equation*}a-p_{B}-f\geq-d_{A}\quad \Leftrightarrow\quad a-p_{B}+d_{A}\geq f, \tag{17}\end{equation*}$$ in order for a rational $B$ to publish the revocation transaction.

This in turn yields a loss for $A$ and hence discourages $A$ from closing dishonestly, which is necessary for the incentive compatibility (P2) of Lightning's closing phase. By swapping $A^{\prime}\mathrm{s}$ and $B^{\prime}\mathrm{s}$ roles, we get the prerequisite formulated in (16). These extreme cases of dishonest closing subsume the others. Thus, the only preconditions we need in the following Theorem V.2 are (15)-(16). In summary, formulas (15)–(16) ensure that ignoring any dishonest closing attempt is worse than publishing the revocation transaction. Property (P2) is then established by the following theorem.

Assume $A$agrees to the update, action $\mathfrak{A}$, and player $B$signs the initially unfair collaborative closing attempt of $A$. Since in the meantime the channel was updated by the exact amount that $A$tried to cheat with, the pending collaborative closing now contains the fair split. Therefore, both players profit from this course of action, yielding utility $(\rho+\alpha,\rho+\alpha)$. The analog can be achieved in subgame $S_{1}^{\prime}$with the history $(\mathfrak{A},\Im,S)$. In fact, for $p_{A}=c$, those histories are the only practical ones and provide the mutually best outcome possible .

However, updating to $(a+c,b-c)$first and then closing honestly and collaboratively yields the exact same result. This is why we study the closing game without the possibility of updating after a closing attempt in the next section Section V-A .

We now state our first main security theorem. Since $(H)$ is not practical, a rational player will not play it. Hence, the terminal history $(H)$ is not secure. We get the following security result instead for $(C_{h},S)$.

Theorem V.2 implies that for honest and rational players the action of collaborative closing followed by signing $(C_{h},S)$ is the best way to close an off-chain channel. It also implies, that rational adversaries will cooperate. Further, Byzantine players represent no threat as long as their channel balances are high enough and they do not engage in special cases of channel updates after a collaborative closing attempt.

We note that for proving our security properties (P1)-(P2) in Theorem V.1–Theorem V.3, we rely on a succinct analysis of the finite graph properties of the closing game $G_{C}(A)$ from Figure 4. While automated approaches analyzing a finite number of graph properties exist, see e.g. ^[43],[44], these approaches cannot handle (game) graphs where graph leaves contain variables, instead of specific numerical values, which is the case of $G_{C}(A)$. For such cases, automated reasoning tools, such as theorem provers, need to be combined with graph-theoretic manipulations of $G_{C}(A)$, an approach we aim to investigate as a future work towards automating the security analysis (and proofs) of closing games.

A. Closing Games Without Updates

We will now consider a variation of closing games without updates, as updating is not beneficial for at least one player upon closing. Furthermore, we avoid special cases such as the one described in Remark 3, which should be equivalent to updating before initiating $G_{c}(A)$, and then closing honestly and collaboratively. As such, the closing game $G_{c}(A)$without updates results from removing all actions $U^{+}$ and $U^{-}$ in Figure 4. For the resulting closing game $G_{c}(A)$ without updates we get the following security result similar to Theorem V.3.

To show practicality, we compute all subgame perfect terminal histories. From $a\geq f$ and $b\geq f$ we have $a+d_{A}\geq f$ and $b+d_{B}\geq f$. Since closing with a dishonest behavior yields utility $a-f+\alpha,\ b-f+\alpha$ respectively, whereas ignoring a dishonest behavior leads to $-d_{A}+\alpha$ and $-d_{B}+\alpha$, we conclude that the best choice after action $D$ is always $P$. Thus, $A^{\prime}\mathrm{s}$ best choice after $(C_{h},\Im)$ and $(C_{c},\Im)$ is $H$. Therefore, $B$ has the two subgame perfect options $\Im$ and $S$ after $(C_{h})$, and only $\Im$ after $(C_{c})$, yielding thus the following practical histories: history $(C_{h},S)$ with utility $(\alpha, \alpha)$; and $(C_{h},\Im,H), (C_{c},\Im,H)$, and $(H)$ each with utility $(\alpha-\varepsilon,\alpha)$. Therefore, both $(H)$ and $(C_{h},S)$ are practical.

Note that every practical terminal history is a Nash Equilibriurn, since if a deviation could benefit a player, the player would have chosen differently already. As CR is equivalent to Nash Equilibria in two-player games (by Definition II.5 and Lemma III.1), we use Definition III.7 and Lemma III.1 to conclude that practicality of $(H)$ and $(C_{h},S)$ implies collusion resistance CR of $(H)$ and $(C_{h},S)$. As $(H)$ and $(C_{h},S)$ are both weak immune, practical and CR, by Definition III.11 we infer that they are also secure.

We further study what happens if a player has almost no funds left in a channel. In particular, we show that security properties, in particular weak immunity and practicality, are violated in this case, thereby formalizing the following folklore in the community.

We next derive the following results on security properties.

B. Optimal Strategy for Closing Off-Chain

To summarize, our security analysis based on closing games for Lightning channels yields the following results. Theorem V.4–Theorem V.5, together with with Corollary 1–Corollary 2, allow us to derive the optimal strategy for closing an off-chain channel for $a$ rational and suspicious player. We next describe and illustrate this optimal strategy, highlighting the main steps of our security analysis based on Theorem V.2–Theorem V.5.

Without loss of generality, we assume the current state of the channel is $(a,b)$.

The player, assumed to be player $A$, who initiated the closing phase shall:

• try to close honestly and collaboratively (action $C_{h}$), if there does not exist an old state $(a+d_{A},b-d_{A})$, where $d_{A} > 0$ and $a+d_{A} < 0$. In case the other player, that is player $B$, does not sign (action $S$), player $A$ shall close honestly and unilaterally (action $H$). If player $B$ closed dishonestly and unilaterally (action $D$), player $A$ shall:
  • state the revocation transaction (action $P$), if the state used for cheating was $(a-d_{B},b+d_{B})$, where $d_{B} > 0$ and $b+d_{B}\geq f$.
  • ignore the cheating otherwise (action $\Im$), as it yields less loss.
• close dishonestly and unilaterally (action $D$), if there exists an old state $(a+d_{A},b-d_{A})$, where $d_{A} > 0$ and $a+d_{A} < f$. In this case, player $A$ shall use the old distribution state $(a+d_{A}^{\prime},b-d_{A})$, with the highest $d_{A}^{\prime} > 0$ that still satisfies $a+d_{A}^{\prime} < f$.

The reacting player, in this case assumed to be player $B$, shall:

• sign the collaborative honest closing attempt (action $S$), if applicable, if there is no old state $(a-d_{B},b+d_{B}), d_{B} > 0$ in which the funds of player $B$ are less then $f$, that is if $b+d_{B} < f$.
• close honestly and unilaterally (action $H$), in case of a dishonest collaborative closing attempt (action $C_{c}$). This holds, if there is no old state $(a-d_{B},b+d_{B}),\ d_{B} > 0$ in which the player $B^{\prime}\mathrm{s}$ funds are less then $f$, that is $b+d_{B} < f$.
• otherwise ignore (action $\Im$) the collaborative and honest/dishonest closing attempt, if applicable, and close dishonestly and unilaterally (action $D$), using the old state $(a-d_{B}^{\prime},b+d_{B}^{\prime})$, with the highest $d_{B}^{\prime} > 0$ that still satisfies $b+d_{B}^{\prime} < f$.
• state the revocation transaction (action $P$), if player $A$ tried to close dishonestly and unilaterally (action $D$) with state $(a+d_{A},b-d_{A})$, where $d_{A} > 0$ and $a+d_{A}\geq f$. • ignore (action $\Im$) if player $A$ closed dishonestly (action $D)$, in the case where $a+d_{A} < f$, as it yields less loss.

The next update could be (1.8,8.2). The best way to close for $A$is still $C_{h}$. Dishonest closing using (3,7), for example, would still cause $B$to publish the revocation transaction. Player $B$would in this case lose $1.8-2=-0.2$, but he would lose more , $7-8.2=-1.2$, by ignoring it .

Another update could be (1,9). Now the optimal strategy for $A$to close is $D$, using the old state (1.8,8.2). Ignoring the dishonest closing (action $\Im$) brings $B-0.8$, but proving $A^{\prime}s$cheating (action $P$) leads to $1-2=-1$. Hence, a rational $B$will choose to ignore (action $\Im$), that means $B$does not publish the revocation transaction .

VI.   Beyond Closing Games for Off-Chain Security

Our game-theoretic analysis so far focused on using closing games to capture security properties of off-chain channels (Section IV), and in particular of Lightning channels (Section V). In this section, we show that our game-theoretic formalism from Section III is expressive enough to analyse more complex protocols than just closing phases in Lightning channels. In particular, we introduce $a$ new EFG, called the Routing Game in Section VI-A, and use this game in Section VI-B to disprove security of Lightning's routing mechanism amid the Wormhole and Griefing attacks ^[7],[20]. We also discuss $a$ natural extension of our analysis to model other off-chain protocols in Section VI-C.

A. Routing Games for Lightning's Routing Module

We first propose $a$ new EFG, called the Routing Game , showing that EFGs can capture actual attacks, in this case the Wormhole attack ^[7] and the Griefing attack ^[20], which were overlooked for example in ^[19]. Specifically, the below defined routing game considers fees f , and supports actions allowing the intermediaries to choose not to claim their money using the secret $x$ but instead to forward it to another intermediary (as explained in Section II-A). Additionally, other deviations such as creating a conditional payment (i.e. HTLC) with a different hash value, a different amount, or a different time-out than expected are also considered. For simplicity, we chose to model our routing game below with five players; however, an arbitrary number of intermediaries can be modeled.

We note that our Routing Game $G_{\text{rout}}$ has four types of subgames, as modeled in Figure 6 and described next: (i) subgames that result from sending the secret to another player $\mathfrak{S}_{i}$; (ii) subgames that result from locking a wrong amount of money in the HTLC $\mathbb{S}_{i}$; (iii) subgames that result from using a wrong time-out in an HTLC $\mathbf{S}_{i}$; and (iv) subgames that result from using a wrong hash value as lock in the HTLC $\mathsf{S}_{i}$. We further note that Figure 6 only gives a partial model, as not all subgames are presented in Figure 6. However, within one type of subgame, the game trees are similar. Therefore, we provide only one instance of each type in ^[39], which are the subgames $\mathbb{S}_{1},\ \mathsf{S}_{2}$, and $\mathbf{S}_{3}$. An instance of a secret forwarding subgame capturing the Wormhole attack can be seen in $G_{\text{rout}}$, as the subtree after history $(S_{H},L,L,L,L, U,S_{S_{E_{1}}})$.

Fig. 6.Fig. 6. Partial definition of the lightning's routing $G_{\text{rout}}$ and the Fulgor Model $G_{\text{Ful}}$. The olive colored subtree only applies for $G_{\text{rout}}$.

Let us emphasize that the utility function $u_{r}$ of $G_{\text{rout}}$ assigns each player $p\in N$ the relative profit of their routing actions and does not mirror the individual channel balances. It also takes the value $\rho$ of a successful payment and the opportunity cost $\varepsilon$ into account.

As in the closing games $G_{c}(A)$ and $G_{c}(B)$, we aim to align utility and monetary outcome as tight as possible. We adjust the ordering $(\mathbb{U},\preccurlyeq)$ of Definition IV.1 by not assuming that $\rho\prec\varepsilon$, since achieving an update is the ultimate goal of the routing protocol. We also consider the utility relative to the amount due to each party.

B. Security Analysis of Lightning's Routing Module

Let us recall Figure 1 and Figure 2, where player $A$ wants to pay another player $B$ money of value $m$. Since, $A$ and $B$ do not share a channel, the three intermediaries $E_{1},\ I$, and $E_{2}$ support the payment, with each receiving a fee $f > 0$ for their collaboration if the payment is successful. Each player who creates an HTLC locks her money for a given time, yielding an opportunity cost of $\varepsilon$ if the money is returned. If the transaction fails, before anyone has unlocked an HTLC, all parties get utility 0 or $-\varepsilon$, depending on whether they created an HTLC or not. Otherwise, the intermediaries' utilities are according to their financial win/loss. The parties $A$ and $B$ both receive $\rho$ once $B$ is paid. Should the transaction fail after $B$ is paid, but before $A$ has paid, she has utility $m+3f+\rho-\varepsilon$; once $E_{1}$ collects the money, $A^{\prime}\mathrm{s}$ utility is $\rho$.

In the sequel, we consider the behavior from Figure 1 as the only honest history in $G_{\text{rout}}$, as also formalized next.

Using our model $G_{\text{rout}}$ and its honest behavior, we derive the following result.

In conclusion, Theorem VI.1 formally proves that Lightning's routing module is susceptible to the Wormhole attack. We further extend this result by noting that not only can $G_{\text{rout}}$ capture the Wormhole attack, but also the Griefing attack, as stated below.

We also obtain the following result as an immediate consequence of Theorem VI.1 and Theorem VI.2.

Corollary 3

(Security of Routing Module). The honest be- havior $(S_{H},L,L,L,L,U,U,U,U)$of the Routing Game $G_{rout}$is not secure. Hence, the Routing Game $G_{rout}$is not secure .

Fig. 7.Fig. 7. Routing in fulgor.

Table VII Possible actions in $G_{\text{rout}}$.

C. Further Routing Protocols Beyond the Lightning Network

We conclude this paper by arguing that our EFG games, either closing or routing games, are not restricted to Lightning networks but can be used for other protocols as well. In the remaining of this section, we illustrate how to model Fulgor ^[38], a payment channel network protocol that fixes the Wormhole attack, but not the Griefing attack.

The routing mechanisms used in Fulgor is similar to Lightning's routing, and is similarly based on HTLCs. The main difference lies in the structure of the secrets and their hashes. Indeed, while Lightning uses the same secret $x$ for every HTLC, Fulgor provides a different secret and hash lock for each player.

Fulgor's routing mechanism is illustrated in Figure 7, where player $A$ generates different secrets and hash locks at the beginning. The secrets and the hashes relate in the following way: $h(x_{1})=y_{1},\ h(x_{1}+x_{2})=y_{2},\ h(x_{1}+x_{2}+x_{3})=y_{3}$ and $h(x_{1}+x_{2}+x_{3}+x_{4})=y_{4}$. Therefore, a player only gets to know a sum of secrets when the right-hand party unlocks and subtracts the secret value received from $A$ to unlock their HTLC. $A$ also provides a zero-knowledge-proof $\text{ZKP}_{i}$ for each intermediary ^[45] to prove that the secrets and hashes constructed this way guarantee successful unlocking of the left HTLC, which is essential to not lose funds.

The game-theoretical (EFG) model of Fulgor $G_{Ful}$ reported in Figure 6 looks similar to the routing game $G_{\text{rout}}$, yet, with one significant difference. Consider the history $(S_{H},L,L,L,L,\ U,S_{S_{E_{1}}})$ in Figure 6, which enables player $E_{1}$ to unlock (action $U$) the HTLC created by $A$. In Fulgor, the same history does not enable $E_{1}$ to unlock the HTLC. As Figure 7 shows, the secrets that $E_{2}$ can share after action 6 are $x_{4}$ and $x_{1}+x_{2}+x_{3}+x_{4}$. Further, $E_{1}$ only knows $x_{2}$, thus there is no way to compute $x_{1}$. This is however the value needed to unlock the HTLC created by $A$. Indeed, Fulgor is not affected by the Wormhole attack. Nevertheless, similarly to Theorem VI.2, the honest behavior of Fulgor is not weak immune, as it is vulnerable to the Griefing attack.

VII.   Conclusions

Our work advocates the use of Extensive Form Games (EFGs) for the game-theoretic security analysis of off-chain protocols. In particular, we introduce two instances of EFGs to model the closing and the routing of the Lightning Network. By doing so, we take the first step towards closing the gap existing security proof techniques have due to using informal arguments about rationality. We express security properties as formal requirements over joint strategies in EFGs, allowing us to establish optimal strategies for closing off-chain and capture security vulnerabilities amid attacks. Given the theoretical expressiveness of our EFGs, future work includes the definitions of new games to capture a wider range of off-chain protocols. To overcome the burden of tedious manual analysis, we also plan to leverage SMT solving and/or automated theorem proving in order to provide automated security proofs.