Automated Security Proofs for Almost-Universal Hash for MAC verification

Martin Gagné; Pascal Lafourcade; Yassine Lakhnech

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 ciphers hash functions message authentication codes automated verification
Contact author(s): gagne @ cs uni-saarland de
History: 2013-06-25: received
Short URL: https://ia.cr/2013/407
License: 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},
      url = {https://eprint.iacr.org/2013/407}
}