This case study is based on the well known dining cryptographers problem [Cha88].

For more information, see: http://www.prismmodelchecker.org/casestudies/dining_crypt.php

=====================================================================================

[Cha88]
D. Chaum
The Dining Cryptographers Problem: Unconditional Sender and Recipient Untraceability
Journal of Cryptology, vol. 1, pp 65-75, 1988