×

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
Full Text: DOI