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.
KeywordsProofs of security Program semantics Compositional security Refinement of ignorance
- 2.Alvim, M.S., Chatzikokolakis, K., Palamidessi, C., Smith, G.: Measuring information leakage using generalized gain functions. In: Proceedings of the 25th IEEE Computer Security Foundations Symposium (CSF 2012), pp. 265–279, June 2012Google Scholar
- 3.Back, R.-J.R.: Correctness preserving program refinements: proof theory and applications, Tract 131, Mathematisch Centrum, Amsterdam (1980)Google Scholar
- 5.Goguen, J.A., Meseguer, J.: Unwinding and inference control. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 75–86. IEEE Computer Society (1984)Google Scholar
- 6.Landauer, J., Redmond, T.: A lattice of information. In: Proceedings of the 6th IEEE Computer Security Foundations Workshop (CSFW 1993), pp. 65–70, June 1993Google Scholar
- 8.Mantel, H.: Preserving information flow properties under refinement. In: Proceedings of the IEEE Symposium Security and Privacy, pp. 78–91 (2001)Google Scholar
- 10.McIver, A.K., Morgan, C.C.: A calculus of revelations. Presented at VSTTE Theories Workshop, October 2008. http://www.cs.york.ac.uk/vstte08/
- 14.Morgan, C.C.: Programming from Specifications, 2nd edn. Prentice-Hall, Upper Saddle River (1994). http://web.comlab.ox.ac.uk/oucl/publications/books/PfS/ zbMATHGoogle Scholar
- 18.Schmidt, B., Schaller, P., Basin, D.: Impossibility results for secret establishment. In: Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF), pp. 261–273 (2010)Google Scholar