Program refinement, perfect secrecy and information flow

Annabelle K. McIver*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingChapter

1 Citation (Scopus)

Abstract

“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
Pages80-102
Number of pages23
Volume9506
Edition1st
ISBN (Print)9783319296272
DOIs
Publication statusPublished - 2016

Publication series

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

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

  • Cite this

    McIver, A. K. (2016). Program refinement, perfect secrecy and information flow. In Z. Liu, & Z. Zhang (Eds.), Engineering Trustworthy Software Systems - 1st International School, SETSS 2014, Tutorial Lectures (1st ed., Vol. 9506, pp. 80-102). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9506). Cham, Switzerland: Springer, Springer Nature. https://doi.org/10.1007/978-3-319-29628-9_2