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 contributionpeer-review

11 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
Country/TerritoryNetherlands
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