(2020) MAC-in-the-Box: Verifying a Minimalistic Hardware Design for MAC Computation.
|
Text
mitb-full.pdf Download (538kB) | Preview |
Abstract
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.
| Item Type: | Conference or Workshop Item (A Paper) (Paper) |
|---|---|
| Divisions: | Hamed Nemati (HM) Robert Künnemann (RK) |
| Conference: | ESORICS European Symposium On Research In Computer Security |
| Depositing User: | Hamed Nemati |
| Date Deposited: | 01 Dec 2020 10:05 |
| Last Modified: | 02 Dec 2020 10:01 |
| Primary Research Area: | NRA2: Reliable Security Guarantees |
| URI: | https://publications.cispa.saarland/id/eprint/3215 |
Actions
Actions (login required)
 |
View Item |