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.
|Title of host publication||Reflections on the work of C.A.R. Hoare|
|Editors||A. W. Roscoe, C. B. Jones, Kenneth B Wood|
|Place of Publication||London|
|Publisher||Springer, Springer Nature|
|Number of pages||28|
|Publication status||Published - 2010|
|Name||History of computing|