A symbolic execution engine for improved proof automation in machine-checked cryptography

点击翻译按钮获取中文摘要

Within the computational model of provable security, EasyCrypt stands out as one of the leading tools for verifying game-based, cryptographic proofs. It is equipped with a proof assistant that provides a set of low-level tactics allowing for a great deal of control over proofs. These tactics maximise EasyCrypt's versatility which grants it similar capabilities as pen-and-paper proofs. However, due to the lack of higher-level tactics, users can and do suffer from the need to carry out a variety of tedious proofs steps that can distract from the larger goal at hand. In contrast, a tool like CryptoVerif can discharge proofs automatically, only requiring user input when stuck. Although CryptoVerif and EasyCrypt operate in a similar space, CryptoVerif distances itself from the implementation of the protocols it is reasoning about; a problem that EasyCrypt specifically targets. Consequently, this project seeks to leverage ideas around proof automation, from static analysis to cryptographic proof tools, and adapt them to EasyCrypt. The main approach is to use a symbolic execution engine to enhance EasyCrypt's proof system allowing for program simplification at no cost to the proof goals. This will afford EasyCrypt users greater productivity and an enhanced user experience. With a keen focus on formal verification of cryptographic proofs this project fits well within the Verification and Correctness EPSRC research area.