Advertisement
Published in:
2005 | OriginalPaper | Chapter
Formal Verification of a SHA-1 Circuit Core Using ACL2
Authors : Diana Toma, Dominique Borrione
Published in: Theorem Proving in Higher Order Logics
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.