In this series of lectures I will describe how to use abstraction and refinement to reason about confidentiality properties in sequential programs. In the first two lectures a simple  model based on Kripke structures is used to give a qualitative semantics to determine whether  secret information is leaked inadvertently and in lectures 3&4 those  ideas are generalised to enable the quantitative analysis of how much any leaked information can be used by  an adversary.

Throughout the lectures the emphasis is on reasoning rules and the comparison of programs (and specifications)  using a refinement order which maintains both functional consistency as well as information flow properties.
The approach is illustrated by a number of well-known case studies drawn from the security literature.