MAC-in-the-Box: Verifying a Minimalistic Hardware Design for MAC Computation

Künnemann, Robert and Nemati, Hamed
(2020) MAC-in-the-Box: Verifying a Minimalistic Hardware Design for MAC Computation.
In: Computer Security - ESORICS 2020 - 25th European Symposium on Research in Computer Security, ESORICS 2020, Guildford, UK, September 14-18, 2020, Proceedings, Part II.
Conference: ESORICS European Symposium On Research In Computer Security


Download (538kB) | Preview
Official URL:\_26


We study the verification of security properties at the state machine level of a minimalistic device, called the MAC-in-the-Box (MITB). This device computes a message authentication code based on the SHA-3 hash function and a key that is stored on device, but never output directly. It is designed for secure password storage, but may also be used for secure key-exchange and second-factor authentication. We formally verify, in the HOL4 theorem prover, that no outside observer can distinguish this device from an ideal functionality that provides only access to a hashing oracle. Furthermore, we propose protocols for the MITB’s use in password storage, key-exchange and second-factor authentication, and formally show that it improves resistance against host-compromise in these three application scenarios.


Actions (login required)

View Item View Item