Information-flow types for homomorphic encryptions

10 years 6 months ago
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...
Cédric Fournet, Jérémy Planul
Added 13 Dec 2011
Updated 13 Dec 2011
Type Journal
Year 2011
Where CCS
Authors Cédric Fournet, Jérémy Planul, Tamara Rezk
Comments (0)