15th Estonian Winter School in Computer Science (EWSCS)
XV Eesti Arvutiteaduse Talvekool

Palmse, Estonia, February 28 -March 5, 2010

Carroll Morgan

School of Computer Science and Engineering
University of New South Wales
Sydney, NSW, Australia

Security, Probability and Abstraction: Rigorous Methods for Source-Level Reasoning


Since 1995 [1] there has been intensive research in source-level assertion-style reasoning for developing probabilistic systems via stepwise refinement [2] through layers of abstraction [3], which work was summarised in a comprehensive text [4] in 2005. Since then the method has been adapted to deal with non-interference-style security, initially without probability [5] but most recently with probability as well [6].

This course will build on a basic understanding of Hoare/Dijkstra reasoning to explain these recent developments and how they fit in to the modern focus of research into secure systems and quantitative reasoning. In particular it will focus on systematic source-level developments of a number of well known probabilistic and security-sensitive algorithms, as examples, as well as explaining and illustrating general principles for doing work of this kind. There are many opportunities of up-to-the-minute topics for further research.


  1. C. Morgan, A. McIver, K. Seidel. Probabilistic predicate transformers. ACM Trans. on Program. Lang. and Syst., v. 18, n. 3, pp. 325-353, 1996. [doi link]
  2. N. Wirth. Program development by stepwise refinement. Commun. of ACM, v. 14. n. 4, pp. 221-227, 1971. [doi link]
  3. J.-R. Abrial. The B Book. Cambridge University Press, 1996.
  4. A. McIver, C. Morgan. Abstraction, Refinement and Proof for Probabilistic Systems, Monographs in Computer Science. Springer, 2005.
  5. C. Morgan. The shadow knows: refinement of ignorance in sequential programs. Sci. of Comput. Program., v. 74, n. 8, pp. 629-653, 2009. [doi link]
  6. C. Morgan. Security, probability and nearly fair coins in the cryptographers' café. In A. Cavalcanti, D. Dams, eds., Proc. of FM 2009, v. 5850 of Lect. Notes in Comput. Sci. pp. 41-71. Springer, 2009. [doi link]

Course materials

Valid CSS! Valid XHTML 1.0 Strict Last changed April 15, 2010 22:14 EET by local organizers, ewscs10(at)cs.ioc.ee
EWSCS'10 page: http://cs.ioc.ee/ewscs/2010/