University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Formal Security Proof of CMAC and its Variants

Baritel-Ruet, Cécile, Dupressoir, Francois, Fouque, Pierre-Alain and Grégoire, Benjamin (2018) Formal Security Proof of CMAC and its Variants In: 31st IEEE Computer Security Foundations Symposium, 09-12 Jul 2018, Oxford, UK.

Formal Security Proof of CMAC and its Variants.pdf - Accepted version Manuscript

Download (422kB) | Preview


The CMAC standard, when initially proposed by Iwata and Kurosawa as OMAC1, was equipped with a complex game-based security proof. Following recent advances in formal verification for game-based security proofs, we formalize a proof of unforgeability for CMAC in EasyCrypt. A side effect of this proof includes improvements and extensions to EasyCrypt’s standard libraries. This formal proof obtains security bounds very similar to Iwata and Kurosawa’s for CMAC, but also proves secure a certain number of intermediate constructions of independent interest, including ECBC, FCBC and XCBC. This work represents one more step in the direction of obtaining a reliable set of independently verifiable evidence for the security of international cryptographic standards.

Item Type: Conference or Workshop Item (Conference Paper)
Divisions : Faculty of Engineering and Physical Sciences > Computing Science
Authors :
Baritel-Ruet, Cécile
Fouque, Pierre-Alain
Grégoire, Benjamin
Date : 9 August 2018
DOI : 10.1109/CSF.2018.00014
Copyright Disclaimer : © 2018 the Author(s).
Related URLs :
Depositing User : Clive Harris
Date Deposited : 01 May 2018 08:41
Last Modified : 31 Oct 2018 15:33

Actions (login required)

View Item View Item


Downloads per month over past year

Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800