A type system for computationally secure information flow

Abstract

The paper presents a novel type system for checking the security of information flow in programs containing operations of symmetric encryption. The type system is correct with respect to the complexity-theoretic security definitions of the encryption primitive. © Springer-Verlag Berlin Heidelberg 2005.