This paper presents a program analysis for secure information flow. The analysis works on a simple imperative programming
language containing a cryptographic primitive—encryption—as a possible operation. The analysis captures the intuitive qualities
of the (lack of) information flow from a plaintext to its corresponding ciphertext. The analysis is proved correct with respect
to a complexity-theoretical definition of the security of information flow. In contrast to the previous results, the analysis
does not put any restrictions on the structure of the program, especially on the ways of how the program uses the encryption
keys.
Supported by Estonian Science Foundation grant #5279. Most of this work was done while the author was at the University of
Saarland, Germany.