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.

57 lines
4.0 KiB

  1. // Formal Model based on Slush from Scalable and Probabilistic Leaderless BFTConsensus through Metastability (https://avalanchelabs.org/QmT1ry38PAmnhparPUmsUNHDEGHQusBLD6T5XJh4mUUn3v.pdf)
  2. // Model Authored by Sarah Jamie Lewis
  3. ctmc
  4. const samples;
  5. const double chanceRed;
  6. const double alpha;
  7. formula color_check = color1 > 0 & color2 > 0 & color3 > 0 & color4 > 0 & color5 > 0;
  8. module player1
  9. color1: [0..2] init 0;
  10. // Sampled This Round
  11. round_samples: [0..samples] init 0;
  12. sampled_1_2: bool init false;
  13. sampled_1_3: bool init false;
  14. sampled_1_4: bool init false;
  15. sampled_1_5: bool init false;
  16. diff_votes_1: [0..samples] init 0;
  17. // Initialize Color
  18. [] (color1 = 0) -> chanceRed: (color1' = 1 ) + 1-chanceRed: (color1' = 2);
  19. // Query Peer 2
  20. [] (round_samples < samples & sampled_1_2 = false & color_check & color1 != color2 & diff_votes_1 < samples) -> (sampled_1_2' = true) & (round_samples' = round_samples + 1) & (diff_votes_1' = diff_votes_1 + 1);
  21. [] (round_samples < samples & sampled_1_2 = false & color_check & color1 = color2) -> (sampled_1_2' = true) & (round_samples' = round_samples + 1);
  22. // Query Peer 3
  23. [] (round_samples < samples & sampled_1_3 = false & color_check & color1 != color3 & diff_votes_1 < samples) ->(sampled_1_3' = true) & (round_samples' = round_samples + 1) & (diff_votes_1' = diff_votes_1 + 1);
  24. [] (round_samples < samples & sampled_1_3 = false & color_check & color1 = color3) -> (sampled_1_3' = true) & (round_samples' = round_samples + 1);
  25. // Query Peer 4
  26. [] (round_samples < samples & sampled_1_4 = false & color_check& color1 != color4 & diff_votes_1 < samples) -> (sampled_1_4' = true) & (round_samples' = round_samples + 1) & (diff_votes_1' = diff_votes_1 + 1);
  27. [] (round_samples < samples & sampled_1_4 = false & color_check & color1 = color4) -> (sampled_1_4' = true) & (round_samples' = round_samples + 1);
  28. // Query Peer 5
  29. [] (round_samples < samples & sampled_1_5 = false & color_check & color1 != color5 & diff_votes_1 < samples) -> (sampled_1_5' = true) & (round_samples' = round_samples + 1) & (diff_votes_1' = diff_votes_1 + 1);
  30. [] (round_samples < samples & sampled_1_5 = false & color_check & color1 = color5) -> (sampled_1_5' = true) & (round_samples' = round_samples + 1);
  31. // Update Color
  32. [] (round_samples = samples & diff_votes_1 < samples*alpha) -> (color1' = color1) & (round_samples' = 0) & (sampled_1_2' = false) & (sampled_1_3' = false) & (sampled_1_4' = false) & (sampled_1_5' = false) & (diff_votes_1' = 0);
  33. [] (round_samples = samples & diff_votes_1 >= samples*alpha & color1 = 1) -> (color1' = 2) & (round_samples' = 0) & (sampled_1_2' = false) & (sampled_1_3' = false) & (sampled_1_4' = false) & (sampled_1_5' = false) & (diff_votes_1' = 0);
  34. [] (round_samples = samples & diff_votes_1 >= samples*alpha & color1 = 2) -> (color1' = 1) & (round_samples' = 0) & (sampled_1_2' = false) & (sampled_1_3' = false) & (sampled_1_4' = false) & (sampled_1_5' = false) & (diff_votes_1' = 0);
  35. endmodule
  36. module peer2 = player1 [ color1=color2, round_samples=round_samples2, sampled_1_2=sampled_2_1, sampled_1_3=sampled_2_3,sampled_1_4=sampled_2_4, sampled_1_5=sampled_2_5, diff_votes_1=diff_votes_2, color2=color1 ] endmodule
  37. module peer3 = player1 [ color1=color3, round_samples=round_samples3, sampled_1_2=sampled_3_1, sampled_1_3=sampled_3_2,sampled_1_4=sampled_3_4, sampled_1_5=sampled_3_5, diff_votes_1=diff_votes_3, color3=color1 ] endmodule
  38. module peer4 = player1 [ color1=color4, round_samples=round_samples4, sampled_1_2=sampled_4_1, sampled_1_3=sampled_4_2,sampled_1_4=sampled_4_3, sampled_1_5=sampled_4_5, diff_votes_1=diff_votes_4, color4=color1 ] endmodule
  39. module peer5 = player1 [ color1=color5, round_samples=round_samples5, sampled_1_2=sampled_5_1, sampled_1_3=sampled_5_2,sampled_1_4=sampled_5_3, sampled_1_5=sampled_5_4, diff_votes_1=diff_votes_5, color5=color1 ] endmodule
  40. label "consensus" = (color1 > 0) & (color1 = color2) & (color3 = color4) & (color3 = color1) & (color1 = color5);
  41. rewards "rounds"
  42. [] (round_samples = samples): 1;
  43. endrewards