MacAlg.UF_CMA_Exp checks message freshness (!log.wasQueried msg), corresponding to WUF-CMA in the Bellare-Namprempre [BN00] terminology (what they call "the standard notion").
Would you consider worth it adding the strictly stronger SUF-CMA notion — where the adversary must produce a new (message, tag) pair rather than just a new message?
SUF-CMA is a prerequisite for Encrypt-then-MAC.
PRF → MAC gives SUF-CMA, not just WUF-CMA. Bellare-Namprempre note: "any pseudorandom function is a strongly unforgeable MAC." Boneh-Shoup Thm 6.2 proves pair-freshness security. Formalizing this standard result requires the SUF-CMA game to exist.
Also, most practical MACs are SUF-CMA.
[BN00] Bellare, Namprempre. "Authenticated Encryption: Relations among notions and analysis of the generic composition paradigm." https://eprint.iacr.org/2000/025
MacAlg.UF_CMA_Expchecks message freshness (!log.wasQueried msg), corresponding to WUF-CMA in the Bellare-Namprempre [BN00] terminology (what they call "the standard notion").Would you consider worth it adding the strictly stronger SUF-CMA notion — where the adversary must produce a new (message, tag) pair rather than just a new message?
SUF-CMA is a prerequisite for Encrypt-then-MAC.
PRF → MAC gives SUF-CMA, not just WUF-CMA. Bellare-Namprempre note: "any pseudorandom function is a strongly unforgeable MAC." Boneh-Shoup Thm 6.2 proves pair-freshness security. Formalizing this standard result requires the SUF-CMA game to exist.
Also, most practical MACs are SUF-CMA.
[BN00] Bellare, Namprempre. "Authenticated Encryption: Relations among notions and analysis of the generic composition paradigm." https://eprint.iacr.org/2000/025