(Chaum)
Three cryptographers are having dinner at their favourite restaurant. The waiter informs them that arrangements have been made for the bill to be paid anonymously: one of the cryptographers might be paying for the dinner, or it might be their master. The three cryptographers respect each other's privacy, but would like to know if the master is paying for dinner. To answer this question the cryptographers take part in the following protocol [Cha88]:
An even number of "agrees"s indicates that the master paid while an odd number indicates that a cryptographer paid.
The above protocol can be generalised to any number N of cryptographers, where:
By way of example, the PRISM source code for the algorithm in the case where N = 3 is given below.
// model of dining cryptographers // gxn/dxp 15/11/06 mdp // number of cryptographers const int N = 3; // constants used in renaming (identities of cryptographers) const int p1 = 1; const int p2 = 2; const int p3 = 3; // global variable which decides who pays // (0 - master pays, i=1..N - cryptographer i pays) global pay : [0..N]; // module for first cryptographer module crypt1 coin1 : [0..2]; // value of its coin s1 : [0..1]; // its status (0 = not done, 1 = done) agree1 : [0..1]; // what it states (0 = disagree, 1 = agree) // flip coin [] coin1=0 -> 0.5 : (coin1'=1) + 0.5 : (coin1'=2); // make statement (once relevant coins have been flipped) // agree (coins the same and does not pay) [] s1=0 & coin1>0 & coin2>0 & coin1=coin2 & (pay!=p1) -> (s1'=1) & (agree1'=1); // disagree (coins different and does not pay) [] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay!=p1) -> (s1'=1); // disagree (coins the same and pays) [] s1=0 & coin1>0 & coin2>0 & coin1=coin2 & (pay=p1) -> (s1'=1); // agree (coins different and pays) [] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay=p1) -> (s1'=1) & (agree1'=1); // synchronising loop when finished to avoid deadlock [done] s1=1 -> true; endmodule // construct further cryptographers with renaming module crypt2 = crypt1 [ coin1=coin2, s1=s2, agree1=agree2, p1=p2, coin2=coin3 ] endmodule module crypt3 = crypt1 [ coin1=coin3, s1=s3, agree1=agree3, p1=p3, coin2=coin1 ] endmodule // set of initial states // (cryptographers in their initial state, "pay" can be anything) init coin1=0&s1=0&agree1=0 & coin2=0&s2=0&agree2=0 & coin3=0&s3=0&agree3=0 endinit // unique integer representing outcome formula outcome = 4*agree1 + 2*agree2 + 1*agree3 ; // parity of number of "agree"s (0 = even, 1 = odd) formula parity = func(mod, agree1+agree2+agree3, 2); // label denoting states where protocol has finished label "done" = s1=1&s2=1&s3=1; // label denoting states where number of "agree"s is even label "even" = func(mod,(agree1+agree2+agree3),2)=0; // label denoting states where number of "agree"s is even label "odd" = func(mod,(agree1+agree2+agree3),2)=1;
The table below shows statistics for the MDPs we have built for different values of the constant N. The tables include:
N: | Model: | Construction time (s): | |||
States: | Transitions: | ||||
3 | 286 | 585 | 0.001 | ||
4 | 1,733 | 4,580 | 0.01 | ||
5 | 9,876 | 32,315 | 0.03 | ||
6 | 54,055 | 211,566 | 0.07 | ||
7 | 287,666 | 1,312,045 | 0.11 | ||
8 | 1,499,657 | 7,813,768 | 0.22 | ||
9 | 7,695,856 | 45,103,311 | 0.34 | ||
10 | 39,005,611 | 253,985,650 | 0.52 | ||
15 | 115,553,171,626 | 1,128,594,416,085 | 3.27 | ||
20 | 304,287,522,253,461 | 3,962,586,180,540,340 | 13.48 |
We have model checked the following properties:
Correctness. To prove correctness we show that:
i.e. that, if the master paid, the parity of the number of "agree"s matches the parity of N and, if a cryptographer paid, it does not. In PRISM, we have:
// Correctness for the case where the master pays // (final parity of number of number of "agrees"s matches that of N) (pay=0) => P>=1 [ F "done" & parity=func(mod, N, 2) ] // Correctness for the case where a cryptographer pays // (final parity of number of number of "agrees"s does not match that of N) (pay>0) => P>=1 [ F "done" & parity!=func(mod, N, 2) ]
where the label "done
" and the formula parity
are defined in the model (above).
Model Checking Times:
N: | master pays: | cryptographers pay: | ||||
time: | iterations: | time: | iterations: | |||
3 | 0.028 | 7 | 0.008 | 7 | ||
4 | 0.061 | 9 | 0.032 | 9 | ||
5 | 0.141 | 11 | 0.085 | 11 | ||
6 | 0.322 | 13 | 0.292 | 13 | ||
7 | 0.778 | 15 | 0.563 | 15 | ||
8 | 1.467 | 17 | 2.25 | 17 | ||
9 | 2.67 | 19 | 4.14 | 19 | ||
10 | 6.30 | 21 | 7.63 | 21 | ||
15 | 56.9 | 31 | 185 | 31 | ||
20 | 268 | 41 | 954 | 41 |
Anonymity. To verify anonymity, namely that when a cryptographer pays then no cryptographer can tell which one has paid, we check that any possible combination of "agree" and "disagree" has the same likelihood no matter which of the cryptographers pays. Furthermore, we need to check that the probability of each combination is the same for any possible scheduling of the cryptographers during the protocol.
We do this by computing, for each of the 2^{N} possible outcomes (only 2^{(N-1)} of which should occur when a cryptographer paid), the minimum and maximum probability it occurring. The PRISM property file is:
const int k; // Anonymity - check for k=0..2^N - both min/max should be the same and equal to 1/2^(N-1) or 0 // (depending on the parity of the number of bits in the binary representation of outcome) Pmin=? [ F "done" & outcome = k {"init"&pay>0}{min} ] Pmax=? [ F "done" & outcome = k {"init"&pay>0}{max} ]
where the formula outcome
(which maps the different possible values of the "agree"s
to distinct unique integer values) is defined in the model (shown above).
The table below gives the results for checking that, when N is odd all the cryptographers state disagree (k=0), and when N is even only the Nth cryptographer states disagree (k=1).
Model Checking Times:
N: | minimum: | maximum: | ||||||
time: | iterations: | probability: | time: | iterations: | probability: | |||
3 | 0.099 | 8 | 0.25 | 0.004 | 8 | 0.25 | ||
4 | 0.041 | 10 | 0.125 | 0.006 | 10 | 0.125 | ||
5 | 0.172 | 12 | 0.0625 | 0.032 | 12 | 0.0625 | ||
6 | 0.231 | 14 | 0.03125 | 0.044 | 14 | 0.03125 | ||
7 | 0.595 | 16 | 0.015625 | 0.301 | 16 | 0.015625 | ||
8 | 1.111 | 18 | 0.0078125 | 0.540 | 18 | 0.0078125 | ||
9 | 2.12 | 20 | 0.00390625 | 1.31 | 20 | 0.00390625 | ||
10 | 3.53 | 22 | 0.001953125 | 2.67 | 22 | 0.001953125 | ||
15 | 45.1 | 32 | 6.103515625E-5 | 36.8 | 32 | 6.103515625E-5 |