# Analysis of the settlement algorithm & attack vectors #188

Closed
opened this issue Jul 13, 2018 · 12 comments
Closed

# Analysis of the settlement algorithm & attack vectors#188

opened this issue Jul 13, 2018 · 12 comments
Labels
Milestone

### loredanacirstea commented Jul 13, 2018 • edited

 I have analyzed some edge cases that could have made attacks possible and demonstrated that there cannot be attacks in those specific cases (until proven wrong). I cannot guarantee that all edge cases have been analyzed. The logic & calculations presented in my 6 comments below should also be verified by others. TODO: I have started by analyzing the current settlement algorithm. It would be worth to also analyze the edge cases irrespective of the current implementation, as mentioned in #188 (comment) and #188 (comment)

# Settlement algorithm

This has been explained in detail here: https://github.com/raiden-network/spec/blob/3a88d245293a3318297764d760ddd5fb198912c2/smart_contracts.rst#protocol-values-and-settlement-algorithm-analysis

## Definitions:

• `valid last BP` = a balance proof that respects the official Raiden client constraints and is the last balance proof known.
• `valid old BP` = a balance proof that respects the official Raiden client constraints, but there are other newer balance proofs that were created after it (additional transfers happened)
• `invalid BP` = a balance proof that does not respect the official Raiden client constraints; E.g. someone else implements a malicious Raiden client and convinces people to use it.
``````Channel participants: P1, P2
D1 = P1's deposit
W1 = P1's withdrawn amount
T1 = P1's transferred amount to P2
L1 = P1's locked amount in pending transfers to P2
Lc1 = P1's locked amount in pending transfers to P2, that can be claimed by P2 (locks secrets have been registered on-chain, in the Secret Registry)
Lu1 = P1's locked amount in pending transfers to P2, that is unclaimable by P2 (locks secrets have not been registered on-chain), therefore belongs to P1
L1 = Lc1 + Lu1

B1 = total final amount that must be received by P1 after channel settlement and unlock
S1 = amount received by P1 at settlement
SL1 = amount locked in the TokenNetwork contract at settlement time, representing L1
SLc1 = amount that can be claimed by P2 from the total SL1 by calling unlock
SLu1 = amount that will go back to P1 from the total SL1 by calling unlock

AB1 = available balance for P1; determines if P1 can make additional transfers to P2 or not

D1k = D1 at time k
T1k = T1 at time k
L1k = L1 at time k
``````

## Constraints that we can expect for valid last balance proofs

• `TN` = enforced by the TokenNetwork contract
• `R` = enforced by the Raiden client
``````(1 TN) Dk <= Dt, time k < time t
(2 TN) Wk <= Wt, time k < time t
(3 R) Tk <= Tt, time k < time t
(4 R) Tk + Lck <= Tt + Lct, time k < time t
(5 R) AB1 = D1 - W1 + T2 - T1 - L1; AB1 >= 0, AB1 <= TAD
(5.1 R) L1 <= AB1, L1 <= TAD, L1 >= 0
(6 R) W1 <= D1 + T2 - T1 - L1
(7 R) T2 + L2 - T1 - L1 <= D2
(8) B1 = D1 - W1 + T2 - T1 + Lc2 - Lc1, B1 >= 0
(9) B2 = D2 - W2 + T1 - T2 + Lc1 - Lc2, B2 >= 0
(10) B1 + B2 = TAD, where TAD = D1 + D2 - W1 - W2, TAD >= 0
``````

(update) added `(4 R)`, as mentioned in #188 (comment). Removed a constraint after #188 (comment), because it was not correct.

## Cases we need to pay attention to

(also read #188 (comment) about the dynamic between `T` and `L`)

``````{1} L1k <= L1t, k < t, T1k <= T1t
n >= delta_t, where:
n =  total token amount from all the P1 -> P2 transfers started during (k, t);
this can go to T or stay locked in L
delta_t = T1t - T1k, P1 -> P2 transfers that have finalized during (k, t)
L1t = L1k - delta_t + n

{2} L1k > L1t, k < t, T1k < T1t
# The locked amount does not monotonically increase between 2 successive balance proofs
# with different transferred amounts.
# This can happen if:
n < delta_t, where:
n = total token amount from all the P1 -> P2 transfers started during (k, t);
this can go to T or stay locked in L
delta_t = T1t - T1k, P1 -> P2 transfers that have finalized during (k, t)
L1t = L1k - delta_t + n

{3} Lu1k <= Lu1t, k < t
# as time passes

{4} Lu1k > Lu1t, k < t
# This can happen if pending transfers have expired and they are removed from the
# merkle tree and the locked amount is therefore reduced
``````

## Final expected balances at the end of the channel lifecycle

(after settlement & unlocks)

• We must ensure that the current implementation is equivalent to (8), (9), (10) - `B1`, `B2` definitions. The current implementation in the smart contract is:
``````(1C)
B1c = S1 + SLc2 + SLu1
B2c = S2 + SLc1 + SLu2
``````

Important

• (*) We must enforce that `P1` receives `B1` and `P2` receives `B2` at the end of the channel lifecycle for any `valid last BP P1` and `valid last BP P2`
• (**) We must enforce that a participant who uses an old balance proof of his partner does not receive more tokens than expected and the partner does not lose tokens:
• We must enforce that `P2` receives `>= B2` => `P1` receives `<= B1` if `P1` uses `valid old BP P2`
• We must enforce that `P1` receives `>= B1` => `P2` receives `<= B2` if `P2` uses `valid old BP P1`

## Settlement algorithm, as implemented now in Solidity:

Line 598 in 4dc3b55

 function getSettleTransferAmounts(

``````RmaxP1 = the maximum receivable amount by P1 at settlement time; this concept exists only for handling the overflows and underflows.
RmaxP2 = the maximum receivable amount by P2 at settlement time; this concept exists only for handling the overflows and underflows.
``````

The following is explained in detail here: https://github.com/raiden-network/spec/blob/3a88d245293a3318297764d760ddd5fb198912c2/smart_contracts.rst#solidity-settlement-algorithm---explained

``````RmaxP1 = (T2 + L2) - (T1 + L1) + D1 - W1

SL2 = min(RmaxP1, L2)
S1 = RmaxP1 - SL2

SL1 = min(RmaxP2, L1)
S2 = RmaxP2 - SL1
``````

Notes:

• `settleChannel` must not fail and it was constructed to handle overflows and underflows without failing. Some explanations here: #117 (comment)

• Due to bounding the values there are some points where attacks might be possible:

``````RmaxP1 = min(TAD, RmaxP1)
``````
``````SL2 = min(RmaxP1, L2)
``````
``````SL1 = min(RmaxP2, L1)
``````

For reference, more explanations on the process of arriving to this settlement algorithm:
#131
#123

For reference, the old implementation of the settlement algorithm:
https://github.com/raiden-network/raiden/blob/80b0ccaae62aa1ca109cd04101fc51f6eaac8cfc/raiden/smart_contracts/NettingChannelLibrary.sol#L309-L341

# Proof of correctness - current settlement algorithm - case 

``````RmaxP1 = min(TAD, RmaxP1)
``````

We need to find the cases where `RmaxP1 > TAD` and see if any attacks are possible due to bounding to `TAD`.

`RmaxP1 > TAD` --> `(T2 + L2) - (T1 + L1) + D1 - W1 > TAD`
This can happen if:

1. `T2 + L2` is bigger than expected
2. `T1 + L1` is smaller than expected
3. `W1` is smaller than expected
4. `D1` is bigger than expected

## 3. & 4.

At settlement time we always have the last known `D1` and `W1`, because the smart contract has direct access to the last value --> 3. & 4. cannot happen

## 1. & 2.

a) at least 1 balance proof is invalid --> this means both participants are using a malicious Raiden client --> smart contract cannot do anything.
b) both balance proofs are valid, 1 balance proof is old
c) both balance proofs are valid & old --> the smart contract has no way to know what are the last balance proofs. This is a case that should never happen when using the Raiden client in the intended way. We assume that if the contract computes the amounts correctly for all other cases, then it will compute a fair amount even in this case, from the values it receives.

Case 2. when b) happens:

`P2` has submitted an old balance proof for `P1` (`P2` can be considered the attacker)
In this case, `P2` must not receive more tokens in this case (`time=k`), compared with `P2` using the last balance proof of `P1` (`time=t, t > k`)

--> `(T2 + L2) - (T1k + L1k) + D1 - W1 > TAD` is possible, but `P1` will nonetheless receive the additional tokens resulted from `T1t + L1t - (T1k + L1k)` Therefore, `P2` will punish himself, receiving `0` tokens `T1t + L1t - (T1k + L1k)` less tokens.
As an edge case, if `P2` does not submit `P1`s balance proof at all, he will receive `0` tokens.

For the sake of analysis, we can have 2 cases:
i) `T1k <= T1t` (3 R) & `L1k <= L1t` {1a}, {2a}
ii) `T1k <= T1t` (3 R) & `L1k > L1t` {1b}, {2b}

For this case, i) and ii) have no additional consequences and `P2` would still punish himself and receive `0` tokens.

as @Dominik1999 pointed out, we have an additional case here:
Case 1. when b) happens:

`P1` has submitted an old balance proof for `P2` (`P1` can be considered the attacker)
Therefore, `P1` submits `T2k` and `L2k`, part of an old balance proof that was valid and last at `time = k` and `T2k + L2k > T2 + L2`, `k < t` (`t` is the time at which the last valid balance proof was emitted, containing `T2` and `L2`)

we know `(4 R) T2k + Lc2k <= T2 + Lc2`
--> `Lu2k > Lu2` (as shown in `{4}`) - the problem lies with the unclaimable, expired locked amount.

The only case where `T2k + L2k > T2 + L2` can happen is if `L2k` contains a bigger amount of tokens corresponding to locked transfers that have expired and are therefore unclaimable by `P1`.
Moreover, if `RmaxP1 > TAD`, then we are bounding the maximum amount of tokens that `P1` can receive. `P2` remains unaffected.

# Proof of correctness - current settlement algorithm - case 

``````SL2 = min(RmaxP1, L2)
``````

An attack might be possible if `RmaxP1 < L2`, because we bound `L2` to `RmaxP1` --> exclude `L2 - RmaxP1` tokens from the calculation.

`RmaxP1 < L2` --> `(T2 + L2) - (T1 + L1) + D1 - W1 < L2` --> `AB1 + L2 < L2` --> `AB1 < 0`

--> this case will never happen for `valid last BP P1` & `valid last BP P2` `(5 R)`
We need to check:
a) `valid last BP P1` & `valid old BP P2`, `T2k + L2k > T1 + L1`
b) `valid old BP P1` & `valid last BP P2`, `T2 + L2 > T1k + L1k`

I use `T2k + L2k > T1 + L1` and `T2 + L2 > T1k + L1k`, maintaining the order in which the `RmaxPx` is computed (`RmaxP1` first, and then `RmaxP2`). The same logic applies for the reverse order (computing `RmaxP2` first and then `RmaxP1`).

``````*o = any already defined variable calculated at settlement time with a valid last BP and a valid old BP, regardless of order
# e.g.
RmaxP1o = RmaxP1 calculated at settlement time with a valid last BP and a valid old BP, regardless of order
``````

## Case a):

`valid last BP P1` at `time=t` & `valid old BP P2` at `time=k`, `T2k + L2k > T1 + L1`, `k < t`

In this case, the attacker is `P1`. For `P1` to actually steal tokens, it means that his final balance (all the tokens that he will receive after settlement & unlock) when using `valid old BP P2` must be greater than his final balance when using `valid last BP P2`. Therefore, the following must be true:

• `B1o > B1` with `(8)` --> `D1 - W1 + T2k - T1 + Lc2k - Lc1 > D1 - W1 + T2 - T1 + Lc2 - Lc1` --> `T2k + Lc2k > T2 + Lc2`

(update: I was previously describing an attack case here. This attack is not actually possible due to an additional constraint that I did not consider at that point in time. The additional constraint is `T2k + Lc2k <= T2t + Lc2t` and was pointed out by @hackaugusto and also mentioned in #188 (comment))

The above attack incentive `T2k + Lc2k > T2 + Lc2` must never be true, as shown in `(4 R)`

However, I do not take into consideration the fact that the attacked participant might be forced to do an on-chain transaction to retrieve all of his tokens.

## Case b):

`valid old BP P1` `time=k` & `valid last BP P2` `time=t`, `T2 + L2 > T1k + L1k`, `k < t`

• P2 is the attacker.

`RmaxP1o < L2` --> `D1 - W1 + T2 + L2 - T1k - L1k < L2` --> `T1k + L1k > T1 + L1`
we know `(4 R) T1k + Lc1k <= T1 + Lc1` & `{4} Lu1k > Lu1` --> the problem lies with the unclaimable, expired locked amount.
The secrets are not known for these expired transfers, therefore they cannot be claimed by `P2` and will return to `P1`.

Therefore:

```T1k + L1k > T1 + L1  # -->
T1k + Lc1k + Lu1k > T1 + Lc1 + Lu1  # -->
Lu1k - Lu1 > T1 + Lc1 - T1k - Lc1k

# we know:
T1 + Lc1 >= T1k + Lc1k  # -->
T1 + Lc1 - T1k - Lc1k >= 0

# we can define:
(i) Lu1k - Lu1 = T1 + Lc1 - T1k - Lc1k + n, n > 0```

In the worst case scenario, the tokens we exclude by bounding the `L2` amount by `RmaxP1o` are all claimable by `P1`. Therefore, we need to demonstrate that what `P1` might "lose" when we bound `L2` is actually returned back to him through `Lu1k`, when the `L1k` tokens are unlocked.
Therefore, we need to prove that:

`L2 - RmaxP1o <= Lu1k - Lu1`

We have `(i)`, we can write that as ` (ii) T1 + Lc1 - T1k - Lc1k = Lu1k - Lu1 - n`

```RmaxP1 - RmaxP1o = D1 - W1 + T2 + L2 - T1 - L1 - (D1 - W1 + T2 + L2 - T1k - L1k)
= T1k + L1k - T1 - L1
= T1k + Lc1k + Lu1k - T1 - Lc1 - Lu1
# we are just changing the order here
= - (T1 + Lc1 - T1k - Lc1k) + Lu1k - Lu1
# using (ii), we get:
= - (Lu1k - Lu1 - n) + Lu1k - Lu1 =
= n```

--> `RmaxP1 - RmaxP1o = n`

We also know that for `valid last` balance proofs `L2 < RmaxP1` --> `L2 - RmaxP1o <= RmaxP1 - RmaxP1o`
Therefore, we have `(iii) L2 - RmaxP1o <= n`

Going back to `(i) Lu1k - Lu1 = T1 + Lc1 - T1k - Lc1k + n, n > 0`, we know that `(4 R) T1 + Lc1 - T1k - Lc1k` >= 0 --> `(iv) Lu1k - Lu1 >= n`

From `(iii)` & `(iv)`: `L2 - RmaxP1o <= n <= Lu1k - Lu1` --> `L2 - RmaxP1o <= Lu1k - Lu1`. This is what we needed to prove.

However, all these `Lu1k - Lu1` tokens are returned to `P1` when `P1`'s pending transfers are unlocked on-chain, as long as `L1 <= RmaxP2o` (no bounding happens at this level).

We showed above that `T1k + L1k > T1 + L1` is required for this to be an attack --> `L1 < T1k + L1k - T1`.
We need to demonstrate that `T1k + L1k - T1 <= RmaxP2o` -->

```T1k + L1k - T1 <= RmaxP2o  # -->
T1k + L1k - T1 <= D2 - W2 + T1k + L1k - T2 - L2  # -->
0 <= D2 - W2 + T1 - T2 - L2   # `(5 R)`, this is the available balance of P2, who has a valid BP, therefore true```

### Test case example 1:

Last known balance proofs at `time=t`:

``````D1 = 45
W1 = 5
T1 = 100
Lc1 = 3
Lu1 = 0

D2 = 60
W2 = 10
T2 = 70
Lc2 = 55
Lu2 = 0
``````

Check if balance proofs are valid `(5 R)`

``````AB1 = D1 - W1 + T2 - T1 - L1 = 45 - 5 + 70 - 100 - 3 = 7 >= 0
AB2 = D2 - W2 + T1 - T2 - L2 = 60 - 10 + 100 - 70 - 55 = 25 >= 0
``````

Expected settlement amounts (8), (9), (10)

``````B1 = D1 - W1 + T2 - T1 + Lc2 - Lc1 = 45 - 5 + 70 - 100 + 55 - 3 = 62
B2 = D2 - W2 + T1 - T2 + Lc1 - Lc2 = 60 - 10 + 100 - 70 + 3 - 55 = 28
B1 + B2 = 90 = TAD
``````

An old balance proof for `P1` at `time=k` might look like:

``````D1 = 45
W1 = 5
T1 = 100
Lc1 = 3
Lu1 = 10
``````
• we calculate how many tokens will `P1` and `P2` receive if `BP_P1k` & `BP_P2` are used:
``````RmaxP1 = (T2 + L2) - (T1k + L1k) + D1 - W1 = 70 + 55 - 100 - 13 + 45 - 5 = 52
SL2 = min(RmaxP1, L2) = min(52, 55) = 52
S1 = 0

RmaxP2 = 90 - 52 = 38
SL1 = 13
S1 = 38 - 13 = 25
``````
• `unlock` `P2`'s pending transfers --> `P1` receives `52`
• `unlock` `P1`'s pending transfers --> `P2` receives `3`, `P1` receives `10`
In this scenario, the final received amounts are:
``````B1 = 52 + 10 = 62
B2 = 25 + 3 = 28
``````

These are the expected amounts.

# Proof of correctness - current settlement algorithm - case 

``````SL1 = min(RmaxP2, L1)
``````

tl;dr - same cases as above, in the reverse order.

An attack might be possible if `RmaxP2 < L1`, because we bound `L1` to `RmaxP2` --> we end up excluding `L1 - RmaxP2` tokens from the calculation.

`RmaxP2 < L1` --> `D2 - W2 + T1 + L1 - (T2 + L2) < L1` --> `AB2 + L1 < L1` --> `AB2 < 0`

--> this case will never happen for `valid last BP P1` & `valid last BP P2` `(5 R)`

We need to check:
a) `valid last BP P1` & `valid old BP P2`, `T2k + L2k >= T1 + L1`
b) `valid old BP P1` & `valid last BP P2`, `T2 + L2 >= T1k + L1k`

``````*o = any already defined variable calculated at settlement time with a valid last BP and a valid old BP, regardless of order
# e.g.
RmaxP1o = RmaxP1 calculated at settlement time with a valid last BP and a valid old BP, regardless of order
``````

## Case a)

`valid last BP P1` & `valid old BP P2`, `T2k + L2k >= T1 + L1`

• `P1` is the attacker

Therefore, we have:
`RmaxP2o < L1` --> `D2 - W2 + T1 + L1 - (T2k + L2k) < L1` --> `D2 - W2 + T1 - T2k - L2k < 0`
We know ` (5 R) D2 - W2 + T1 - T2 - L2 >= 0`

--> `T2k + L2k > T2 + L2`
`(4 R) T2k + Lc2k <= T2 + Lc2` & `{4}`
--> `Lu2k > Lu2` - the problem lies with the unclaimable, expired locked amount.

Same logic as in #188 (comment)
Taking the above into consideration, we have `Lu2k - Lu2 = T2 + Lc2 - T2k - Lc2k + n, n > 0`.

```RmaxP2 - RmaxP2o = D2 - W2 + T1 + L1 - T2 - L2 - (D2 - W2 + T1 + L1 - T2k - L2k)
= T2k + L2k - T2 - L2
= T2k + Lc2k + Lu2k - T2 - Lc2 - Lu2
= - (T2 + Lc2 - T2k - Lc2k) + Lu2k - Lu2
= - (Lu2k - Lu2 - n) + Lu2k - Lu2 =
= n```

In the worst case scenario, the tokens we exclude by bounding the `L1` amount by `RmaxP2o` are all claimable by `P2`. But `RmaxP2 > L1` --> `L1 - RmaxP2o < RmaxP2 - RmaxP2o` --> `L1 - RmaxP2o < n`. However, these `n` tokens are in fact returned to `P2` when `P2`'s pending transfers are unlocked, as long as `L2 <= RmaxP1o`.

We showed above that `T2k + L2k > T2 + L2 --> L2 < T2k + L2k - T2`.
We need to demonstrate that `T2k + L2k - T2 <= RmaxP1o` -->

```T2k + L2k - T2 <= RmaxP1o  # -->
T2k + L2k - T2 <= D1 - W1 + T2k + L2k - T1 - L1   # -->
0 <= D1 - W1 + T2 - T1 - L1   # (5 R), this is the available balance of P1, who has a valid BP, therefore true```

## Case b)

`valid old BP P1` & `valid last BP P2`, `T2 + L2 >= T1k + L1k`

• `P2` is the attacker

Same logic as in #188 (comment)

Therefore, we have:
`RmaxP2o < L1k` --> `D2 - W2 + T1k + L1k - (T2 + L2) < L1k` --> `D2 - W2 + T1k - (T2 + L2) < 0`
We know `(5 R) D2 - W2 + T1 - (T2 + L2) > 0`

--> `T1k = T1 - AB2 - n, T1k >= 0, n >= 0`

```RmaxP2o = D2 - W2 + T1k + L1k - T2 - L2
= D2 - W2 + (T1 - AB2 - n) + L1k - T2 - L2
= D2 - W2 + T1 - (D2 - W2 + T1 - T2 - L2) - n + L1k - T2 - L2
= L1k - n```

In this case, the attacker is `P2`. For `P2` to actually steal tokens, the following must be true:

• `B2o > B2` --> with `(8)` --> `D2 - W2 + T1k - T2 + Lc1k - Lc2 > D2 - W2 + T1 - T2 + Lc1 - Lc2` --> `T1k + Lc1k > T1 + Lc1`

The above attack incentive `T1k + Lc1k > T1 + Lc1` must never be true, as shown in `(4 R)`

However, I do not take into consideration the fact that the attacked participant might be forced to do an on-chain transaction to retrieve all of his tokens.

# General cases to explore, regardless of algorithm implementation

(work in progress)

1. `valid last BP P1` & `valid last BP P2`
2. `valid last BP P1` & `valid old BP P2`, `B1 >= B2`
3. `valid old BP P1` & `valid last BP P2`, `B1 >= B2`
4. at least 1 invalid BP - this case implies both P1 and P2 are using an unofficial, malicious Raiden client. The TokenNetwork smart contract has no way to determine the correct final amounts. Therefore, there are no guarantees about the channel settlement amounts.

These cases need to be explored in the context of any settlement algorithm & protocol that we implement.

# Mitigation

update - there were no real issues found yet, previous issues were based on a constraint that was not taken into consideration, mentioned in #188 (comment)

### hackaugusto commented Jul 18, 2018

#### Constraints that must be enforced by the Raiden client

The list is missing the following constraint:

``````(5R) T1k + Lc1k <= T1t + Lc1t, k < t
``````

Which is required to enforce the monotonicity of the transferred amount value.

#### Final expected balances at the end of the channel lifecycle

I think the following needs to be rephrased:

We must ensure that the current implementation is equivalent to (4), (5), (6).

Because the given constraints are only valid for the two `valid last BP`. If we rewrite the constraints as the following it will be more correct:

``````(#) Net1 = (T2 + Lc2) - (T1 + Lc1), where T2 + Lc2 >= T1 + Lc1
(#) B1 = min(max(D1 - W1 + Net1, 0), TAD)
(#) B2 = TAD - B1
``````

If the above is changed, the section name Important also needs to be reviewed.

### Settlement algorithm

#### Constraints

`(7) Lck <= Lct, k < t` is not correct. example:

1. A opens a channel with B, deposits 10
2. A sends a mediated transfer to B with lock.amount equal to 3 (Ta=0, Lca=0, Lua=3)
3. B requests the secret, and A sends the secret reveal (Ta=0, Lca=3, Lua=0)
4. A sends the unlock to B (Ta=3, Lca=0, Lua=0)

For `k=3` and `t=4` we have `Lca3=3`, `Lca4=0`. The correct constraint is:

(5R) T1k + Lc1k <= T1t + Lc1t, k < t

### loredanacirstea commented Jul 24, 2018

 Thank you, removed `(7)`. It should not affect the logic of the proofs, because they use `(5R)`

### hackaugusto commented Jul 24, 2018

 Suggestions on how to frame the problem: For any valid channel were both nodes follow the protocol, there will be a well-ordered list `l` of valid balance proofs. An attacker `A` may choose any of these balance proofs to take advantage during settlement. To guarantee safety Raiden's protocol must never benefit an attacker A which uses an old balance proof for settlement. Any two consecutive balance proofs `a` and `b` were `a < b` must respect the following constraints: A direct transfer with `value` was done, therefor `b.transferred_amount == a.transferred_amount + value` and `b.locked_amount == a.locked_amount`. A lock message with `value` was done, therefor `b.transferred_amount == a.transferred_amount` `b.locked_amount == a.locked_amount + value`. A unlock message for a previous `value` was done, therefor `b.transferred_amount == a.transferred_amount + value`, `b.locked_amount == a.locked_amount - value` An expire message for a previous `value` was done, therefor `b.transferred_amount == a.transferred_amount`, `b.locked_amount == a.locked_amount - value` Considering a channel which has more than two balance proofs sent to the attacker `A` by it's honest counter party `B`, `len(l) >= 2`, there are two balance proofs `k` and `t` where `k` is older than `t`, `k < t`.
added a commit to loredanacirstea/spec that referenced this issue Aug 9, 2018
``` Add protocol values constraints and settlement algorithm requirements ```
``` 4513c05 ```
`Protocol value constraints and settlement algorithm (already implemented or in plan) were gathered and discussed here: raiden-network/raiden-contracts#188`
added a commit to raiden-network/spec that referenced this issue Aug 9, 2018
``` Add protocol values constraints and settlement algorithm requirements ```
``` 4f68afa ```
`Protocol value constraints and settlement algorithm (already implemented or in plan) were gathered and discussed here: raiden-network/raiden-contracts#188`

### loredanacirstea commented Sep 3, 2018

 In my opinion we can close this issue. The specs have been improved (raiden-network/spec#110), to explain the settlement algorithm and my above proofs have not been disproved after the internal audit. @LefterisJP, @hackaugusto can we close this?

### LefterisJP commented Sep 3, 2018

 Well as far as an internal analysis is concerned I would say yes we can close this issue.