Paper 2013/407

Automated Security Proofs for Almost-Universal Hash for MAC verification

Martin Gagné, Pascal Lafourcade, and Yassine Lakhnech

Abstract

Message authentication codes (MACs) are an essential primitive in cryptography. They are used to ensure the integrity and authenticity of a message, and can also be used as a building block for larger schemes, such as chosen-ciphertext secure encryption, or identity-based encryption. MACs are often built in two steps: first, the `front end' of the MAC produces a short digest of the long message, then the `back end' provides a mixing step to make the output of the MAC unpredictable for an attacker. Our verification method follows this structure. We develop a Hoare logic for proving that the front end of the MAC is an almost-universal hash function. The programming language used to specify these functions is fairly expressive and can be used to describe many block-cipher and compression function-based MACs. We implemented this method into a prototype that can automatically prove the security of almost-universal hash functions. This prototype can prove the security of the front-end of many CBC-based MACs (DMAC, ECBC, FCBC and XCBC to name only a few), PMAC and HMAC. We then provide a list of options for the back end of the MAC, each consisting of only two or three instructions, each of which can be composed with an almost-universal hash function to obtain a secure MAC.

Metadata
Available format(s)
PDF
Category
Secret-key cryptography
Publication info
Published elsewhere. Proceedings version accepted in ESORICS 2013
Keywords
block ciphershash functionsmessage authentication codesautomated verification
Contact author(s)
gagne @ cs uni-saarland de
History
2013-06-25: received
Short URL
https://ia.cr/2013/407
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2013/407,
      author = {Martin Gagné and Pascal Lafourcade and Yassine Lakhnech},
      title = {Automated Security Proofs for Almost-Universal Hash for MAC verification},
      howpublished = {Cryptology ePrint Archive, Paper 2013/407},
      year = {2013},
      note = {\url{https://eprint.iacr.org/2013/407}},
      url = {https://eprint.iacr.org/2013/407}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.