Formal Security Proof of CMAC and Its Variants
2018 IEEE 31st Computer Security Foundations Symposium (CSF)(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.
更多查看译文
关键词
Easycrypt,Formal-proof,MAC,Security,Block-cipher-mode,collision-probability,Security-proof
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络