Automated Security Proofs for Almost-Universal Hash for MAC Verification

International audienceMessage 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. We present a method for automatically proving the security for block-cipher-based and hash-based MACs in the ideal cipher model. Our method proceeds in two steps, following the traditional method for constructing MACs. 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. 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 quite expressive. As a result, our logic can be used to prove functions based on block ciphers and hash functions. Second, we 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. Using our method, we implemented a tool that can prove the security of many CBC-based MACs (DMAC, ECBC, FCBC and XCBC to name only a few), PMAC and HMAC