/* BYZANTINE AGREEMENT PROTOCOL */ /* this files contains the proof of probabilistic progress */ /* gxn 9/12/2001 */ /* replaced the probabilistic choice of the coins by a non-deterministic choice */ /* and suppose that the coin in round $r$ is flipped when at least $n-2t$ honest parties have read the main votes in round $r$ */ /* note that the coin can never be tossed earlier than this since $n-t$ shares are required before it can be revealed */ /* note that we have change the notations for the coins: for round r the coin is denoted \smvusersym{coin}$[r+1]$ */ /* this is to simplify the code: it allows the pre-votes for each round to be based on the coin for the previous round */ /* by setting the coin for round -1 (\smvusersym{coin}$[0]$) always to 0 */ /* instead of parties reading votes individually, we store the total number of honest votes for each preference */ /* and for corrupted parties we include only boolean variables indicating what corrupted parties can vote for */ /* recalling that different parties may see corrupted parties vote for different values */ /* based on these totals we then know what combination of votes each party can read */ /* that is what the adversary can make parties vote for */ /* note that sometimes there will be a non-deterministic choice as to what a party will vote for */ /* this is a choice of the adversary since it depends on which votes a party reads */ /* an honest party must get at least $n-2t$ votes from other honest parties */ /* and the remaining votes can come from either honest or corrupted parties */ /* if we can show: ``if an honest party has a vote for a value then corrupted parties can also vote for this value'' */ /* we need only count up to $n-2t$ honest party votes and use corrupted parties for the remaining votes */ /* this has been proved (properties corrupted3 and corrupted4 in lemmas.smv) */ /* note that to deal with the validity part of the proof and to keep things consistent the initial round is 0 instead of 1 */ /* this is because the round variable is an ordset and cannot specify round=1, but we can specify round=0 */ /* one further change is that we let the pre-votes be cast before they are cast in the actual protocol */ /* now they are cast when a party reads the main-votes of the previous round */ /* note that this can only give the adversary more power */ /* however, in the original protocol at the time when the pre-votes are now cast */ /* an honest party has read the main-votes it will use to cast a pre-vote */ /* therefore at this time the adversary already knows what pre-vote the party is going make */ /* and hence moving the casting of pre-votes to this point makes no difference to what the adversary knows */ /* there is one added complication: we need to store two different possible pre-votes which depend on */ /* what value of the corresponding coin becomes when it is tossed */ /*-----------------------------------------------------------------------------------*/ /* CONSTANTS (n=10 & t=3) */ #define N 7 /* number of honest parties */ #define M 4 /* M=n-2t number of honest pre and main votes that must be read */ #define K 4 /* K=2t+1-t=t+1 number of honest pre processing votes that must be read */ /* ABSTRACT DATA TYPES */ ordset PROC 1..N; /* set of parties */ ordset VOTES 0..M; /* honest pre and main votes */ ordset PRE_PROC_VOTES 0..K; /* honest preprocessing votes */ ordset ROUNDS 0..; /* round numbers */ /* DATA TYPES */ typedef PC {INITIAL , PRE_PROCESSING , MAIN , DECIDE , COIN , DONE }; /* INITIAL - make preprocessing vote (initial state) */ /* PRE_PROCESSING - read preprocessing votes and make initial pre-vote */ /* MAIN - read pre-votes and make main vote */ /* DECIDE - read main votes and make choice whether to decide or not and next pre-vote */ /* COIN - generate share of the coin */ /* DONE - finished */ /*-----------------------------------------------------------------------------------*/ module main(act){ /*------------------------------INPUTS------------------------------------------*/ act : PROC; /* SCHEDULER left unspecified */ /* in certain cases a party can cast different votes depending on which votes it reads */ /* we represent these choices using the following variables */ /* note since this is decided by the adversary we leave these variables unspecified */ /* pre votes */ nd_pre : 0..1; /* non deterministic choice between voting for 0 and 1 */ nd_pre1 : {0,2}; /* non deterministic choice between voting for 0 and coin */ nd_pre2 : 1..2; /* non deterministic choice between voting for 1 and coin */ /* main votes */ nd_main1 : {0,2}; /* non deterministic choice between voting for 0 and 2 */ nd_main2 : 1..2; /* non deterministic choice between voting for 1 and 2 */ start : array PROC of 0..1; /* initial values of parties left unspecified */ /* -------------------THE PROTOCOL FOR HONEST PARTIES---------------------------- */ /* PHASE */ pc : array PROC of PC; /* pc[i] - phase of party i */ /* VALUES OF VOTES */ /* pre-processing-votes: 0 or 1 */ /* pre-votes: 0 or 1 */ /* main-votes: 0, 1 or 2 where 2 denotes abstain */ /* PRE_PROCESSING */ pre_proc : PRE_PROC_VOTES; /* pre_proc - number of pre processing votes */ pre_proc_votes : array 0..1 of PRE_PROC_VOTES; /* pre_proc_votes[v] - number of pre processing votes for v */ /* PRE_VOTE */ pre : array ROUNDS of VOTES; /* pre[r] - number of pre-votes in round r */ pre_votes : array ROUNDS of array 0..1 of array 0..1 of VOTES; /* pre_votes[r][c][v] - number of pre-votes for v in round r if the coin in round r equals c */ /* MAIN_VOTE */ main : array ROUNDS of VOTES; /* main[r] - number of main-votes so far in round r */ main_votes : array ROUNDS of array 0..2 of VOTES; /* main_votes[r][v] - number of main-votes so far for v in round r */ /* ROUND */ round : array PROC of ROUNDS; /* round[i] - round party i is currently in */ /* DECIDING */ decide : array ROUNDS of array PROC of boolean; /* decide[r][i] party i decided in round r */ decide_value : array ROUNDS of array PROC of 0..1; /* decide[r][i][v]=v what value party i decided on in round r (if the party decides) */ /* COIN */ coin : array ROUNDS of { not_tossed , 0 , 1 }; /* coin[r] value of the coin in round r */ /* INITIAL VALUES */ forall (i in PROC) { init(pc[i]) := INITIAL; init(round[i]) := 0; } /* set all totals to be zero */ init(pre_proc) := 0; for(v = 0; v <= 1; v = v + 1) init(pre_proc_votes[v]) := 0; forall(r in ROUNDS){ init(pre[r]) := 0; init(main[r]) := 0; for(c = 0; c <= 1; c = c + 1) for(v = 0; v <= 1; v = v + 1) init(pre_votes[r][c][v]) := 0; for(v = 0; v <= 2; v = v + 1) init(main_votes[r][v]) := 0; } /* initially undecided */ forall(r in ROUNDS) forall(i in PROC) init(decide[r][i]) := 0; /* as explained the coin in round 0 is set to 0 then never changed */ /* the remaining coins initially are not tossed */ forall(r in ROUNDS) init(coin[r]) := (r=0) ? 0 : not_tossed; /* NEXT VALUES */ switch (pc[act]) { INITIAL : { /* move to pre processing */ next(pc[act]) := PRE_PROCESSING; /* make pre processing vote based on the value of start[act] */ next(pre_proc_votes[start[act]]) := (pre_proc_votes[start[act]])=K ? pre_proc_votes[start[act]] : pre_proc_votes[start[act]]+1; /* record that a pre processing vote has been cast */ next(pre_proc) := pre_proc=K ? pre_proc : pre_proc+1; } PRE_PROCESSING : { if (pre_proc=K) { /* sufficient pre processing votes */ /* move to MAIN */ next(pc[act]) := MAIN; /* record that a pre vote has been cast */ next(pre[round[act]]) := pre[round[act]]=M ? pre[round[act]] : pre[round[act]]+1; for(c = 0; c <= 1; c = c + 1) { /* sufficient votes to have a pre vote for either value therefore the vote is the adversary's choice */ if (pre_proc_votes[0]>0 & pre_proc_votes[1]>0) next(pre_votes[round[act]][c][nd_pre]) := pre_votes[round[act]][c][nd_pre]=M ? pre_votes[round[act]][c][nd_pre] : pre_votes[round[act]][c][nd_pre]+1; /* pre vote for 0 only */ else if (pre_proc_votes[0]>0) next(pre_votes[round[act]][c][0]) := pre_votes[round[act]][c][0]=M ? pre_votes[round[act]][c][0] : pre_votes[round[act]][c][0]+1; /* pre vote for 1 only */ else if (pre_proc_votes[1]>0) next(pre_votes[round[act]][c][1]) := pre_votes[round[act]][c][1]=M ? pre_votes[round[act]][c][1] : pre_votes[round[act]][c][1]+1; /* the above should be the only cases but as a default suppose the adversary can choose */ else next(pre_votes[round[act]][c][nd_pre]) := pre_votes[round[act]][c][nd_pre]=M ? pre_votes[round[act]][c][nd_pre] : pre_votes[round[act]][c][nd_pre]+1; } } } MAIN : { /* read pre votes and cast main vote */ /* to simplify the conditions have used the assumptions that there cannot be M votes for two distinct values in the same round */ if ( pre[round[act]]=M & !coin[round[act]]=not_tossed ) { /* sufficient pre votes and the coin has been tossed */ /* move DECIDE */ next(pc[act]) := DECIDE; /* record that the party has made a main vote */ next(main[round[act]]) := main[round[act]]=M ? main[round[act]] : main[round[act]]+1; /* main vote for 0 or abstain only */ if (pre_votes[round[act]][coin[round[act]]][0]=M & corrupted_pre[round[act]][coin[round[act]]][0] & (pre_votes[round[act]][coin[round[act]]][1]>0 | corrupted_pre[round[act]][coin[round[act]]][1]) ) next(main_votes[round[act]][nd_main1]) := main_votes[round[act]][nd_main1]=M ? main_votes[round[act]][nd_main1] : main_votes[round[act]][nd_main1]+1; /* main vote for 1 or abstain only */ else if (pre_votes[round[act]][coin[round[act]]][1]=M & corrupted_pre[round[act]][coin[round[act]]][1] & (pre_votes[round[act]][coin[round[act]]][0]>0 | corrupted_pre[round[act]][coin[round[act]]][0]) ) next(main_votes[round[act]][nd_main2]) := main_votes[round[act]][nd_main2]=M ? main_votes[round[act]][nd_main2] : main_votes[round[act]][nd_main2]+1; /* main vote for 0 only */ else if (pre_votes[round[act]][coin[round[act]]][0]=M & corrupted_pre[round[act]][coin[round[act]]][0]) next(main_votes[round[act]][0]) := main_votes[round[act]][0]=M ? main_votes[round[act]][0] : main_votes[round[act]][0]+1; /* main vote for 1 only */ else if (pre_votes[round[act]][coin[round[act]]][1]=M & corrupted_pre[round[act]][coin[round[act]]][1]) next(main_votes[round[act]][1]) := main_votes[round[act]][1]=M ? main_votes[round[act]][1] : main_votes[round[act]][1]+1; /* left with only a main vote for abstain */ else next(main_votes[round[act]][2]) := main_votes[round[act]][2]=M ? main_votes[round[act]][2] : main_votes[round[act]][2]+1; } } DECIDE : { /* to simplify the model we allow decide_value to be set without decide being set to true in the case the value of decide_value does not matter */ /* and again use the assumptions that there cannot be M votes for two distinct values in the same round */ if (main[round[act]]=M) { /* sufficient main votes */ next(pc[act]) := COIN; /* record that a pre vote has been cast */ next(pre[round[act]+1]) := pre[round[act]+1]=M ? pre[round[act]+1] : pre[round[act]+1]+1; /* must decide on 0 and cast a pre-vote for 0 */ if (main_votes[round[act]][0]=M & corrupted_main[round[act]][0] & main_votes[round[act]][2]=0 & !corrupted_main[round[act]][2] & main_votes[round[act]][1]=0 & !corrupted_main[round[act]][1] ) { next(decide[round[act]][act]) := 1; next(decide_value[round[act]][act]) := 0; for(c = 0; c <= 1; c = c + 1) next(pre_votes[round[act]+1][c][0]) := pre_votes[round[act]+1][c][0]=M ? pre_votes[round[act]+1][c][0] : pre_votes[round[act]+1][c][0]+1; } /* must decide on 1 and cast a pre-vote for 1 */ else if (main_votes[round[act]][1]=M & corrupted_main[round[act]][1] & main_votes[round[act]][2]=0 & !corrupted_main[round[act]][2] & main_votes[round[act]][0]=0 & !corrupted_main[round[act]][0] ) { next(decide[round[act]][act]) := 1; next(decide_value[round[act]][act]) := 1; for(c = 0; c <= 1; c = c + 1) next(pre_votes[round[act]+1][c][1]) := pre_votes[round[act]+1][c][1]=M ? pre_votes[round[act]+1][c][1] : pre_votes[round[act]+1][c][1]+1; } /* may decide on 0 and must cast a pre-vote for 0 */ else if (main_votes[round[act]][0]=M & corrupted_main[round[act]][0] & main_votes[round[act]][1]=0 & !corrupted_main[round[act]][1] ) { next(decide[round[act]][act]) := {0,1}; next(decide_value[round[act]][act]) := 0; for(c = 0; c <= 1; c = c + 1) next(pre_votes[round[act]+1][c][0]) := pre_votes[round[act]+1][c][0]=M ? pre_votes[round[act]+1][c][0] : pre_votes[round[act]+1][c][0]+1; } /* may decide on 1 and must cast a pre-vote for 1 */ else if (main_votes[round[act]][1]=M & corrupted_main[round[act]][1] & main_votes[round[act]][0]=0 & !corrupted_main[round[act]][0] ) { next(decide[round[act]][act]) := {0,1}; next(decide_value[round[act]][act]) := 1; for(c = 0; c <= 1; c = c + 1) next(pre_votes[round[act]+1][c][1]) := pre_votes[round[act]+1][c][1]=M ? pre_votes[round[act]+1][c][1] : pre_votes[round[act]+1][c][1]+1; } /* cannot decide and must cast a pre-vote for 0 */ else if ( (main_votes[round[act]][0]>0 | corrupted_main[round[act]][0]) & (main_votes[round[act]][2]0 | corrupted_main[round[act]][1]) & (main_votes[round[act]][2]0 | corrupted_main[round[act]][0]) & (main_votes[round[act]][2]>0 | corrupted_main[round[act]][2]) & main_votes[round[act]][1]=0 & !corrupted_main[round[act]][1] ) { if (nd_pre1=0) { /* concrete vote for 0 */ for(c = 0; c <= 1; c = c + 1) next(pre_votes[round[act]+1][c][0]) := pre_votes[round[act]+1][c][0]=M ? pre_votes[round[act]+1][c][0] : pre_votes[round[act]+1][c][0]+1; } else { /* coin */ for(c = 0; c <= 1; c = c + 1) next(pre_votes[round[act]+1][c][c]) := pre_votes[round[act]+1][c][c]=M ? pre_votes[round[act]+1][c][c] : pre_votes[round[act]+1][c][c]+1; } } /* may vote for 1 or coin (cannot decide) */ else if ( (main_votes[round[act]][1]>0 | corrupted_main[round[act]][1]) & (main_votes[round[act]][2]>0 | corrupted_main[round[act]][2]) & main_votes[round[act]][0]=0 & !corrupted_main[round[act]][0] ) { if (nd_pre2=1) { /* concrete vote for 1 */ for(c = 0; c <= 1; c = c + 1) next(pre_votes[round[act]+1][c][1]) := pre_votes[round[act]+1][c][1]=M ? pre_votes[round[act]+1][c][1] : pre_votes[round[act]+1][c][1]+1; } else { /* coin */ for(c = 0; c <= 1; c = c + 1) next(pre_votes[round[act]+1][c][c]) := pre_votes[round[act]+1][c][c]=M ? pre_votes[round[act]+1][c][c] : pre_votes[round[act]+1][c][c]+1; } } else { /* left with a vote for coin (cannot decide) */ for(c = 0; c <= 1; c = c + 1) next(pre_votes[round[act]+1][c][c]) := pre_votes[round[act]+1][c][c]=M ? pre_votes[round[act]+1][c][c] : pre_votes[round[act]+1][c][c]+1; } } } COIN : { /* if decided in previous round then done else continue */ next(pc[act]) := (round[act]>0 & decide[round[act]-1][act]) ? DONE : MAIN; next(round[act]) := (round[act]>0 & decide[round[act]-1][act]) ? round[act] : round[act]+1; /* increase round */ /* toss coin if at least M honest parties have reached this stage and the coin has not been tossed */ next(coin[round[act]+1]) := pre[round[act]+1]=M & coin[round[act]+1]=not_tossed ? {0,1} : coin[round[act]+1]; } } /* -------------------------CORRUPTED PARTIES------------------------------------------ */ /* corrupted_pre[v] is true if a corrupted party can have a pre vote for v in round r */ corrupted_pre : array ROUNDS of array 0..1 of array 0..1 of boolean; /* corrupted_main[v] is true if a corrupted party can have a main vote for v in round r */ corrupted_main : array ROUNDS of array 0..2 of boolean; /* INITIAL VALUES */ /* initially cannot vote for either */ forall(r in ROUNDS){ for(c = 0; c <= 1; c = c + 1) for(v = 0; v <= 1; v = v + 1) init(corrupted_pre[r][c][v]) := 0; for(v = 0; v <= 2; v = v + 1) init(corrupted_main[r][v]) := 0; } /* NEXT VALUES */ /* pre votes: for round 0 need at least one preprocessing vote from an honest party for a value to vote for that value */ /* in general to vote v either need a main vote for v (from either an honest or corrupted party) in the previous round */ /* or is able to vote for the coin, that is, there are need sufficient abstain main votes in the previous round */ forall (r in ROUNDS) { if (r=0) { for(v = 0; v <= 1; v = v + 1) next(corrupted_pre[r][0][v]) := (next(pre_proc_votes[v])>0); for(v = 0; v <= 1; v = v + 1) next(corrupted_pre[r][1][v]) := (next(pre_proc_votes[v])>0); } else { next(corrupted_pre[r][0][0]) := (next(main[r-1])=M & ( (next(main_votes[r-1][0])>0 | next(corrupted_main[r-1][0])) | (next(main_votes[r-1][2])=M & next(corrupted_main[r-1][2])) )) ? 1 : 0; next(corrupted_pre[r][0][1]) := (next(main[r-1])=M & (next(main_votes[r-1][1])>0 | next(corrupted_main[r-1][1]))) ? 1 : 0; next(corrupted_pre[r][1][0]) := (next(main[r-1])=M & (next(main_votes[r-1][0])>0 | next(corrupted_main[r-1][0]))) ? 1 : 0; next(corrupted_pre[r][1][1]) := (next(main[r-1])=M & ( (next(main_votes[r-1][1])>0 | next(corrupted_main[r-1][1])) | (next(main_votes[r-1][2])=M & next(corrupted_main[r-1][2])) )) ? 1 : 0; } } /* main votes: to vote for v (0 or 1) need M pre votes for v from honest parties also pre votes for v from corrupted parties */ /* to vote for abstain need a pre vote for 0 and a pre vote for 1 (from either honest or corrupted parties) */ forall (r in ROUNDS) { if (next(coin[r])=0) { for(v = 0; v <= 1; v = v + 1) next(corrupted_main[r][v]) := (next(pre[r])=M & next(pre_votes[r][0][v])=M & next(corrupted_pre[r][0][v]) ) ? 1 : 0; next(corrupted_main[r][2]) := ( next(pre[r])=M & (next(pre_votes[r][0][0])>0 | next(corrupted_pre[r][0][0])) & (next(pre_votes[r][0][1])>0 | next(corrupted_pre[r][0][1])) ) ? 1 : 0; } else if (next(coin[r])=1) { for(v = 0; v <= 1; v = v + 1) next(corrupted_main[r][v]) := (next(pre[r])=M & next(pre_votes[r][1][v])=M & next(corrupted_pre[r][1][v]) ) ? 1 : 0; next(corrupted_main[r][2]) := ( next(pre[r])=M & (next(pre_votes[r][1][0])>0 | next(corrupted_pre[r][1][0])) & (next(pre_votes[r][1][1])>0 | next(corrupted_pre[r][1][1])) ) ? 1 : 0; } } /* -----------------------END OF PROTOCOL----------------------------------- */ /*-------------------------------HISTORY VARIABLES---------------------------------------*/ /* for each round records the first party to have a main-vote for each value */ history_main_votes : array ROUNDS of array 0..2 of PROC; forall (r in ROUNDS) for(v = 0; v <= 2; v = v + 1) { init(history_main_votes[r][v]) := act; next(history_main_votes[r][v]) := next(main_votes[r][v])>0 & main_votes[r][v]=0 ? act : history_main_votes[r][v]; } /* for each round records the first party to have a pre-vote for each value */ history_pre_votes : array ROUNDS of array 0..1 of array 0..1 of PROC; forall (r in ROUNDS) for(c = 0; c <= 1; c = c + 1) for(v = 0; v <= 1; v = v + 1) { init(history_pre_votes[r][c][v]) := act; next(history_pre_votes[r][c][v]) := next(pre_votes[r][c][v])>0 & pre_votes[r][c][v]=0 ? act : history_pre_votes[r][c][v]; } /* for each round records the first party to have a pre-vote */ history_pre : array ROUNDS of PROC; forall (r in ROUNDS) { init(history_pre[r]) := act; next(history_pre[r]) := next(pre[r])>0 & pre[r]=0 ? act : history_pre[r]; } /* records the first party to have a pre-processing-vote for each value */ history_pre_proc_votes : array 0..1 of PROC; for(v = 0; v <= 1; v = v + 1) { init(history_pre_proc_votes[v]) := act; next(history_pre_proc_votes[v]) := next(pre_proc_votes[v])>0 & pre_proc_votes[v]=0 ? act : history_pre_proc_votes[v]; } /* records the party which flips the coin */ history_coin : array ROUNDS of PROC; forall (r in ROUNDS) { init(history_coin[r]) := act; next(history_coin[r]) := !next(coin[r])=not_tossed & coin[r]=not_tossed ? act : history_coin[r]; } /*---------------------------ASSUMPTIONS-------------------------------------*/ /* 1-4: there cannot be M votes for v and M votes for v' */ /* these follows from the fact if this was not true there would be */ /* M+M=(N-2T) + (N-2T)=N-T+(N-3T)>N-T honest parties */ /* which is a contradiction since there are only N-T honest parties */ forall (r in ROUNDS) { assumption1[r] : assert G !( main_votes[r][2]=M & main_votes[r][0]=M); assumption2[r] : assert G !( main_votes[r][2]=M & main_votes[r][1]=M); assumption3[r] : assert G !( main_votes[r][0]=M & main_votes[r][1]=M); assume assumption1[r], assumption2[r], assumption3[r]; } forall (r in ROUNDS) for(c = 0; c <= 1; c = c + 1) { assumption4[r][c] : assert G !( pre_votes[r][c][0]=M & pre_votes[r][c][1]=M); assume assumption4[r][c]; } /*------------------ADDITIONAL INVARIANTS-----------------------------------*/ /* these are proved in a separate file (lemmas.smv) */ forall (r in ROUNDS) forall (n in VOTES) { lemma5[r][n] : assert G ( pre[r]=n -> G (pre[r]>=n) ); assume lemma5[r][n]; } forall (r in ROUNDS) for(c = 0; c <= 1; c = c + 1) for(v = 0; v <= 1; v = v + 1) forall (n in VOTES) { lemma9[r][c][v][n] : assert G ( pre_votes[r][c][v]>=n -> G (pre_votes[r][c][v]>=n) ); assume lemma9[r][c][v][n]; } forall (r in ROUNDS) for(c = 0; c <= 1; c = c + 1) for(v = 0; v <= 1; v = v + 1) { lemma11[r][c][v] : assert G (pre_votes[r][c][v]>0 -> G (pre_votes[r][c][v]>0) ); assume lemma11[r][c][v]; } forall (r in ROUNDS) for(c = 0; c <= 1; c = c + 1) { lemma16[r][c] : assert G ( pre_votes[r][c][1]=0 -> pre_votes[r][c][0]=pre[r] ); assume lemma16[r][c]; } forall (r in ROUNDS) for(c = 0; c <= 1; c = c + 1) { lemma17[r][c] : assert G ( pre_votes[r][c][0]=0 -> pre_votes[r][c][1]=pre[r] ); assume lemma17[r][c]; } forall (r in ROUNDS) forall (n in VOTES) { lemma19[r][n] : assert G ( main[r]>=n -> G (main[r]>=n) ); assume lemma19[r][n]; } forall (r in ROUNDS) for(v = 0; v <= 2; v = v + 1) forall (n in VOTES) { lemma23[r][v][n] : assert G ( main_votes[r][v]>=n -> G (main_votes[r][v]>=n) ); assume lemma23[r][v][n]; } forall (r in ROUNDS) for(v = 0; v <= 2; v = v + 1) { lemma25[r][v] : assert G ( main_votes[r][v]>0 -> G (main_votes[r][v]>0) ); assume lemma25[r][v]; } forall (r in ROUNDS) { lemma31[r] : assert G ( (main_votes[r][1]=0 & main_votes[r][2]=0) -> main_votes[r][0]=main[r] ); assume lemma31[r]; } forall (r in ROUNDS) { lemma32[r] : assert G ( (main_votes[r][0]=0 & main_votes[r][2]=0) -> main_votes[r][1]=main[r] ); assume lemma32[r]; } forall (r in ROUNDS) { lemma33[r] : assert G ( (main_votes[r][0]=0 & main_votes[r][1]=0) -> main_votes[r][2]=main[r] ); assume lemma33[r]; } forall (r in ROUNDS) forall (i in PROC) { lemma37[r][i] : assert G ( decide[r][i] -> G (decide[r][i]) ); assume lemma37[r][i]; } forall (r in ROUNDS) for (v = 0; v <= 2; v = v + 1) { corrupted1[r][v] : assert G ( corrupted_main[r][v] -> G (corrupted_main[r][v]) ); assume corrupted1[r][v]; } forall (r in ROUNDS) for (c = 0; c <= 1; c = c + 1) for (v = 0; v <= 1; v = v + 1) { corrupted2[r][c][v] : assert G ( corrupted_pre[r][c][v] -> G (corrupted_pre[r][c][v]) ); assume corrupted2[r][c][v]; } forall (r in ROUNDS) for (v = 0; v <= 2; v = v + 1) { corrupted5[r][v] : assert G ( main_votes[r][v]>0 -> corrupted_main[r][v] ); assume corrupted5[r][v]; } forall (r in ROUNDS) for (c = 0; c <= 1; c = c + 1) for (v = 0; v <= 1; v = v + 1) { corrupted6[r][c][v] : assert G ( pre_votes[r][c][v]>0 -> corrupted_pre[r][c][v] ); assume corrupted6[r][c][v]; } forall (r in ROUNDS) for(c = 0; c <= 1; c = c + 1) { coin2[r][c] : assert G ( coin[r]=c -> G ( coin[r]=c ) ); assume coin2[r][c]; } forall (r in ROUNDS) { lemma40[r] : assert G ( (main_votes[r][0]>0 | corrupted_main[r][0]) -> ( main_votes[r][1]=0 & !corrupted_main[r][1] ) ); assume lemma40[r]; } forall (r in ROUNDS) { lemma41[r] : assert G ( (main_votes[r][1]>0 | corrupted_main[r][1]) -> ( main_votes[r][0]=0 & !corrupted_main[r][0] ) ); assume lemma41[r]; } /* ------------------------PROBABILISTIC PROGRESS PROOF---------------------------------*/ /* the prove probabilistic progress has the following structure */ /* consider an arbitrary party i that has not decided before round r+1 and show that */ /* (P1) if there is a concrete pre vote for v in round r+1 before the coin in r+1 is tossed, */ /* then if after the coin in round r+1 is tossed it equals v, then the party decides in round r+1 */ /* (P2) if there are no concrete pre votes in round r+1 before the coin in round r+1 is tossed, */ /* then either the party decides in round r+1 or if after the coins in round r+1 and round r+2 are tossed they are equal, */ /* then the party decides in round r+2 */ /* we consider round r+1 as opposed to round r because in round 0 no coin is tossed */ /* a concrete vote for 0 (1) implies pre_vote[r+1][1][0]>0 (pre_vote[r+1][0][1]>0) */ /* if c=0 or c=1 then we can use (c+1 mod 2) to denote the alternative value of the coin */ /* we therefore assume that the party has not decided before round r+1 */ /* that is the party reaches round r+2 */ /* and if the process does not decide in round r+1 then it reaches round r+2 */ /* note that this includes fairness requirements: */ /* to reach round r+2 there must be sufficient pre and main votes case in round r+1 */ forall (i in PROC) forall (r in ROUNDS) { progress_assumption1[i][r] : assert ( G ( !decide[r][i] ) -> F ( round[i]=r+2 | decide[r+1][i] ) ); progress_assumption2[i][r] : assert ( G ( !decide[r][i] & !decide[r+1][i] ) -> F ( round[i]=r+3 | decide[r+2][i] ) ); assume progress_assumption1[i][r], progress_assumption2[i][r]; } /*----------------------------------------------------------------*/ /* sub for lemmas (P1) (concrete votes before the coin is tossed) */ /* if there is a concrete pre-vote for c then there are main votes for !c in the previous round */ forall (r in ROUNDS) for (c = 0; c <= 1; c = c + 1) { inv1[r][c] : assert G ( pre_votes[r+1][c+1 mod 2][c]>0 -> ( main_votes[r][c]>0 | corrupted_main[r][c] ) ); forall (i in PROC) { subcase inv1[r][c][i] of inv1[r][c] for i=history_pre_votes[r+1][c+1 mod 2][c]; using lemma11[r+1][c+1 mod 2][c], lemma25[r][0], lemma25[r][1], lemma25[r][2], corrupted1[r][c], /* abstractions */ VOTES->{0,M}, ROUNDS->{r,r+1}, /* free variables */ coin//free, corrupted_main//free, corrupted_main[r][c], corrupted_pre//free, decide//free, main//free, main_votes//free, main_votes[r][c], pre//free, pre_proc//free, pre_proc_votes//free, pre_votes//free, pre_votes[r+1][c+1 mod 2][c], start//free prove inv1[r][c][i]; } } /* if there is a concrete pre-vote for c then there are no concrete pre votes for !c */ forall (r in ROUNDS) for (c = 0; c <= 1; c = c + 1) { inv2[r][c] : assert G ( pre_votes[r+1][c+1 mod 2][c]>0 -> ( pre_votes[r+1][c][c+1 mod 2]=0 & !corrupted_pre[r+1][c][c+1 mod 2] ) ); forall (i in PROC) { subcase inv2[r][c][i] of inv2[r][c] for i=history_pre_votes[r+1][c][c+1 mod 2]; using inv1[r][c], lemma11[r+1][c+1 mod 2][c], lemma25[r][0], lemma25[r][1], lemma25[r][2], lemma40[r], corrupted1[r], /* abstractions */ VOTES->{0,M}, ROUNDS->{0,r,r+1}, /* free variables */ coin//free, corrupted_main//free, corrupted_pre//free, corrupted_pre[r+1][c][c+1 mod 2], decide//free, main//free, main_votes//free, pre//free, pre_proc//free, pre_proc_votes//free, pre_votes//free, pre_votes[r+1][c][c+1 mod 2], start//free prove inv2[r][c][i]; } } /* if there is a concrete pre-vote for c and the coin equals c then there are no main votes for !c */ forall (r in ROUNDS) for (c = 0; c <= 1; c = c + 1) { inv3[r][c] : assert G ( (pre_votes[r+1][c+1 mod 2][c]>0 & coin[r+1]=c) -> ( main_votes[r+1][c+1 mod 2]=0 & !corrupted_main[r+1][c+1 mod 2] ) ); forall (i in PROC) { subcase inv3[r][c][i] of inv3[r][c] for i=history_main_votes[r+1][c+1 mod 2]; using inv2[r][c], lemma11[r+1][0][0], lemma11[r+1][0][1], lemma25[r+1][c+1 mod 2], corrupted1[r+1][c+1 mod 2], corrupted2[r+1][c], coin2[r+1], /* abstractions */ VOTES->{0,M}, ROUNDS->{r,r+1}, /* free variables */ coin//free, corrupted_main//free, corrupted_main[r+1][c+1 mod 2], corrupted_pre//free, decide//free, main//free, main_votes//free, main_votes[r+1][c+1 mod 2], pre//free, pre_proc//free, pre_proc_votes//free, pre_votes//free, start//free prove inv3[r][c][i]; } } /* if there is a concrete pre-vote for c and the coin equals c then there are no main votes for abstain */ forall (r in ROUNDS) for (c = 0; c <= 1; c = c + 1) { inv4[r][c] : assert G ( (pre_votes[r+1][c+1 mod 2][c]>0 & coin[r+1]=c) -> ( main_votes[r+1][2]=0 & !corrupted_main[r+1][2] ) ); forall (i in PROC){ subcase inv4[r][c][i] of inv4[r][c] for i=history_main_votes[r+1][2]; using inv2[r][c], lemma11[r+1][c], lemma16[r+1][c], lemma17[r+1][c], lemma25[r+1][c+1 mod 2], corrupted2[r+1][c], corrupted6[r+1][c][c], coin2[r+1], /* abstractions */ VOTES->{0,M}, ROUNDS->{r,r+1}, /* free variables */ coin//free, corrupted_main//free, corrupted_main[r+1][2], corrupted_pre//free, decide//free, main//free, main[r+1], main_votes//free, main_votes[r+1][2], pre//free, pre[r+1], pre_proc//free, pre_proc_votes//free, pre_votes//free, start//free prove inv4[r][c][i]; } } /*----------------------------------------------------------------*/ /* sub for lemmas (P2) (no concrete pre votes before the coin is tossed) */ /* if there are no concrete votes for a value then when the coin is tossed the are M pre votes for the coin */ /* first require a one step argument */ forall (r in ROUNDS) for (c = 0; c <= 1; c = c + 1) { inv5[r][c] : assert G ( ( (coin[r+1]=not_tossed -> (pre_votes[r+1][0][1]=0 & pre_votes[r+1][1][0]=0)) & X (coin[r+1]=c) ) -> pre_votes[r+1][c][c]=M ); forall (i in PROC) { subcase inv5[r][c][i] of inv5[r][c] for i=history_coin[r+1]; using (inv5[r][c]), lemma16[r+1], lemma17[r+1], coin2[r+1], /* abstractions */ VOTES->{0,M}, ROUNDS->{r,r+1}, /* free variables */ coin//free, coin[r+1], corrupted_main//free, corrupted_pre//free, decide//free, main//free, main_votes//free, pre//free, pre[r+1], pre_proc//free, pre_proc_votes//free, pre_votes//free, pre_votes[r+1][c][0], pre_votes[r+1][c][1] prove inv5[r][c][i]; } } /* then using the one step case we have what we want */ forall (r in ROUNDS) for (c = 0; c <= 1; c = c + 1) { inv6[r][c] : assert G ( ( (coin[r+1]=not_tossed -> (pre_votes[r+1][0][1]=0 & pre_votes[r+1][1][0]=0)) & F (coin[r+1]=c) ) -> F (pre_votes[r+1][c][c]=M) ); using inv5[r][c], coin2[r+1], /* abstractions */ VOTES->{0,M}, ROUNDS->{r,r+1}, /* free variables */ coin//free, coin[r+1], corrupted_main//free, corrupted_pre//free, main//free, main_votes//free, pre//free, pre_proc//free, pre_proc_votes//free, pre_votes//free prove inv6[r][c]; } /* if there are no concrete votes for either value before the coin is tossed then the are no main votes other than for the coin */ forall (r in ROUNDS) for (c = 0; c <= 1; c = c + 1) { inv7[r][c] : assert G ( ( (coin[r+1]=not_tossed ->(pre_votes[r+1][0][1]=0 & pre_votes[r+1][1][0]=0)) & F (coin[r+1]=c) ) -> (main_votes[r+1][c+1 mod 2]=0 & !corrupted_main[r+1][c+1 mod 2]) ); forall (i in PROC) { subcase inv7[r][c][i] of inv7[r][c] for i=history_main_votes[r+1][c+1 mod 2]; using inv6[r][c], lemma9[r+1][c][0][M], lemma9[r+1][c][1][M], lemma11[r+1][c][0], lemma11[r+1][c][1], lemma25[r+1][c+1], coin2[r+1], /* assumptions */ assumption4[r+1][c], /* abstractions */ VOTES->{0,M}, ROUNDS->{r,r+1}, /* free variables */ coin//free, coin[r+1], corrupted_main//free, corrupted_main[r+1][c+1 mod 2], corrupted_pre//free, decide//free, main//free, main_votes//free, main_votes[r+1][c+1 mod 2], pre//free, pre_proc//free, pre_proc_votes//free, pre_votes//free prove inv7[r][c][i]; } } /* if there are no concrete votes for either value before the coin is tossed then the are no pre votes other than for the coin */ forall (r in ROUNDS) for (c = 0; c <= 1; c = c + 1) { inv8[r][c] : assert G ( ( (coin[r+1]=not_tossed ->(pre_votes[r+1][0][1]=0 & pre_votes[r+1][1][0]=0)) & F (coin[r+1]=c) ) -> (pre_votes[r+2][c][c+1 mod 2]=0 & !corrupted_pre[r+2][c][c+1 mod 2]) ); forall (i in PROC) { subcase inv8[r][c][i] of inv8[r][c] for i=history_pre_votes[r+2][c][c+1 mod 2]; using inv7[r][c], lemma25[r+1][c+1 mod 2], corrupted2[r+2][c][c+1 mod 2], coin2[r+1], /* abstractions */ VOTES->{0,M}, ROUNDS->{0,r,r+1,r+2}, /* free variables */ coin//free, coin[r+1], corrupted_main//free, corrupted_pre//free, corrupted_pre[r+2][c][c+1 mod 2], decide//free, main//free, main_votes//free, main_votes[r+1][c+1 mod 2], pre//free, pre_proc//free, pre_proc_votes//free, pre_votes//free, pre_votes[r+2][c][c+1 mod 2] prove inv8[r][c][i]; } } /* if there are no concrete votes for either value before the coin is tossed in round r+1 and the coins in rounds r+1 and r+2 are equal then */ /* there are no main votes other than for the value of the coins */ /* first for concrete votes */ forall (r in ROUNDS) for (c = 0; c <= 1; c = c + 1) { inv9[r][c] : assert G ( ( (coin[r+1]=not_tossed ->(pre_votes[r+1][0][1]=0 & pre_votes[r+1][1][0]=0)) & F (coin[r+1]=c) & F (coin[r+2]=c) ) -> (main_votes[r+2][c+1 mod 2]=0 & !corrupted_main[r+2][c+1 mod 2]) ); forall (i in PROC) { subcase inv9[r][c][i] of inv9[r][c] for i=history_main_votes[r+2][c+1 mod 2]; using inv8[r][c], lemma11[r+2][c+1 mod 2], lemma25[r+2][c+1 mod 2], corrupted1[r+2][c+1 mod 2], coin2[r+1], coin2[r+2], /* abstractions */ VOTES->{0,M}, ROUNDS->{r,r+1,r+2}, /* free variables */ coin//free, coin[r+1], coin[r+2], corrupted_main//free, corrupted_main[r+2][c+1 mod 2], corrupted_pre//free, decide//free, main//free, main_votes//free, main_votes[r+2][c+1 mod 2], pre//free, pre_proc//free, pre_proc_votes//free, pre_votes//free prove inv9[r][c][i]; } } /* now for abstain votes */ forall (r in ROUNDS) for (c = 0; c <= 1; c = c + 1) { inv10[r][c] : assert G ( ( (coin[r+1]=not_tossed ->(pre_votes[r+1][0][1]=0 & pre_votes[r+1][1][0]=0)) & F (coin[r+1]=c) & F (coin[r+2]=c) ) -> (main_votes[r+2][2]=0 & !corrupted_main[r+2][2]) ); forall (i in PROC) { subcase inv10[r][c][i] of inv10[r][c] for i=history_main_votes[r+2][2]; using inv8[r][c], lemma5[r+2][M], lemma9[r+2][c][c][M], lemma11[r+2][c+1 mod 2], lemma16[r+2][c], lemma17[r+2][c], lemma25[r+2][2], corrupted1[r+2][2], corrupted6[r+2][c][c], coin2[r+1], coin2[r+2], /* abstractions */ VOTES->{0,M}, ROUNDS->{r,r+1,r+2}, /* free variables */ coin//free, coin[r+1], coin[r+2], corrupted_main//free, corrupted_main[r+2][2], corrupted_pre//free, decide//free, main//free, main_votes//free, main_votes[r+2][2], pre//free, pre_proc//free, pre_proc_votes//free, pre_votes//free prove inv10[r][c][i]; } } /*------------------------------MAIN PROOF---------------------------------------------*/ /* proof of (P1): */ /* If there is a concrete pre vote for v in round r+1 before the coin in r+1 is tossed, */ /* then if after the coin in round r+1 is tossed it equals v, then the party decides in round r+1 */ forall (r in ROUNDS) for (c = 0; c <= 1; c = c + 1) forall (i in PROC) { progress1[r][c][i] : assert G ( ( G (!decide[r][i]) & pre_votes[r+1][c+1 mod 2][c]>0 & coin[r+1]=not_tossed & X (!coin[r+1]=not_tossed) ) -> ( F( coin[r+1]=c) -> F ( decide[r+1][i] ) ) ); using inv3[r][c], inv4[r][c], lemma11[r+1], lemma25[r+1], lemma31[r+1], lemma32[r+1], corrupted1[r+1], corrupted5[r+1], coin2[r+1], /* assumptions */ progress_assumption1[i][r], /* abstractions */ VOTES->{0,M}, ROUNDS->{r,r+1}, /* free variables */ coin//free, coin[r+1], corrupted_main//free, corrupted_pre//free, decide//free, decide[r-1][i], decide[r][i], decide[r+1][i], main//free, main[r+1], main_votes//free, pre//free, pre_proc//free, pre_proc_votes//free, pre_votes//free, start//free prove progress1[r][c][i]; } /* proof of (P2): */ /* if there are no concrete pre votes in round r+1 before the coin in round r+1 is tossed, */ /* then either the party decides in round r+1 or if after the coins in round r+1 and round r+2 are tossed they are equal, */ /* then the party decides in round r+2 */ forall (r in ROUNDS) for (c = 0; c <= 1; c = c + 1) forall (i in PROC) { progress2[r][c][i] : assert G ( ( G (!decide[r][i]) & coin[r+1]=not_tossed & X (!coin[r+1]=not_tossed) & pre_votes[r+1][0][1]=0 & pre_votes[r+1][1][0]=0 ) -> F ( decide[r+1][i] | ( (coin[r+1]=c & coin[r+2]=c) -> decide[r+2][i]) ) ); using inv9[r][c], inv10[r][c], lemma11[r+1][0][1], lemma11[r+1][1][0], lemma19[r+2][M], lemma23[r+2][c][M], lemma25[r+2], lemma31[r+2], lemma32[r+2], coin2[r+1], coin2[r+2], corrupted5[r+2][c], /* assumptions */ progress_assumption1[i][r], progress_assumption2[i][r], /* abstractions */ VOTES->{0,M}, ROUNDS->{0,r,r+1,r+2}, /* free variables */ coin//free, coin[r+1], coin[r+2], corrupted_main//free, corrupted_pre//free, decide//free, decide[r+1][i], decide[r+2][i], main//free, main[r+2], main_votes//free, main_votes[r+2][c], pre//free, pre_proc//free, pre_proc_votes//free, pre_votes//free prove progress2[r][c][i]; } /* we also require the following property concerning when the coins are tossed (P3) */ /* whereas property (P4) is given by inv2 in this file the remaining properties (P5) and (P6) */ /* can be found in the additional invariants file (lemma9 and coin2) */ /* if the coin in round r+1 is not tossed then neither is the coin in round r+2 */ forall (r in ROUNDS) { progress3[r] : assert G (coin[r+1]=not_tossed -> coin[r+2]=not_tossed); forall (i in PROC) { subcase progress3[r][i] of progress3[r] for i=history_coin[r+2]; using coin2[r+1], coin2[r+2], /* ABSTRACTIONS */ ROUNDS->{r..r+2}, /* free variables */ coin//free, coin[r+1], coin[r+2], corrupted_main//free, corrupted_pre//free, decide//free, main//free, main_votes//free, pre//free, pre_proc//free, pre_proc_votes//free, pre_votes//free, start//free prove progress3[r][i]; } } /*-----------------------------END OF FILE-----------------------------------*/ }