Finding a Middle Ground for Computer-Aided Cryptography
Motivated by the ever-increasing difficulty of proofs of security and correctness, cryptographers have drawn inspiration from the more general software and hardware verification communities and integrated formal methods tools and techniques into their workflows. Though this practice of computer-aided cryptography is still comparatively young, it has spawned a number of automated cryptographic analysis tools. These tools can be categorized in one of two ways: tools focused on theoretical, or “provable,” aspects of security; and tools focused on verifying more practical implementation details. This paper discusses our motivation for, and early work towards, finding an approachable middle ground of the current cryptographic tool spectrum.
- 3.Bellare, M., Rogaway, P.: Code-Based Game-Playing Proofs and the Security of Triple Encryption. Cryptology ePrint Archive, Report 2004/331 (2004)Google Scholar
- 5.Claessen, K., Hughes, J.: QuickCheck: a Lightweight Tool for Random Testing of Haskell Programs. In: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, ICFP 2000, pp. 268–279. ACM, New York (2000)Google Scholar
- 6.Crockett, E., Peikert, C.: \(\Lambda \, o \, \lambda \): functional lattice cryptography. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, CCS 2016, pp. 993–1005. ACM, New York (2016). http://doi.acm.org/10.1145/2976749.2978402
- 9.Erkök, L., Matthews, J.: High assurance programming in cryptol. In: Proceedings of the 5th Annual Workshop on Cyber Security and Information Intelligence Research: Cyber Security and Information Intelligence Challenges and Strategies, CSIIRW 2009, pp. 60:1–60:2. ACM, New York (2009)Google Scholar
- 10.Halevi, S.: A plausible approach to computer-aided cryptographic proofs. Cryptology ePrint Archive, Report 2005/181 (2005)Google Scholar
- 12.Shoup, V.: Sequences of games: a tool for taming complexity in security proofs. Cryptology ePrint Archive, Report 2004/332 (2004)Google Scholar