Computationally sound typing for non-interference: The case of deterministic encryption

Abstract

Type systems for secure information flow aim to prevent a program from leaking information from variables that hold secret data to variables that hold public data. In this work we present a type system to address deterministic encryption. The intuition that encrypting a secret yields a public value, that can be stored in a public variable, is faithful for probabilistic encryption but erroneous for deterministic encryption. We prove the computational soundness of our type system in the concrete security framework. © Springer-Vorlag Berlin Heidelberg 2007.