Sums and lovers

Case studies in security, compositionality and refinement

Annabelle K. McIver, Carroll C. Morgan

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

10 Citations (Scopus)

Abstract

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. Our 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 program constructors are monotonic with respect to "security-aware" refinement, which is in turn a generalisation of compositionality.

Original languageEnglish
Title of host publicationFM 2009: Formal Methods
Subtitle of host publicationSecond World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings
EditorsAna Cavalcanti, Dennis R. Dams
Place of PublicationBerlin
PublisherSpringer, Springer Nature
Pages289-304
Number of pages16
ISBN (Electronic)9783642050893
ISBN (Print)9783642050886
DOIs
Publication statusPublished - 2009
Event2nd World Congress on Formal Methods, FM 2009 - Eindhoven, Netherlands
Duration: 2 Nov 20096 Nov 2009

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume5850
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other2nd World Congress on Formal Methods, FM 2009
CountryNetherlands
CityEindhoven
Period2/11/096/11/09

Fingerprint Dive into the research topics of 'Sums and lovers: Case studies in security, compositionality and refinement'. Together they form a unique fingerprint.

  • Cite this

    McIver, A. K., & Morgan, C. C. (2009). Sums and lovers: Case studies in security, compositionality and refinement. In A. Cavalcanti, & D. R. Dams (Eds.), FM 2009: Formal Methods: Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings (pp. 289-304). (Lecture Notes in Computer Science; Vol. 5850). Berlin: Springer, Springer Nature. https://doi.org/10.1007/978-3-642-05089-3_19