On the Emerging Trend of Computer-Aided Cryptology and the Technology Transition Gap it Presents

Presented as part of the 2018 HCSS conference.

BIO

Dr. Evan Austin is a scientist in the Research and Applied Science competency of Space and Naval Warfare (SPAWAR) Systems Center Atlantic in Charleston, South Carolina.  Since joining SPAWAR Systems Center Atlantic in 2015, Dr. Austin has served as the principal investigator on a number of internally and externally funded basic and applied research projects with the shared theme of high-assurance software and systems development.  He also serves as the technical lead for SPAWAR Systems Center Atlantic's recently formed Automated Cryptology research and development team and as a member of their Science and Technology Advisory Council. 

Dr. Austin holds Bachelor of Science, Master of Science, and Doctor of Philosophy degrees in computer science, all from the University of Kansas.  His primary research interests are applied formal methods and programming language theory.

ABSTRACT

Modern cryptography has greatly benefited from calls for open standardization. The push for “one size fits all” solutions like the Advanced Encryption Standard (AES) and the Secure Hash Algorithms family has promoted interoperability and allowed researchers to focus on improving the security and performance of the most widely adopted cryptosystems, maximizing the impact of their efforts. However, the looming quantum computing threat and desires to utilize cryptography in previously unidentified domains and applications have precipitated a shift towards alternative cryptographic primitives. To date, these new algorithms and parameter sets have not received the same level of scrutiny and review that a system like AES has enjoyed over its last twenty years.

There is a shared belief that the lack of analysis, especially in the form of formal verification, is due to the increasingly complex constructions that new cryptoschemes are founded on. Borrowing the words of Halevi, Bellare, and Rogaway – “[cryptographers] generate more proofs than [they] carefully verify”1 because “many proofs in cryptography have become essentially unverifiable”2. Inspired by the more general software and hardware verification communities, cryptologists have leveraged advances in formal methods and language theory research in the development of tools and techniques to address this issue giving rise to the comparatively young field of computer-aided cryptology.

The purpose of this talk is to communicate our experiences investigating and working with a subset of cryptologic reasoning tools. The specific focus will be on the challenges we faced trying to transition research software to a more operationally focused environment staffed with subject matter, but not necessarily formal methods and programming language, experts. We will also highlight areas where we think the application of these tools would be of immediate benefit, including in blockchain assurance, one of this year’s highlighted themes of the High Confidence Software and Systems Conference.

1 A Plausible Approach to Computer-Aided Cryptographic Proofs, Shai Halevi
2 Code-Based Game-Playing Proofs and the Security of Triple Encryption, Mihir Bellare and Phillip Rogaway