Note: This version is outdated!
For the latest version, please look at https://interledger.org/developers/rfcs/interledger-protocol/.

A Protocol for Interledger Payments
Stefan Thomas & Evan Schwartz{stefan,evan}@ripple.com

Abstract
We present a protocol for payments across payment systems. It enables secure transfers between ledgers andallows anyone with accounts on two ledgers to create a connection between them. Ledger-provided escrow removes the need to trust these connectors. Connections can be composed to enable payments between
any ledgers, creating a global graph of liquidity orInterledger.
Unlike previous approaches, this protocol requires noglobal coordinating system or blockchain. Transfers
are escrowed in series from the sender to the recipientand executed using one of two modes. In the Atomicmode, transfers are coordinated using an ad-hoc groupof notaries selected by the participants. In the Universal mode, there is no external coordination. Instead,bounded execution windows, participant incentives anda “reverse” execution order enable secure payments between parties without shared trust in any system or institution.

In this paper, we present a protocol for interledger payments that enables anyone with accounts on two ledgers
to create connections between them. It uses ledgerprovided escrow—conditional locking of funds—to allow secure payments through untrusted connectors.
Any ledger can integrate this protocol simply by enabling
escrowed transfers. Unlike previous approaches, our protocol does not rely on any global coordinating system orledger for processing payments—centralized [10] or decentralized [15, 17, 19].
Our protocol lowers the barriers to facilitating interledger
payments. Connectors compete to provide the best rates
and speed. The protocol can scale to handle unlimited
payment volume, simply by adding more connectors andledgers. Composing connectors into chains enables payments between any ledgers and give small or new payment systems the same network effects as the most established systems. This can make every item of value
spendable anywhere—from currencies to commodities,
computing resources and social credit.
Our protocol provides:• Secure payments through any connector using
ledger-provided escrow.

1

Introduction

Sending money today within any single payment system
is relatively simple, fast and inexpensive. However, moving money between systems is cumbersome, slow andcostly, if it is possible at all.
Digital payment systems use ledgers to track accounts
and balances and to enable local transfers between theirusers. Today, there are few connectors facilitating payments between these ledgers and there are high barriers
to entry for creating new connections. Connectors are
not standardized and they must be trusted not to steal thesender’s money.

• The sender of a payment is guaranteed a cryptographically signed receipt from the recipient, if thepayment succeeds, or else the return of their escrowed funds.
• Two modes of executing payments: In the Atomicmode, transfers are coordinated by an ad-hoc groupof notaries selected by the participants to ensure
all transfers either execute or abort. The Universal mode instead uses bounded execution windows
and incentives to remove the need for any mutuallytrusted system or institution.

Note: This version is outdated!
For the latest version, please look at https://interledger.org/developers/rfcs/interledger-protocol/.

The following sections describe our protocol in greater
depth. Section 2 introduces the core concepts of the
protocol, including the actors involved and the need forledger-provided escrow. Section 3 presents the Atomicmode. Section 4 presents the Universal mode. Sequence
diagrams and the formal protocol specifications can befound in the Appendix.

2

the payment correctly. This severely limits the set of institutions that can act as connectors, resulting in a highly
uncompetitive and disconnected global payment system.
Ledger-provided escrow guarantees the sender that theirfunds will only be transferred to the connector once theledger receives proof that the recipient has been paid. Escrow also assures the connector that they will receive thesender’s funds once they complete their end of the agreement.

Interledger Payments

A ledger may be used to track anything of value—fromcurrency or stocks to physical goods and titles—and may
be centralized or decentralized [17]. As illustrated in
Figure 1, payments between accounts in the same system are accomplished with a simple book transfer.

Figure 3: Funds are escrowed by the sender and connector on their respective ledgers

Figure 1: Book transfer
A connector is a system that facilitates interledger
payments by coordinating book transfers on multiple
ledgers. Connectors can also translate between different
protocols used by these ledgers. As illustrated in Figure
2, connector Chloe accepts a transfer into her account on
one ledger in exchange for a transfer out of her accounton another ledger.

Figure 4: The transfers to the connector and recipient areeither executed or aborted together
The simple arrangement illustrated here can be extended
into arbitrarily long chains of connectors to facilitate
payments between any sender and any recipient. This
brings the small-world network effect (commonly known
as the “six degrees of separation”) [3, 21] to payments
and creates a global graph of liquidity or Interledger.

2.1

Byzantine and Rational Actors

A truly open protocol for payments cannot rely on highly
trusted actors for security. It must lower the barriers toparticipation through built-in protections against potentially faulty, self-interested, or malicious behavior by theparticipants.

Figure 2: Connector controls accounts on two ledgers
The problem with existing payment protocols is that thesender must trust the connector to follow through on paying the intended recipient. Nothing technically prevents
connectors from losing or stealing money, so they must
be bound by reputation and legal contracts to complete

We use the Byzantine, Altruistic, Rational (BAR) model
introduced by [2] for categorizing participants. Byzan2

Note: This version is outdated!
For the latest version, please look at https://interledger.org/developers/rfcs/interledger-protocol/.

tine actors may deviate from the protocol for any reason,
ranging from technical failure to deliberate attempts toharm other parties or simply impede the protocol. Altruistic actors follow the protocol exactly. Rational actors
are self-interested and will follow or deviate from theprotocol to maximize their short and long-term benefits.

acknowledgement that the recipient has received their
payment. The recipient is assured by their ledger thatthey will be paid when they provide such an acknowledgement. Connectors also use their ledgers’ escrow toprotect themselves from risk.
Cryptographic signatures are a simple way for ledgers tosecurely validate the outcome of the external conditions
upon which a transfer is escrowed. Any one-way function can be used [18]. Using asymmetric cryptography,
the ledger escrows funds pending the presentation of avalid signature for a pre-defined public key and message
or hash. The ledger can then easily validate the signaturewhen it is presented and determine if the condition has
been met.

We assume all actors in the payment are either Rationalor Byzantine. Protocols that rely on highly trusted actors
effectively assume all to be Altruistic—or bound by factors external to the protocol. Assuming the actors to be
self-interested or malicious requires the protocol to provide security even when participants are bound only by
the algorithm itself.
We assume that, as Rational actors, ledgers and connectors may require some fee to incentivize their participation in a payment. These fees may be paid in the flow of
the payment, or out of band. In this paper, we will only
discuss the details of fees necessary to mitigate risks andattacks specific to interledger payments.
While ledgers may be Byzantine, we do not attempt to
introduce fault-tolerance—protection against accidental
or malicious errors—for participants who hold accounts
with such a ledger. Ledgers themselves can be madeByzantine fault-tolerant [15, 17, 19], and participants canchoose the ledgers with which they hold accounts. We
only seek to isolate participants who hold accounts on
non-faulty ledgers from risk.

Figure 5: Transfer states
Figure 5 illustrates the states of a transfer. First, a transfer is proposed to the participants, but no changes are
made to the ledger. Once affected account holders haveauthorized the transfer, the ledger checks that funds areavailable and that all of its rules and policies have beensatisfied. The ledger places the funds in escrow and thetransfer is prepared. If the execution condition e is fulfilled, the transfer is executed. If any of the checks fail, or
if an abort condition e0 is fulfilled, the transfer is aborted
and the escrowed funds are returned to their originator.

We assume that connectors will agree to participate ina payment only if they face negligible or manageablerisk for doing so, and that they will charge fees accordingly. Connectors will only deliver money on a destination ledger if doing so benefits them directly.
Any of the participants in a payment may attempt to overload or defraud any of the other actors involved. Thus,
escrow is needed to make secure interledger payments.

2.2

3

Atomic Interledger Payments

Interledger payments consist of transfers on different
ledgers. If the payment partially executes, at least oneof the participants loses money. Thus, participants wantatomicity—a guarantee that all of the component transfers will either execute or that all will be aborted.

Cryptographic Escrow

Ledger-provided escrow enables secure interledger payments by isolating each participant from the risks of failure or malicious behavior by others involved in the payment. It represents the financial equivalent of the statesin the Two-Phase Commit Protocol [13, 14].

Executing transfers atomically across multiple ledgers
requires a transaction commit protocol. The simplest
such protocol is the Two-Phase Commit, in which all
systems involved first indicate their readiness to complete the transaction, and then execute or abort based onwhether all of the other systems have agreed. The basic form of that protocol uses a transaction manager tocollect the responses of the various system and disseminate the decision. Fault tolerance can be added to the
Two-Phase Commit by replacing the single transaction

Providing escrowed transfers is the main requirement forledgers to enable secure interledger payments.
All participants rely upon their ledgers to escrow funds
and release them only when a predefined condition ismet. The sender is assured by their ledger that their funds
are transferred only upon delivery of a non-repudiable3Note: This version is outdated!
For the latest version, please look at https://interledger.org/developers/rfcs/interledger-protocol/.

Figure 6: Payment chain
manager with a group of coordinators that use a consensus algorithm to agree on the outcome of the payment[14].

Notaries N must only agree on the D Execute or D Abort
messages if they have received a signed receipt, theR ReceiptSignature, from the recipient pn before a timeout t. The recipient’s signature provides non-repudiable
proof that they have been paid. The recipient pn signs thereceipt once the transfer into their account is L Preparedand escrowed pending their signature.

The Atomic execution mode uses a Byzantine faulttolerant agreement algorithm amongst an ad-hoc groupof coordinators or notaries to synchronize the executionof the component transfers. Additionally, it guarantees
that the sender receive a cryptographically signed payment receipt from the recipient if funds are transferred.

To ensure all of the transfers B can be executed atomically, all of the execution conditions E must dependon the D Execute message from the notaries and the
R ReceiptSignature from the recipient:Figure 6 shows a payment through a chain of participants
P and ledgers L. There are n participants in P, such that
|P| = n. The sender is the first participant p1 and therecipient is the last participant pn . The connectors C are
participants p2 through pn−1 , such that {pi ∈ C | C ⊂P ∧ i ∈ Z+ ∧ 1 < i < n}. The payment consists of n − 1book transfers B on n − 1 ledgers, such that |B| = |L| =n − 1. The first participant, the sender p1 , has an accounton ledger `1 . The last participant, the recipient pn , has
an account on ledger `n−1 . Each connector pi ∈ C has
accounts on ledgers `i−1 and `i and facilitates payments
between them.

3.1∀e ∈ E : e = R ReceiptSignature ∧ D Execute(1)

The abort conditions E 0 for each transfer in B are dependent only on the abort message D Abort. Receipt ofa message fulfilling the abort condition e0i where {i ∈Z+ ∧ i < n} causes the ledger `i to immediately transition the L Proposed or L Prepared transfer bi to the
L Aborted state and release the funds to the originator.
∀e0 ∈ E 0 : e0 = D Abort

Notaries

In the Atomic mode, transfers are coordinated by a groupof notaries N that serve as the source of truth regarding
the success or failure of the payment. They take the placeof the transaction manager in a basic Two-Phase Commit. Importantly, notaries are organized in ad-hoc groups
for each payment and our protocol does not require one
globally trusted set of notaries.

3.2

(2)

Fault Tolerance

The Atomic mode only guarantees atomicity when notaries N act honestly. Like all other participants, we assume notaries are either rational or Byzantine. Rational
actors can be incentivized to participate with a fee.

All of the escrow conditions for the book transfers B
comprising the payment must depend on the notaries either sending a D Execute or D Abort message. If the escrow conditions were based solely on a message fromN, however, faulty notaries could cause the transfers
to execute before the final transfer to the recipient is
L Prepared. [11].

Byzantine notaries, however, could sign both D Executeand D Abort messages, communicate them to different
ledgers and cause some transfers to be executed and otherto be aborted. In order to protect against this, we must
set a fault-tolerance threshold f . This means that the outcome of the agreement protocol will be correct so longas there are no more than f Byzantine notaries in N.
4

Note: This version is outdated!
For the latest version, please look at https://interledger.org/developers/rfcs/interledger-protocol/.

If f = 0, we only need a single notary N = {N1 } and the
D Execute and D Abort messages are simply signaturesby that notary N1 .

from each participant p, N p ( fc ) and calculates the candidate set Nc ( fc ) at threshold fc as the intersection ofthese sets. Each p ∈ P chooses N p ( fc ) such that they believe that there is no Byzantine subset Nevil where Nevil ⊆N p ( fc ), |Nevil | > f which will collude against them.

If f ≥ 1, notaries use a Byzantine fault-tolerant (BFT)
agreement protocol. Using the method from [14, 16],
a BFT replication algorithm, such as PBFT [8] or Tangaroa, a BFT version of Raft [9], can be simplified into abinary agreement protocol.

∀ fc ∈ Z + ∧ fc < fmax : Nc ( fc ) =(3)

Finally the sender chooses a fault tolerance threshold fand a corresponding set of notaries N such that N ⊆Nc ( f ) ∧ |N| ≥ 3 f + 1. If no such set exists, the sendercannot rely on the Atomic mode and must instead use
the Universal mode as described in Section 4.

The D Execute and D Abort messages are collections ofsignatures from some representative subset Nrep such that
Nrep ⊆ N and |Nrep | = f + 1 vouching for the outcome of
the agreement protocol.

3.4.2

Timeout

ProposalIn the proposal phase, the sender p1 notifies each connector {pi | i ∈ Z+ ∧ 1 < i < n} about the the book transfersbi−1 and bi in the upcoming payment. Upon receiving
the proposal, each connector pi will verify the proposed
spread between the payments matches its exchange rate,
charge its fee and store the payment details. pi accepts
the terms of the book transfers bi−1 and bi and the sender
p1 proceeds to the next phase.

To ensure that funds cannot be held in escrow forever,even in the case of failure, notaries N enforce a timeout
t. The recipient pn must submit the R ReceiptSignature
to the notaries N before t is reached, or the payment will
be aborted and the escrowed funds returned. t must be
sufficient to account for the duration of the phases of the
protocol leading up to Execution.

3.4

Np ( fc )p∈P

The minimum number of processes required to toleratef Byzantine faults is |N| = 3 f + 1 as shown by [5].

3.3

\

3.4.3

Phases of the Protocol

Preparation

Unlike in a basic Two-Phase Commit, book transfers{bi ∈ B | i ∈ Z+ ∧ 1 < i < n} are prepared in sequence
from b1 to bn−1 . Each connector is only willing to escrow their funds if they know funds have already been
escrowed for them.

Before a payment can occur, the sender p1 must find asuitable set of connectors C forming a path to the recipient pn . Connectors have an interest in making their liquidity information available in order to attract payment
flows. The problems of minimum-cost and multicommodity flow have been studied extensively in the context
of planning [1, 7, 20].

Appendix A.1 illustrates the phases of the protocol, excluding Notary Selection and Notary Setup.

The sender p1 first authorizes and sends the instruction toprepare the first transfer b1 on `1 . p1 then requests thatthe first connector p2 prepare b2 on `2 . The connector
p2 is comfortable preparing b2 because b1 is preparedand the funds have been escrowed by `1 . Similarly, eachconnector pi prepares transfer bi once it is notified that`i−1 has prepared bi−1 and escrowed the corresponding
funds.

3.4.1

3.4.4

In the following, we assume that a path has already beenchosen and the exchange rates and any fees quoted by theconnectors in C are known.

Notary Selection

Execution

Once the last book transfer bn−1 has been prepared andthe funds escrowed, the recipient pn must sign the receipt before the timeout t. pn is comfortable signing
the receipt because they know that doing so will fulfill
the condition of the escrowed funds waiting for them on`n−1 . pn submits the R ReceiptSignature to the notaries

Notaries are selected by the participants P.
For each candidate fault tolerance threshold fc wherefc ∈ Z + ∧ fc < fmax and fmax is the sender’s maximum
fault tolerance threshold, the sender requests the set of all
notaries trusted at the given fault tolerance threshold fc
5Note: This version is outdated!
For the latest version, please look at https://interledger.org/developers/rfcs/interledger-protocol/.

N, who then run the agreement protocol (see Section 3.2)
to decide whether the payment should execute.

As mentioned in Section 3.3, the notaries will initiate
their agreement protocol spontaneously after a timeout
t. From the liveness property of the underlying agreement protocol, we know that the notaries will eventually
decide to either D Execute or D Abort and broadcast thatdecision to the participants. Each ledger is connected toat least two participants. If one of these participants is
non-faulty, it will forward the decision to the ledger.

If N agree that the R ReceiptSignature was received intime, they submit it and a signed D Execute message toall participants P. Each participant {pi ∈ P | i ∈ Z+ ∧ 1 <i ≤ n} submits the R ReceiptSignature and D Execute
message to `i−1 to execute bi−1 and claim the funds they
are due.

Note that if notaries could broadcast directly to theledgers, our protocol could maintain liveness even when
all participants are faulty. However, in real world applications, some ledgers use proprietary protocols or private
networks, so we cannot rely on the fact that the notaries
can reach them directly.

If N agree that the payment timed out, they submit the asigned D Abort message to P. Each participant {p j ∈ P |j ∈ Z+ ∧ 1 ≥ j < n} submits the D Abort message to ` jand reclaims its escrowed funds.

3.5

If a transfer is in the L Prepared state, at least one of theparticipants has an interest in seeing the transfer reach a
final state, because the escrowed funds would be transferred to them. If this participant is rational they will
therefore eventually forward the notaries’ decision. A
Byzantine participant in this position may not, but in doing so does not hurt anyone else.

Correctness

The Atomic mode of the protocol inherits the assumptions and level of fault-tolerance from the Byzantine
agreement protocol used amongst the notaries. For the
purpose of this section, we assume the notaries use PBFT
[8].
Given the assumptions in [8] we require no additional
assumptions.

3.6

3.5.1

Each connector in C incurs some costs and risks for participating in a payment, which can be priced into the connectors’ fees.

SafetyWhen trading different assets, connectors in C effectively
write the sender p1 an American option [4, 6] which, on
exercise, swaps an asset on one ledger for an equivalent
asset on another ledger. In addition to the factors considered in standard option pricing, the connector should
also account for the following attack in its fee.

Safety means that if one non-faulty ledger transitions
its transfer to the L Executed state, then no non-faulty
ledger will transition a transfer belonging to the same
payment to the L Aborted state and vice versa. If liveness also holds, all transfers will eventually be executedor all aborted.
Given the safety of the consensus algorithm used by thenotaries, we know that all ledgers will only receive oneof either: f + 1 D Execute, or f + 1 D Abort messages
from notaries. A correct ledger only executes the transfer
when it has received f + 1 D Execute messages which
precludes the possibility that any other correct ledger
has aborted their transfer. Equally, a correct ledger only
aborts the transfer when it has received f + 1 D Abort
messages which precludes the possibility that any othercorrect ledger has received f + 1 D Execute messages
and aborted their transfer.

3.5.2

Fees

3.6.1

Liquidity Starvation

An attacker can attempt to temporarily tie up all of a connector’s liquidity in payments it knows will fail. This attack is rendered uneconomical if the connector sets its
fee to cover its costs and the profit it would expect if thepayment were successful. Furthermore, connectors, including those operated by the same entity as a ledger,
can prevent their funds from being completely tied up by
escalating their fees as a function of the percentage of
their total liquidity being held in escrow.

Liveness

Liveness means that every non-faulty ledger connected
to at least one non-faulty, rational participant will eventually execute or abort its transfer.
6Note: This version is outdated!
For the latest version, please look at https://interledger.org/developers/rfcs/interledger-protocol/.

4

Universal Interledger Payments

following section discusses expiration times and the message delay risk connectors must manage.

While the Atomic mode uses notaries to ensure proper
execution of a payment, the Universal mode relies on the
incentives of rational participants instead to eliminate theneed for external coordination. It provides safety andliveness for all non-faulty participants connected to only
non-faulty ledgers, under an assumption of bounded synchrony with a known bound. In Section 4.4.1 we discuss
the practical considerations of using Universal mode in asystem that does not guarantee bounded synchrony, e.g.
the Internet.

4.2

Each book transfer in B must have an expiration time t
to ensure liveness. In order for a connector {pi ∈ P | i ∈Z+ ∧ 1 < i < n} to agree to take part in the payment,
they must be able to pass the R ReceiptSignature fromledger `i to `i−1 and execute bi−1 before it expires. If
bi is executed but bi−1 expires, pi loses money. Because
bi may execute very close to its expiration time ti , theexpiration time ti−1 for transfer bi−1 must be greater thanthat of bi by some finite time difference ti−1 − ti .

Appendix A.2 illustrates the phases of the payment inthis mode.

4.1

This time difference ti−1 − ti must account for the messaging delays M(`i , pi ) from `i to pi and M(pi , `i−1 ) frompi to `i−1 (which includes the processing delays at pi , `iand `i−1 respectively) and the clock skew K(`i−1 , `i ) between ledgers `i−1 and `i .

Execution Order

In Universal mode, there are no notaries. The booktransfers B must be executed in a specific order to ensure all participants’ incentives are aligned to executethe payment properly and to ensure delivery of the
R ReceiptSignature to the sender p1 .

ti ≥ ti+1 + M(`i , pi+1 ) + M(pi+1 , `i ) + S(`i , `i+1 )The transfers B are escrowed only on the condition ofreceiving the R ReceiptSignature:∀e ∈ E : e = R ReceiptSignature

Message Delay(5)

The timeout tn−1 for the destination transfer bn−1 is equal
to the timeout t in Atomic mode introduced in Section
3.3. That is, it is large enough to allow for the preparationof the transfers and for the recipient to sign and submit
the R ReceiptSignature.

(4)

Instead of having a global timeout, each book transferin {bi ∈ B | i ∈ Z+ ∧ i < n} has its own expiration time
enforced by the ledger `i . After the last book transfer
bn−1 is prepared, the recipient pn signs the receipt andpresents the R ReceiptSignature directly to their ledger`n−1 . If it is before the transfer’s expiration time tn−1 ,bn−1 will be executed immediately.

4.3

Correctness

For our analysis of Universal mode, we consider both
safety and liveness under bounded synchrony. We definebounded synchrony similar to the definition given in [12]as a system in which there is a known upper bound M on
messaging delays between processes and a known upperbound S on clock skew between two nodes. We assume
that processing times are negligible and included in M.

Once bn−1 is executed and the recipient pn is paid,
connector pn−1 has a very strong incentive to pass the
R ReceiptSignature back to `n−2 , as they have paid out
money but have not yet been paid. When each connector {p j ∈ P | j ∈ Z+ ∧ 1 < j < n} learns of theexecution of the book transfer b j , they must get the
R ReceiptSignature from ` j and submit it to ` j−1 to claim
the money waiting in escrow for them.

4.3.1

SafetySafety means that there will be no book transfer {bi ∈ B |i ∈ Z+ ∧ i < n − 1} which expires if bi+1 executed unless`i , `i+1 or participant pi+1 are faulty.

Thus, the transfers in B are executed in “backwards” order, from the recipient pn to the sender p1 . Once thefirst transfer b1 is executed, the sender p1 can get the
R ReceiptSignature from their ledger `1 .

Let bi+1 execute at time φ0 . We know that bi+1 was not
expired, therefore:

If the last transfer bn−1 times out before pn submits the
R ReceiptSignature, all transfers in B will expire and theescrowed funds will be returned to their originator. The

φ0 < ti+1
7(6)Note: This version is outdated!
For the latest version, please look at https://interledger.org/developers/rfcs/interledger-protocol/.

A correct ledger `i+1 will send ahM ExecuteNotify, R ReceiptSignaturei totor pi+1 which will arrive at time φ1 :4.4.1

messageconnec-φ1 ≤ φ0 + M(`i , pi+1 )Optimal Timeouts

In an asynchronous system, message delays and clock
skew are unbounded, so a connector {pi ∈ P | i ∈Z+ ∧ 1 < i < n} may lose the race to forward the
R ReceiptSignature from `i to `i−1 , causing them to losemoney.

(7)

The rational connector pi+1 will send a message
hM ExecuteRequest, R ReceiptSignaturei to ledger `iwhich will arrive at time φ2 .
(8)

However, by observing prior performance of the network, pi can estimate the probability Pr(ti−1 − ti ≥M(`i , pi+1 ) + M(pi+1 , `i ) + S(`i , `i+1 )), calculate thevalue of the risk to them and include it in their fee.

The correct ledger `i is guaranteed to execute transfer
bi if and only if the message arrives before the timeout
ti . However, so far we have expressed all times in termsof `i+1 ’s local clock. In order to ensure that bi is not
expired, we must account for clock skew:

As ti−1 − ti becomes larger, the risk decreases. However,
the expiration time for each transfer {b j ∈ B | j ∈ Z+ ∧j < i − 1} also increases. Longer expiration times incur
higher fees, because funds may be held in escrow for alonger period. The sender p1 will try to choose ti−1 − tisuch that the total amount of fees is minimized.

φ2 ≤ φ1 + M(pi+1 , `i )ti ≥ φ2 + S(`i , `i+1 )

(9)
4.4.2

Robust Messaging

From equations (5), (6), (7), (8) and (9):The other participants may collude in an attempt to defraud a connector. In order to do so, they must interferewith the messaging as mentioned in the previous section
to prevent the connector {pi ∈ P | i ∈ Z+ ∧ 1 < i < n}from completing the transfer bi−1 thereby profiting at
pi ’s expense.

ti ≥ φ2 + S(`i , `i+1 )≥ φ1 + M(pi+1 , `i ) + S(`i , `i+1 )≥ φ0 + M(`i , pi+1 ) + M(pi+1 , `i ) + S(`i , `i+1 )(10)≥ ti+1 + M(`i , pi+1 ) + M(pi+1 , `i ) + S(`i , `i+1 )The mitigation for this attack varies based on the technical characteristics of each ledger. However, in all cases,
it is a type of Denial of Service mitigation. Both connectors and ledgers have an interest in establishing reliablecommunication.

Since `i is a correct ledger, it will execute the transfer. A
transfer that has been executed on a correct ledger cannot
expire, therefore bi cannot expire.
4.3.2

Liveness

4.4.3

Liveness means that eventually each book transfer {bi ∈B | i ∈ Z+ ∧ i < n} on a non-faulty ledger `i must either
be L Executed or L Aborted.

The recipient pn does not have to transfer any money, but
we assume that the act of signing the receipt has someexternal meaning, such as nullifying an existing asset ofthe recipient (e.g. an invoice) or creating a new liability.

All book transfers bi have a finite expiry time ti . A correct ledger `i will expire transfer bi at time ti unless it has
already executed.

To claim the funds escrowed for them, the recipient pn
must submit R ReceiptSignature to `n−1 before the transfer bn−1 is executed. In an asynchronous system, bn−1
might timeout while this message is in transit.

Therefore after time ti , transfer bi will be either
L Executed or L Aborted.

4.4

Receipt Privacy

In order to guarantee safety for the recipient then, wemust introduce another property of ledgers, ReceiptPrivacy. A correct ledger that offers ReceiptPrivacy does
not disclose a hD Execute, R ReceiptSignaturei message(or the R ReceiptSignature contained therein) unless bi
is executed successfully.

Fault and Attack Mitigation

In Section 3.6 we discussed the connector fee in Atomicmode. In Universal mode, there are additional costs thatthe connector must take into account:8

Note: This version is outdated!
For the latest version, please look at https://interledger.org/developers/rfcs/interledger-protocol/.

If the recipient chooses an honest ledger with ReceiptPrivacy, they are not at risk, even in an asynchronous system, because their ledger `n−1 will disclose
R ReceiptSignature if and only if bn−1 executes.

5[7] C AI , X., S HA , D., AND W ONG , C. Time-varying minimum costflow problems. European Journal of Operational Research 131,
2 (2001), 352–374.
[8] C ASTRO , M., L ISKOV, B., ET AL . Practical byzantine fault tolerance. In OSDI (1999), vol. 99, pp. 173–186.
[9] C OPELAND , C., AND Z HONG , H. Tangaroa: a byzantine fault
tolerant raft.

Conclusion[10] DAVIES , D. W., AND P RICE , W. L. Security for computer networks: and introduction to data security in teleprocessing andelectronic funds transfer. John Wiley & Sons, Inc., 1989.

We have proposed a protocol for secure interledger payments across an arbitrary chain of ledgers and connectors. It uses ledger-provided escrow based on cryptographic conditions to remove the need to trust the connectors.

[11] D OLEV, D., AND S TRONG , H. R. Authenticated algorithms forbyzantine agreement. SIAM Journal on Computing 12, 4 (1983),
656–666.
[12] DWORK , C., LYNCH , N., AND S TOCKMEYER , L. Consensus in
the presence of partial synchrony. Journal of the ACM (JACM)
35, 2 (1988), 288–323.

The Atomic mode of the protocol provides atomicity for
payment chains in which the participants can agree upona group of notaries. The Universal mode uses the incentives of rational actors to enable practical payments
between participants that do not all share trust in any institution or system.

[13] G RAY, J. Notes on data base operating systems. In Operating Systems, An Advanced Course (London, UK, UK, 1978),Springer-Verlag, pp. 393–481.
[14] G RAY, J., AND L AMPORT, L. Consensus on transaction commit.
ACM Transactions on Database Systems (TODS) 31, 1 (2006),
133–160.
[15] M AZI ÈRES , D. The stellar consensus protocol: A federated
model for internet-level consensus.

Our protocol does not rely on any single system forprocessing payments, so there is no limit to its scalability. Payments can be as fast and cheap as the constituent ledgers and connectors allow and transaction details are private to their participants. The separation ofconcerns and the minimal standardization requirements
enable continuous optimization and competition between
connectors and between ledgers.

[16] M OHAN , C., S TRONG , R., AND F INKELSTEIN , S. Methodfor distributed transaction commit and recovery using byzantine
agreement within clusters of processors. In Proceedings of thesecond annual ACM symposium on Principles of distributed computing (1983), ACM, pp. 89–103.
[17] NAKAMOTO , S. Bitcoin: A Peer-to-Peer electronic cash system.
[18] ROMPEL , J. One-way functions are necessary and sufficient for
secure signatures. In Proceedings of the twenty-second annual
ACM symposium on Theory of computing (1990), ACM, pp. 387–
394.

Removing the need to trust the connector enables anyone with accounts on two or more ledgers to make connections between them. Connectors can be composed tomake payments and the financial system more accessible, competitive and resilient. This enables the creationof a global graph of liquidity or Interledger.

[19] S CHWARTZ , D., YOUNGS , N., AND B RITTO , A. The ripple protocol consensus algorithm. Ripple Labs Inc White Paper (2014).
[20] WAGNER , H. M. On a class of capacitated transportation problems. Management Science 5, 3 (1959), 304–318.
[21] WATTS , D. J., AND S TROGATZ , S. H. Collective dynamics ofsmall-worldnetworks. nature 393, 6684 (1998), 440–442.

References[1] A HUJA , R. K., M AGNANTI , T. L., AND O RLIN , J. B. Network
flows. Tech. rep., DTIC Document, 1988.
[2] A IYER , A. S., A LVISI , L., C LEMENT, A., DAHLIN , M., M AR TIN , J.-P., AND P ORTH , C. Bar fault tolerance for cooperative
services. In ACM SIGOPS Operating Systems Review (2005),
vol. 39, ACM, pp. 45–58.
[3] A LBERT, R., J EONG , H., AND BARAB ÁSI , A.-L. Internet: Diameter of the world-wide web. Nature 401, 6749 (1999), 130–131.
[4] B LACK , F., AND S CHOLES , M. The pricing of options and corporate liabilities. The journal of political economy (1973), 637–
654.
[5] B RACHA , G., AND T OUEG , S. Asynchronous consensus andbroadcast protocols. Journal of the ACM (JACM) 32, 4 (1985),
824–840.
[6] B RENNAN , M. J., AND S CHWARTZ , E. S. The valuation ofamerican put options. Journal of Finance (1977), 449–462.

9

Note: This version is outdated!
For the latest version, please look at https://interledger.org/developers/rfcs/interledger-protocol/.

A
A.1

Appendix
Atomic Mode Sequence Diagram

Figure 7: Phases of a payment in the Atomic mode10

Note: This version is outdated!
For the latest version, please look at https://interledger.org/developers/rfcs/interledger-protocol/.

A.2

Universal Mode Sequence Diagram

Figure 8: Phases of a payment in the Universal mode

11

Note: This version is outdated!
For the latest version, please look at https://interledger.org/developers/rfcs/interledger-protocol/.

A.3

Formal Specification: Atomic mode
module Atomic

Formal Specification in TLA+ of the Interledger Protocol Atomic (ILP /A)
Modeled after the excellent Raft specification by Diego Ongaro.
Available at https://github.com/ongardie/raft.tla
Copyright 2014 Diego Ongaro.
This work is licensed under the Creative Commons Attribution-4.0
International License https://creativecommons.org/licenses/by/4.0/

extends Naturals, Sequences, Bags, TLC
The set of ledger IDs

constants Ledger
The set of participant IDs

constants Participant
The notary

constants Notary
Sender states

constants S Ready, S Waiting, S Done
Notary states

constants N Waiting, N Committed , N Aborted
Ledger states

constants L Proposed , L Prepared , L Executed , L Aborted
Message types

constants PrepareRequest, ExecuteRequest, AbortRequest,
PrepareNotify, ExecuteNotify, AbortNotify,
SubmitReceiptRequest
Receipt signature

constants R ReceiptSignature
Global variables
A bag of records representing requests and responses sent from one process
to anothervariable messages
Sender variables
State of the sender (S Ready, S Waiting, S Done)variable senderStateAll sender variables∆

senderVars = hsenderStatei
The following variables are all per ledger (functions with domain Ledger )The ledger state (L Proposed, L Prepared, L Executed or L Aborted)variable ledgerState
12

Note: This version is outdated!
For the latest version, please look at https://interledger.org/developers/rfcs/interledger-protocol/.

All ledger variables∆

ledgerVars = hledgerStatei
Notary variables
State of the notary (N Waiting, N Committed, N Aborted)variable notaryStateAll notary variables∆

notaryVars = hnotaryStatei
All variables; used for stuttering (asserting state hasn’t changed)∆vars = hmessages, senderVars, ledgerVars, notaryVarsi
Helpers
Add a set of new messages in transit∆

Broadcast(m) = messages 0 = messages ⊕ SetToBag(m)Add a message to the bag of messages∆

Send (m) = Broadcast({m})
Remove a message from the bag of messages. Used when a process is done
processing a message.
∆

Discard (m) = messages 0 = messages

SetToBag({m})

Respond to a message by sending multiple messages∆

ReplyBroadcast(responses, request) =messages 0 = messages SetToBag({request}) ⊕ SetToBag(responses)
Combination of Send and Discard∆

Reply(response, request) =ReplyBroadcast({response}, request)
Return the minimum value from a set, or undefined if the set is empty.
∆

Min(s) = choose x ∈ s : ∀ y ∈ s : x ≤ yReturn the maximum value from a set, or undefined if the set is empty.
∆

Max (s) = choose x ∈ s : ∀ y ∈ s : x ≥ y
Is a final ledger state∆

IsFinalLedgerState(i ) = i ∈ {L Executed , L Aborted }Sender∆Sender = Min(Participant)
Recipient∆

Recipient = Max (Participant)Set of connectors∆

Connector = Participant \ {Sender , Recipient}
Define type specification for all variables∆

TypeOK = ∧ IsABag(messages)∧ senderState ∈ {S Ready, S Waiting, S Done}∧ ledgerState ∈ [Ledger → {L Proposed , L Prepared , L Executed , L Aborted }]13

Note: This version is outdated!
For the latest version, please look at https://interledger.org/developers/rfcs/interledger-protocol/.

∆Consistency =∀ l 1, l 2 ∈ Ledger : ¬ ∧ ledgerState[l 1] = L Aborted∧ ledgerState[l 2] = L Executed∆

Inv = ∧ TypeOK∧ Consistency
Define initial values for all variables∆

InitSenderVars = ∧ senderState = S Ready∆

InitLedgerVars = ∧ ledgerState = [i ∈ Ledger 7→ L Proposed ]∆InitNotaryVars = ∧ notaryState = N Waiting∆

Init = ∧ messages = EmptyBag∧ InitSenderVars∧ InitLedgerVars∧ InitNotaryVars
Define state transitions
Participant i starts off the chain∆

Start(i ) =∧ senderState = S Ready∧ senderState 0 = S Waiting∧ Send ([mtype 7→ PrepareRequest,msource 7→ i ,mdest 7→ i + 1])∧ unchanged hledgerVars, notaryVarsi
Notary times out∆

NotaryTimeout =∧ notaryState = N Waiting∧ notaryState 0 = N Aborted∧ Broadcast({[mtype7→ AbortRequest,msource 7→ Notary,
mdest
7→ k ] : k ∈ Ledger })∧ unchanged hsenderVars, ledgerVarsi
Ledger spontaneously aborts∆

LedgerAbort(l ) =∧ ledgerState[l ] = L Proposed∧ ledgerState 0 = [ledgerState except ! [l ] = L Aborted ]∧ Send ([mtype 7→ AbortNotify,msource 7→ l ,mdest 7→ l − 1])∧ unchanged hsenderVars, notaryVarsi
Message handlers
i = recipient, j = sender, m = message
Ledger i receives a Prepare request from process j∆

LedgerHandlePrepareRequest(i , j , m) =14

Note: This version is outdated!
For the latest version, please look at https://interledger.org/developers/rfcs/interledger-protocol/.

∆let valid = ∧ ledgerState[i ] = L Proposed∧j =i −1in ∨ ∧ valid∧ ledgerState 0 = [ledgerState except ! [i ] = L Prepared ]∧ Reply([mtype 7→ PrepareNotify,msource 7→ i ,mdest 7→ i + 1], m)∧ unchanged hsenderVars, notaryVarsi∨ ∧ ¬valid∧ Discard (m)∧ unchanged hsenderVars, ledgerVars, notaryVarsi
Ledger i receives an Execute request from process j∆

LedgerHandleExecuteRequest(i , j , m) =∆let valid = ∧ ledgerState[i ] = L Prepared∧ j = Notaryin ∨ ∧ valid∧ ledgerState 0 = [ledgerState except ! [i ] = L Executed ]∧ Reply([mtype 7→ ExecuteNotify,msource 7→ i ,mdest 7→ i − 1], m)∧ unchanged hsenderVars, notaryVarsi∨ ∧ ¬valid∧ Discard (m)∧ unchanged hsenderVars, ledgerVars, notaryVarsi
Ledger i receives an Abort request from process j∆

LedgerHandleAbortRequest(i , j , m) =∆let valid = ∧ ∨ ledgerState[i ] = L Proposed∨ ledgerState[i ] = L Prepared∧ j = Notaryin ∨ ∧ valid∧ ledgerState 0 = [ledgerState except ! [i ] = L Aborted ]∧ Reply([mtype 7→ AbortNotify,msource 7→ i ,mdest 7→ i − 1], m)∧ unchanged hsenderVars, notaryVarsi∨ ∧ ¬valid∧ Discard (m)∧ unchanged hsenderVars, ledgerVars, notaryVarsi
Ledger i receives a message∆

LedgerReceive(i , j , m) =∨ ∧ m.mtype = PrepareRequest∧ LedgerHandlePrepareRequest(i , j , m)
∨ ∧ m.mtype = ExecuteRequest∧ LedgerHandleExecuteRequest(i , j , m)
∨ ∧ m.mtype = AbortRequest∧ LedgerHandleAbortRequest(i , j , m)
Ledger j notifies sender that the transfer is executed∆

SenderHandleExecuteNotify(i , j , m) =∨ ∧ senderState = S Waiting∧ senderState 0 = S Done
∧ Discard (m)15Note: This version is outdated!
For the latest version, please look at https://interledger.org/developers/rfcs/interledger-protocol/.

∧ unchanged hledgerVars, notaryVarsi∨ ∧ senderState 6= S Waiting∧ Discard (m)∧ unchanged hsenderVars, ledgerVars, notaryVarsi
Ledger j notifies sender that the transfer is aborted∆

SenderHandleAbortNotify(i , j , m) =∆let isSenderWaiting = ∨ senderState = S Waiting∨ senderState = S Readyin ∨ ∧ isSenderWaiting∧ senderState 0 = S Done
∧ Discard (m)∧ unchanged hledgerVars, notaryVarsi∨ ∧ ¬isSenderWaiting∧ Discard (m)∧ unchanged hsenderVars, ledgerVars, notaryVarsi
Sender receives a message∆

SenderReceive(i , j , m) =∨ ∧ m.mtype = ExecuteNotify∧ SenderHandleExecuteNotify(i , j , m)
∨ ∧ m.mtype = AbortNotify∧ SenderHandleAbortNotify(i , j , m)
Ledger j notifies recipient that the transfer is prepared∆

RecipientHandlePrepareNotify(i , j , m) =∧ Reply([mtype
7→ SubmitReceiptRequest,msource 7→ i ,mdest
7→ Notary,
mreceipt 7→ R ReceiptSignature], m)∧ unchanged hsenderVars, ledgerVars, notaryVarsi
Recipient receives a message∆

RecipientReceive(i , j , m) =∧ m.mtype = PrepareNotify∧ RecipientHandlePrepareNotify(i , j , m)
Ledger j notifies connector i that the transfer is prepared∆

ConnectorHandlePrepareNotify(i , j , m) =∧ Reply([mtype 7→ PrepareRequest,msource 7→ i ,mdest 7→ i + 1], m)∧ unchanged hsenderVars, ledgerVars, notaryVarsi
Ledger j notifies connector i that the transfer is executed∆

ConnectorHandleExecuteNotify(i , j , m) =∧ Reply([mtype 7→ ExecuteRequest,msource 7→ i ,mdest 7→ i − 1], m)∧ unchanged hsenderVars, ledgerVars, notaryVarsi
Ledger j notifies connector i that the transfer is aborted∆

ConnectorHandleAbortNotify(i , j , m) =∧ Discard (m)∧ unchanged hsenderVars, ledgerVars, notaryVarsi
Connector receives a message

16

Note: This version is outdated!
For the latest version, please look at https://interledger.org/developers/rfcs/interledger-protocol/.

∆ConnectorReceive(i , j , m) =∨ ∧ m.mtype = PrepareNotify∧ ConnectorHandlePrepareNotify(i , j , m)
∨ ∧ m.mtype = ExecuteNotify∧ ConnectorHandleExecuteNotify(i , j , m)
∨ ∧ m.mtype = AbortNotify∧ ConnectorHandleAbortNotify(i , j , m)
Notary receives a signed receipt∆

NotaryHandleSubmitReceiptRequest(i , j , m) =∨ ∧ m.mreceipt = R ReceiptSignature∧ notaryState = N Waiting∧ notaryState 0 = N Committed∧ ReplyBroadcast({[mtype7→ ExecuteRequest,msource 7→ i ,mdest
7→ k ] : k ∈ Ledger }, m)∧ unchanged hsenderVars, ledgerVarsi∨ ∧ notaryState 6= N Waiting∧ Discard (m)∧ unchanged hsenderVars, ledgerVars, notaryVarsi
Notary receives a message∆

NotaryReceive(i , j , m) =∧ m.mtype = SubmitReceiptRequest∧ NotaryHandleSubmitReceiptRequest(i , j , m)Receive a message∆

Receive(m) =∆let i = m.mdest∆
j = m.msourcein ∨ ∧ i ∈ Ledger∧ LedgerReceive(i , j , m)
∨ ∧ i = Sender∧ SenderReceive(i , j , m)
∨ ∧ i = Recipient∧ RecipientReceive(i , j , m)
∨ ∧ i ∈ Connector∧ ConnectorReceive(i , j , m)
∨ ∧ i = Notary∧ NotaryReceive(i , j , m)
End of message handlers
Defines how the variables may transition∆

Termination =∧ ∀ l ∈ Ledger : IsFinalLedgerState(ledgerState[l ])∧ senderState = S Done
∧ unchanged vars∆

Next = ∨ Start(Sender )∨ NotaryTimeout∨ ∃ l ∈ Ledger : LedgerAbort(l )∨ ∃ m ∈ domain messages : Receive(m)∨ Termination
17

Note: This version is outdated!
For the latest version, please look at https://interledger.org/developers/rfcs/interledger-protocol/.

The specification must start with the initial state and transition according
to Next.

Spec = Init ∧ 2[Next]vars∆

18

Note: This version is outdated!
For the latest version, please look at https://interledger.org/developers/rfcs/interledger-protocol/.

A.4

Formal Specification: Universal mode
module Universal

Formal Specification in TLA+ of the Interledger Protocol Universal (ILP /U )Modeled after the excellent Raft specification by Diego Ongaro.
Available at https://github.com/ongardie/raft.tla
Copyright 2014 Diego Ongaro.
This work is licensed under the Creative Commons Attribution-4.0
International License https://creativecommons.org/licenses/by/4.0/

extends Naturals, Sequences, FiniteSets, Bags, TLC
The set of ledger IDs

constants Ledger
The set of participant IDs

constants Participant
Sender states

constants S Ready, S ProposalWaiting, S Waiting, S Done
Connector states

constants C Ready, C Proposed
Ledger states

constants L Proposed , L Prepared , L Executed , L Aborted
Message types

constants PrepareRequest, ExecuteRequest, AbortRequest,
PrepareNotify, ExecuteNotify, AbortNotify,
SubpaymentProposalRequest, SubpaymentProposalResponse
Receipt signature

constants R ReceiptSignature
Global variables
Under synchrony we are allowed to have a global clock

variable clock
A bag of records representing requests and responses sent from one process
to anothervariable messages
Sender variables
State of the sender (S Ready, S Waiting, S Done)variable senderState
Whether the sender has received a response from a given connector

variable senderProposalResponses
All sender variables∆

senderVars = hsenderState, senderProposalResponsesi
Connector variables

19Note: This version is outdated!
For the latest version, please look at https://interledger.org/developers/rfcs/interledger-protocol/.

State of the connector (C Ready, C Proposed)

variable connectorStateAll sender variables∆

connectorVars = hconnectorStatei
The following variables are all per ledger (functions with domain Ledger )The ledger state (L Proposed, L Prepared, L Executed or L Aborted)variable ledgerState
The timeouts for each of the the transfers

variable ledgerExpiration
All ledger variables∆

ledgerVars = hledgerState, ledgerExpirationi

All variables; used for stuttering (asserting state hasn’t changed)∆vars = hclock , messages, senderVars, connectorVars, ledgerVarsi

Helpers
Add a set of new messages in transit∆

Broadcast(m) = messages 0 = messages ⊕ SetToBag(m)Add a message to the bag of messages∆

Send (m) = Broadcast({m})
Remove a message from the bag of messages. Used when a process is done
processing a message.
∆

Discard (m) = messages 0 = messages

SetToBag({m})

Respond to a message by sending multiple messages∆

ReplyBroadcast(responses, request) =messages 0 = messages SetToBag({request}) ⊕ SetToBag(responses)
Combination of Send and Discard∆

Reply(response, request) =ReplyBroadcast({response}, request)
Return the minimum value from a set, or undefined if the set is empty.
∆

Min(s) = choose x ∈ s : ∀ y ∈ s : x ≤ yReturn the maximum value from a set, or undefined if the set is empty.
∆

Max (s) = choose x ∈ s : ∀ y ∈ s : x ≥ y
Is a final ledger state∆

IsFinalLedgerState(i ) = i ∈ {L Executed , L Aborted }Sender∆Sender = Min(Participant)
Recipient∆

Recipient = Max (Participant)Set of connectors∆

Connector = Participant \ {Sender , Recipient}
20Note: This version is outdated!
For the latest version, please look at https://interledger.org/developers/rfcs/interledger-protocol/.

The clock value we expect to be at after the proposal phase∆

ClockAfterProposal = 2 ∗ Cardinality(Connector ) + 2
The clock value we expect after the preparation phase∆

ClockAfterPrepare = ClockAfterProposal + 2 ∗ Cardinality(Ledger ) + 1
The clock value we expect to be at after the execution phase∆

ClockAfterExecution = ClockAfterPrepare + 2 ∗ Cardinality(Ledger ) + 1
Define type specification for all variables∆

TypeOK = ∧ clock ∈ Nat∧ IsABag(messages)∧ senderState ∈ {S Ready, S ProposalWaiting, S Waiting, S Done}∧ senderProposalResponses ∈ [Connector → boolean ]∧ connectorState ∈ [Connector → {C Ready, C Proposed }]∧ ledgerState ∈ [Ledger → {L Proposed , L Prepared , L Executed , L Aborted }]∧ ledgerExpiration ∈ [Ledger → Nat]∆

Consistency =∀ l 1, l 2 ∈ Ledger : ¬ ∧ ledgerState[l 1] = L Aborted∧ ledgerState[l 2] = L Executed∆

Inv = ∧ TypeOK∧ Consistency
Define initial values for all variables∆

InitSenderVars = ∧ senderState = S Ready∧ senderProposalResponses = [i ∈ Connector 7→ false]∆

InitConnectorVars = connectorState = [i ∈ Connector 7→ C Ready]∆

InitLedgerVars = ∧ ledgerState = [i ∈ Ledger 7→ L Proposed ]∧ ledgerExpiration = [i ∈ Ledger 7→ ClockAfterExecution − i ]∆Init = ∧ clock = 0∧ messages = EmptyBag∧ InitSenderVars∧ InitConnectorVars∧ InitLedgerVars
Define state transitions
Participant i proposes all the subpayments∆

StartProposalPhase(i ) =∧ senderState = S Ready∧ senderState 0 = S ProposalWaiting∧ Broadcast({[mtype
7→ SubpaymentProposalRequest,msource 7→ i ,
mdest
7→ k
] : k ∈ Connector })∧ unchanged hledgerVars, connectorVars, senderProposalResponsesi
Participant i starts off the preparation chain

21

Note: This version is outdated!
For the latest version, please look at https://interledger.org/developers/rfcs/interledger-protocol/.

∆StartPreparationPhase(i ) =∧ senderState = S ProposalWaiting∧ ∃ p ∈ domain senderProposalResponses : senderProposalResponses[p]∧ senderState 0 = S Waiting∧ Send ([mtype 7→ PrepareRequest,msource 7→ i ,mdest 7→ i + 1])∧ unchanged hledgerVars, connectorVars, senderProposalResponsesi
Ledger spontaneously aborts∆

LedgerAbort(l ) =∧ ledgerState[l ] = L Proposed∧ ledgerState 0 = [ledgerState except ! [l ] = L Aborted ]∧ Send ([mtype 7→ AbortNotify,msource 7→ l ,mdest 7→ l − 1])∧ unchanged hsenderVars, connectorVars, ledgerExpirationi
Transfer times out∆

LedgerTimeout(l ) =∧ ¬IsFinalLedgerState(ledgerState[l ])∧ ledgerExpiration[l ] ≤ clock∧ ledgerState 0 = [ledgerState except ! [l ] = L Aborted ]∧ Send ([mtype 7→ AbortNotify,msource 7→ l ,mdest 7→ l − 1])∧ unchanged hsenderVars, connectorVars, ledgerExpirationi
If no messages are in flight and the sender isn’t doing anything, advance theclock∆

NothingHappens =∧ clock ≤ Max ({ledgerExpiration[x ] : x ∈ Ledger })∧ BagCardinality(messages) = 0∧ senderState 6= S Ready∧ ∨ senderState 6= S ProposalWaiting∨ ∀ p ∈ domain senderProposalResponses : ¬senderProposalResponses[p]∧ unchanged hmessages, senderVars, connectorVars, ledgerVarsi
Message handlers
i = recipient, j = sender, m = message
Ledger i receives a Prepare request from participant j∆

LedgerHandlePrepareRequest(i , j , m) =∆let valid = ∧ ledgerState[i ] = L Proposed∧j =i −1in ∨ ∧ valid∧ i ∈ Ledger∧ ledgerState 0 = [ledgerState except ! [i ] = L Prepared ]∧ Reply([mtype 7→ PrepareNotify,msource 7→ i ,mdest 7→ i + 1], m)∧ unchanged hsenderVars, connectorVars, ledgerExpirationi∨ ∧ ¬valid∧ i ∈ Ledger∧ Discard (m)22Note: This version is outdated!
For the latest version, please look at https://interledger.org/developers/rfcs/interledger-protocol/.

∧ unchanged hsenderVars, connectorVars, ledgerVarsi
Ledger i receives an Execute request from process j∆

LedgerHandleExecuteRequest(i , j , m) =∆let valid = ∧ ledgerState[i ] = L Prepared∧ ledgerExpiration[i ] > clock∧ m.mreceipt = R ReceiptSignaturein ∨ ∧ valid∧ ledgerState 0 = [ledgerState except ! [i ] = L Executed ]∧ Reply([mtype
7→ ExecuteNotify,msource 7→ i ,mdest
7→ i − 1,
mreceipt 7→ m.mreceipt], m)∧ unchanged hsenderVars, connectorVars, ledgerExpirationi∨ ∧ ¬valid∧ Discard (m)∧ unchanged hsenderVars, connectorVars, ledgerVarsi
Ledger i receives a message∆

LedgerReceive(i , j , m) =∨ ∧ m.mtype = PrepareRequest∧ LedgerHandlePrepareRequest(i , j , m)
∨ ∧ m.mtype = ExecuteRequest∧ LedgerHandleExecuteRequest(i , j , m)
Sender receives a SubpaymentProposal request∆

SenderHandleSubpaymentProposalResponse(i , j , m) =∧ i = Sender∧ senderProposalResponses 0 = [senderProposalResponses except ! [j ] = true]∧ Discard (m)∧ unchanged hconnectorVars, ledgerVars, senderStatei
Ledger j notifies sender that the transfer is executed∆

SenderHandleExecuteNotify(i , j , m) =∨ ∧ senderState = S Waiting∧ senderState 0 = S Done
∧ Discard (m)∧ unchanged hledgerVars, connectorVars, senderProposalResponsesi∨ ∧ senderState 6= S Waiting∧ Discard (m)∧ unchanged hsenderVars, connectorVars, ledgerVarsi
Ledger j notifies sender that the transfer is aborted∆

SenderHandleAbortNotify(i , j , m) =∆let isSenderWaiting = senderState ∈ {S ProposalWaiting, S Waiting, S Ready}in ∨ ∧ isSenderWaiting∧ senderState 0 = S Done
∧ Discard (m)∧ unchanged hledgerVars, connectorVars, senderProposalResponsesi∨ ∧ ¬isSenderWaiting∧ Discard (m)∧ unchanged hsenderVars, connectorVars, ledgerVarsi
Sender receives a message∆

SenderReceive(i , j , m) =∨ ∧ m.mtype = SubpaymentProposalResponse
23Note: This version is outdated!
For the latest version, please look at https://interledger.org/developers/rfcs/interledger-protocol/.

∧ SenderHandleSubpaymentProposalResponse(i , j , m)
∨ ∧ m.mtype = ExecuteNotify∧ SenderHandleExecuteNotify(i , j , m)
∨ ∧ m.mtype = AbortNotify∧ SenderHandleAbortNotify(i , j , m)
Ledger j notifies recipient that the transfer is prepared∆

RecipientHandlePrepareNotify(i , j , m) =∨ ∧ Reply([mtype
7→ ExecuteRequest,msource 7→ i ,mdest
7→ i − 1,
mreceipt 7→ R ReceiptSignature], m)∧ unchanged hsenderVars, connectorVars, ledgerVarsi
Recipient receives a message∆

RecipientReceive(i , j , m) =∨ ∧ m.mtype = PrepareNotify∧ RecipientHandlePrepareNotify(i , j , m)Connector i receives a SubpaymentProposal request∆

ConnectorHandleSubpaymentProposalRequest(i , j , m) =∧ connectorState 0 = [connectorState except ! [i ] = C Proposed ]∧ Reply([mtype
7→ SubpaymentProposalResponse,msource 7→ i ,mdest
7→ j ], m)∧ unchanged hsenderVars, ledgerVarsi
Ledger j notifies connector i that the transfer is prepared∆

ConnectorHandlePrepareNotify(i , j , m) =∨ ∧ Reply([mtype 7→ PrepareRequest,msource 7→ i ,mdest 7→ i + 1], m)∧ unchanged hsenderVars, connectorVars, ledgerVarsi
Ledger j notifies connector i that the transfer is executed∆

ConnectorHandleExecuteNotify(i , j , m) =∧ Reply([mtype
7→ ExecuteRequest,msource 7→ i ,mdest
7→ i − 1,
mreceipt 7→ m.mreceipt], m)∧ unchanged hsenderVars, connectorVars, ledgerVarsi
Ledger j notifies connector i that the transfer is aborted∆

ConnectorHandleAbortNotify(i , j , m) =∧ Discard (m)∧ unchanged hsenderVars, connectorVars, ledgerVarsi
Connector receives a message∆

ConnectorReceive(i , j , m) =∨ ∧ m.mtype = SubpaymentProposalRequest∧ ConnectorHandleSubpaymentProposalRequest(i , j , m)
∨ ∧ m.mtype = PrepareNotify∧ ConnectorHandlePrepareNotify(i , j , m)
∨ ∧ m.mtype = ExecuteNotify∧ ConnectorHandleExecuteNotify(i , j , m)
∨ ∧ m.mtype = AbortNotify
24Note: This version is outdated!
For the latest version, please look at https://interledger.org/developers/rfcs/interledger-protocol/.

∧ ConnectorHandleAbortNotify(i , j , m)Receive a message∆

Receive(m) =∆let i = m.mdest∆
j = m.msourcein ∨ ∧ i ∈ Ledger∧ LedgerReceive(i , j , m)
∨ ∧ i = Sender∧ SenderReceive(i , j , m)
∨ ∧ i = Recipient∧ RecipientReceive(i , j , m)
∨ ∧ i ∈ Connector∧ ConnectorReceive(i , j , m)
End of message handlers
Defines how the variables may transition∆

Termination =∧ ∀ l ∈ Ledger : IsFinalLedgerState(ledgerState[l ])∧ senderState = S Done
∧ unchanged vars∆

Next = ∨ ∧ ∨ StartProposalPhase(Sender )∨ StartPreparationPhase(Sender )∨ ∃ l ∈ Ledger : LedgerAbort(l )∨ ∃ l ∈ Ledger : LedgerTimeout(l )∨ ∃ m ∈ domain messages : Receive(m)∨ NothingHappens∧ clock 0 = clock + 1∨ Termination
The specification must start with the initial state and transition according
to Next.

Spec = Init ∧ 2[Next]vars∆

25