(Cachin, Kursawe & Shoup)
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
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
All experiments were run on a 440 MHz SUN Ultra 10 workstation with 512 Mb memory under the Solaris 2.7 operating system.
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).
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.
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:
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.
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):
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:
|n||t||Time per iter. (s)||Iterations:||Time per iter. (s)||Iterations:|
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.