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. In this work, we investigate tools for programmatically altering existing cryptographic constructions to reflect particular design goals. Our techniques enhance both security and efficiency with the assistance of advanced tools including Satisfiability Modulo Theories (SMT) solvers.
Specifically, we propose two complementary tools, Au-toGroup and AutoStrong. AutoGroup converts a pairingbased encryption or signature scheme written in (simple) symmetric group notation into a specific instantiation in the more efficient, asymmetric setting. Some existing symmetric schemes have hundreds of possible asymmetric translations, and this tool allows the user to optimize the construction according to a variety of metrics, such as ciphertext size, key size or computation time. The AutoStrong tool focuses on the security of digital signature schemes by automatically converting an existentially unforgeable signature scheme into a strongly unforgeable one. The main technical challenge here is to automate the "partitioned" check, which allows a highly-efficient transformation.
These tools integrate with and complement the Auto-Batch tool (ACM CCS 2012), but also push forward on the * Joseph A.