Formal Verification of Anti-Cheating Protocols in Cryptoeconomic Systems
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

#### 131 lines 6.3 KiB Raw Permalink Blame History

 ``````// Formal Model based on Snowflake from Scalable and Probabilistic Leaderless BFTConsensus through Metastability (https://avalanchelabs.org/QmT1ry38PAmnhparPUmsUNHDEGHQusBLD6T5XJh4mUUn3v.pdf) // Model Authored by Sarah Jamie Lewis ctmc const samples; const alpha; const beta; const color1init; const color2init; const color3init; const color4init; const timeout_max; const origcol1 = color1init; const origcol2 = color1init; const origcol3 = color1init; formula hsum = (color1+color2+color3); formula htotal_diff = (hsum=3 | hsum=6) ? 0 : 1; formula sum = (color1+color2+color3+jit); formula total_diff = (sum=4 | sum=8) ? 0 : ( (sum=5 | sum=7) ? 1 : 2 ); // This will always return false. formula consensus_check = (color1 > 0) & (color1 = color2) & (color3 = jit) & (color3 = color1); formula have_enough_samples = samples = 2 ? (sampled_1_2 > 0 & sampled_1_3 > 0) | (sampled_1_2 > 0 & sampled_1_4 > 0) | (sampled_1_3 > 0 & sampled_1_4 > 0) : (sampled_1_2 > 0 & sampled_1_3 > 0 & sampled_1_4 > 0); formula opposite_color = (color1 = 1) ? 2 : 1; formula diff2 = (sampled_1_2 = opposite_color); formula diff3 = (sampled_1_3 = opposite_color); formula diff4 = (sampled_1_4 = opposite_color); formula count_diff = (diff2 & diff3 & diff4) ? 3 : ( (diff2 & diff3) | (diff3 & diff4) | (diff2 & diff4) ? 2 : ( (diff2 | diff3 | diff4) ? 1 : 0 )); formula over_alpha = (count_diff >= alpha); // If all honest nodes have reached their beta then we are done formula done = (count1 = beta) & (count2 = beta) & (count3 = beta); // If there is no skew among the honest nodes, seed doubt formula jit = (htotal_diff = 0) ? opposite_color: color1; module adversarial_scheduler [p1] (color1 > 0) -> true; [p2] (count1 = beta) -> true; [p3] (count2 = beta) -> true; endmodule module peer1 color1: [0..2] init color1init; // Sampled This Round sampled_1_2: [0..samples] init 0; sampled_1_3: [0..samples] init 0; sampled_1_4: [0..samples] init 0; count1: [0..beta] init 0; delay: bool init false; timeout: [0..(timeout_max+1)] init 0; // Atomic Lookups make this *much* easier for the correct nodes...yet they will still fail... [] (samples=2 & !delay & consensus_check = false & count1 < beta & sampled_1_2 = 0 & sampled_1_3 = 0 & have_enough_samples = false) -> (sampled_1_2' = color2) & (sampled_1_3' = color3); [] (samples=2 & !delay & consensus_check = false & count1 < beta & sampled_1_4 = 0 & sampled_1_2= 0 & have_enough_samples = false) -> (delay' = true) & (sampled_1_2' = color2) & (timeout' = 0); [] (samples=2 & !delay & consensus_check = false & count1 < beta & sampled_1_4 = 0 & sampled_1_3 = 0 & have_enough_samples = false) -> (delay' = true) & (sampled_1_3' = color3) & (timeout' = 0); [] (samples=3 & !delay & consensus_check = false & count1 < beta & sampled_1_4 = 0 & sampled_1_3 = 0 & sampled_1_2 = 0 & have_enough_samples = false) -> (delay' = true) & (timeout' = 0) & (sampled_1_3' = color3) & (sampled_1_2' = color2) ; // Delay and Reset [](delay = true & timeout < timeout_max) -> (delay' = true) & (timeout' = timeout + 1); []((delay = true & timeout = timeout_max) | timeout_max = 0) -> (delay' = false) & (timeout' = 0) & (sampled_1_2' = 0) & (sampled_1_3' = 0) & (sampled_1_4' = 0); // Original non-atomic sampling code // Query Peer 2 //[p1] (consensus_check = false & count1 < beta & sampled_1_2 = 0 & have_enough_samples = false) -> (sampled_1_2' = color2); // Query Peer 3 //[p1] (consensus_check = false & count1 < beta & sampled_1_3 = 0 & have_enough_samples = false) -> (sampled_1_3' = color3); // Query Peer 4 //[] (consensus_check = false & count1 < beta & sampled_1_4 = 0 & have_enough_samples = false) -> (sampled_1_4' = color4); // Model an adversarial node [p1] (samples=2 & delay = true & consensus_check = false & count1 < beta & sampled_1_4 = 0 & sampled_1_2 = 0 & have_enough_samples = false) -> (sampled_1_4' = opposite_color) & (delay' = false); [p1] (samples=2 & delay = true & consensus_check = false & count1 < beta & sampled_1_4 = 0 & sampled_1_3 = 0 & have_enough_samples = false) -> (sampled_1_4' = opposite_color) & (delay' = false); [p1] (samples=3 & delay = true & consensus_check = false & count1 < beta & sampled_1_4 = 0 & have_enough_samples = false) -> (sampled_1_4' = opposite_color) & (delay' = false); // If there are more of the opposite color than our chosen color, switch and reset the count [] (consensus_check = false & count1 < beta & have_enough_samples & over_alpha) -> (color1' = opposite_color) & (count1' = 0) & (sampled_1_2' = 0) & (sampled_1_3' = 0) & (sampled_1_4' = 0) & (delay' = false); // If the threshold isn't met then increase count [] (consensus_check = false & count1 < beta & have_enough_samples & over_alpha = false) -> (count1' = count1 + 1) & (sampled_1_2' = 0) & (sampled_1_3' = 0) & (sampled_1_4' = 0) & (delay' = false); // Update Color [] (consensus_check = true | count1 = beta) -> (color1' = color1); endmodule module peer2 = peer1 [ color1=color2, color2=color1, color1init = color2init, color3=color3, count1=count2, round_samples=round_samples2, sampled_1_2=sampled_2_1, sampled_1_3=sampled_2_3,sampled_1_4=sampled_2_4, diff_votes_1=diff_votes_2,p1=p2, delay = delay2, timeout = timeout2,origcol1=origcol2 ] endmodule module peer3 = peer1 [ color1=color3, color2=color1, color3=color1, color1init = color3init, count1=count3, round_samples=round_samples3, sampled_1_2=sampled_3_1, sampled_1_3=sampled_3_2,sampled_1_4=sampled_3_4, diff_votes_1=diff_votes_3, p1=p3, delay = delay3, timeout = timeout3,origcol1=origcol3 ] endmodule //module peer4 = peer1 [ color1=color4,color1init=color4init, count1=count4, round_samples=round_samples4, sampled_1_2=sampled_4_1, sampled_1_3=sampled_4_2,sampled_1_4=sampled_4_3, diff_votes_1=diff_votes_4, color4=color1 ] endmodule label "finished" = done; label "consensus" = done & (color1 = color2) & (color2 = color3); formula done_split = done & (((color1 +color2 + color3) = 3) | ((color1 +color2 + color3) = 6)) = false; label "finished_without_consensus" = done & (((color1 +color2 + color3) = 3) | ((color1 +color2 + color3) = 6)) = false; // Calculate probability of consensus rewards "network_skew" true: 1 - (htotal_diff/2); endrewards // Calculate chance of revision rewards "beta" true: count1/beta; endrewards rewards "time" true : 1; endrewards``````