CAVES: Cryptographic Analysis, Verification, Exploration, and Synthesis Navy SBIR FY2016.1 Sol No.: Navy SBIR FY2016.1 Topic No.: N161-058 Topic Title: CAVES: Cryptographic Analysis, Verification, Exploration, and Synthesis Proposal No.: N161-058-0065 Firm: Galois, Inc. 421 SW Sixth Ave Suite 300 Portland, Oregon 97204 Contact: Aaron Tomb Phone: (503) 808-7206 Web Site: http://www.galois.com Abstract: Developing secure cryptography to meet the constraints of a given application is currently a difficult, time-consuming, and error-prone process. Recent research suggests, however, that the work of evaluating the security of cryptographic algorithms, and of exploring the security tradeoffs of alternative designs within a general class, can be at least partly automated. We propose to build a comprehensive cryptographic analysis, verification, exploration and synthesis tool suite that provides users a wide variety of automated capabilities that assist in developing new cryptographic algorithms. CAVES will build upon Galois' existing Cryptol and SAW tools, which already allow for formal specification and verification of cryptographic implementations. The resulting tool kit will ultimately allow cryptographers to quickly describe an algorithm, automatically or semi-automatically perform a collection of cryptanalysis tasks to assess its likely level of security, and automatically enumerate various alternative designs along with assessment of their comparative security levels. Benefits: The proposed work will involve extending the existing Cryptol and SAW tools, which are freely available for non-commercial use, by integration with third-party open source tools. Cryptol and SAW are already in use within a variety of U.S. Government agencies, and we are in discussions with several commercial entities about licensing arrangements. The extensions developed in the proposed work will be made available as part of the core Cryptol and SAW implementations, and therefore to all existing users of the tools. Return