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.

88 lines
3.7 KiB

  1. dtmc
  2. // probability of forwarding
  3. const double PF = 0.8;
  4. const double notPF = .2; // must be 1-PF
  5. // probability that a crowd member is bad
  6. const double badC = .167;
  7. // probability that a crowd member is good
  8. const double goodC = 0.833;
  9. // Total number of protocol runs to analyze
  10. const int TotalRuns = 5;
  11. // size of the crowd
  12. const int CrowdSize = 10;
  13. module crowds
  14. // protocol phase
  15. phase: [0..4] init 0;
  16. // crowd member good (or bad)
  17. good: bool init false;
  18. // number of protocol runs
  19. runCount: [0..TotalRuns] init 0;
  20. // observe_i is the number of times the attacker observed crowd member i
  21. observe0: [0..TotalRuns] init 0;
  22. observe1: [0..TotalRuns] init 0;
  23. observe2: [0..TotalRuns] init 0;
  24. observe3: [0..TotalRuns] init 0;
  25. observe4: [0..TotalRuns] init 0;
  26. observe5: [0..TotalRuns] init 0;
  27. observe6: [0..TotalRuns] init 0;
  28. observe7: [0..TotalRuns] init 0;
  29. observe8: [0..TotalRuns] init 0;
  30. observe9: [0..TotalRuns] init 0;
  31. // the last seen crowd member
  32. lastSeen: [0..CrowdSize - 1] init 0;
  33. // get the protocol started
  34. [] phase=0 & runCount<TotalRuns -> 1: (phase'=1) & (runCount'=runCount+1) & (lastSeen'=0);
  35. // decide whether crowd member is good or bad according to given probabilities
  36. [] phase=1 -> goodC : (phase'=2) & (good'=true) + badC : (phase'=2) & (good'=false);
  37. // if the current member is a good member, update the last seen index (chosen uniformly)
  38. [] phase=2 & good -> 1/10 : (lastSeen'=0) & (phase'=3) + 1/10 : (lastSeen'=1) & (phase'=3) + 1/10 : (lastSeen'=2) & (phase'=3) + 1/10 : (lastSeen'=3) & (phase'=3) + 1/10 : (lastSeen'=4) & (phase'=3) + 1/10 : (lastSeen'=5) & (phase'=3) + 1/10 : (lastSeen'=6) & (phase'=3) + 1/10 : (lastSeen'=7) & (phase'=3) + 1/10 : (lastSeen'=8) & (phase'=3) + 1/10 : (lastSeen'=9) & (phase'=3);
  39. // if the current member is a bad member, record the most recently seen index
  40. [] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> 1: (observe0'=observe0+1) & (phase'=4);
  41. [] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> 1: (observe1'=observe1+1) & (phase'=4);
  42. [] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> 1: (observe2'=observe2+1) & (phase'=4);
  43. [] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> 1: (observe3'=observe3+1) & (phase'=4);
  44. [] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> 1: (observe4'=observe4+1) & (phase'=4);
  45. [] phase=2 & !good & lastSeen=5 & observe5 < TotalRuns -> 1: (observe5'=observe5+1) & (phase'=4);
  46. [] phase=2 & !good & lastSeen=6 & observe6 < TotalRuns -> 1: (observe6'=observe6+1) & (phase'=4);
  47. [] phase=2 & !good & lastSeen=7 & observe7 < TotalRuns -> 1: (observe7'=observe7+1) & (phase'=4);
  48. [] phase=2 & !good & lastSeen=8 & observe8 < TotalRuns -> 1: (observe8'=observe8+1) & (phase'=4);
  49. [] phase=2 & !good & lastSeen=9 & observe9 < TotalRuns -> 1: (observe9'=observe9+1) & (phase'=4);
  50. // good crowd members forward with probability PF and deliver otherwise
  51. [] phase=3 -> PF : (phase'=1) + notPF : (phase'=4);
  52. // deliver the message and start over
  53. [] phase=4 -> 1: (phase'=0);
  54. endmodule
  55. label "observe0Greater1" = observe0>1;
  56. label "observe1Greater1" = observe1>1;
  57. label "observe2Greater1" = observe2>1;
  58. label "observe3Greater1" = observe3>1;
  59. label "observe4Greater1" = observe4>1;
  60. label "observe5Greater1" = observe5>1;
  61. label "observe6Greater1" = observe6>1;
  62. label "observe7Greater1" = observe7>1;
  63. label "observe8Greater1" = observe8>1;
  64. label "observe9Greater1" = observe9>1;
  65. label "observeIGreater1" = observe1>1|observe2>1|observe3>1|observe4>1|observe5>1|observe6>1|observe7>1|observe8>1|observe9>1;
  66. label "observeOnlyTrueSender" = observe0>1&observe1<=1&observe2<=1&observe3<=1&observe4<=1&observe5<=1&observe6<=1&observe7<=1&observe8<=1&observe9<=1;