-- Byzantine agreement protocol -- gxn 18/10/01 -- N=4 and T=1 -- we construct the abstract Byzantine model used to prove fast convergence in prism -- and the concrete Byzantine protocol (restricted to two rounds) -- encoding both the probabilistic choices and the non-deterministic choice in the actions of the processes -- we then can prove the correctness of the abstract model constructed prism -- by showing trace inclusion between the concrete model and the abstract model -- and using the results presented in [KNS01] -- 0 corresponds to round r-1 -- 1 corresponds to round r -- 2 corresponds to round r+1 --%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -- CONSTANTS --n-t M=3 -- n-2t K=2 --%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -- CHANNELS -- MAKING MAIN VOTES -- initial choice in round r-1 (for abstract protocol made by the environment) channel choose_0, choose_1 -- initial choice in round r-1 (for concrete protocol) channel main_vote0_0, main_vote0_1, main_vote0_abs -- choice in round r channel main_vote1_0, main_vote1_1, main_vote1_abs : {1..M} -- READING MAIN VOTES -- for calculating totals required for knowing when the coins can be tossed channel read_main0, read_main1 -- and deciding on pre votes channel pre1_0, pre1_1, pre1_coin, pre2_0, pre2_1, pre2_coin : {1..M} -- MAKING PRE VOTES (in round r and r+1) channel pre_vote1, pre_vote2 : {0..1}.{1..M} -- COIN FLIPPING IN ROUNDS r-1 AND r -- flipping channel flip_heads0, flip_tails0, flip_heads1, flip_tails1 -- reading value channel value_coin_0, value_coin_1 : {0..1} --%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -- ABSTRACT PARTY -- note: a party synchronize with the environment which restricts the votes that can be cast -- and the actions encode both the source and target state as well as the casting of votes ABS_PARTY(i) = let -- read main votes and decide on pre vote round r-1 ABS_READ_MAIN0(i) = (pre1_0!i -> read_main0 -> ABS_PRE1_0(i) ) [] (pre1_1!i -> read_main0 -> ABS_PRE1_1(i) ) [] (pre1_coin!i -> read_main0 -> ABS_PRE1_COIN(i) ) -- cast pre vote round r ABS_PRE1_COIN(i) = value_coin_0?k -> pre_vote1!k!i -> ABS_MAIN1(i) -- for coin ABS_PRE1_0(i) = pre_vote1!0!i -> ABS_MAIN1(i) -- for 0 ABS_PRE1_1(i) = pre_vote1!1!i -> ABS_MAIN1(i) -- for 1 -- read pre votes and cast main vote round r ABS_MAIN1(i) = main_vote1_abs!i -> ABS_READ_MAIN1(i) [] main_vote1_0!i -> ABS_READ_MAIN1(i) [] main_vote1_1!i -> ABS_READ_MAIN1(i) -- read main votes round r ABS_READ_MAIN1(i) = pre2_coin!i -> read_main1 -> ABS_PRE2_COIN(i) [] pre2_0!i -> read_main1 -> ABS_PRE2_0(i) [] pre2_1!i -> read_main1 -> ABS_PRE2_1(i) -- cast pre vote round r+1 (then finished) ABS_PRE2_COIN(i) = value_coin_1?k -> pre_vote2!k!i -> SKIP -- for coin ABS_PRE2_0(i) = pre_vote2!0!i -> SKIP -- for 0 ABS_PRE2_1(i) = pre_vote2!1!i -> SKIP -- for 1 within ABS_READ_MAIN0(i) -- set of abstract parties ABS_PARTIES = ABS_PARTY(1) ||| ABS_PARTY(2) ||| ABS_PARTY(3) --%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -- PARTY -- note: a party synchronize with the environment which restricts the votes that can be cast -- and the actions encode both the source and target state as well as the casting of votes PARTY(i) = let -- cast main vote round r-1 (note: non-deterministic choice) -- (the environment stops there being a pre vote for both values) MAIN0(i) = main_vote0_abs -> READ_MAIN0(i) |~| main_vote0_0 -> READ_MAIN0(i) |~| main_vote0_1 -> READ_MAIN0(i) -- read main votes round r-1 READ_MAIN0(i) = pre1_0!i -> read_main0 -> PRE1_0(i) [] pre1_1!i -> read_main0 -> PRE1_1(i) [] pre1_coin!i -> read_main0 -> PRE1_COIN(i) -- cast pre vote round r PRE1_COIN(i) = value_coin_0?k -> pre_vote1!k!i -> MAIN1(i) -- for coin PRE1_0(i) = pre_vote1!0!i -> MAIN1(i) -- for 0 PRE1_1(i) = pre_vote1!1!i -> MAIN1(i) -- for 0 -- read pre votes and cast main vote (round r) MAIN1(i) = main_vote1_abs!i -> READ_MAIN1(i) [] main_vote1_0!i -> READ_MAIN1(i) [] main_vote1_1!i -> READ_MAIN1(i) -- read main votes (round r) READ_MAIN1(i) = pre2_0!i -> read_main1 -> PRE2_0(i) [] pre2_1!i -> read_main1 -> PRE2_1(i) [] pre2_coin!i -> read_main1 -> PRE2_COIN(i) -- cast pre vote (round r+1) then finished PRE2_COIN(i) = value_coin_1?k -> pre_vote2!k!i -> SKIP -- for coin PRE2_0(i) = pre_vote2!0!i -> SKIP -- for 0 PRE2_1(i) = pre_vote2!1!i -> SKIP -- for 0 within MAIN0(i) -- set of parties PARTIES = PARTY(1) ||| PARTY(2) ||| PARTY(3) --%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -- COUNTERS -- counts the number of parties that have read the main votes in round r-1 -- required for knowing when coin in round r-1 can be flipped in concrete protocol -- the coin must then synchronize with counter to prevent the coin being flip too earlier -- stop counting at K to ensure finiteness C0 = let N0(i) = (if i N0(i+1) else read_main0 -> N0(i) [] flip_heads0 -> N0(i) [] flip_tails0 -> N0(i) ) within N0(0) -- counts the number of parties that have read the main votes in round r -- required for knowing when coin in round r can be flipped in concrete protocol -- the coin must then synchronize with counter to prevent the coin being flip too earlier -- stop counting at K to ensure finiteness C1 = let N1(i) = (if i N1(i+1) else read_main1 -> N1(i) [] (flip_heads1 -> N1(i) [] flip_tails1 -> N1(i)) ) within N1(0) -- abstract version (both coins flipped after K parties have read the main votes in round r-1) -- the coin must then synchronize with counter to prevent the coin being flip too earlier ABS_C = let ABS_N(i) = (if i ABS_N(i+1) else read_main0 -> ABS_N(i) [] flip_heads0 -> ABS_N(i) [] flip_tails0 -> ABS_N(i) [] flip_heads1 -> ABS_N(i) [] flip_tails1 -> ABS_N(i) ) within ABS_N(0) --%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -- COIN IN ROUND r -- no dependences so can define separately from environment -- we have done this to reduce the size of the model -- we encode the probabilistic choices is the actions of the coins -- c1=0 coin in round r-1 not tosses c1=0 coin in round r-1 tossed -- v1 value of the coin in round r-1 COIN1 = let C1(c1,v1) = (c1==0) & (flip_heads1 -> C1(1,0) |~| flip_tails1 -> C1(1,1)) -- flip coin [] (c1==1) & value_coin_1!v1 -> C1(c1,v1) -- read coin within C1(0,0) --%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -- ABS_TOTALS construct as one process because of dependence between values -- (conjunctions and disjunctions in condition makes it hard to do any other way by parallel composition) -- variables -- c0=0 coin in round r-1 not tosses c0=0 coin in round r-1 tossed -- v0 value of the coin in round r-1 -- c1=0 coin in round r-1 not tosses c1=0 coin in round r-1 tossed -- v1 value of the coin in round r-1 -- m0_1 and m0_1 main vote for 0 and 1 in round r-1 respectively (boolean) -- p1_1 and p1_1 total pre votes for 0 and 1 in round r respectively -- m1_1, m1_1 and m1_abs main votes for 0, 1 and abstain in round r respectively -- p2_1 and p2_1 main vote for 0 and 1 in round r+1 respectively (boolean) -- note that we limit the values of the totals to ensure finiteness ABS_TOTALS = let ABS_TOTAL(c0,v0,m0_0,m0_1,p1_0,p1_1,m1_0,m1_1,m1_abs) = -- nondeterministic choice as to main votes in round r-1 (m0_0==0 and m0_1==0) & ( choose_0 -> ABS_TOTAL(c0,v0,1,m0_1,p1_0,p1_1,m1_0,m1_1,m1_abs) |~| choose_1 -> ABS_TOTAL(c0,v0,m0_0,1,p1_0,p1_1,m1_0,m1_1,m1_abs) ) -- restrict pre votes that can be made in round r [] (m0_0==1) & pre1_0?i -> ABS_TOTAL(c0,v0,m0_0,m0_1,p1_0,p1_1,m1_0,m1_1,m1_abs) [] (m0_1==1) & pre1_1?i -> ABS_TOTAL(c0,v0,m0_0,m0_1,p1_0,p1_1,m1_0,m1_1,m1_abs) -- casting pre vote in round r [] (if p1_0 ABS_TOTAL(c0,v0,m0_0,m0_1,p1_0+1,p1_1,m1_0,m1_1,m1_abs) else pre_vote1!0?i -> ABS_TOTAL(c0,v0,m0_0,m0_1,p1_0,p1_1,m1_0,m1_1,m1_abs) ) [] (if p1_1 ABS_TOTAL(c0,v0,m0_0,m0_1,p1_0,p1_1+1,m1_0,m1_1,m1_abs) else pre_vote1!1?i -> ABS_TOTAL(c0,v0,m0_0,m0_1,p1_0,p1_1,m1_0,m1_1,m1_abs) ) -- flipping of coins in round r [] (c0==0) & (flip_heads0 -> ABS_TOTAL(1,0,m0_0,m0_1,p1_0,p1_1,m1_0,m1_1,m1_abs) |~| flip_tails0 -> ABS_TOTAL(1,1,m0_0,m0_1,p1_0,p1_1,m1_0,m1_1,m1_abs) ) -- reading coins in round r [] (c0==1) & value_coin_0!v0 -> ABS_TOTAL(c0,v0,m0_0,m0_1,p1_0,p1_1,m1_0,m1_1,m1_abs) -- restrict main votes that can be made in round r -- vote for abstain [] (p1_0+p1_1>=K and (p1_0>0 or (c0==1 and v0==0) or m0_0==1) and (p1_1>0 or (c0==1 and v0==1) or m0_1==1)) & main_vote1_abs?i -> ABS_TOTAL(c0,v0,m0_0,m0_1,p1_0,p1_1,m1_0,m1_1,1) -- vote for 0 [] (p1_0+p1_1>=K and p1_0>=K) & main_vote1_0?i -> ABS_TOTAL(c0,v0,m0_0,m0_1,p1_0,p1_1,1,m1_1,m1_abs) -- vote for 1 [] (p1_0+p1_1>=K and p1_1>=K) & main_vote1_1?i -> ABS_TOTAL(c0,v0,m0_0,m0_1,p1_0,p1_1,m1_0,1,m1_abs) -- restrict pre votes that can be made in round r -- vote for coin [] (m1_abs==1) & pre2_coin?i -> ABS_TOTAL(c0,v0,m0_0,m0_1,p1_0,p1_1,m1_0,m1_1,m1_abs) -- vote for 0 [] (m1_0==1 or p1_0>=K) & pre2_0?i -> ABS_TOTAL(c0,v0,m0_0,m0_1,p1_0,p1_1,m1_0,m1_1,m1_abs) -- vote for 1 [] (m1_1==1 or p1_1>=K) & pre2_1?i -> ABS_TOTAL(c0,v0,m0_0,m0_1,p1_0,p1_1,m1_0,m1_1,m1_abs) within ABS_TOTAL(0,0,0,0,0,0,0,0,0) --%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -- TOTALS construct as one party because of dependence between values -- (conjunctions and disjunctions in condition makes it hard to do any other way by parallel composition) -- variables -- c0=0 coin in round r-1 not tosses c0=0 coin in round r-1 tossed -- v0 value of the coin in round r-1 -- m0_1, m0_1 and m0_abs main votes for 0, 1 and abstain in round r-1 respectively -- p1_1 and p1_1 total pre votes for 0 and 1 in round r respectively -- m1_1, m1_1 and m1_abs main votes for 0, 1 and abstain in round r respectively -- p2_1 and p2_1 main vote for 0 and 1 in round r+1 respectively -- note that we limit the values of the totals to get finite parties TOTALS = let TOTAL(c0,v0,m0_0,m0_1,m0_abs,p1_0,p1_1,m1_0,m1_1,m1_abs) = -- casting main vote in round r-1 -- for 0 need no main votes for 1 (m0_0 TOTAL(c0,v0,m0_0+1,m0_1,m0_abs,p1_0,p1_1,m1_0,m1_1,m1_abs) [] (m0_0>=K and m0_1==0) & main_vote0_0 -> TOTAL(c0,v0,m0_0,m0_1,m0_abs,p1_0,p1_1,m1_0,m1_1,m1_abs) -- for 1 need no main votes for 0 [] (m0_1 TOTAL(c0,v0,m0_0,m0_1+1,m0_abs,p1_0,p1_1,m1_0,m1_1,m1_abs) [] (m0_1>=K and m0_0==0) & main_vote0_1 -> TOTAL(c0,v0,m0_0,m0_1,m0_abs,p1_0,p1_1,m1_0,m1_1,m1_abs) -- always cast a main vote for abstain [] (if m0_abs TOTAL(c0,v0,m0_0,m0_1,m0_abs+1,p1_0,p1_1,m1_0,m1_1,m1_abs) else main_vote0_abs -> TOTAL(c0,v0,m0_0,m0_1,m0_abs,p1_0,p1_1,m1_0,m1_1,m1_abs) ) -- restrict pre votes that can be made in round r --coin (suppose that corrupted parties can always vote for abstain in round r-1) [] m0_abs>=K & pre1_coin?i -> TOTAL(c0,v0,m0_0,m0_1,m0_abs,p1_0,p1_1,m1_0,m1_1,m1_abs) --vote for 0 (suppose that corrupted parties can always vote for what honest parties vote for in round r-1) [] (m0_abs+m0_0+m0_1>=K and m0_0>0) & pre1_0?i -> TOTAL(c0,v0,m0_0,m0_1,m0_abs,p1_0,p1_1,m1_0,m1_1,m1_abs) --vote for 1 (suppose that corrupted parties can always vote for what honest parties vote for in round r-1) [] (m0_abs+m0_0+m0_1>=K and m0_1>0) & pre1_1?i -> TOTAL(c0,v0,m0_0,m0_1,m0_abs,p1_0,p1_1,m1_0,m1_1,m1_abs) -- casting pre vote in round r [] (if p1_0 TOTAL(c0,v0,m0_0,m0_1,m0_abs,p1_0+1,p1_1,m1_0,m1_1,m1_abs) else pre_vote1!0?i -> TOTAL(c0,v0,m0_0,m0_1,m0_abs,p1_0,p1_1,m1_0,m1_1,m1_abs) ) [] (if p1_1 TOTAL(c0,v0,m0_0,m0_1,m0_abs,p1_0,p1_1+1,m1_0,m1_1,m1_abs) else pre_vote1!1?i -> TOTAL(c0,v0,m0_0,m0_1,m0_abs,p1_0,p1_1,m1_0,m1_1,m1_abs) ) -- flipping of coins in round r [] (c0==0) & (flip_heads0 -> TOTAL(1,0,m0_0,m0_1,m0_abs,p1_0,p1_1,m1_0,m1_1,m1_abs) |~| flip_tails0 -> TOTAL(1,1,m0_0,m0_1,m0_abs,p1_0,p1_1,m1_0,m1_1,m1_abs) ) -- reading coins in round r [] (c0==1) & value_coin_0!v0 -> TOTAL(c0,v0,m0_0,m0_1,m0_abs,p1_0,p1_1,m1_0,m1_1,m1_abs) -- restrict main votes that can be made in round r -- vote for abstain (need pre vote for 0 and vote for 1 from either honest or corrupted parties) [] (m1_abs=K and (p1_0>0 or (c0==1 and v0==0) or m0_0>0) and (p1_1>0 or (c0==1 and v0==1) or m0_1>0)) & main_vote1_abs?i -> TOTAL(c0,v0,m0_0,m0_1,m0_abs,p1_0,p1_1,m1_0,m1_1,m1_abs+1) [] (m1_abs>=K and p1_0+p1_1>=K and (p1_0>0 or (c0==1 and v0==0) or m0_0>0) and (p1_1>0 or (c0==1 and v0==1) or m0_1>0)) & main_vote1_abs?i -> TOTAL(c0,v0,m0_0,m0_1,m0_abs,p1_0,p1_1,m1_0,m1_1,m1_abs) -- vote for 0 [] (m1_0=K and p1_0>=K) & main_vote1_0?i -> TOTAL(c0,v0,m0_0,m0_1,m0_abs,p1_0,p1_1,m1_0+1,m1_1,m1_abs) [] (m1_0>=K and p1_0+p1_1>=K and p1_0>=K) & main_vote1_0?i -> TOTAL(c0,v0,m0_0,m0_1,m0_abs,p1_0,p1_1,m1_0,m1_1,m1_abs) -- vote for 1 [] (m1_1=K and p1_1>=K) & main_vote1_1?i -> TOTAL(c0,v0,m0_0,m0_1,m0_abs,p1_0,p1_1,m1_0,m1_1+1,m1_abs) [] (m1_1>=K and p1_0+p1_1>=K and p1_1>=K) & main_vote1_1?i -> TOTAL(c0,v0,m0_0,m0_1,m0_abs,p1_0,p1_1,m1_0,m1_1,m1_abs) -- restrict pre votes that can be made in round r -- vote for coin [] (m1_abs>=K and (p1_1>0 or m0_0>0 or (c0==1 and v0==0)) and (p1_1>0 or m0_1>0 or (c0==1 and v0==1))) & pre2_coin?i -> TOTAL(c0,v0,m0_0,m0_1,m0_abs,p1_0,p1_1,m1_0,m1_1,m1_abs) -- vote for 0 [] (m1_abs+m1_0+m1_1>=K and m1_0>0 and (p1_0>=K or (c0==1 and v0==0))) & pre2_0?i -> TOTAL(c0,v0,m0_0,m0_1,m0_abs,p1_0,p1_1,m1_0,m1_1,m1_abs) -- vote for 1 [] (m1_abs+m1_0+m1_1>=K and m1_1>0 and (p1_1>=K or (c0==1 and v0==1))) & pre2_1?i -> TOTAL(c0,v0,m0_0,m0_1,m0_abs,p1_0,p1_1,m1_0,m1_1,m1_abs) within TOTAL(0,0,0,0,0,0,0,0,0,0) --%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -- ENVIRONMENTS -- combine the totals, counter and coins to give the environments -- environment for abstract protocol ABS_ENV = ABS_C [| {flip_heads0 , flip_tails0 , flip_heads1 , flip_tails1} |] ( ABS_TOTALS ||| COIN1 ) -- environment for concrete protocol ENV = ( C0 ||| C1 ) [| {flip_heads0 , flip_tails0 , flip_heads1 , flip_tails1} |] ( TOTALS ||| COIN1 ) --%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -- SETS OF ACTIONS -- alphabets for synchronization ABS_ALPHA = { pre1_0.1 , pre1_0.2 , pre1_0.3 , pre1_1.1 , pre1_1.2 , pre1_1.3 , read_main0 , value_coin_0.0 , value_coin_0.1 , pre_vote1.0.1 , pre_vote1.0.2 , pre_vote1.0.3 , pre_vote1.1.1 , pre_vote1.1.2 , pre_vote1.1.3 , main_vote1_0.1 , main_vote1_0.2 , main_vote1_0.3 , main_vote1_1.1 , main_vote1_1.2 , main_vote1_1.3 , main_vote1_abs.1 , main_vote1_abs.2 , main_vote1_abs.3 , pre2_coin.1 , pre2_coin.2 , pre2_coin.3 , pre2_0.1 , pre2_0.2 , pre2_0.3 , pre2_1.1 , pre2_1.2 , pre2_1.3 , value_coin_1.0 , value_coin_1.1 } ALPHA = { main_vote0_0, main_vote0_1 , main_vote0_abs , pre1_0.1 , pre1_0.2 , pre1_0.3 , pre1_1.1 , pre1_1.2 , pre1_1.3 , pre1_coin.1 , pre1_coin.2 , pre1_coin.3 , read_main0 , value_coin_0.0 , value_coin_0.1 , pre_vote1.0.1 , pre_vote1.0.2 , pre_vote1.0.3 , pre_vote1.1.1 , pre_vote1.1.2 , pre_vote1.1.3 , main_vote1_0.1 , main_vote1_0.2 , main_vote1_0.3 , main_vote1_1.1 , main_vote1_1.2 , main_vote1_1.3 , main_vote1_abs.1 , main_vote1_abs.2 , main_vote1_abs.3 , pre2_coin.1 , pre2_coin.2 , pre2_coin.3 , read_main1 , pre2_0.1 , pre2_0.2 , pre2_0.3 , pre2_1.1 , pre2_1.2 , pre2_1.3 , value_coin_1.0 , value_coin_1.1 } -- alphabet for hiding -- we hide only the action for the main votes of round r-1 -- since these votes are not actually made by the parties in the abstract protocol HIDE_ALPHA = { main_vote0_0, main_vote0_1 , main_vote0_abs , choose_0 , choose_1 } --%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -- SYSTEMS -- abstract system ABS_SYSTEM = ( ABS_ENV [| ABS_ALPHA |] ABS_PARTIES ) \ HIDE_ALPHA -- concrete system SYSTEM = ( ENV [| ALPHA |] PARTIES ) \ HIDE_ALPHA -- traces of SYSTEM included in the traces of ABS_SYSTEM assert ABS_SYSTEM [T= SYSTEM