Program Refinement, Perfect Secrecy and Information Flow

摘要

"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.