Formal Verification of a SHA-1 Circuit Core Using ACL2
Formal Verification of a SHA-1 Circuit Core Using ACL2
复制标题
使用 ACL2 对 SHA-1 电路核心进行形式验证
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
D. Borrione
中科院分区：
文献类型：
--
作者：
Diana Toma;D. Borrione
我们的研究是一个项目的一部分，该项目旨在设计和验证计算机和终端智能卡读卡器之间的安全通信电路。电路中包括SHA-1组件。SHA-1是一种加密原语，它为任何消息生成160位的消息摘要。我们形式化了ACL2中的标准规范，然后自动生成用于VHDLRTL设计的ACL2模型，最后证明了该实现符合该规范。我们应用了一种逐步的方法，使用中间摘要函数来证明关于RTL设计的每个计算步骤的定理。
Our study was part of a project aiming at the design and verification of a circuit for secure communications between a computer and a terminal smart card reader. A SHA-1 component is included in the circuit. SHA-1 is a cryptographic primive that produces, for any message, a 160 bit message digest. We formalize the standard specification in ACL2, then automatically produce the ACL2 model for the VHDL RTL design; finally, we prove the implementation compliant with the specification. We apply a stepwise approach that proves theorems about each computation step of the RTL design, using intermediate digest functions.