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.