Security and probability are both artefacts that we hope to bring increasingly within the reach of refinement-based Formal
Methods; although we have worked on them separately, in the past, the goal has always been to bring them together.
In this report we describe our ongoing work in that direction: we relate it to a well known problem in security, Chaum’s Dining Cryptographers, where the various criteria of correctness that might apply to it expose precisely the issues we have found to be significant
in our efforts to deal with security, probability and abstraction all at once.
Taking our conviction into this unfamiliar and demanding territory, that abstraction and refinement are the key tools of software
development, has turned out to be an exciting challenge.