Compositional refinement in agent-based security protocols

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, rigorous techniques: proof or model-checking. Informally, they are difficult or impossible to achieve. Our rigorous technique is refinement, until recently not much applied to security. We argue its benefits by using refinement-based program algebra to develop several security case studies. That is one of our contributions here. The soundness of the technique follows from its compositional semantics, one which we defined (elsewhere) to support a specialisation of standard refinement by enriching standard semantics with information that tracks correlations between hidden state and visible behaviour. A further contribution is to extend the basic theory of secure refinement (Morgan in Mathematics of program construction, Springer, Berlin, vol. 4014, pp. 359-378, 2006) with special features required by our case studies, namely agent-based systems with complementary security requirements, and looping programs.