// probabilistic fair exchange [Rab81] // Gethin Norman and Vitaly Shmatikov 2004 mdp module parties mA : [0..10]; // number in the last message sent by A mB : [0..10]; // number in the last message sent by B turn : [0..1]; // who last sent a message (0- B did and 1 - A did) // can only send messages when d=0 (i.e. before the future date arrives) [] turn=0 & mA<10 & d=0 -> (turn'=1) & (mA'=mA+1); // party A sends a message [] turn=1 & mA<10 & d=0 -> (turn'=0) & (mB'=mA); // party B sends a message endmodule module date d : [0..1]; [] d=0 -> (d'=1); // future date arrives endmodule module third_party i : [0..10]; // integer chosen // randomly choose integer on the future date [] i=0 & d=1 -> 1/10 : (i'=1) + 1/10 : (i'=2) + 1/10 : (i'=3) + 1/10 : (i'=4) + 1/10 : (i'=5) + 1/10 : (i'=6) + 1/10 : (i'=7) + 1/10 : (i'=8) + 1/10 : (i'=9) + 1/10 : (i'=10); endmodule