Computationally Sound Typing for Non-interference: The Case of Deterministic Encryption

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.

• Type: Conference
• Year: 2007
• Where: FSTTCS
• Authors: Judicaël Courant, Cristian Ene, Yassine Lakhnech
• Keywords: Deterministic Encryption, FSTTCS 2007, Information flow Aim, Type System