Sums and Lovers: Case studies in security,

Abstract. A truly secure protocol is one which never violates its se-curity requirements, no matter how bizarre the circumstances, provided those circumstances are within its terms of reference. Such cast-iron guar-antees, as far as they are possible, require formal techniques: proof or model-checking. Informally, they are difficult or impossible to achieve. Our formal technique is refinement, until recently not much applied to security. We argue its benefits by giving rigorous formal developments, in refinement-based program algebra, of several security case studies. A conspicuous feature of our studies is their layers of abstraction and –for the main study, in particular – that the protocol is unbounded in state, placing its verification beyond the reach of model checkers. Correctness in all contexts is crucial for our goal of layered, refinement-based developments. This is ensured by our semantics in which the pro-gram constructors are monotonic with respect to “security-aware ” re-finement, which is in turn a generalisation of compositionality