Byzantine Agreement

(Cachin, Kursawe & Shoup)

Introduction
Model and MTBDD Sizes
Model Construction Times
Model Checking
Correctness of PRISM Model

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];

// main-votes so far made in round r-1
// 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

// to count the pre-votes so far made in round r
global pre1_0 : [0..M]; // number for 0
global pre1_1 : [0..M]; // number for 1


// pre-votes so far made in round r+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
module adversary 

	//  main-votes so far made in round r-1
	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];
	// 0 - read main-votes r-1
	// 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
	// 5 - read main-votes 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
	
	// read main votes in round r-1
	[] (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);
	
	// read main votes in round r
	// 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

View: printable version Download: byzantine4_1.nm

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	States:	Nodes:	Leaves:
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:
n	t	Time per iter. (s)	Iterations:	MTBDD	Sparse	Hybrid	Iterations:
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.