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.
260 lines
9.7 KiB
260 lines
9.7 KiB
// CROWDS [Reiter,Rubin]
|
|
// Vitaly Shmatikov, 2002
|
|
|
|
// Note:
|
|
// Change everything marked CWDSIZ when changing the size of the crowd
|
|
// Change everything marked CWDMAX when increasing max size of the crowd
|
|
|
|
dtmc
|
|
|
|
// Probability of forwarding
|
|
const double PF = 0.8;
|
|
|
|
// Probability that a crowd member is bad
|
|
const double badC = 0.091;
|
|
// const double badC = 0.167;
|
|
|
|
const int CrowdSize; // CWDSIZ: actual number of good crowd members
|
|
const int MaxGood=20; // CWDMAX: maximum number of good crowd members
|
|
|
|
// Process definitions
|
|
module crowds
|
|
|
|
// Auxiliary variables
|
|
launch: bool init true; // Start modeling?
|
|
new: bool init false; // Initialize a new protocol instance?
|
|
start: bool init false; // Start the protocol?
|
|
run: bool init false; // Run the protocol?
|
|
lastSeen: [0..MaxGood] init MaxGood; // Last crowd member to touch msg
|
|
good: bool init false; // Crowd member is good?
|
|
bad: bool init false; // ... bad?
|
|
recordLast: bool init false; // Record last seen crowd member?
|
|
badObserve: bool init false; // Bad members observes who sent msg?
|
|
deliver: bool init false; // Deliver message to destination?
|
|
done: bool init false; // Protocol instance finished?
|
|
|
|
[] launch -> (new'=true) & (launch'=false);
|
|
// Set up a new protocol instance
|
|
[newrun] new -> (new'=false) & (start'=true);
|
|
|
|
// SENDER
|
|
// Start the protocol
|
|
[] start -> (lastSeen'=0) & (run'=true) & (deliver'=false) & (start'=false);
|
|
|
|
// CROWD MEMBERS
|
|
// Good or bad crowd member?
|
|
[] !good & !bad & !deliver & run ->
|
|
1-badC : (good'=true) & (recordLast'=true) & (run'=false) +
|
|
badC : (bad'=true) & (badObserve'=true) & (run'=false);
|
|
|
|
// GOOD MEMBERS
|
|
// Forward with probability PF, else deliver
|
|
[] good & !deliver & run -> PF : (good'=false) + 1-PF : (deliver'=true);
|
|
// Record the last crowd member who touched the msg;
|
|
// all good members may appear with equal probability
|
|
// Note: This is backward. In the real protocol, each honest
|
|
// forwarder randomly chooses the next forwarder.
|
|
// Here, the identity of an honest forwarder is randomly
|
|
// chosen *after* it has forwarded the message.
|
|
[] recordLast & CrowdSize=2 ->
|
|
1/2 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
|
|
1/2 : (lastSeen'=1) & (recordLast'=false) & (run'=true);
|
|
[] recordLast & CrowdSize=4 ->
|
|
1/4 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
|
|
1/4 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
|
|
1/4 : (lastSeen'=2) & (recordLast'=false) & (run'=true) +
|
|
1/4 : (lastSeen'=3) & (recordLast'=false) & (run'=true);
|
|
[] recordLast & CrowdSize=5 ->
|
|
1/5 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
|
|
1/5 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
|
|
1/5 : (lastSeen'=2) & (recordLast'=false) & (run'=true) +
|
|
1/5 : (lastSeen'=3) & (recordLast'=false) & (run'=true) +
|
|
1/5 : (lastSeen'=4) & (recordLast'=false) & (run'=true);
|
|
[] recordLast & CrowdSize=10 ->
|
|
1/10 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
|
|
1/10 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
|
|
1/10 : (lastSeen'=2) & (recordLast'=false) & (run'=true) +
|
|
1/10 : (lastSeen'=3) & (recordLast'=false) & (run'=true) +
|
|
1/10 : (lastSeen'=4) & (recordLast'=false) & (run'=true) +
|
|
1/10 : (lastSeen'=5) & (recordLast'=false) & (run'=true) +
|
|
1/10 : (lastSeen'=6) & (recordLast'=false) & (run'=true) +
|
|
1/10 : (lastSeen'=7) & (recordLast'=false) & (run'=true) +
|
|
1/10 : (lastSeen'=8) & (recordLast'=false) & (run'=true) +
|
|
1/10 : (lastSeen'=9) & (recordLast'=false) & (run'=true);
|
|
[] recordLast & CrowdSize=15 ->
|
|
1/15 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
|
|
1/15 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
|
|
1/15 : (lastSeen'=2) & (recordLast'=false) & (run'=true) +
|
|
1/15 : (lastSeen'=3) & (recordLast'=false) & (run'=true) +
|
|
1/15 : (lastSeen'=4) & (recordLast'=false) & (run'=true) +
|
|
1/15 : (lastSeen'=5) & (recordLast'=false) & (run'=true) +
|
|
1/15 : (lastSeen'=6) & (recordLast'=false) & (run'=true) +
|
|
1/15 : (lastSeen'=7) & (recordLast'=false) & (run'=true) +
|
|
1/15 : (lastSeen'=8) & (recordLast'=false) & (run'=true) +
|
|
1/15 : (lastSeen'=9) & (recordLast'=false) & (run'=true) +
|
|
1/15 : (lastSeen'=10) & (recordLast'=false) & (run'=true) +
|
|
1/15 : (lastSeen'=11) & (recordLast'=false) & (run'=true) +
|
|
1/15 : (lastSeen'=12) & (recordLast'=false) & (run'=true) +
|
|
1/15 : (lastSeen'=13) & (recordLast'=false) & (run'=true) +
|
|
1/15 : (lastSeen'=14) & (recordLast'=false) & (run'=true);
|
|
[] recordLast & CrowdSize=20 ->
|
|
1/20 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
|
|
1/20 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
|
|
1/20 : (lastSeen'=2) & (recordLast'=false) & (run'=true) +
|
|
1/20 : (lastSeen'=3) & (recordLast'=false) & (run'=true) +
|
|
1/20 : (lastSeen'=4) & (recordLast'=false) & (run'=true) +
|
|
1/20 : (lastSeen'=5) & (recordLast'=false) & (run'=true) +
|
|
1/20 : (lastSeen'=6) & (recordLast'=false) & (run'=true) +
|
|
1/20 : (lastSeen'=7) & (recordLast'=false) & (run'=true) +
|
|
1/20 : (lastSeen'=8) & (recordLast'=false) & (run'=true) +
|
|
1/20 : (lastSeen'=9) & (recordLast'=false) & (run'=true) +
|
|
1/20 : (lastSeen'=10) & (recordLast'=false) & (run'=true) +
|
|
1/20 : (lastSeen'=11) & (recordLast'=false) & (run'=true) +
|
|
1/20 : (lastSeen'=12) & (recordLast'=false) & (run'=true) +
|
|
1/20 : (lastSeen'=13) & (recordLast'=false) & (run'=true) +
|
|
1/20 : (lastSeen'=14) & (recordLast'=false) & (run'=true) +
|
|
1/20 : (lastSeen'=15) & (recordLast'=false) & (run'=true) +
|
|
1/20 : (lastSeen'=16) & (recordLast'=false) & (run'=true) +
|
|
1/20 : (lastSeen'=17) & (recordLast'=false) & (run'=true) +
|
|
1/20 : (lastSeen'=18) & (recordLast'=false) & (run'=true) +
|
|
1/20 : (lastSeen'=19) & (recordLast'=false) & (run'=true);
|
|
|
|
// BAD MEMBERS
|
|
// Remember from whom the message was received and deliver
|
|
// CWDMAX: 1 rule per each good crowd member
|
|
[obs0] lastSeen=0 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false);
|
|
[obs1] lastSeen=1 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false);
|
|
[obs2] lastSeen=2 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false);
|
|
[obs3] lastSeen=3 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false);
|
|
[obs4] lastSeen=4 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false);
|
|
[obs5] lastSeen=5 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false);
|
|
[obs6] lastSeen=6 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false);
|
|
[obs7] lastSeen=7 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false);
|
|
[obs8] lastSeen=8 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false);
|
|
[obs9] lastSeen=9 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false);
|
|
[obs10] lastSeen=10 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false);
|
|
[obs11] lastSeen=11 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false);
|
|
[obs12] lastSeen=12 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false);
|
|
[obs13] lastSeen=13 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false);
|
|
[obs14] lastSeen=14 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false);
|
|
[obs15] lastSeen=15 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false);
|
|
[obs16] lastSeen=16 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false);
|
|
[obs17] lastSeen=17 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false);
|
|
[obs18] lastSeen=18 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false);
|
|
[obs19] lastSeen=19 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false);
|
|
|
|
// RECIPIENT
|
|
// Delivery to destination
|
|
[] deliver & run -> (done'=true) & (deliver'=false) & (run'=false) & (good'=false) & (bad'=false);
|
|
// Start a new instance
|
|
[] done -> (new'=true) & (done'=false) & (run'=false) & (lastSeen'=MaxGood);
|
|
|
|
endmodule
|
|
|
|
rewards "num_runs"
|
|
[newrun] true : 1;
|
|
endrewards
|
|
|
|
rewards "observe0"
|
|
[obs0] true : 1;
|
|
endrewards
|
|
|
|
rewards "observe1"
|
|
[obs1] true : 1;
|
|
endrewards
|
|
|
|
rewards "observe2"
|
|
[obs2] true : 1;
|
|
endrewards
|
|
|
|
rewards "observe3"
|
|
[obs3] true : 1;
|
|
endrewards
|
|
|
|
rewards "observe4"
|
|
[obs4] true : 1;
|
|
endrewards
|
|
|
|
rewards "observe5"
|
|
[obs5] true : 1;
|
|
endrewards
|
|
|
|
rewards "observe6"
|
|
[obs6] true : 1;
|
|
endrewards
|
|
|
|
rewards "observe7"
|
|
[obs7] true : 1;
|
|
endrewards
|
|
|
|
rewards "observe8"
|
|
[obs8] true : 1;
|
|
endrewards
|
|
|
|
rewards "observe9"
|
|
[obs9] true : 1;
|
|
endrewards
|
|
|
|
rewards "observe10"
|
|
[obs10] true : 1;
|
|
endrewards
|
|
|
|
rewards "observe11"
|
|
[obs11] true : 1;
|
|
endrewards
|
|
|
|
rewards "observe12"
|
|
[obs12] true : 1;
|
|
endrewards
|
|
|
|
rewards "observe13"
|
|
[obs13] true : 1;
|
|
endrewards
|
|
|
|
rewards "observe14"
|
|
[obs14] true : 1;
|
|
endrewards
|
|
|
|
rewards "observe15"
|
|
[obs15] true : 1;
|
|
endrewards
|
|
|
|
rewards "observe16"
|
|
[obs16] true : 1;
|
|
endrewards
|
|
|
|
rewards "observe17"
|
|
[obs17] true : 1;
|
|
endrewards
|
|
|
|
rewards "observe18"
|
|
[obs18] true : 1;
|
|
endrewards
|
|
|
|
rewards "observe19"
|
|
[obs19] true : 1;
|
|
endrewards
|
|
|
|
rewards "observeI"
|
|
[obs1] true : 1;
|
|
[obs2] true : 1;
|
|
[obs3] true : 1;
|
|
[obs4] true : 1;
|
|
[obs5] true : 1;
|
|
[obs6] true : 1;
|
|
[obs7] true : 1;
|
|
[obs8] true : 1;
|
|
[obs9] true : 1;
|
|
[obs10] true : 1;
|
|
[obs11] true : 1;
|
|
[obs12] true : 1;
|
|
[obs13] true : 1;
|
|
[obs14] true : 1;
|
|
[obs15] true : 1;
|
|
[obs16] true : 1;
|
|
[obs17] true : 1;
|
|
[obs18] true : 1;
|
|
[obs19] true : 1;
|
|
endrewards
|
|
|
|
|