# Byzantine Agreement

(Cachin, Kursawe & Shoup)

### Introduction:

This case study concerns modelling and verifying the Byzantine agreement protocol of Cachin, Kurwawe and Shoup [CKS00] using PRISM. The property of the Byzantine agreement protocol we wish to verify is

• Fast Convergence: The probability that an honest party advances more than 2r+1 rounds is bounded above by 2-r.
• Since there may be an unbounded number of rounds, we cannot model the full protocol in PRISM. However, following the proof of [CKS00] it is sufficient to show that, from the start of any round r, with probability at least 1/2 all honest parties have the same pre-vote in round r+1. We therefore construct an abstract version of this protocol concentrating on an arbitrary round r. More precisely, we consider only the choices made by the parties in round r and round r+1, and abstract the choices made in earlier rounds. Then to prove Fast Convergence, it suffices to show that, in the initial state of the abstract protocol, with probability at least 1/2 all honest parties have the same pre-vote in round r+1.

More details on the abstraction are given in [KN02] and the verification of the correctness of the abstraction is explained below.

An example of the source code for this model (when n=4 and t=1) is given below.

```// Byzantine agreement protocol - abstract protocol for proving fast convergence
// show that within two rounds all honest pre votes will be the same with probability 1/2
// dxp/gxn 05/09/01

mdp

// CONSTANTS
// N=4 (number of parties) T=1 (number of corrupted parties)
// number of honest parties (M=N-T)
const M=3;
// minimum number of votes from honest parties needed before a vote can be made K=N- 2T
const K=2;

// abstraction of actual protocol for proving probabilistic progress
// need to include only:
// main votes for round r-1
// pre votes for round r
// main votes for round r
// pre votes for round r+1
// where r is an arbitrary round

// one question we have is when the coins in rounds r-1 and r are flipped
// (these coins are needed for the pre-votes in round r and round r+1 respectively)
// we have chosen that this can happen any time after at least n-2t honest parties have
// read the main votes in round r-1 (that is chosen their pre-vote)

// VARIABLES

// counts the number of parties that have read the main votes in round r-1
// used to know what coins can be flipped
global n0 :  [0..K];

// note only boolean values
global main1_0 : [0..1]; // vote for 0
global main1_1 : [0..1]; // vote for 1
global main1_abs : [0..1]; // vote for 1

global pre1_0 : [0..M]; // number for 0
global pre1_1 : [0..M]; // number for 1

// note only boolean values
global pre2_0 : [0..1]; // vote for 0
global pre2_1 : [0..1]; // vote for 1

// PROCESSES

// adversary which decides which main votes in round r-1 can be cast

main0_0 : [0..1]; // vote for 0
main0_1 : [0..1]; // vote for 1

// adversary decide which main vote is possible can do this at any time
[] (main0_0=0) & (main0_1=0) -> (main0_0'=1);
[] (main0_0=0) & (main0_1=0) -> (main0_1'=1);

endmodule

// module for tossing coin in round R-1
module coin1

f1 : [0..1];
coin1 : [0..1];

[] (coin1=0) & (n0>=K) -> 0.5 : (f1'=0) & (coin1'=1) + 0.5 : (f1'=1) & (coin1'=1);

endmodule

// module for tossing coin in round R
module coin2=coin1[coin1=coin2,f1=f2] endmodule

// honest party
module party1

// local state
s1 : [0..9];
// 1 - pre-vote for coin in round r
// 2 - pre-vote for 0 in round r
// 3 - pre-vote for 1 in round r
// 4 - collect and make main vote in round r
// 6 - pre-vote for coin r+1
// 7 - pre-vote for 0 in round r+1
// 8 - pre-vote for 1 in round r+1
// 9 - done

[] (s1=0) & (main0_0=1) -> (s1'=1) & (n0'=min(K,n0+1)); // pre vote for 0
[] (s1=0) & (main0_1=1) -> (s1'=2) & (n0'=min(K,n0+1)); // pre vote for 1
[] (s1=0)               -> (s1'=3) & (n0'=min(K,n0+1)); // pre vote for coin

// make pre-vote in round r (need to wait for coin)
[] (s1=1) & (coin1=1)          -> (s1'=4) & (pre1_0'=pre1_0+1);
[] (s1=2) & (coin1=1)          -> (s1'=4) & (pre1_1'=pre1_1+1);
[] (s1=3) & (coin1=1) & (f1=0) -> (s1'=4) & (pre1_0'=pre1_0+1);
[] (s1=3) & (coin1=1) & (f1=1) -> (s1'=4) & (pre1_1'=pre1_1+1);

// collect pre-votes and make main vote in round r
[] (s1=4) & (pre1_0+pre1_1>=K) & ((pre1_0>0) | (f1=0) | (main0_0=1)) & ((pre1_1>0) | (f1=1) | (main0_1=1)) -> (s1'=5)  & (main1_abs'=1);
[] (s1=4) & (pre1_0+pre1_1>=K) & (pre1_0>=K) -> (s1'=5) & (main1_0'=1);
[] (s1=4) & (pre1_0+pre1_1>=K) & (pre1_1>=K) -> (s1'=5) & (main1_1'=1);

// to get all abstain votes need at least all honest parties to have abstain
[] (s1=5) & (main1_abs=1) -> (s1'=6);
// to vote for 0 or 1 need a pre vote for 0 or 1 either from honest or corrupt parties
[] (s1=5) & ((main1_0=1) | (pre1_0>=K))	-> (s1'=7);
[] (s1=5) & ((main1_1=1) | (pre1_1>=K))	-> (s1'=8);

// make pre-votes in round r+1 (need to wait for the coin
[] (s1=6) & (coin2=1) & (f2=0) -> (s1'=9) & (pre2_0'=1);
[] (s1=6) & (coin2=1) & (f2=1) -> (s1'=9) & (pre2_1'=1);
[] (s1=7) & (coin2=1)          -> (s1'=9) & (pre2_0'=1);
[] (s1=8) & (coin2=1)          -> (s1'=9) & (pre2_1'=1);

endmodule

// construct further parties through renaming
module party2=party1[s1=s2] endmodule
module party3=party1[s1=s3] endmodule
```

All experiments were run on a 440 MHz SUN Ultra 10 workstation with 512 Mb memory under the Solaris 2.7 operating system.

### Model and MTBDD Sizes:

The table below shows statistics for each model and the MTBDD which represents it. The first column gives the size of the model (i.e. the number of states). The second two columns refer to the MTBDD: the total number of nodes in the structure and the number of leaves (or terminal nodes).

 Model: States: Nodes: Leaves: n t 4 1 16,468 17,856 3 5 1 99,772 32,712 3 6 1 567,632 48,158 3 7 2 1,303,136 70,733 3 8 2 8,197,138 99,003 3 9 2 50,022,552 128,102 3 10 3 98,209,858 161,171 3 11 3 640,388,556 203,846 3 12 3 4,089,261,632 247,187 3 13 4 7,247,209,720 290,597 3 14 4 48,562,817,530 347,457 3 15 4 319,913,572,942 405,793 3 16 5 527,308,719,290 458,923 3 17 5 3,605,408,189,674 531,165 3 18 5 24,294,110,158,354 604,634 3 19 6 37,922,603,935,954 667,739 3 20 6 263,297,811,600,566 755,333 3

### Model Construction Times:

The table below gives the times taken to construct the models. There are two stages. Firstly, the system description (in our module based language) is parsed and converted to the MTBDD representing it. Secondly, reachability is performed to identify non-reachable states and the MTBDD is filtered accordingly. Reachability is performed using a BDD based fixpoint algorithm. The number of iterations for this process is also given.

 Model: Construction: n t Time (s): Iterations: 4 1 3.00 19 5 1 5.41 24 6 1 8.53 29 7 2 10.9 29 8 2 20.0 34 9 2 27.0 39 10 3 33.8 39 11 3 62.4 44 12 3 75.4 49 13 4 98.3 49 14 4 157 54 15 4 194 59 16 5 241 59 17 5 363 64 18 5 610 69 19 6 694 69 20 6 1,079 74

### Model Checking:

The model checking procedure uses a precomputation step Prob0A which finds all those states such that the maximum probability of satisfying the formula is 0. The precomputation involves a BDD based fixpoint algorithm.

In the main algorithm we stop iterating when the relative error between subsequent iteration vectors is less than 1e-6, that is: ### Requirements:

When model checking, we have the following requirement:

Scheduler-Liveness: "for each time t and any party i, there exists a time t' > t in which i is scheduled."

This corresponds to the conditions on the adversary/scheduler which we impose by model checking against only fair adversaries.

### Properties:

We have verified that: from the start of any round r, with probability at least 1/2 all honest parties have the same pre-vote in round r+1. This property can be expressed in PCTL as follows (where n=4 and t=1):

P>=0.5 [ true U s1=9 & s2=9 & s3=9 & ((pre2_0=1 & pre2_1=0) | (pre2_1=1 & pre2_0=0)) ]

The table below give the model checking results for the MTBDD, Sparse and Hybrid engines and includes the minimum probability of, from the intial state, reaching a state where all honest parties have the same pre-vote in round r+1.

Model checking times:

 Model: Precomputation: Main Algorithm: Result: n t Time per iter. (s) Iterations: Time per iter. (s) Iterations: MTBDD Sparse Hybrid 4 1 0.035 18 0.051 0.017 0.038 12 true 5 1 0.088 23 0.170 0.172 0.228 14 true 6 1 0.153 28 0.171 0.937 3.56 16 true 7 2 0.378 28 0.298 2.31 9.15 15 true 8 2 0.389 33 0.407 - 59.6 17 true 9 2 0.634 38 0.569 - 18 true 10 3 0.829 38 0.993 - - 17 true 11 3 1.399 43 1.08 - - 20 true 12 3 1.44 48 1.84 - - 22 true 13 4 2.09 48 3.09 - - 20 true 14 4 3.67 53 3.69 - - 22 true 15 4 6.29 58 3.92 - - 25 true 16 5 8.81 58 5.51 - - 22 true 17 5 12.6 63 6.97 - - 25 true 18 5 16.0 68 7.65 - - 27 true 19 6 19.7 68 17.8 - - 25 true 20 6 26.0 73 29.8 - - 27 true

Conclusion: the property holds in the initial state.

### Correctness of the PRISM Model:

To prove the correctness of the abstract model constructed in PRISM, we follow the technique presented in [KNS03b] (for timed probabilistic systems), which reduces verifying the correctness of the abstraction to constructing non-probabilistic variants of the abstract and concrete models to checking trace refinement between these systems. The method is reliant on when constructing the non-probabilistic models encoding the probabilistic information and choices of the adversary in actions. Since the Cadence SMV language does not support actions, we use the process algebra CSP [Ros97] and the model checker FDR.

More formally, we translate both the abstract protocol and the Cadence SMV version of the protocol (restricted to two arbitrary rounds and with the probabilistic choices correctly modelled) into CSP, encoding both the probabilistic choices and the possible non-deterministic choices of the adversary into the actions of the CSP processes. Using the tool FDR we were then able to show that the concrete protocol is a trace refinement of the abstract protocol, and hence the correctness of our abstraction. Note that we were only able to do this for finite configurations.

The FDR code for the case when n=4 and t=1 can be found here here.