Cryptology ePrint Archive: Report 2013/407

Automated Security Proofs for Almost-Universal Hash for MAC verification

Martin Gagné and 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.

Category / Keywords: secret-key cryptography / block ciphers, hash functions, message authentication codes, automated verification

Publication Info: Proceedings version accepted in ESORICS 2013

Date: received 20 Jun 2013, last revised 20 Jun 2013

Contact author: gagne at cs uni-saarland de

Available format(s): PDF | BibTeX Citation

Version: 20130625:155050 (All versions of this report)

Short URL:

[ Cryptology ePrint archive ]