Compositional refinement in agent-based security protocols

A. K. McIver*, C. C. Morgan

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

3 Citations (Scopus)


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. BCS

Original languageEnglish
Pages (from-to)711-737
Number of pages27
JournalFormal Aspects of Computing
Issue number6
Publication statusPublished - Nov 2011


Dive into the research topics of 'Compositional refinement in agent-based security protocols'. Together they form a unique fingerprint.

Cite this