Program Refinement, Perfect Secrecy and Information Flow

  • Annabelle K. McIverEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9506)


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


Proofs of security Program semantics Compositional security Refinement of ignorance 

Supplementary material


  1. 1.
    Abrial, J.-R.: The B Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)CrossRefzbMATHGoogle Scholar
  2. 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. 3.
    Back, R.-J.R.: Correctness preserving program refinements: proof theory and applications, Tract 131, Mathematisch Centrum, Amsterdam (1980)Google Scholar
  4. 4.
    Denning, D.: Cryptography and Data Security. Addison-Wesley, Boston (1983)zbMATHGoogle Scholar
  5. 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. 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
  7. 7.
    Leino, K.R.M., Joshi, R.: A semantic approach to secure information flow. Sci. Comput. Program. 37(1–3), 113–138 (2000)MathSciNetzbMATHGoogle Scholar
  8. 8.
    Mantel, H.: Preserving information flow properties under refinement. In: Proceedings of the IEEE Symposium Security and Privacy, pp. 78–91 (2001)Google Scholar
  9. 9.
    McIver, A.K.: The secret art of computer programming. In: Leucker, M., Morgan, C. (eds.) ICTAC 2009. LNCS, vol. 5684, pp. 61–78. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  10. 10.
    McIver, A.K., Morgan, C.C.: A calculus of revelations. Presented at VSTTE Theories Workshop, October 2008.
  11. 11.
    McIver, A.K., Morgan, C.C.: Sums and Lovers: Case Studies in Security, Compositionality and Refinement. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 289–304. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  12. 12.
    McIver, A., Meinicke, L., Morgan, C.: Compositional closure for bayes risk in probabilistic noninterference. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 223–235. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  13. 13.
    McIver, A., Morgan, C., Smith, G., Espinoza, B., Meinicke, L.: Abstract channels and their robust information-leakage ordering. In: Abadi, M., Kremer, S. (eds.) POST 2014 (ETAPS 2014). LNCS, vol. 8414, pp. 83–102. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  14. 14.
    Morgan, C.C.: Programming from Specifications, 2nd edn. Prentice-Hall, Upper Saddle River (1994). zbMATHGoogle Scholar
  15. 15.
    Morgan, C.C.: The shadow knows: refinement of ignorance in sequential programs. In: Uustalu, T. (ed.) Math Prog Construction. Springer, vol. 4014, pp. 359–378. Springer, Treats Dining Cryptographers (2006)CrossRefGoogle Scholar
  16. 16.
    Morgan, C.C., Knows, T.S.: Refinement of ignorance in sequential programs. Sci. Comput. Program. 74(8), 629–653 (2009). Treats Oblivious TransferCrossRefGoogle Scholar
  17. 17.
    Sabelfeld, A., Sands, D.: A PER model of secure information flow in sequential programs. High.-Ord. Symbolic Comput. 14(1), 59–91 (2001)CrossRefzbMATHGoogle Scholar
  18. 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
  19. 19.
    Shamir, A.: How to share a secret. Commun. ACM 22(11), 612–613 (1979)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Shannon, C.E.: Theory of secrecy systems. Bell Syst. Tech. J. 28, 656–715 (1949)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.Department of ComputingMacquarie UniversitySydneyAustralia

Personalised recommendations