The thousand-and-one cryptographers

Annabelle McIver, Carroll Morgan

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review


Chaum's Dining Cryptographers protocol crystallises the essentials of security just as other famous diners once captured deadlock and livelock: it is a benchmark for security models and their associated verification methods.

Here we give a correctness proof of the Cryptographers in a new style, one in which stepwise refinement plays a prominent role. Furthermore, our proof applies to arbitrarily many Diners: to our knowledge we are only the second group to have done that.

The proof is based on the Shadow Security Model which integrates non-interference and program refinement: with it, we try to make a case that stepwise development of security protocols is not only possible but actually is quite a good idea. It benefits from more than three decades' of experience of how layers of abstraction can both simplify the design process and make its outcomes more likely to be correct.
Original languageEnglish
Title of host publicationEngineering Secure and Dependable Software Systems
EditorsAlexander Pretschner, Peter Müller, Patrick Stöckle
Place of PublicationAmsterdam
PublisherIOS Press
Number of pages26
ISBN (Electronic)9781614999775
ISBN (Print)9781614999768
Publication statusPublished - 2019

Publication series

NameNATO Science for Peace and Security Series. Sub-Series D: Information and Communication Security
ISSN (Print)1874-6268
ISSN (Electronic)1879-8292


Dive into the research topics of 'The thousand-and-one cryptographers'. Together they form a unique fingerprint.

Cite this