|
Computer-Aided Cryptographic Algorithm Design and Exploration Workbench
Navy SBIR 2016.1 - Topic N161-058 ONR - Ms. Lore-Anne Ponirakis - [email protected] Opens: January 11, 2016 - Closes: February 17, 2016 N161-058 TITLE: Computer-Aided Cryptographic Algorithm Design and Exploration Workbench TECHNOLOGY AREA(S): Information Systems OBJECTIVE: Design and develop an integrated workbench and tools for computer-aided design and exploration for cryptographic algorithms. DESCRIPTION: Cryptography has been one of the foundational building blocks for privacy and security in the cyber environment. Researchers in the field of cryptography are continuously exploring and developing new algorithms, classes/types, and capabilities; recent advancements in cryptography include fully homomorphic encryption (FHE) and attribute-based encryption. However, algorithmic exploration in cryptography remains a laborious mathematical exercise. In addition, verifying the correctness and security of a cryptographic algorithm is equally laborious, manual, and error prone. For instance, several publications in cryptography have had to be retracted due to unforeseen errors in the formalizations of security proofs. The complexity and brittleness of the security properties of cryptographic algorithms make it especially difficult to develop an automated generator and verifier for new algorithms. However, recent developments in academic research have demonstrated the power of automation in cryptographic design [1,2] and in verifying the security of cryptographic proofs [3]. Currently, the tools developed for these works exist as academic prototypes and may not have been developed to interoperate with other tools. Relatively immature, these tools often require significant formal programming knowledge to operate successfully, and hence are not easily accessible to mainstream cryptographers (users). An easy-to-use cryptographic design and verification workbench can significantly reduce the amount of effort required and the error potential associated with cryptographic design exploration and verification. Such a toolset could serve as an integrated design environment capable of performing the full process of automated cryptographic algorithm design, from algorithmic exploration to proving security properties under many different attack scenarios (e.g., chosen ciphertext and/or plaintext attacks, etc.). This cryptographic workbench should integrate various theorem provers with a mechanized verification process, build special automated exploration tools for cryptographic algorithm design, and must be able to accommodate the integration of future tools. This workbench will also serve as a platform for fostering the integration and collaboration of researchers and developers of cryptographic automation tools. The tools and workbench developed in this SBIR topic would lower the barrier for cryptographic algorithm design and exploration, hence accelerating the discovery of various new types of cryptographic algorithms and protocols. The workbench should allow cryptographers to explore a wider range of the design space and construction for cryptographic algorithms, far beyond what can be achieved with manual exploration, without requiring its users to be experts in formal programming. Besides reducing the design effort and potential for error, computer-aided cryptography may allow for the discovery of a large number of secure algorithms of certain types and properties. The availability of a large collection of similarly secure algorithms would allow for further filtering of algorithms according to properties orthogonal to security, such as computational requirements, implementation complexity, and power requirements, depending on the particular needs of an application. PHASE I: Identify an initial set of tools suitable for computer-aided cryptographic design, design any missing elements in the tool chain, and devise methods which allow tools to interoperate. Design an extensible workbench to integrate the tools into an environment capable of performing the full process of automated cryptographic algorithm design. Develop an initial proof-of concept prototype for the workbench. PHASE II: Based upon the Phase I effort, develop and enhance the integrated workbench and tools for computer-aided design and exploration for cryptographic algorithms prototype into a fully functioning workbench. Demonstrate and evaluate the efficacy of the tool for exploring selected types of cryptographic algorithms and corresponding design goals, for example by showing that the workbench can successfully be used to design and develop a new cryptographic algorithm or be used to verify the security properties of an existing cryptographic algorithm. PHASE III DUAL USE APPLICATIONS: Upon successful completion of Phase II, the performer will provide support in transitioning the cryptographic workbench to the Navy for its intended use. The performer will develop a plan for integrating the product into the Navy�s information system security framework. Usually as a result of the requirements of the operating environment, non-standard cryptographic algorithms have been employed in a variety of commercial devices and applications, e.g., RFID, embedded sensors, business and financial transactions, data warehousing, etc. Such custom cryptographic algorithms are often sub-par in the quality of security they provide. As such, the ability to automatically design, develop, and verify a secure (high-quality) cryptographic algorithm which fits particular design requirements will have strong commercial demand, and will improve the security of commercial devices and applications. The availability of the cryptographic workbench will also accelerate the discovery of various novel cryptographic capabilities such as homomorphic encryption and attribute-based-encryption at research institutes and universities around the world. REFERENCES: 1. Joseph A. Akinyele, Matthew Green, and Susan Hohenberger. Using smt solvers to automate design tasks for encryption and signature schemes. In Proceedings of the 2013 ACM Conference on Computer and Communications Security, CCS '13, pages 399-410, New Yo 2. Joseph A. Akinyele, Matthew Green, Susan Hohenberger, and Matthew W. Pagano. Machine- generated algorithms, proofs and software for the batch verification of digital signature schemes. In Proceedings of the 2012 ACM Conference on Computer and Communications Security, CCS '12, pages 474-487, New York, NY, USA, 2012. ACM. 3. Gilles Barthe, Benjamin Gregoire, Sylvain Heraud, and SantiagoZanella Beguelin. Computer-aided security proofs for the working cryptographer. In Phillip Rogaway, editor, Advances in Cryptology CRYPTO 2011, volume 6841 of Lecture Notes in Computer Scien 4. Daniel Bleichenbacher. Chosen ciphertext attacks against protocols based on the rsa encryption standard pkcs #1. In CRYPTO, pages 1-12, 1998. 5. Johannes Blomer and Gennadij Liske. Direct chosen-ciphertext secure attribute-based key encapsulations without random oracles. Cryptology ePrint Archive, Report 2013/646, 2013. http://eprint.iacr.org/. KEYWORDS: cryptography; algorithmic design; automation; security proofs; cyber; encryption TPOC-1: Ryan Craven Email: [email protected] TPOC-2: Sukarno Mertoguno Email: [email protected] Questions may also be submitted through DoD SBIR/STTR SITIS website.
|