The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
Abstract
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.
How it got here
How it got here
agent via openalex
Added
2026-10-28 23:30 UTC
Not denied by
a person 2026-10-29 17:12 UTC
Cite it as
@misc{baritelruet2018formal,
title = {Formal Security Proof of CMAC and Its Variants},
author = {Cécile Baritel-Ruet and François Dupressoir and Pierre-Alain Fouque and Benjamin Grégoire},
year = {2018},
journal = {IEEE Computer Security Foundations Workshop (CSFW)},
publisher = {Institute of Electrical and Electronics Engineers},
pages = {91--104},
doi = {10.1109/csf.2018.00014},
}