Download PDFOpen PDF in browser

Formal Security Proof of CMAC and its Variants

EasyChair Preprint no. 104

14 pagesPublished: April 28, 2018


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 effects of this proof are improvements of EasyCrypt 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.

Keyphrases: block cipher mode, collision probability, EasyCrypt, formal proof, MAC, Security, security proof

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
  author = {Cécile Baritel-Ruet and François Dupressoir and Pierre-Alain Fouque and Benjamin Grégoire},
  title = {Formal Security Proof of CMAC and its Variants},
  howpublished = {EasyChair Preprint no. 104},
  doi = {10.29007/2xpx},
  year = {EasyChair, 2018}}
Download PDFOpen PDF in browser