Automating Cryptographic Design Tasks
Abstract
Abstract: Cryptographic design tasks are primarily performed by hand today. Shifting more of this burden to computers could make the design process faster, more accurate and less expensive. As part of our past work, we investigated tools for programmatically altering existing cryptographic constructions to reflect particular design goals. For instance, we developed a suite of tools, which could work together, for improving the efficiency of signature verification (AutoBatch), altering the algebraic setting of a signature or encryption scheme to optimize performance on a per application basis (AutoGroup), to strengthen the security of a digital signature scheme (AutoStrong), and more. Often, in the cryptographic literature, a single scheme is presented for peer?review, but hundreds or thousands of deviations of this scheme are possible, and some of these variations may be more desirable than the original in different applications. Our work allows users to quickly (in a matter of seconds or less) find a provably secure scheme optimized for their needs. Our automation implementations are enhanced with the assistance of advanced tools including Satisfiability Modulo Theories (SMT) solvers and Mathematica. Our objective for this proposal is to deepen our understanding and capabilities for cryptographic automation by developing new tools and proof techniques for automation and by exploring new problem spaces. Our approach to automation is to first search for naturally occurring patterns in cryptographic design that might lend themselves to automation. The next step is to devise a means for translating the creative design task into a problem that computers are better at solving (e.g., an SMT problem). After this, we implement our automation to test its accuracy and performance. Finally, we must formally prove that the scheme resulting from this transformation process are both correct and secure. For this proposal, we will specifically investigate new automation areas, such as leveraging the power of obfuscation for automation, understanding whether some existing automations are indeed secure (e.g., AutoGroup, CloudSource), and further exploring the automation of authenticated encryption, block cipher modes and related building blocks. The hope is that this might supplement the limited set of modes currently supplied by NIST standards, and offer security assurances for those modes that are currently authorized by NIST, but have not been proven secure. This proposal may have numerous applications for government and industry. For example, it may allow for the dynamic construction of other primitives such as hash functions based on program synthesis of underlying building blocks, including compression functions and round functions.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Aug 12, 2016
- Source ID
- N000141512778
Entities
People
- Susan Hohenberger
Organizations
- Johns Hopkins University
- Office of Naval Research
- United States Navy