Program refinement, perfect secrecy and information flow

Annabelle K. McIver*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review

1 Citation (Scopus)


“Classical” proofs of secure systems are based on reducing the hardness of one problem (defined by the protocol) to that of another (a known difficult computational problem). In standard program development [1,3,14] this “comparative approach” features in stepwise refinement: describe a system as simply as possible so that it has exactly the required properties and then apply sound refinement rules to obtain an implementation comprising specific algorithms and data-structures. More recently the stepwise refinement method has been extended to include “information flow” properties as well as functional properties, thus supporting proofs about secrecy within a program refinement method. In this paper we review the security-by-refinement approach and illustrate how it can be used to give an elementary treatment of some well known security principles.

Original languageEnglish
Title of host publicationEngineering Trustworthy Software Systems - 1st International School, SETSS 2014, Tutorial Lectures
EditorsZhiming Liu, Zili Zhang
Place of PublicationCham, Switzerland
PublisherSpringer, Springer Nature
Number of pages23
ISBN (Print)9783319296272
Publication statusPublished - 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)03029743
ISSN (Electronic)16113349


Dive into the research topics of 'Program refinement, perfect secrecy and information flow'. Together they form a unique fingerprint.

Cite this