# Dining Cryptographers

(Chaum)

### Introduction

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]:

• Each cryptographer flips an unbiased coin and only informs the cryptographer on the right of the outcome.
• Each cryptographer states whether the two coins that it can see (the one it flipped and the one the left-hand neighbour flipped) are the same ("agree") or different ("disagree").
• However, if a cryptographer actually paid for dinner, then it instead states the the opposite ("disagree" if the coins are the same and "agree" if the coins are different).

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:

• if N is odd, then an odd number of "agree"s indicates that the master paid while an even number indicates that a cryptographer paid.
• if N is even, then an even number of "agree"s indicates that the master paid while an odd number indicates that a cryptographer paid;

### The model

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;
```

### Model Statistics

The table below shows statistics for the MDPs we have built for different values of the constant N. The tables include:

• the number of states and transitions in the MDP representing the model;
• the construction time which equals the time taken for the system description to be parsed and converted to the MTBDD representing it, and the time to perform reachability, identify the non-reachable states and filter the MTBDD accordingly.
 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

### Model Checking

We have model checked the following properties:

• Correctness. To prove correctness we show that:

• if N is odd, then an odd number of "agree"s indicates that the master paid while an even number indicates that a cryptographer paid.
• if N is even, then an even number of "agree"s indicates that the master paid while an odd number indicates that a cryptographer paid;

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

Conclusion: the properties hold in all states
• 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 2N 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).