Toma, Diana; Borrione, Dominique Formal verification of a SHA-1 circuit core using ACL2. (English) Zbl 1152.68535 Hurd, Joe (ed.) et al., Theorem proving in higher order logics. 18th international conference, TPHOLs 2005, Oxford, UK, August 22–25, 2005. Proceedings. Berlin: Springer (ISBN 3-540-28372-2/pbk). Lecture Notes in Computer Science 3603, 326-341 (2005). Summary: 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 primitive 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.For the entire collection see [Zbl 1087.68005]. MSC: 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 68P25 Data encryption (aspects in computer science) Software:ACL2; EVC PDFBibTeX XMLCite \textit{D. Toma} and \textit{D. Borrione}, Lect. Notes Comput. Sci. 3603, 326--341 (2005; Zbl 1152.68535) Full Text: DOI