CAVES: Cryptographic Analysis, Verification, Exploration, and Synthesis

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.