## Cryptology ePrint Archive: Report 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.

Category / Keywords: foundations / garbled circuits, synthesis

Original Publication (with major differences): IACR-CRYPTO-2016

Date: received 1 Jun 2016, last revised 20 Jun 2016

Contact author: carmerb at eecs oregonstate edu

Available format(s): PDF | BibTeX Citation

Short URL: ia.cr/2016/548

[ Cryptology ePrint archive ]