Enabling Machine-aided Cryptographic Design
Embargo until
Date
2013-11-13
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Johns Hopkins University
Abstract
The design of cryptographic primitives such as digital signatures and public-key encryption is very often a manual process conducted by expert cryptographers. This persists despite the fact that many new generic or semi-generic methods have been proposed to construct new primitives by transforming existing ones in interesting ways. However, manually applying transformations to existing primitives can be error-prone, ad-hoc and tedious. A natural question is whether automating the process of applying cryptographic transformations would yield competitive or better results?
In this thesis, we explore a compiler-based approach for automatically performing certain cryptographic designs. Similar approaches have been applied to various types of cryptographic protocol design with compelling results. We extend this same approach and show that it also can be effective towards automatically applying cryptographic transformations.
We first present our extensible architecture that automates a class of cryptographic transformations on primitives. We then propose several techniques that address the aforementioned question including the Charm cryptographic framework, which enables rapid prototyping of cryptographic primitives from abstract descriptions. We build on this work and show the extent to which transformations can be performed automatically given these descriptions. To illustrate this automation, we present a series of cryptographic tools that demonstrate the effectiveness of our automated approach. Our contributions are listed as follows:
- AutoBatch: Batch verification is a transformation that improves signature verification time by efficiently processing many signatures at once. Historically, this manual process has been prone to error and tedious for practitioners. We describe the design of an automated tool that finds efficient batch verification algorithms from abstract descriptions of signature schemes.
- AutoGroup: Cryptographers often prefer to describe their pairing-based constructions using symmetric group notation for simplicity, while they prefer asymmetric groups for implementation due to the efficiency gains. The symmetric- to-asymmetric translation is usually performed through manual analysis of a scheme and finding an efficient translation that suits applications can be quite challenging. We present an automated tool that uses SMT solvers to find efficient asymmetric translations from abstract descriptions of cryptographic schemes.
- AutoStrong: Strongly unforgeable signatures are desired in practice for a variety of cryptographic protocols. Several transformations exist in the literature that show how to obtain strongly unforgeable signatures from existentially unforgeable ones. We focus on a particular highly-efficient transformation due to Boneh, Shen and Waters that is applicable if the signature satisfies a notion of partitioning. Checking for this property can be challenging and has been less explored in the literature. We present an automated tool that also utilizes SMT solvers to determine when this property is applicable for constructing efficient strongly unforgeable signatures from abstract descriptions.
We anticipate that these proof-of-concept tools embody the notion that certain cryptographic transformations can be safely and effectively outsourced to machines.
Description
Keywords
digital signatures, public-key encryption, pairing-based cryptography, automation, cryptographic compilers