Automated Analysis and Synthesis of Message Authentication Codes

Milius S, Paulus D, Schröder D, Schröder L, Thomas J (2025)

Publication Type: Conference contribution

Publication year: 2025

Publisher: IEEE Computer Society

Pages Range: 489-504

Conference Proceedings Title: Proceedings - IEEE Computer Security Foundations Symposium

Event location: Santa Cruz, CA US

ISBN: 9798331510817

DOI: 10.1109/CSF64896.2025.00015

Abstract

Message Authentication Codes (MACs) represent a fundamental symmetric key primitive, serving to ensure the authenticity and integrity of transmitted data. As a building block in authenticated encryption and in numerous deployed standards, including TLS, IPsec, and SSH, MACs play a central role in practice. Due to their importance for practice, MACs have been subject to extensive research, leading to prominent schemes such as HMAC, CBCMAC, or LightMAC. Despite the existence of various MACs, there is still considerable interest in creating schemes that are more efficient, potentially parallelizable, or have specific non-cryptographic attributes, such as being patent-free. In this context, we introduce an automated method for analyzing and synthesizing MAC schemes. In order to achieve this goal, we have constructed a framework that restricts the class of MACs in such a way that it is sufficiently expressive to cover known constructions, yet also admits automated reasoning about the security guarantees of both known and new schemes. Our automated analysis has identified a novel category of MACs, termed 'hybrid' MACs. These MACs operate by processing multiple blocks concurrently, with each block managed by a different, specified MAC scheme. A key finding is that in certain scenarios, the hybrid MAC marginally outperforms the simultaneous operation of the individual MACs. This improvement is attributed to the hybrid approach exploiting the strengths and compensating for the weaknesses of each distinct MAC scheme involved. Our implementation confirms that we have successfully identified new schemes that have comparable performance with state-of-the-art schemes and in some settings seem to be slightly more efficient.

Authors with CRIS profile

Stefan Milius Lehrstuhl für Informatik 8 (Theoretische Informatik) Dominik Paulus Lehrstuhl für Informatik 8 (Theoretische Informatik) Lutz Schröder Lehrstuhl für Informatik 8 (Theoretische Informatik) Julian Thomas Lehrstuhl für Informatik 13 (Angewandte Kryptographie)

Involved external institutions

Technische Universität Wien / Vienna University of Technology AT Austria (AT)

How to cite

APA:

Milius, S., Paulus, D., Schröder, D., Schröder, L., & Thomas, J. (2025). Automated Analysis and Synthesis of Message Authentication Codes. In Proceedings - IEEE Computer Security Foundations Symposium (pp. 489-504). Santa Cruz, CA, US: IEEE Computer Society.

MLA:

Milius, Stefan, et al. "Automated Analysis and Synthesis of Message Authentication Codes." Proceedings of the 38th IEEE Computer Security Foundations Symposium, CSF 2025, Santa Cruz, CA IEEE Computer Society, 2025. 489-504.

BibTeX: Download