Name
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. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.1109/CSF.2018.00014 | 2018 IEEE 31st Computer Security Foundations Symposium (CSF) |
Keywords | Field | DocType |
Easycrypt,Formal-proof,MAC,Security,Block-cipher-mode,collision-probability,Security-proof | Message authentication code,Computer science,Cryptography,Theoretical computer science,Mathematical proof,Verifiable secret sharing,Formal verification,Formal proof | Conference |
ISSN | ISBN | Citations |
1940-1434 | 978-1-5386-6681-4 | 0 |
PageRank | References | Authors |
0.34 | 15 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Cecile Baritel-Ruet | 1 | 0 | 0.34 |
| François Dupressoir | 2 | 174 | 9.68 |
| Pierre-Alain Fouque | 3 | 1762 | 107.22 |
| Benjamin Grégoire | 4 | 817 | 48.93 |