Information-flow types for homomorphic encryptions

We develop a flexible information-flow type system for a range of encryption primitives, precisely reflecting their diverse functional and security features. Our rules enable encryption, blinding, homomorphic computation, and decryption, with selective key re-use for different types of payloads. We show that, under standard cryptographic assumptions, any well-typed probabilistic program using encryptions is secure (that is, computationally non-interferent) against active adversaries, both for confidentiality and integrity. We illustrate our approach using ElGamal and Paillier encryption. We present two applications of cryptographic verification by typing: (1) private search on data streams; and (2) the bootstrapping part of Gentry’s fully homomorphic encryption. We provide a prototype typechecker for our system. Categories and Subject Descriptors K.6.m [Security and Protection]: Security; D.2.0 [Software Engineering]: Protection Mechanisms; F.3.1 [Specifying and Verifying and R...

• Type: Journal
• Year: 2011
• Where: CCS
• Authors: Cédric Fournet, Jérémy Planul, Tamara Rezk
• Keywords: CCS 2011, Data Streams, Design Languages, Protection Mechanisms, Security Privacy