The thousand-and-one cryptographers

A. K. McIver, C. C. 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 demonstrated 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: that is unusually general. 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 also actually to be recommended. It benefits from more than 3 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 publicationReflections on the work of C.A.R. Hoare
EditorsA. W. Roscoe, C. B. Jones, Kenneth B Wood
Place of PublicationLondon
PublisherSpringer, Springer Nature
Number of pages28
ISBN (Print)9781848829121
Publication statusPublished - 2010

Publication series

NameHistory of computing


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

Cite this