Paper 2016/548

Linicrypt: A Model for Practical Cryptography

Brent Carmer and Mike Rosulek


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.

Available format(s)
Publication info
A major revision of an IACR publication in Crypto 2016
garbled circuitssynthesis
Contact author(s)
carmerb @ eecs oregonstate edu
2016-06-20: revised
2016-06-02: received
See all versions
Short URL
Creative Commons Attribution


      author = {Brent Carmer and Mike Rosulek},
      title = {Linicrypt: A Model for Practical Cryptography},
      howpublished = {Cryptology ePrint Archive, Paper 2016/548},
      year = {2016},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.