Sums and Lovers: Case Studies in Security, Compositionality and Refinement

摘要

A truly secure protocol is one which never violates its security requirements, no matter how bizarre the circumstances, provided those circumstances are within its terms of reference. Such cast-iron guarantees, as far as they are possible, require formal techniques: proof or model-checking. Informally, they are difficult or impossible to achieve.rnOur 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.rnA 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.rnCorrectness in all contexts is crucial for our goal of layered, refinement-based developments. This is ensured by our semantics in which the program constructors are monotonic with respect to "security-aware" refinement, which is in turn a generalisation of compositionality.