Paper 2016/548
Linicrypt: A Model for Practical Cryptography
Brent Carmer and Mike Rosulek
Abstract
A wide variety of objectively practical cryptographic schemes can be constructed using only symmetric-key operations and linear operations. To formally study this restricted class of cryptographic algorithms, we present a new model called {\em Linicrypt}. A Linicrypt program has access to a random oracle whose inputs and outputs are field elements, and otherwise manipulates data only via fixed linear combinations. Our main technical result is that it is possible to decide {\em in polynomial time} whether two given Linicrypt programs induce computationally indistinguishable distributions (against arbitrary PPT adversaries, in the random oracle model). We show also that indistinguishability of Linicrypt programs can be expressed as an existential formula, making the model amenable to {\em automated program synthesis.} In other words, it is possible to use a SAT/SMT solver to automatically generate Linicrypt programs satisfying a given security constraint. Interestingly, the properties of Linicrypt imply that this synthesis approach is both sound and complete. We demonstrate this approach by synthesizing Linicrypt constructions of garbled circuits.
Metadata
- Available format(s)
-
PDF
- Category
- Foundations
- Publication info
- A major revision of an IACR publication in CRYPTO 2016
- Keywords
- garbled circuitssynthesis
- Contact author(s)
- carmerb @ eecs oregonstate edu
- History
- 2016-06-20: revised
- 2016-06-02: received
- See all versions
- Short URL
- https://ia.cr/2016/548
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2016/548,
author = {Brent Carmer and Mike Rosulek},
title = {Linicrypt: A Model for Practical Cryptography},
howpublished = {Cryptology {ePrint} Archive, Paper 2016/548},
year = {2016},
url = {https://eprint.iacr.org/2016/548}
}
