CISPA
Browse
cispa_all_3215.pdf (525.71 kB)

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

Download (525.71 kB)
conference contribution
posted on 2023-11-29, 18:13 authored by Robert KünnemannRobert Künnemann, Hamed Nemati
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.

History

Preferred Citation

Robert Künnemann and Hamed Nemati. MAC-in-the-Box: Verifying a Minimalistic Hardware Design for MAC Computation. In: European Symposium on Research in Computer Security (ESORICS). 2020.

Primary Research Area

  • Algorithmic Foundations and Cryptography

Name of Conference

European Symposium on Research in Computer Security (ESORICS)

Legacy Posted Date

2020-12-01

Open Access Type

  • Unknown

BibTeX

@inproceedings{cispa_all_3215, title = "MAC-in-the-Box: Verifying a Minimalistic Hardware Design for MAC Computation", author = "Künnemann, Robert and Nemati, Hamed", booktitle="{European Symposium on Research in Computer Security (ESORICS)}", year="2020", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC