@inbook{52d6910bf11c474fa4eb6e4c05b6dc70,
title = "Program refinement, perfect secrecy and information flow",
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.",
author = "McIver, {Annabelle K.}",
year = "2016",
doi = "10.1007/978-3-319-29628-9_2",
language = "English",
isbn = "9783319296272",
volume = "9506",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer, Springer Nature",
pages = "80--102",
editor = "Zhiming Liu and Zili Zhang",
booktitle = "Engineering Trustworthy Software Systems - 1st International School, SETSS 2014, Tutorial Lectures",
address = "United States",
edition = "1st",
}