Computer-Aided Security Proofs for the Working Cryptographer
Computer-Aided Security Proofs for the Working Cryptographer
复制标题
DOI：
10.1007/978-3-642-22792-9_5
复制
发表时间：
2011-08
期刊：
影响因子：
--
通讯作者：
G. Barthe;B. Grégoire;S. Heraud;Santiago Zanella-Béguelin
中科院分区：
文献类型：
--
作者：
G. Barthe;B. Grégoire;S. Heraud;Santiago Zanella-Béguelin
我们提出了EasyCrypt，这是一个自动工具，用于从证明草图中阐述密码系统的安全证明-证明的本质作为一系列游戏和提示的紧凑、正式的表示。使用现成的SMT解算器和自动化的定理证明器自动检查校样草图，然后在证书加密框架中将其编译为可验证的校样。该工具支持大多数常见的推理模式，并且比它的前身更容易使用。我们认为EasyCrypt是一个可能被工作的密码学家采用的候选方案，并举例说明了它在Cramer-Shoup和哈希德·ElGamal密码系统的安全证明中的应用。
We present EasyCrypt, an automated tool for elaborating security proofs of cryptographic systems from proof sketches–compact, formal representations of the essence of a proof as a sequence of games and hints. Proof sketches are checked automatically using off-the-shelf SMT solvers and automated theorem provers, and then compiled into verifiable proofs in the CertiCrypt framework. The tool supports most common reasoning patterns and is significantly easier to use than its predecessors. We argue that EasyCrypt is a plausible candidate for adoption by working cryptographers and illustrate its application to security proofs of the Cramer-Shoup and Hashed ElGamal cryptosystems.