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

在可证明安全性的计算模型中，EasyCrypt是验证基于游戏的加密证明的领先工具之一。它配备了一个证明助手，提供了一套低级别的策略，允许大量的控制证明。这些策略最大限度地提高了EasyCrypt的多功能性，使其具有与纸笔证明类似的功能。然而，由于缺乏更高层次的策略，用户可能并且确实需要进行各种繁琐的证明步骤，这些步骤可能会分散对手头更大目标的注意力。相比之下，像CryptoVerif这样的工具可以自动排出证明，只需要用户输入就可以了。虽然CryptoVerif和EasyCrypt在类似的空间中运行，但CryptoVerif与它所推理的协议的实现保持距离;这是EasyCrypt专门针对的问题。因此，该项目旨在利用有关证明自动化的想法，从静态分析到加密证明工具，并使其适应EasyCrypt。主要的方法是使用一个符号执行引擎来增强EasyCrypt的证明系统，允许在不牺牲证明目标的情况下简化程序。这将为EasyCrypt用户提供更高的生产力和增强的用户体验。该项目专注于加密证明的形式化验证，非常适合验证和正确性EPSRC研究领域。

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.